! ho.txt - axioms for higher-order predicates
!/
  (finite_set <set> <elem_seq>) - defines finite set of elements
  ((< <set>) <elem1> <elem2>) - ordering of finite set elements 
  (ord <set> <elem> <n>) - ordinal number of a finite set element
  (all_valid ..<expr>..) - valid if all exprs in list are valid
  (one_valid ..<expr>..) - valid if one expr in list is valid
  (valid ..<expr>..) - conclusion used to generate all exprs in list as valid
  (axiom <conclu> ..<conds>..) - define axiom in an expression
  (axioms ..<axiom>..) - generate a set of axioms from an expression
  (all <setname> <seq>) - sequence with all its elements from a specified set
  (1* <binrel> <arg1> <arg2_seq>) - binary rel between 1 arg1 and many arg2s
  (binrel* <binrel> <seq>) - binary rel applies to each pair of elems in seq
  ((map <pred>) ..<arg seqs>..) - map predicate to sequences of arguments
!\

! finite_set - a finite set defined in a single valid expression
!    (finite_set <setname> <elem_sequence>)
! (used as an axiom conclusion)

  (%set %elem)<            ! define finite set of elements
    (finite_set %set ($1 %elem $2)).

! (< <set>) - 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 <conclu> ..<conds>..)
! (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 ..<axiom>..)
! (used as a conclusion)

  (axiom $axiom)< (axioms $1 ($axiom) $2).

! all - sequence with all its elements from a specified set
! (all <setname> (..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* <binrel> <arg1> <arg2_seq>)
! (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> <seq>)

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