proposition: Lemma If_RealiseIn R1 R2 R3 k1 k2 k3 : pM1 ⊨c(k1) R1 -> pM2 ⊨c(k2) R2 -> pM3 ⊨c(k3) R3 -> If ⊨c(1 + k1 + Nat.max k2 k3) (R1 |_true) ∘ R2 ∪ (R1 |_false) ∘ R3.
proof: Proof. intros. eapply RealiseIn_monotone. - eapply Switch_RealiseIn; eauto. intros. cbn in f. destruct f. + eapply RealiseIn_monotone. * destruct pM2. eassumption. * instantiate (1 := Nat.max k2 k3). lia. * instantiate (1 := fun t => match t with true => R2 | _ => R3 end). reflexivity. + eapply RealiseIn_monotone. * destruct pM3. eassumption. * lia. * reflexivity. - lia. - hnf. intros H2 (f& t). intros ([ | ]& (y & H3&H3')). + left. hnf. eauto. + right. hnf. eauto. Qed.
imports: Undecidability.TM(Util.TM_facts Switch)