proposition: Lemma Switch_RealiseIn (R1 : Rel _ (F * _)) (R2 : F -> Rel _ (F' * _)) k1 k2: pM1 ⊨c(k1) R1 -> (forall f : F, pMf f ⊨c(k2) R2 f) -> Switch ⊨c(1 + k1 + k2) (⋃_f (R1 |_ f) ∘ R2 f).
proof: Proof. intros (H1&H2) % Realise_total H3. apply Realise_total. split. - eapply Switch_Realise; eauto. intros ?. eapply Realise_total; eauto. - eapply TerminatesIn_monotone. + apply Switch_TerminatesIn; eauto. intros ?. eapply Realise_total; eauto. + firstorder. Qed.
imports: Undecidability(TM.Util.TM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts