proposition: Lemma M_to_P n s y : Nat.iter n (obind (MPM2.step M)) (Some (to_Config s)) = Some y -> exists t, y = to_Config t /\ ((1, P) // s ->> t).
proof: Proof. move=> Hn. suff : exists t : mm_state 2, y = to_Config t /\ sss_steps (@mm_sss _) (1, P) n s t. { move=> [t] [? ?]. exists t. split; [done|by exists n]. } elim: n s Hn. { move=> s [<-]. exists s. split; first done. by apply: sss_steps_0. } move=> n IH s /=. rewrite obind_oiter. case Hz: (MPM2.step M (to_Config s)) => [z|]; last by rewrite oiter_None. move: Hz => /M_to_P_step [u] [->] Hsu. move=> /IH [t] [? ?]. exists t. split; first done. have ->: S n = 1 + n by done. apply: sss_steps_trans; last by eassumption. by apply: sss_steps_1. Qed.
imports: PeanoNat Lia List Undecidability.MinskyMachines(MM MM_sss) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) ssreflect ssrbool ssrfun