b>0 and CApprox(n,up,um,ud,trace) and e=2^n and [(b*um+ap*ud)*e+2*b*ud < (b*up+am*ud)*e or (b*up+am*ud)*e+2*b*ud < (b*um+ap*ud)*e].
Proposed arity: 9. Parameters: ap am b n up um ud e trace. No reviewed kernel definition exists yet.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.