Function VALUE-AT

• Defined in theory: Unary-scalar-functions
• Source code: unary-scalar-functions.lisp

Slots on this function:

Documentation:

The function value-at returns the value of a quantity at some point in 'time' (or whatever the independent state variable is). The 'time' argument is just a constant scalar-quantity, such as a time-quantity. If the quantity is a function-quantity, then its value-at is its function value applied to the 'time' argument. If the quantity is constant-quantity, then its value-at is the quantity itself for all 'times'.

Instance-Of: Function

Arity: 3

Axioms:

(Nth-Domain Value-At 2 Scalar-Quantity)

(Nth-Domain Value-At 1 Physical-Quantity)

Other Related Axioms:

(<- (Value-At ?Q ?Time)
    (If (Function-Quantity ?Q) (Value ?Q ?Time) ?Q))

(Forall (@Args)
        (<=> (Holds ?R @Args)
             (Forall (?T)
                     (=> (=> (Item ?Q (Listof @Args))
                             (Defined (Value-At ?Q ?T)))
                         (Member (Map (Lambda (?Q) (Value-At ?Q ?T))
                                      (Listof @Args))
                                 ?R)))))

(<=> (Holds ?R ?Q1 ?Q2)
     (Forall (?T)
             (=> (And (Defined (Value-At ?Q1 ?T))
                      (Defined (Value-At ?Q2 ?T)))
                 (Holds ?R (Value-At ?Q1 ?T) (Value-At ?Q2 ?T)))))

(<=> (Relation-Extended-To-Function-Quantities ?R)
     (Forall (@Args)
             (<=> (Holds ?R @Args)
                  (Forall (?T)
                          (=> (=> (Item ?Q (Listof @Args))
                                  (Defined (Value-At ?Q ?T)))
                              (Member (Map (Lambda (?Q)
                                                   (Value-At ?Q ?T))
                                           (Listof @Args))
                                      ?R))))))