proposition: Lemma ZERO_spec' X v offset : (offset, ZERO X offset) // (offset, v) -+> (ZERO_len + offset, vec_change v X 0).
proof: Proof. have [[|k]] := ZERO_spec X v offset. - move=> /sss_steps_0_inv /(f_equal fst) /=. rewrite /ZERO_len /DEC_len. lia. - move=> Hk. exists (S k). by split; [lia|]. 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