proposition: Lemma simulation_sss_step i a v w i' a' v' w' : sss_step (mma_sss (n:=num_counters)) (1, P) (i, a ## (Vector.append v w)) (i', a' ## (Vector.append v' w')) -> sss_step (mma_sss (n:=num_counters')) (1, P') (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. rewrite /P'. move=> [offset'] [l] [instr] [r] [v'']. move=> [[<-]] /[dup] HP. move=> -> [/config_eqE2] [->] [->] [-> ->] Hinstr. eexists 1, (map shift_instr l), (shift_instr instr), (map shift_instr r ++ _), _. split; [|split]. - congr pair. by rewrite map_app /= -app_assoc. - congr pair. rewrite map_length shift_addr_range //. rewrite HP app_length /=. lia. - apply: simulation_mma_sss Hinstr. rewrite HP app_length /=. lia. 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