Function DERIV

Slots on this function:

deriv[?x] is the derivative of unary-scalar-function-quantity ?x {deriv[f[x]] = f'[x]}. Deriv is only defined on continuous functions.

Deriv has the normal algebraic properties of derivatives of real-valued functions; see the axioms for the exact behavior of differentiation with respect to sums and products of unary-scalar-function-quantities.

Arity: 2
Domain: Continuous, Unary-scalar-function-quantity
Range: Unary-scalar-function-quantity


(Forall (?F ?G ?R)
        (=> (And (Unary-Scalar-Function-Quantity ?F)
                 (Unary-Scalar-Function-Quantity ?G)
                 (Real-Number ?R))
            (And (= (Deriv (+ ?F ?G)) (+ (Deriv ?F) (Deriv ?G)))
                 (= (Deriv (* ?F ?G))
                    (+ (* (Deriv ?F) ?G) (* ?F (Deriv ?G))))
                 (= (Deriv (Expt ?F ?R))
                    (* ?R (Expt (Deriv ?F) (1- ?R)))))))