proposition: Lemma INIT_s0_spec offset v : vec_pos v U = 0 -> (offset, INIT_s0 offset) // (offset, v) ->> (INIT_s0_len+offset, vec_change v U (enc_term s0)).
proof: Proof. suff : forall j m offset v, j <= m -> v#>Fin.R (1 + k0) pos5 = m-j -> (offset, compose (repeat (INC U) m) offset) // ((m-j)+offset, v) ->> (m + offset, vec_change v U m). { move=> /(_ (enc_term s0) (enc_term s0)). rewrite Nat.sub_diag. by apply. } elim. { move=> m {}offset {}v _. rewrite !Nat.sub_0_r => ?. apply: sss_compute_refl'. by rewrite vec_change_same'. } move=> j IH m {}offset {}v ? Hv. have EmSj : m - S j = length (compose (firstn (m - S j) (repeat (INC U) m)) offset). { rewrite (length_compose (lengths := repeat INC_len (m - S j))). - apply: Forall2_repeat. { rewrite firstn_length repeat_length. lia. } rewrite firstn_repeat. by apply /Forall_forall => ? /repeat_spec ->. - by rewrite list_sum_repeat /INC_len Nat.mul_1_r. } rewrite EmSj. apply: (compose_sss_compute_trans). { rewrite (nth_indep _ _ (INC U)). { rewrite repeat_length. lia. } rewrite nth_repeat. apply: INC_spec. } rewrite -EmSj. have -> : 1 + (m - S j + offset) = (m - j) + offset by lia. rewrite Hv. apply: sss_compute_trans. { apply: IH; [lia|]. by rewrite vec_change_eq; [|lia]. } rewrite vec_change_idem. 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