proposition: Lemma recognizable_co_recognizable_to_decidable: forall L, Recognizable L -> Recognizable (compl L) -> Decidable L.
proof: Proof. intros. destruct H as (f_pos, Hpos). destruct H0 as (f_neg, Hneg). destruct (code_of f_pos) as (m_pos, c_pos). destruct (code_of f_neg) as (m_neg, c_neg). destruct par_run_exists with (m1:=m_pos) (m2:=m_neg) as (mpar, (Hr,Hp)). { intros. apply recognizes_co_recognizes_disjoint with (m1:=Call m_pos) (m2:=Call m_neg) (L:=L); eauto. - unfold Recognizes in *. intros k. rewrite <- Hpos. rewrite (code_of_run_rw c_pos). reflexivity. - unfold Recognizes in *. intros k. rewrite <- Hneg. rewrite (code_of_run_rw c_neg). reflexivity. } apply decidable_def with (p:=mpar). apply decides_def. + unfold Recognizes. intros. rewrite (Hr i). rewrite (code_of_run_rw c_pos). rewrite (recognizes_accept_rw Hpos). reflexivity. + unfold Decider. intros. assert (Hp := Hp i). intuition; eauto using run_to_halt. Qed.
imports: Turing Coq.Bool.Bool