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.
|