! noteq.ax - utility predicates related to inequality of expressions
! -- Note that inequality is not built in, so we basicaly define inequality
!    between expressions based on "explicitly declared" atoms.

! commutativity of /=

  (/= %1 %2)< (/= %2 %1).
     ! -- eliminates some axioms below

! "declaring" a set of atoms

  (atoms ` `0 `1 `char).

! defining inequality between distinct ["declared"] atoms

  (/= %1 %2)< (atoms $a %1 $b %2 $c).
     ! -- (/= %2 %1) follows from commutativity axiom

! defining inequality between ["declared"] atom and a sequence

  (/= % ($))< (atoms $a % $b).
     ! -- (/= ($) %) likewise

! /= - inequality on sequences

  (/= () (% $)).      ! inequality between sequences of different length
     ! -- (/= (% $) ()) follows

  (/= (%1 $1) (%2 $2))<  ! inequality for unequal sub-expressions
    (/= %1 %2).

  (/= (% $1) (% $2))<    ! skip identical prefixes
    (/= ($1) ($2)).

! From the above axioms we get inequality between distinct characters,
! character strings, and symbols.

! not_in - expression not in sequence

  (not_in %x ()).
  (not_in %x (% $))<
    (/= %x %),
    (not_in %x ($)).

! all_diff - all elements in a sequence are different

  (all_diff ()).
  (all_diff (% $))<
    (all_diff ($)),
    (not_in % ($)).

! elim_dupl - eliminate duplicate elements from a sequence
! (elim_dupl <seq w duplications> <seq w/o duplications>)

!/ old:
  (elim_dupl %nodups %nodups)<
    (all_diff %nodups).
  (elim_dupl %dups' %nodups)<
    (elim_dupl %dups %nodups),
    (in % %nodups),
    (insert % %dups %dups').     ! duplicate another element

 ! The above definition constrains the order of the unduplicated elements.
!\
 ! An alternative definition below allows duplicates in any order.

  (elim_dupl () ()).
  (elim_dupl %dups' (% $nodups))<    ! adding 1st occurrence of an element
    (elim_dupl %dups ($nodups)),
    (not_in % ($nodups)),
    (insert % %dups %dups').
  (elim_dupl %dups' %nodups)<        ! adding repeat occurrence of an element
    (elim_dupl %dups %nodups),
    (in % %nodups),             ! or (in % %dups),
    (insert % %dups %dups').

! union - get union of two sets (with no duplicates in result)

  (union ($set1) ($set2) %union)<
    (elim_dupl ($set1 $set2) %union).
      ! union elements are nondeterministically in any order and w/o duplicates

! merge_sets - merge two sets sharing a common element

  (merge_sets ($sets1 %setA $sets2 %setB $sets3)
              ($sets1 $sets2 $sets3 %setAB))<
    (in %e %setA),         ! same element is in both sets A & B
    (in %e %setB),
    (union %setA %setB %setAB).      ! union the sets

! disjoint - two sets (sequences) are disjoint (no elements in common)

  (disjoint () ($set)).
  (disjoint (% $) ($set))<
    (not_in % ($set)),
    (disjoint ($) ($set)).

  ! *** use higher-order definition from /=

! disjoint_all - a set is disjoint wrt all sets in a sequence
! *** use higher-order form here!

  (disjoint_all %set ()).
  (disjoint_all %set (% $))<
    (disjoint %set %),
    (disjoint_all %set ($)).

! partition - a set of sets is a partition if sets are pairwise disjoint

  (partition ()).                ! no sets is a partition
  (partition (%set $sets))<
    (partition ($sets)),
    (disjoint_all %set ($sets)).    ! new set disjoint wrt other sets

 
! Boolean functions involving inequality tests
! -- These return atoms `t or `f.

! ==? - test if two (comparable) expressions are identical or not

  (==? % % `t).         ! expressions are identical

  (==? %1 %2 `f)<       ! expressions have inequality defined between them
    (/= %1 %2).

!/ possible extension:
! ==? - variation of ==? for a single >=2-element sequence argument:

  (==? (%a %b $) %t/f)<
    (==? %a %b %t/f).
    ! -- any elements beyond the second are ignored
!\ -- for now we will use the "1" higher-order form

! in? - test if expression is in a sequence

  (in? %expr %seq `t)<
    (in %expr %seq).
  (in? %expr %seq `f)<
    (not_in %expr %seq).

! in_set? - test whether expression is element of a finite set
! ((in_set? <set_name>) <elem> <t/f>)

  ((in_set? %set) %elem %t/f)<
    (finite_set %set %elems),
    (in? %elem %elems %t/f).

  ! -- This only works if finite set elements have inequality relation defined
  !    (A finite set of atoms probably would not.)
 
! prefix? - test whether first sequence is a prefix of the second

  (prefix? ($pre) ($pre $suf) `t).        ! is prefix
  (prefix? ($pre %1 $1) ($pre) `f).        ! not prefix - 2nd arg too short
  (prefix? ($pre %1 $1) ($pre %2 $2) `f)<   ! not prefix - unequal expressions
    (/= %1 %2).

! not - Boolean 'not' function

  (not `f `t).
  (not `t `f).

! and - Boolean 'and' function 

  (and `f `f `f).
  (and `f `t `f).
  (and `t `f `f).
  (and `t `t `t).

! or - Boolean 'or' function

  (or `f `f `f).
  (or `f `t `t).
  (or `t `f `t).
  (or `t `t `t).


! subset - a sequence [set] of elements is contained in another sequence [set]

  (subset () %seq).
  (subset (% $) %seq)<
    (in % %seq),
    (subset ($) %seq).

 ! or:

   (subset %elems %seq)<
     ((*1 in) %elem %seq).

! ~subset - a sequence [set] is not contained in another sequence [set]

  (~subset ($1 % $2) %seq)<   ! not a subset if
    (not_in % %seq).          !  any element not in sequence

! subset? - Boolean test for one sequence a subset of another

  (subset? %elems %seq `t)< (subset %elems %seq).
  (subset? %elems %seq `f)< (~subset %elems %seq).

! =sets? - test for two sets being "equal"

  (=sets? %set1 %set2 %t/f)<      ! 2 sets equal if each is subset of other
    (subset? %set1 %set2 %t/f1),
    (subset? %set2 %set1 %t/f2),
    (and %t/f1 %t/f2 %t/f).

  ! -- Note that element duplications are ok and order doesn't matter.

! set_in - a set is in a sequence of sets

  (set_in %set ($1 % $2))<
    (=sets %set %).

! ~set_in - a set is not in a sequence of sets

  (~set_in %set ()).
  (~set_in %set (% $))<
    (=sets? %set % `f),   ! arg1 set not equal to each set in arg2 sequence
    (~set_in %set ($)).

! subsset - a set of sets is a subset of another set of sets
! *** We use the notation "sset" for "set of sets".

  (subsset () %seq).
  (subsset (% $) %seq)<
    (set_in % %seq),
    (subsset ($) %seq).

! ~subsset - a set of sets is not a subset of another set of sets

  (~subsset ($1 % $2) %seq)<    ! not a subsset if
    (~set_in % %seq).           !  any set not in sset

! subsset? - Boolean test for one sset a subset of another sset

  (subsset? %sset1 %sset2 `t)< (subsset %sset1 %sset2).
  (subsset? %sset1 %sset2 `f)< (~subsset %sset1 %sset2).

! =ssets? - test for two sets-of-sets being equal

  (=ssets? %sset1 %sset2 %t/f)<     ! each a subsset of the other?
    (subsset %sset1 %sset2 %t/f1),
    (subsset %sset2 %sset1 %t/f2),
    (and %t/f1 %t/f2 %t/f).
  
! *** Note that =ssets? is defined from =sets? the same way =sets? can be
!     defined from ==?.  A higher-order form could be used here!