proposition: Lemma MM2_HALTING_iff_terminates {a b} : MM2_HALTING (P, a, b) <-> deterministic_simulation.terminates (mm2_step P) (1, (a, b)).
proof: Proof. done. 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