proposition: Lemma seek_M n {i mm2i} : mm2_instr_at mm2i i P -> nth_error M (n + fs i) = match n with | 0 | 1 | 2 | 3 | 4 | 5 => nth_error (encode_instruction (mm2i, i)) n | _ => nth_error M (n + fs i) end.
proof: Proof. have [->|Hn] : n = 6 + (n - 6) \/ n < 6 by lia. { done. } move=> [Pl] [Pr] [HP Hi]. suff: nth_error M (n + fs i) = nth_error (encode_instruction (mm2i, i)) n. { move=> ->. by move: n Hn => [|[|[|[|[|[|?]]]]]]. } rewrite /M HP -Hi. rewrite nth_error_app2. { rewrite !map_length !seq_length /=. lia. } rewrite nth_error_app2. { rewrite !map_length !seq_length /=. lia. } rewrite !map_length !seq_length. suff: forall k, nth_error (flat_map encode_instruction (combine P (seq k (length P)))) (n + length Pl * 6) = nth_error (encode_instruction (mm2i, k + length Pl)) n. { move=> <-. rewrite HP /=. congr nth_error. lia. } rewrite HP. elim: Pl {HP Hi}. { move=> ?. rewrite /= !Nat.add_0_r. by rewrite nth_error_app1; [case: mm2i|]. } move=> instr Pl IH k. have ->: k + length (instr :: Pl) = (k+1) + length Pl. { by rewrite -Nat.add_assoc. } rewrite -IH /= nth_error_app2 length_encode_instruction. { lia. } have ->: k+1 = S k by lia. congr nth_error. lia. 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