proposition: Lemma simulation_init offset w : (offset, COMPUTE offset) // (offset, Vector.append (0 ## w) vec_zero) ->> ((list_sum (firstn 3 COMPUTE_lengths))+offset, Vector.append vec_zero (0 ## 0 ## 0 ## 0 ## 0 ## enc_closure (closure [] (fold_left (fun s n => app s (L.nat_enc n)) (Vector.to_list w) s0)) ## vec_nil)).
proof: Proof. have compose_trans := (compose_sss_compute_length_trans _ (COMPUTE_lengths_spec offset)). rewrite ?vec_simpl. apply: (compose_trans 0). { by apply: INIT_INPUT_spec. } rewrite ?vec_simpl list_sum_append. apply: (compose_trans 1). { by apply: INIT_s0_spec. } rewrite ?vec_simpl list_sum_append. apply: (compose_trans 2). { by apply: INIT_spec. } rewrite ?vec_simpl list_sum_append. by apply: sss_compute_refl. 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