proposition: Lemma co_self_tm_unrecognizable: ~ Recognizable (compl SELF_tm).
proof: Proof. intros N. destruct N as (f, Hr). destruct (code_of f) as (p, hp). destruct (run_true_or_negative (Call p (encode_mach p))) as [He|He]. all: run_simpl_all. all: assert (Hx := He). - eapply recognizes_run_true_to_in in He; eauto. unfold compl, SELF_tm in *. contradict He. run_simpl_all. assumption. - assert (~ compl SELF_tm [[ p ]]) by eauto using recognizes_negative_to_not_in. contradict H. unfold compl, SELF_tm. intros N. run_simpl_all. Qed.
imports: Coq.Setoids.Setoid Turing.Turing Turing.LangDec Turing.LangRed