proposition: Lemma co_a_tm_red_eq_tm: compl A_tm <=m EQ_tm.
proof: Proof. apply reducible_iff with (f:=fun p => let (M, w) := decode_mach_input p in let M1 : input := [[ compile (Ret false) ]] in let M2 : input := [[ compile (Call M w) ]] in encode_pair (M1 , M2) ). unfold EQ_tm; split; intros. - unfold A_tm, compl in *. destruct (decode_mach_input w) as (M, x) eqn:Heq. run_simpl_all. intros. repeat rewrite compile_run_rw. split; intros. { run_simpl_all. } contradiction. - destruct (decode_mach_input w) as (M, x) eqn:Heq. run_simpl_all. intros N. specialize (H x). assert (Hm: Run (Call M x) true). { unfold A_tm in *. rewrite Heq in *. assumption. } clear N. repeat rewrite compile_run_rw in H. rewrite <- H in Hm. inversion Hm. Qed.
imports: Coq.Setoids.Setoid Turing.Turing Turing.LangDec Turing.LangRed