proposition: Lemma fold_left_vec_zero_eq {n : nat} {w : Vector.t nat n} ps : (forall i, not (In i ps) -> vec_pos w i = 0) -> fold_left (fun v i => vec_change v i 0) ps w = vec_zero.
proof: Proof. elim: ps w. - move=> w Hw /=. apply: vec_pos_ext => ?. by rewrite vec_zero_spec Hw. - move=> i ps IH w Hips /=. apply: IH => j Hjps. have [->|?] := pos_eq_dec i j. + by rewrite vec_change_eq. + rewrite vec_change_neq //. apply: Hips. by case. 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