A relation-extended-to-function-quantities is a relation that is defined for both constant-quantities and unary-scalar-function-quantities. The relation holds on some arguments (which may be function-quantities), if and only if whenever all the arguments have a value-at some ?t, the relation holds on those values. The relation may be of any arity. Since value-at is defined for both function-quantities and constant-quantities, a relation-extended-to-function-quantities can be defined on sequences of arguments that are mixes of function-quantities and constant-quantities.For example, the inequality relation < is a relation-extended-to-function-quantities. Consider the case of (< ?x ?y). Whenever (value-at ?x ?t) is defined and (value-at ?y ?t) is defined, then (< (value-at ?x ?t) (value-at ?y ?t)). There can be some ?t for which ?x or ?y is undefined, as long as for those ?t on which they are both defined, they < relation holds on their values. Either ?x or ?y or both can be constant-quantities, since (value-at ?x ?t) is just ?x when ?x is a constant.
Since functions are relations, a function may also be extended to apply to function quantities. The same axioms hold. Intuitively, a the value of a function F over function-quantities qf1 and qf2 is another function-quantity (F qf1 qf2) such that for all ?t where (qf1 ?t) and (qf2 ?t) are defined, (F qf1 qf2) = (F (qf1 ?t) (qf2 ?t)).
(<=> (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))))))