proposition: Lemma CM1_halting_iff_terminates {x} : (exists n, CM1.halting M (Nat.iter n (CM1.step M) x)) <-> deterministic_simulation.terminates cm1_step x.
proof: Proof. split. - move=> [n]. have /(@deterministic_simulation.terminates_extend CM1.Config) := cm1_steps n x. move: (Nat.iter n (CM1.step M) x) => y H Hy. apply: H. exists y. by split; [apply: rt_refl|apply: cm1_halting_stuck]. - move=> [y] []. move=> /(@clos_rt_rt1n CM1.Config). elim. + move=> {}x /(_ (CM1.step M x)) Hx. exists 0. rewrite /CM1.halting /=. have [|] := Config_eq_dec x (CM1.step M x); [done|]. tauto. + move=> > [Hxy ?] _ IH /IH [n {}IH]. exists (n+1). by rewrite /Nat.iter nat_rect_plus /= Hxy. Qed.
imports: ZArith List PeanoNat Lia Relations.Relation_Operators Relations.Operators_Properties Undecidability.MinskyMachines.MM2 Undecidability.CounterMachines.Util.CM1_facts Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun