proposition: Lemma reflection : CM1.CM1_HALT (exist _ M M_capped) -> MM2_HALTING (P, a0, b0).
proof: Proof. move=> /(terminating_reaches_iff init_M) /CM1_halting_iff_terminates H. apply /MM2_HALTING_iff_terminates. move: H. apply: deterministic_simulation.terminates_reflection. - by move=> > [<- _] [<- _]. - exact: P_to_M_step. - by apply: mm2_exists_step_dec. - by split; [|exists 0]. 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