proposition: Theorem HALT_tm_undecidable: ~ Decidable HALT_tm.
proof: Proof. intros N. destruct N as (solves_HALT, H). apply a_tm_undecidable. apply decidable_def with (p:=fun p => let (M, w) := decode_mach_input p in mlet b <- solves_HALT p in if b then Call M w else Ret false ). apply decides_def. { unfold A_tm. constructor. all: intros Ha. all: destruct (decode_mach_input i) as (p, j) eqn:r1. - inversion Ha; subst; clear Ha. destruct b1. + assumption. + inversion H4. - apply run_seq with (b1:=true). + apply decides_in_to_run_true with (L:=HALT_tm); auto. unfold HALT_tm. rewrite r1. eauto using run_to_halt. + assumption. } apply decider_def. intros. destruct (decode_mach_input i) as (p, j) eqn:r1. apply halt_seq_alt. { eauto using decides_to_halt. } intros. destruct b. - apply decides_run_true_to_in with (L:=HALT_tm) in H0. + unfold HALT_tm in *. rewrite r1 in *. assumption. + assumption. - constructor. Qed.
imports: Coq.Setoids.Setoid Turing.Turing Turing.LangDec Turing.LangRed