proposition: Lemma simulation offset y n w : machine (closure [] (fold_left (fun s n => app s (L.nat_enc n)) (Vector.to_list w) s0)) [] y -> flatten y = L.nat_enc n -> (offset, COMPUTE offset) // (offset, Vector.append (0 ## w) vec_zero) ->> (COMPUTE_len+offset, n ## vec_zero).
proof: Proof. move=> /PROG_simulation /[apply] HPROG. have compose_trans := (compose_sss_compute_length_trans _ (COMPUTE_lengths_spec offset)). apply: sss_compute_trans. { by apply: simulation_init. } rewrite ?vec_simpl. apply: (compose_trans 3). { by apply: HPROG. } rewrite list_sum_append. apply: sss_compute_refl'. congr pair. rewrite (vec_zero_S k0) /=. congr Vector.cons. clear. by elim: (k0) => [|k IH]; [|rewrite /= IH]. Qed.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA L.L) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss Code.subcode) Undecidability(MinskyMachines.Util.MMA_pairing L.AbstractMachines.wCBV) PeanoNat List Lia Wf_nat ssreflect ssrbool ssrfun