proposition: Lemma INIT_INPUT_len_spec {offset} : length (INIT_INPUT offset) = INIT_INPUT_len.
proof: Proof. rewrite /INIT_INPUT /INIT_INPUT_codes (length_compose (lengths := repeat PACK_len k0)). - apply: Forall2_repeat. + by rewrite !map_length rev_length pos_list_length. + apply /Forall_map /Forall_map /Forall_map /Forall_forall => *. by apply: PACK_len_spec. - by rewrite list_sum_repeat. 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