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