proposition: Lemma terminates2E {s' t' : TM_facts.mconfig Σ (state P) (S n)} : clos_refl_trans _ step2 s' t' -> Sim.stuck step2 t' -> exists k, TM_facts.loopM s' k = Some t'.
proof: Proof. move=> /clos_rt_rt1n_iff. elim. - move=> {}s' /stuck_step2E Hs'. exists 0. by rewrite /= Hs'. - move=> > [E ->] _ /[apply] - [k] ?. exists (S k). by rewrite /= E. 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