proposition: Lemma INC_spec X v offset : (offset, INC X offset) // (offset, v) ->> (1 + offset, vec_change v X (S (vec_pos v X))).
proof: Proof. exists 1. apply: in_sss_steps_S; [|by apply: in_sss_steps_0]. eexists offset, nil, _, nil, v. rewrite /= Nat.add_0_r. by split; [|split;[|constructor]]. 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