proposition: Lemma eval_iff P n m : fractran_eval P n m <-> fractran_compute P n m /\ fractran_stop P m.
proof: Proof. split. - induction 1 as [ P n | P n m m' Hstep H [[k IH1] IH2]]. + split. * exists 0. econstructor. * firstorder. + split. * exists (1 + k). econstructor. eauto. * eauto. - intros [[k H1] H2]. induction k in n, m, H1, H2 |- *. + inversion H1 as []. subst. econstructor. firstorder. + inversion H1 as [m' [H3 H4]]. econstructor; eauto. Qed.
imports: List Arith Undecidability.Shared.Libs.DLW(gcd rel_iter pos vec) Undecidability.FRACTRAN.Util(prime_seq) Undecidability.FRACTRAN.FRACTRAN