proposition: Lemma par_mach_lang: forall m1 m2, (forall i, Disjoint (Call m1 i) (Call m2 i)) -> Recognizes (par_mach m1 m2) (fun i => Run (Call m1 i) true).
proof: Proof. unfold par_mach. intros m1 m2 Hr; intros. unfold Recognizes; intros. rewrite run_par_rw in *. split; intros. { inversion H; subst; clear H; run_simpl_all. * destruct b; run_simpl_all. assumption. * destruct b; run_simpl_all. assert (Ha: Negative (Call m1 i)). { auto using negative_loop. } rewrite (disjoint_run_true_2_rw _ _ (Hr i)) in *. run_simpl_all. * destruct b1; run_simpl_all. assumption. } destruct (halt_or_loop (Call m2 i)) as [He|Hl]. { assert (Run (Call m2 i) false). { rewrite halt_rw in *. destruct He as ([],He); auto. rewrite <- (disjoint_run_true_1_rw _ _ (Hr i)) in H. run_simpl_all. } eapply run_par_both; eauto. constructor. } apply run_par_l with (b:=true); auto. constructor. Qed.
imports: Turing Coq.Bool.Bool