fact: Definition poly_time_nonuniform(cost : CostModel)(A B : nat -> Type)(f : forall n, (A n) -> (B n)) := exists x, polynomial x /\ forall n, (exists c, (cost _ _ (f n)) c /\ c <= x n).
imports: FCF.Crypto FCF.Asymptotic