fact: Definition admissible_oc_func_2(cost : FunctionCostModel)(A B C D E : nat -> Set)(c : forall n, A n -> B n -> OracleComp (C n) (D n) (E n)) := (forall n a b, well_formed_oc (c n a b)) /\ poly_time_nonuniform_oc_func_2 cost _ _ _ _ _ c /\ polynomial_queries_oc_func_2 _ _ _ _ _ c.
imports: FCF.FCF FCF.Admissibility FCF.Asymptotic