proposition: Lemma decision (v: vec nat 2) : ((1, P) // (1, v) ↓) + (not ((1, P) // (1, v) ↓)).
proof: Proof. have [H|H] := MPM2.decision M (to_Config (1, v)). - left. move: H => [n]. elim: n; first done. move=> n IH /=. case Hy: (MPM2.steps M n (to_Config (1, v))) => [y|]. + move: Hy => /M_to_P [t] [->] Ht H't. exists t. split; first done. move: t {Ht} H't => [[|p] w] /=; first by lia. rewrite (decompose_vec2 w) /to_Config /= /MPM2.step /=. case Hi: (nth_error M p) => [i|]; first last. { move: Hi => /nth_error_None. rewrite /M map_length. lia. } case: i Hi; [|done..]. move=> /(@nth_error_In MPM2.Instruction) /in_map_iff. by move=> [[]] => [?|??] []. + by move: (IH Hy). - right. move=> [t] [/=] /P_to_M [n] Hn Ht. apply: (H (S n)). rewrite /= /MPM2.steps Hn. move: t Ht {Hn} => [[|p] w]. + rewrite /= /MPM2.step /to_Config (decompose_vec2 w) /=. suff ->: nth_error M (length P) = None by done. apply /nth_error_None. by rewrite /M map_length. + move=> /= [|?]; first by lia. rewrite /= /MPM2.step /to_Config (decompose_vec2 w) /=. suff ->: nth_error M p = None by done. apply /nth_error_None. rewrite /M map_length. lia. Qed.
imports: PeanoNat Lia List Undecidability.MinskyMachines(MM MM_sss) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) ssreflect ssrbool ssrfun