! ho.txt - axioms for higher-order predicates !/ (finite_set ) - defines finite set of elements ((< ) ) - ordering of finite set elements (ord ) - ordinal number of a finite set element (all_valid ....) - valid if all exprs in list are valid (one_valid ....) - valid if one expr in list is valid (valid ....) - conclusion used to generate all exprs in list as valid (axiom ....) - define axiom in an expression (axioms ....) - generate a set of axioms from an expression (all ) - sequence with all its elements from a specified set (1* ) - binary rel between 1 arg1 and many arg2s (binrel* ) - binary rel applies to each pair of elems in seq ((map ) ....) - map predicate to sequences of arguments !\ ! finite_set - a finite set defined in a single valid expression ! (finite_set ) ! (used as an axiom conclusion) (%set %elem)< ! define finite set of elements (finite_set %set (\$1 %elem \$2)). ! (< ) - ordering of finite set elements ((< %set) %elem1 %elem2)< (finite_set %set (\$a %elem1 \$b %elem2 \$c)). ! -- Note that we could use this to define a particular character ordering: ! (finite_set display_order "...AaBbCc...")). ! all_valid - expression is valid if all expressions in list are valid ! (used as an axiom condition) (all_valid). ! empty list has all-valid exprs (all_valid % \$)< ! adding a valid expr to list % , (all_valid \$). ! -- Note that we need the space before the comma to keep the comma ! from being part of the expression variable symbol. ! one_valid - at least one expression in list is valid ! (used as a condition) (one_valid \$1 % \$2)< % . ! valid - generate all expressions in list as valid expressions ! (used as a conclusion) % < (valid \$1 % \$2). ! axiom - represent an axiom in an expression ! (axiom ....) ! (used asa conclusion) %conclu < (axiom %conclu \$conds), ! conclusion is valid, (all_valid \$conds). ! if all axiom conditions are valid ! axioms - generate a set of axioms from an expression ! (axioms ....) ! (used as a conclusion) (axiom \$axiom)< (axioms \$1 (\$axiom) \$2). ! all - sequence with all its elements from a specified set ! (all (..elems..)) ! (used as a condition) (all %setname ()). (all %setname (%elem \$elems))< (%setname %elem), (all %setname (\$elems)). ! 1* - binary relation applies between 1 first arg and sequence of second args ! (1* ) ! (used as a condition) (1* %binrel %arg1 ()). ! relation holds if no second args (1* %binrel %arg1 (%arg2 \$arg2s))< (%binrel %arg1 %arg2), (1* %binrel %arg1 (\$arg2s)). ! binrel* - binary relation applies all pairs of elements in sequence ! (binrel* ) (binrel* %rel ()). ! relation applies vacuously to empty sequence (binrel* %rel (% \$))< (1* %rel % (\$)), ! new elem has relation to all elems in sequence (binrel* %rel (\$)). ! map - map predicate to sequences of arguments ((map %pred) \$nulls)< ! map always applies if no argument tuples (nulls \$nulls). ((map %pred) \$argseqs')< ((map %pred) \$argseqs), (%pred \$args), (distr (\$args) (\$argseqs) (\$argseqs')).