proposition: Lemma DEC_spec X p v offset : (offset, DEC X p offset) // (offset, v) ->> match vec_pos v X with | 0 => (1 + offset, v) | S x => (p, vec_change v X x) end.
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. split; [done|split;[done|]]. case EX: (v#>X) => [|n]; by 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