proposition: Lemma terminates2I k {s' t' : TM_facts.mconfig Σ (state P) (S n)} : TM_facts.loopM s' k = Some t' -> Sim.terminates step2 s'.
proof: Proof. elim: k s'. { move=> s' /= Hs'. apply: halt'_terminates. by case: (halt' (TM_facts.cstate s')) Hs'. } move=> k IH s' /=. case E: (halt' (TM_facts.cstate s')) => []. - move=> ?. by apply: halt'_terminates. - move=> /IH [u'] [? ?]. exists u'. split; [|done]. by apply: rt_trans; [apply: rt_step|eassumption]. 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