proposition: Lemma a_tm_red_eq_tm: 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 true) ]] in let M2 : input := [[ compile (Call M w) ]] in encode_pair (M1 , M2) ). unfold EQ_tm; split; intros. - destruct (decode_mach_input w) as (M, x) eqn:Heq. run_simpl_all. intros. run_simpl_all. split; intros; run_simpl_all. + unfold A_tm in *. rewrite Heq in *. assumption. + apply run_ret. - unfold A_tm. destruct (decode_mach_input w) as (M, x) eqn:Heq. run_simpl_all. specialize (H w). run_simpl_all. rewrite <- H. constructor. Qed.
imports: Coq.Setoids.Setoid Turing.Turing Turing.LangDec Turing.LangRed