0520righ1113 ◆OPKWA8uhcY
2016/07/12(火) 22:09:14.33ID:5e2oe2QmCoqでは止まらない再帰関数は書けないので、
>>373では、再帰を有限回で0終了させる引数yを入れてあります。
で、どんなxに対してもlast collatz03が0にならないyが存在する、という事で、
Require Import List.して
Theorem collatz_is_true:
forall (x:nat), x<>0 -> (exists y:nat, 1=(last (collatz03 x y) 0)).
ってとこじゃないでしょうか。