Distinction | Partial Order | Total Order

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.

 Back to the beginning.

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.

 Back to the beginning.
 

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.

 Back to the beginning.










WebAni |
Ani | 
RAT | 
AG | 
Actions | 
People |
Action Notation | 
Data Notation







[Created by Jin Jin Yi and Ana Carla Santos. Last modified at 21 Dec 1997 by Jin Jing Yi]