proposition: Theorem co_a_tm_unrecognizable: ~ Recognizable (compl A_tm).
proof: Proof. apply reducible_unrecognizable with (A:=compl SELF_tm). - apply co_a_tm_red_co_self_tm. - apply co_self_tm_unrecognizable. Qed.
imports: Coq.Setoids.Setoid Turing.Turing Turing.LangDec Turing.LangRed