proposition: Lemma RealiseIn_split n (F : Type) (pM : pTM F n) R1 R2 (k : nat) : pM ⊨c(k) R1 /\ pM ⊨c(k) R2 <-> pM ⊨c(k) R1 ∩ R2.
proof: Proof. split; swap 1 2; [ intros H | intros (H1&H2)]. - firstorder eauto. - repeat intros ?. specialize (H1 input) as (outc &H1&H1'). specialize (H2 input) as (outc2&H2&H2'). pose proof loop_injective H1 H2 as <-. exists outc. split; hnf; eauto. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM