proposition: Lemma INIT_INPUT_spec offset w v : vec_pos (Vector.append (0 ## w) v) CTX = 0 -> (offset, INIT_INPUT offset) // (offset, Vector.append (0 ## w) v) ->> (INIT_INPUT_len+offset, vec_change (Vector.append vec_zero v) CTX (enc_list (Vector.to_list w))).
proof: Proof. suff: forall (ps : list (Fin.t k0)) offset ns (w : vec nat k0) v, vec_pos v pos4 = enc_list ns -> NoDup ps -> (offset, compose (map (PACK Fin.F1 CTX) (map (Fin.L 6) (map Fin.FS ps))) offset) // (offset, Vector.append (0 ## w) v) ->> ((PACK_len * (length ps)) + offset, Vector.append (0 ## fold_left (fun w i => vec_change w i 0) ps w) (vec_change v pos4 (enc_list ((map (vec_pos w) (rev ps)) ++ ns)))). { move=> + /[dup] Hv. rewrite ?vec_simpl. move=> /(_ _ offset nil w v) /[apply]. move=> /(_ (rev (pos_list k0))). apply: unnest. { apply: NoDup_rev. by apply: pos_list_NoDup. } congr sss_compute. congr pair. - rewrite /INIT_INPUT_len rev_length pos_list_length. lia. - rewrite ?vec_simpl in Hv. congr Vector.append. + rewrite fold_left_vec_zero_eq //. move=> i H. exfalso. apply: H. by have /In_rev := pos_list_prop i. + rewrite rev_involutive app_nil_r. congr vec_change. congr enc_list. rewrite map_pos_list_vec. by elim: w; [|move=> > /= ->]. } elim. { move=> *. cbn. apply: sss_compute_refl'. by rewrite vec_change_same'. } move=> i ps IH {}offset ns {}w {}v Hv /NoDup_cons_iff [Hi /IH {}IH]. apply: (compose_sss_compute_trans 0). { apply: PACK_spec; [done..|]. apply: nesym. by apply: Fin_L_R_neq. } rewrite /=. apply: subcode_sss_compute. { by apply: subcode_right. } have := (IH (PACK_len+offset) (vec_pos w i :: ns) (vec_change w i 0) (vec_change v pos4 (enc_list (vec_pos w i :: ns)))). apply: unnest. { by rewrite vec_change_eq. } rewrite PACK_len_spec /= ?vec_simpl Hv. congr sss_compute. - congr pair. lia. - congr pair; [lia|]. congr Vector.cons. congr Vector.append. rewrite vec_change_idem /= map_app /= -app_assoc /=. congr vec_change. congr enc_list. congr List.app. apply /map_ext_in_iff => j Hj. apply: vec_change_neq => ?. apply: Hi. apply /In_rev. by subst j. 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