proposition: Theorem E_tm_undecidable: ~ Decidable E_tm.
proof: Proof. intros HD. destruct HD as (solve_E, H). destruct (code_of solve_E) as (s, hs). apply a_tm_undecidable. destruct (closure_of (fun p x => let (M, w) := decode_mach_input p in if input_eq_dec x w then ( Call M w ) else Ret false ) ) as (inner, Hr). apply decidable_def with (p:= fun p => let (M, w) := decode_mach_input p in mlet b <- Call s [[ inner p ]] in if b then Ret false else Ret true ). apply decides_def. { apply recognizes_def; intros. unfold A_tm. destruct (decode_mach_input i) as (p, j) eqn:r1. assert (rw1: Run (Call p j) true <-> Run (Call s [[ inner i ]]) false). { run_simpl_all. erewrite decides_false_rw; eauto. unfold E_tm. run_simpl. split; intros. { intros N. specialize (N j). rewrite (closure_of_negative_rw Hr) in N. rewrite r1 in *. destruct (input_eq_dec j j); try contradiction. rewrite negative_rw in *. contradiction. } destruct (run_true_or_negative (Call p j)) as [Ht|Hf]; auto. match goal with H: ~ (forall i, Negative _) |- _ => contradict H end. intros k. rewrite (closure_of_negative_rw Hr) in *. rewrite r1. destruct (input_eq_dec k j). { subst. assumption. } apply negative_ret. } rewrite rw1; clear rw1. split; intros hr. { inversion_clear hr. run_simpl_all. destruct b1; run_simpl_all. assumption. } apply run_seq with (b1:=false); auto. constructor. } apply decider_def. intros i. destruct (decode_mach_input i) as (p, j) eqn:hr1. apply halt_seq_alt. { run_simpl_all. eauto using decides_to_halt. } intros. destruct b; constructor. Qed.
imports: Coq.Setoids.Setoid Turing.Turing Turing.LangDec Turing.LangRed