proposition: Lemma par_run_spec: forall m1 m2, (forall i, Disjoint (Call m1 i) (Call m2 i)) -> par_run (fun i => Call m1 i) (fun i => Call m2 i) (par_mach m1 m2).
proof: Proof. intros m1 m2 Hr. unfold par_run. unfold par_mach in *. intros. destruct (run_true_or_negative (Call m1 i)) as [Ha|Hl]; subst. { left. assert (hn: Negative (Call m2 i)). { rewrite disjoint_run_true_1_rw; eauto. } split; auto. rewrite negative_alt_rw in hn. rewrite run_par_rw in *. destruct hn as [hn|hn]. - eapply run_par_both; eauto. constructor. - eapply run_par_l; eauto. constructor. } right. assert (hr: Run (Call m2 i) true). { rewrite disjoint_run_true_2_rw in Hl; eauto. } split; auto. rewrite negative_alt_rw in *. rewrite run_par_rw in *. destruct Hl as [hl|hl]. - eapply run_par_both; eauto. constructor. - eapply run_par_r; eauto. constructor. Qed.
imports: Turing Coq.Bool.Bool