proposition: Corollary reaches'I x : { y | reaches' x y /\ (forall z, step y z -> index z = 1 \/ mm2_stop M z) }.
proof: Proof. Proof using HM. move Hn: ((S (length M)) - index x) => n. elim: n x Hn. { move=> x ?. exists x. split; first by exists 0. move=> ? [?] [/mm2_instr_at_bounds]. lia. } move=> n IH x ?. case Hy: (step' x) => [y|]. - move: (Hy) => /step'_inc_index ?. have /IH : ((S (length M) - index y = n)) by lia. move=> [z] [Hyz ?]. exists z. split; last done. move: Hyz => [k Hk]. exists (k+1). by rewrite /steps' /Nat.iter nat_rect_plus /= Hy. - exists x. split; first by exists 0. move: Hy. rewrite /step' /step. rewrite (mm2_state_eta x) /=. case: (index x) => [|p]. { move=> _ ? [?] [/mm2_instr_at_bounds]. lia. } case Hi: (nth_error M p) => [i|]; first last. { move: Hi => /nth_error_None ? _ ? [?] [/mm2_instr_at_bounds]. lia. } case: i Hi; [done|done| |]. + move: (value1 x) => [|a]; first done. move=> q /[dup] /target_index_a Hq. move=> /nth_error_Some_mm2_instr_at_iff /mm2_instr_at_unique HSp _ ?. move=> [?] [/HSp <-] H. inversion H; cbn; subst. by case: Hq => ?; [left|right]. + move: (value2 x) => [|b]; first done. move=> q /[dup] /target_index_b Hq. move=> /nth_error_Some_mm2_instr_at_iff /mm2_instr_at_unique HSp _ ?. move=> [?] [/HSp <-] H. inversion H; cbn; subst. by case: Hq => ?; [left|right]. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Transitive_Closure Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun