proposition: Theorem a_tm_undecidable: ~ Decidable A_tm.
proof: Proof. intros N. destruct N as (solve_A, (Hrec, Hdec)). destruct (code_of (negator solve_A)) as (n, Hn). destruct (run_exists (Call n [[n]]) ) as [([], He)|He]. all: assert (Hx := He). - eapply negator_accept in He; eauto. eapply recognizes_run_false_to_not_in in He; eauto. contradict He. unfold A_tm. run_simpl_all. assumption. - eapply negator_reject in He; eauto. eapply recognizes_run_true_to_in in He; eauto. unfold A_tm in *. run_simpl_all. - eapply negator_loop in Hx; eauto. Qed.
imports: Coq.Setoids.Setoid Turing.Turing Turing.LangDec Turing.LangRed