proposition: Lemma stuck_step2E s' : Sim.stuck step2 s' -> halt' (TM_facts.cstate s') = true.
proof: Proof. move=> Hs'. case E: (halt' (TM_facts.cstate s')); [done|]. exfalso. by apply: (Hs' (@TM_facts.step _ _ P s')). 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