Instant

Distinction | Partial Order | Total Order


  1.Distinction
   Introduces: s , _ is _.
  • s = ž.
  • _ is _ :: s , s -> truth-value (partial, commutative).
    (1) x:s is x = true.
    (2)x is y = true; y:s; y is z = true => x:s is z:s = true.
    (3) x is y = false => (x:s)&(y:s) = nothing.


   2.Partial Order


   Includes: Distinction (s , _ is _).
   Introduces: _ is less than _, _ is greater than _.
  • _ is _ :: s, s -> truth-value (total, commutative).
  • _ is less than _ :: s, s -> truth-value (total).
  • _ is greater than _ :: s, s -> truth-value (total).

   (1) x:s is less than y:s = true => y is less than x = false; x is y = false .
   (2) x:s is y:s = true => x is less than y = false.
   (3) x is less than y = true; y:s ; y is less than z = true => x:s is less than z:s = true .
   (4) x:s is y:s = true; y is less than z:s = true => x is less than z = true.
   (5) x:s is y:s = true; z:s is less than y = true => z is less than x = true.
   (6) x:s is greater than y:s = y is less than x.



     3.Total Order


  Includes: Partial Order: (s , _ is _ , _ is less than _ , _is greater than _).
  Introduces: _ [min _ ] , _ [max _ ] .
  • _ [min _ ] :: s, s -> s (partial).
  • _ [max _ ] :: s, s -> s (partial).
    (1) any (x is less than y, x:s is y:s, y is less than x) = true.
    (2) (y:s) [min x:s] = when not (y is less than x) then y.
    (3) (y:s) [max x:s] = when not (y is greater than x) then y.
    (4) (z <= s) [min x:s] = z & s [min x] .
    (5) (z <= s) [max x:s] = z & s [max x] .
    (6) (z <= s) [min x:s] [max y:s] = z [max y] [min x].
    (7) y is less than x = true => (z <= s) [min x:s] [max y:s] = nothing.


   Data Notation | Tuples | Truth-Values | Numbers | Characters | Lists | Strings | Syntax | Sets | Maps