proposition: Lemma simulation_mma_sss i instr a v w i' a' v' w' : 1 <= i < S (length P) -> mma_sss instr (i, a ## (Vector.append v w)) (i', a' ## (Vector.append v' w')) -> mma_sss (shift_instr instr) (shift_addr i, Vector.append (0 ## v) (Vector.append w (a ## vec_nil))) (shift_addr i', Vector.append (0 ## v') (Vector.append w' (a' ## vec_nil))).
proof: Proof. move E1: ((i, a ## Vector.append v w)) => iavw. move E2: ((i', a' ## Vector.append v' w')) => i'a'v'w' Hi Hinstr. rewrite (shift_addr_range i). { lia. } case: Hinstr i a v w i' a' v' w' Hi E1 E2. - move=> > ? /=. move=> /pair_equal_spec [<- <-] /pair_equal_spec [->] E3. apply: in_mma_sss_inc'. { apply: shift_addr_range. lia. } by rewrite vec_pos_shift_counter (vec_change_shift_counter E3). - move=> > ? i > ?. move=> /pair_equal_spec [??] /pair_equal_spec [?]. subst. move=> /Vector.cons_inj [?] /vec_append_inj [??]. subst. rewrite (shift_addr_range). { lia. } apply: in_mma_sss_dec_0'; [done..|]. by rewrite vec_pos_shift_counter. - move=> > ? i > ?. move=> /pair_equal_spec [??] /pair_equal_spec [?] E3. subst. rewrite /=. apply: in_mma_sss_dec_1'; [done| |rewrite vec_pos_shift_counter; eassumption]. by rewrite (vec_change_shift_counter E3). Qed.
imports: Undecidability(TM.TM) Undecidability.MinskyMachines(MM MMA MMA.mma_defs Util.MMA_computable) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) List PeanoNat Lia Relations ssreflect