proposition: Lemma in_mma_sss_dec_1' n u (i i' : nat) (x : pos n) p (v v' : vec nat n) : i' = p -> v' = vec_change v x u -> vec_pos v x = S u -> mma_sss (DEC x p) (i, v) (i', v').
proof: Proof. move=> -> ->. by constructor. Qed.
imports: Undecidability(TM.TM) Undecidability.MinskyMachines(MM MMA MMA.mma_defs Util.MMA_computable) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) List PeanoNat Lia Relations ssreflect