proposition: Theorem co_a_tm_not_recognizable: ~ Recognizable (compl A_tm).
proof: Proof. intros N. assert (Hx : Recognizable A_tm /\ Recognizable (compl A_tm)). { split. - apply a_tm_recognizable. - assumption. } apply dec_rec_co_rec in Hx. apply a_tm_undecidable. assumption. Qed.
imports: Coq.Setoids.Setoid Turing.Turing Turing.LangDec Turing.LangRed