proposition: Lemma step1_intro s : (exists t, step1 s t) \/ (Sim.stuck step1 s).
proof: Proof. have [|] := subcode.in_out_code_dec (fst s) (1, P). - move=> /in_code_step ?. by left. - move=> /out_code_iff ?. by right. 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