proposition: Lemma transport : MM2_HALTING (P, a0, b0) -> CM1.CM1_HALT (exist _ M M_capped).
proof: Proof. move=> /MM2_HALTING_iff_terminates H. rewrite /CM1.CM1_HALT. apply /(terminating_reaches_iff init_M). apply /CM1_halting_iff_terminates. move: H. apply: deterministic_simulation.terminates_transport. - exact: P_to_M_step. - rewrite /deterministic_simulation.stuck. move=> x x' Hx Hxx'. rewrite /deterministic_simulation.terminates. exists x'. split; [by apply: rt_refl|]. rewrite /deterministic_simulation.stuck. move=> y' [Hx'y' H'x'y']. move: Hx => /mm2_stop_index_iff. subst y'. move: x' Hxx' H'x'y'. move=> [p [|c]] /=; [done|]. case Hinstr: (nth_error M p) => [instr|]; [|done]. have /nth_error_Some : nth_error M p <> None by congruence. rewrite M_length. move: x => [i [a b]] /= HpM [? _] _. move=> [?|?]; subst. + move: HpM => /=. lia. + move: HpM. have -> /= : i = S (i-1) by lia. lia. - 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