proposition: Lemma a_tm_recognizable: Recognizable A_tm.
proof: Proof. apply recognizable_def with (p:=fun p => let (M, w) := decode_mach_input p in Call M w ). apply recognizes_def. intros. unfold A_tm. destruct (decode_mach_input i) as (p, j). reflexivity. Qed.
imports: Coq.Setoids.Setoid Turing.Turing Turing.LangDec Turing.LangRed