proposition: Lemma recognizes_co_recognizes_disjoint: forall m1 m2 L, Recognizes m1 L -> Recognizes m2 (compl L) -> (forall i, Disjoint (m1 i) (m2 i)).
proof: Proof. intros. unfold Disjoint. destruct (run_true_or_negative (m1 i)) as [Ha|Ha], (run_true_or_negative (m2 i)) as [Hb|Hb]; auto. - assert (H_yes: L i) by (eapply recognizes_run_true_to_in; eauto). contradict H_yes. eapply recognizes_run_true_to_in with (L:=compl L) in Hb; eauto. - assert (~ L i). { eauto using recognizes_negative_to_not_in. } assert (Run (m2 i) true). { eapply co_recognizes_not_in_to_run_true; eauto. } run_simpl_all. Qed.
imports: Turing Coq.Bool.Bool