! relation.txt - utility predicates for ordering & [in]equality predicates
!/
(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 is not in a sequence (given /=)
(different ) - all elements in sequence are pair-wise unequal
(different- ) - all different elements in seq are from named set
!\
! ? Should we define lexicographic ordering (< ) on set elements?
! " other relations (<= ), (> ), ... 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).