proposition: Lemma Switch_Realise (R1 : Rel _ (F * _)) (R2 : F -> Rel _ (F' * _)) : pM1 ⊨ R1 -> (forall f : F, pMf f ⊨ R2 f) -> Switch ⊨ (⋃_f (R1 |_ f) ∘ R2 f).
proof: Proof. intros HRel1 HRel2. hnf in HRel1. hnf. intros t i outc HLoop. apply Switch_split in HLoop as (k1&c1&k2&c2&HLoop1&HLoop2&->). cbn. exists (p1 (cstate c1)), (ctapes c1). split. - apply (HRel1 _ _ _ HLoop1). - apply (HRel2 _ _ _ _ HLoop2). Qed.
imports: Undecidability(TM.Util.TM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts