fact: Record EfficientProcedureWithOracle (efficient : EfficiencyPredicate) (DP RP DO RO : DataTypeFamily) :={ EPWO_to_concrete : forall n, ProcedureWithOracle (DP n) (RP n) (DO n) (RO n); EPWO_efficient : efficientPWO efficient EPWO_to_concrete }.
imports: FCF CompFold Asymptotic