proposition: Theorem reducible_recognizable: forall A B, A <=m B -> Recognizable B -> Recognizable A.
proof: Proof. intros A B Hred Ha. unfold Recognizes in *. destruct Hred as (f, Hr). destruct Ha as (M, Ha). destruct (code_of M) as (R, hc). apply recognizable_def with (p:= fun w => Call R (f w)). apply recognizes_def. intros. rewrite (reduction_rw Hr). rewrite <- (recognizes_rw Ha). rewrite (code_of_run_rw hc). reflexivity. Qed.
imports: Coq.Setoids.Setoid Turing.Turing