proposition: Lemma P_to_M_step s t : sss_step (@mm_sss _) (1, P) s t -> MPM2.step M (to_Config s) = Some (to_Config t).
proof: Proof. rewrite /sss_step. move=> [k] [P1] [i] [P2] [v] [[<- HP]] [->]. rewrite /MPM2.step. have -> : nth_error M (MPM2.state (to_Config (1 + length P1, v))) = Some (to_Instruction i). { rewrite /M HP map_app (decompose_vec2 v) nth_error_app2. { by rewrite /= map_length. } by rewrite /= map_length Nat.sub_diag. } move Hc: (1 + length P1, v) => c H. case: H Hc. - move=> ? d w [<- <-]. rewrite [to_Instruction _]/= (decompose_vec2 v). by case: (case_pos2 d) => /= ->. - move=> ? d q w + [<- ?]. subst w. rewrite (decompose_vec2 v) /=. case: (case_pos2 d). + move=> /= -> ->. by case: q. + move=> /= -> ->. by case: q. - move=> ? d q w u + [<- ?]. subst w. rewrite (decompose_vec2 v) /=. case: (case_pos2 d). + by move=> /= -> ->. + by move=> /= -> ->. Qed.
imports: PeanoNat Lia List Undecidability.MinskyMachines(MM MM_sss) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) ssreflect ssrbool ssrfun