proposition: Lemma Switch_TerminatesIn (R1 : Rel _ (F * _)) T1 T2 : pM1 ⊨ R1 -> M1 ↓ T1 -> (forall f : F, Mf f ↓(T2 f)) -> projT1 Switch ↓ (fun tin i => exists i1 i2, T1 tin i1 /\ 1 + i1 + i2 <= i /\ forall tout yout, R1 tin (yout, tout) -> T2 yout tout i2).
proof: Proof. unfold Switch. intros HRel1 HTerm1 HTerm2. hnf in HRel1, HTerm1. hnf. intros t i (i1&i2&HT1&Hk&H). specialize HTerm1 with (1 := HT1) as (c1&HLoop1). specialize HRel1 with (1 := HLoop1). specialize H with (1 := HRel1). specialize (HTerm2 _ _ _ H) as (c2&HLoop2). pose proof Switch_merge HLoop1 HLoop2 as HLoop. exists (lift_confR c2). eapply loop_monotone; eauto. lia. Qed.
imports: Undecidability(TM.Util.TM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts