0373righ1113 ◆OPKWA8uhcY
2016/05/22(日) 16:19:17.83ID:As5SZbzkRequire Import Coq.Program.Wf.
Require Import Omega.
Program Fixpoint collatz03 (x y : nat) {measure y} : list nat :=
match y with
| 0 => 0::nil
| _ => match x with
| 0 => 0::nil
| 1 => 1::nil
| _ => if Nat.odd x then (3*x+1) :: collatz03 (3*x+1) (y-1)
else (x/2) :: collatz03 (x/2) (y-1)
end
end.
Next Obligation.
omega.
Qed.
Next Obligation.
omega.
Qed.
ここまでで3日かかりました。www