proposition: Lemma simulation v v' w' c m : (1, P) // (1, 0 ## Vector.append v (Vector.const 0 k')) ->> (c, m ## (Vector.append v' w')) -> c < 1 \/ S (length P) <= c -> (1, P') // (1, 0 ## Vector.append v (Vector.const 0 (k' + 1))) ->> (5 + length P, m ## (Vector.append v' (Vector.append w' (0 ## vec_nil)))).
proof: Proof. move=> /sss_compute_iff. move=> /(Sim.clos_refl_trans_transport fstep) => /(_ _ sync_intro). move=> [t'] [/syncE] /=. rewrite Vector.splitat_append /=. move=> [?] -> + /shift_addr_outcode Hc. rewrite Nat.sub_0_r Hc vec_append_const => H1. apply: sss_compute_trans; apply /sss_compute_iff; [eassumption|]. by apply /sss_compute_iff /finalization. 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