proposition: Lemma disjoint_halt_halt: forall m1 m2 i, Disjoint (Call m1 i) (Call m2 i) -> Halt (Call m1 i) -> Halt (Call m2 i) -> exists b, Run (Call m1 i) b /\ Run (Call m2 i) (negb b).
proof: Proof. intros. rewrite halt_rw in *. destruct H0 as ([], Ha), H1 as ([], Hb); eauto. - erewrite <- disjoint_run_true_1_rw in Ha; eauto. run_simpl_all. - assert (Hr: Negative (Call m2 i)). { auto using negative_run_false. } erewrite disjoint_run_true_1_rw in Hr; eauto. Qed.
imports: Turing Coq.Bool.Bool