Class UNARY-SCALAR-FUNCTION-QUANTITY


Slots on this class:

Documentation:
A unary function that maps from a scalar-quantity to a scalar-quantity.
Instance-Of: Class
Subclass-Of: Function-quantity, Unary-function
Domain-Of: Deriv
Range-Of: Deriv, The-identity-unary-scalar-function-for-domain
Superclass-Of: Continuous, Time-dependent-quantity


Slots on instances of this class:

Domain: Scalar-quantity
Range: Scalar-quantity

Equivalence Axioms:

(<=> (Unary-Scalar-Function-Quantity ?X)
     (And (Function-Quantity ?X)
          (Unary-Function ?X)
          (Domain ?X Scalar-Quantity)
          (Range ?X Scalar-Quantity)))


Axioms:

(Unary-Function ?X)

(Function-Quantity ?X)


Other Related Axioms:

(<= (Range $X Scalar-Quantity) (Unary-Scalar-Function-Quantity $X))

(<= (Domain $X Scalar-Quantity) (Unary-Scalar-Function-Quantity $X))

(<=> (Unary-Scalar-Function-Quantity ?X)
     (And (Function-Quantity ?X)
          (Unary-Function ?X)
          (Domain ?X Scalar-Quantity)
          (Range ?X Scalar-Quantity)))

(=> (And (Unary-Scalar-Function-Quantity ?X)
         (Unary-Scalar-Function-Quantity ?Y)
         (+ ?X ?Y ?Z))
    (Unary-Scalar-Function-Quantity ?Z))

(=> (And (Unary-Scalar-Function-Quantity ?X)
         (Unary-Scalar-Function-Quantity ?Y)
         (* ?X ?Y ?Z))
    (Unary-Scalar-Function-Quantity ?Z))

(=> (And (Unary-Scalar-Function-Quantity ?X) (Recip ?X ?Y))
    (Unary-Scalar-Function-Quantity ?Y))

(=> (And (Unary-Scalar-Function-Quantity ?X)
         (Real-Number ?R)
         (Expt ?X ?R ?Z))
    (Unary-Scalar-Function-Quantity ?Z))

(=> (The-Identity-Unary-Scalar-Function-For-Domain $X $Y)
    (Unary-Scalar-Function-Quantity $Y))

(Nth-Domain The-Zero-Unary-Scalar-Function-For-Dimension
            3
            Unary-Scalar-Function-Quantity)

(=> (Deriv $X $Y) (Unary-Scalar-Function-Quantity $Y))

(=> (Deriv $X $Y) (Unary-Scalar-Function-Quantity $X))

(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)))))))

(<=> (Time-Dependent-Quantity ?X)
     (And (Unary-Scalar-Function-Quantity ?X)
          (Continuous ?X)
          (Subclass-Of (Exact-Domain ?X) Time-Quantity)))