! relation.txt - utility predicates for ordering & [in]equality predicates
!/
  (bit <bit>) - set of bit atoms (`0 `1)
  < - ordering for natural numbers and bits
  < - lexicographic ordering of sequences of number & bit expressions
  <=, >, >=, /= - other relational operations defined from <
  = - identical expressions (same as ==)
  (not_in <x> <seq>) - x is not in a sequence (given /=)
  (different <seq>) - all elements in sequence are pair-wise unequal
  (different- <set> <seq>) - all different elements in seq are from named set
!\

! ? Should we define lexicographic ordering (< <set>) on set elements?
!            "       other relations (<= <set>), (> <set>), ... too?

! bit - set of bit atoms

  (finite_set bit (`0 `1)).
  ! -- this defines ord and < on bit atoms

! < - top-level ordering relation applies to natural numbers or bits

  (< %1 %2)< (one_valid ((< num) %1 %2) ((< bit) %1 %2)).
  ! -- note that natural number and bit types are distinct

! < - lexicographic ordering of expressions with natural numbers and bits

  (< ($) ($ % $x)).
  (< ($ %1 $1) ($ %2 $2))< (< %1 %2).

  ! From bit ordering we get ordering of characters, char strings, and symbols. 

! <=, >, >=, /= - other ordering relations

  (<= % %).
  (<= %1 %2)< (< %1 %2).

  (> %1 %2)< (< %2 %1).

  (>= %1 %2)< (<= %2 %1).

  (/= %1 %2)< (one_valid (< %1 %2) (> %1 %2)).
  ! This gives inequality between distinct characters, character strings,
  ! and symbols, as well as different natural numbers.

! = - equal (identical) expressions
! (Might be nice to limit this to just natural number & bit expressions?)

  (= % %).

! not_in - (not_member) - element is not in a sequence (given /= relation)
! -- This is only defined where the inequality relation /= holds.

  (not_in %x %seq)<
    (1* /= %x %seq).

! different - all elements in sequence are pair-wise unequal (/=)

  (different %seq)<
    (binrel* /= %seq).

! different- - all different elements in sequence are from the named set
! - set must have inequality relation defined

  (different- %set %seq)<
    (all %set %seq),
    (different %seq).