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, M). - move=> /in_code_step ?. by left. - move=> /out_code_iff ?. by right. Qed.
imports: Undecidability.TM(TM) Undecidability.MinskyMachines(MM MMA.mma_defs Reductions.MMA_computable_to_MMA_mon_computable) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss Code.subcode) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Undecidability.Shared.Libs.PSL(CompoundFinTypes) Undecidability.Shared.Libs.PSL.EqDec List Lia PeanoNat Compare_dec Relations ssreflect ssrbool ssrfun