proposition: Lemma halt'_terminates s' : halt' (TM_facts.cstate s') = true -> Sim.terminates step2 s'.
proof: Proof. move:s' => [[[] p] ts] /=; [done|]. rewrite /halt' /=. have [->|[q ->]] := pos_S_inv p; [|done]. rewrite Nat.eqb_refl /= => _. eexists. split; [apply: rt_refl|]. move=> {}t' /=. rewrite Nat.eqb_refl. by case. 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