19/12/17 20:51:53.85 YS+T9+Lq.net
>>452-453
どうも。スレ主です。
情報ありがとう
これか（＾＾
URLﾘﾝｸ(ja.wikipedia.org)
コラッツの問題
URLﾘﾝｸ(en.wikipedia.org)
Collatz conjecture
コラッツ予想がとけたらいいな その2
ｽﾚﾘﾝｸ(math板:750番)-
750 名前：righ1113 ◆OPKWA8uhcY [sage] 投稿日：2019/08/21(水) 08:04:36.17 ID:1YNIVvH6 [1/5]
GitHubのWikiとprogram3は直しかけです。
証明の流れは以下です。
①まず、二つの述語を用意します。
FirstLimited x ： xの完全割数列は有限長である
AllLimited x ： xの完全割数列および拡張完全割数列達は全て有限長である
示したい命題は、x -> FirstLimited x です。 ---(a)
②次に、パースの法則の述語論理版を用意します。
"∀x::nat. ￢(∀z::nat. (P z -> Q z))
-> (∀z::nat. (P z -> Q z) -> (∀n::nat. P n))
-> P x"
これは定理証明支援系Isabelleで自動証明したので間違いないと思います。