proposition: Lemma Seq_TerminatesIn R1 T1 T2 : pM1 ⊨ R1 -> projT1 pM1 ↓ T1 -> projT1 pM2 ↓ T2 -> projT1 Seq ↓ (fun tin i => exists i1 i2, T1 tin i1 /\ 1 + i1 + i2 <= i /\ forall tout yout, R1 tin (yout, tout) -> T2 tout i2).
proof: Proof. intros HRealise HTerm1 HTerm2. eapply TerminatesIn_monotone. - eapply Switch_TerminatesIn; eauto. instantiate (1 := fun _ => T2). auto. - intros tin i (i1&i2&Hi&HT1&HT2). exists i1, i2; repeat split; auto. Qed.
imports: Undecidability.TM(Util.TM_facts Switch)