proposition: Lemma ZERO_spec X v offset : (offset, ZERO X offset) // (offset, v) ->> (ZERO_len+offset, vec_change v X 0).
proof: Proof. elim /(induction_ltof1 _ (fun w => vec_pos w X)) : v => v IH. case EX: (vec_pos v X) => [|n]. { apply: (compose_sss_compute_trans 0). { by apply: DEC_spec. } rewrite EX (vec_change_same' EX). by apply: sss_compute_refl. } apply: (compose_sss_compute_trans 0). { by apply: DEC_spec. } rewrite EX. apply: sss_compute_trans. { apply: IH. by rewrite /= EX vec_change_eq. } apply: sss_compute_refl'. by rewrite vec_change_idem. Qed.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) PeanoNat List Lia Wf_nat ssreflect ssrbool ssrfun