David Tran’s blog

Axiom 3A
For all p, any r1, r2, and r3:
(r1 `Intersect` (r2 `Union` r3)) `containsR` p
<=> (r1 `containsR` p) && ((r2 `Union` r3) `containsR` p)
<=> (r1 `containsR` p) && (r2 `containsR` p || r3 `containsR` p)
<=> (r1 `containsR` p && r2 `containsR` p) || (r1 `containsR` p && r3 `containsR` p)
<=> (r1 `Intersect` r2) `containsR` p || (r1 `Intersect` r3) `containsR` p
<=> ((r1 `Intersect` r2) `Union` (r1 `Intersect` r3)) `containsR` p
so,
r1 `Intersect` (r2 `Union` r3) <=> (r1 `Intersect` r2) `Union` (r1 `Intersect` r3)

Axiom 3B
For all p, any r1, r2, and r3:
(r1 `Union` (r2 `Intersect` r3)) `containsR` p
<=> (r1 `containsR` p) || ((r2 `Intersect` r3) `containsR` p)
<=> (r1 `containsR` p) || (r2 `containsR` p && r3 `containsR` p)
<=> (r1 `containsR` p || r2 `containsR` p) && (r1 `containsR` p || r3 `containsR` p)
<=> (r1 `Union` r2) `containsR` p && (r1 `Union` r3) `containsR` p
<=> ((r1 `Union` r2) `Intersect` (r1 `Union` r3)) `containsR` p
so,
r1 `Union` (r2 `Intersect` r3) <=> (r1 `Union` r2) `Intersect` (r1 `Union` r3)

Axiom 4A
For all p, any r:
(r `Union` Empty) `containsR` p
<=> (r `containsR` p) || (Empty `containsR` p)
<=> (r `containsR` p) || False
<=> r `containsR` p
so,
r `Union` Empty <=> r

Axiom 4B
For all p, any r:
(r `Intersect` univ) `containsR` p
<=> (r `containsR` p) && ((Complement Empty) `containsR` p)
<=> (r `containsR` p) && (not (Empty `containsR` p))
<=> (r `containsR` p) && (not False)
<=> (r `containsR` p) && True
<=> r `containsR` p
so,
r `Intersect` univ <=> r

Axiom 5A
For all p, any r:
(r `Union` Complement r) `containsR` p
<=> (r `containsR` p) || (Complement r `containsR` p)
<=> (r `containsR` p) || (not (r `containsR` p))
<=> True

and
univ `containsR` p
<=> (Complement Empty) `containsR` p
<=> not (Empty `containsR` p)
<=> not False
<=> True

so,
r `Union` Complement r <=> univ

Axiom 5B
For all p, any r:
(r `Intersect` Complement r) `containsR` p
<=> (r `containsR` p) && (Complement r `containsR` p)
<=> (r `containsR` p) && (not (r `containsR` p))
<=> False

and
Empty `containsR` p
<=> False

so,
r `Intersect` Complement r <=> Empty

This entry was posted on Thursday, May 31st, 2007 at 4:23 pm and is filed under Haskell - SOE. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.