{"id":37,"date":"2007-08-01T21:46:30","date_gmt":"2007-08-02T04:46:30","guid":{"rendered":"http:\/\/www.elbeno.com\/haskell_soe_blog\/?p=37"},"modified":"2008-01-07T22:26:47","modified_gmt":"2008-01-08T06:26:47","slug":"exercise-88","status":"publish","type":"post","link":"https:\/\/www.elbeno.com\/haskell_soe_blog\/?p=37","title":{"rendered":"Exercise 8.8"},"content":{"rendered":"<p>Leaving aside the argument about axioms by definition not requiring proof&#8230;<\/p>\n<p>Axiom 3:<\/p>\n<pre lang=\"haskell\">(r1 `Intersect` (r2 `Union` r3)) `containsR` p\r\n=> (r1 `containsR` p) && ((r2 `Union` r3) `containsR` p)\r\n=> (r1 `containsR` p) && ((r2 `containsR` p) || (r3 `containsR` p))\r\n=> ((r1 `containsR` p) && (r2 `containsR` p))\r\n  || ((r1 `containsR` p) && (r3 `containsR` p))\r\n=> ((r1 `Intersect` r2) `containsR` p) || ((r1 `Intersect` r3) `containsR` p)\r\n=> ((r1 `Intersect` r2) `Union` (r1 `Intersect` r3)) `containsR` p\r\n\r\n\u00e2\u02c6\u00b4 (r1 `Intersect` (r2 `Union` r3))\r\n  \u00e2\u2030\u00a1 ((r1 `Intersect` r2) `Union` (r1 `Intersect` r3))\r\n\r\n(r1 `Union` (r2 `Intersect` r3)) `containsR` p\r\n=> (r1 `containsR` p) || ((r2 `Intersect` r3) `containsR` p)\r\n=> (r1 `containsR` p) || ((r2 `containsR` p) && (r3 `containsR` p))\r\n=> ((r1 `containsR` p) || (r2 `containsR` p))\r\n  && ((r1 `containsR` p) || (r3 `containsR` p))\r\n=> ((r1 `Union` r2) `containsR` p) && ((r1 `Union` r3) `containsR` p)\r\n=> ((r1 `Union` r2) `Intersect` (r1 `Union` r3)) `containsR` p\r\n\r\n\u00e2\u02c6\u00b4 (r1 `Union` (r2 `Intersect` r3))\r\n  \u00e2\u2030\u00a1 ((r1 `Union` r2) `Intersect` (r1 `Union` r3))<\/pre>\n<p>Axiom 4:<\/p>\n<pre lang=\"haskell\">univ = Complement Empty\r\n\r\n(r `Union` Empty) `containsR` p\r\n=> (r `containsR` p) || (Empty `containsR` p)\r\n=> (r `containsR` p) || False\r\n=> r `containsR` p\r\n\r\n\u00e2\u02c6\u00b4 (r `Union` Empty) \u00e2\u2030\u00a1 r\r\n\r\n(r `Intersect` univ) `containsR` p\r\n=> (r `Intersect` Complement Empty) `containsR` p\r\n=> (r `containsR` p) && (Complement Empty `containsR` p)\r\n=> (r `containsR` p) && not (Empty `containsR` p)\r\n=> (r `containsR` p) && not False\r\n=> (r `containsR` p) && True\r\n=> r `containsR` p\r\n\r\n\u00e2\u02c6\u00b4 (r `Intersect` univ) \u00e2\u2030\u00a1 r<\/pre>\n<p>Axiom 5:<\/p>\n<pre lang=\"haskell\">(r `Union` Complement r) `containsR` p\r\n=> (r `containsR` p) || (Complement r `containsR` p)\r\n=> (r `containsR` p) || not (r `containsR` p)\r\n=> True\r\n=> not False\r\n=> not (Empty `containsR` p)\r\n=> Complement Empty `containsR` p\r\n=> univ `containsR` p\r\n\r\n\u00e2\u02c6\u00b4 (r `Union` Complement r) \u00e2\u2030\u00a1 univ\r\n\r\n(r `Intersect` Complement r) `containsR` p\r\n=> (r `containsR` p) && (Complement r `containsR` p)\r\n=> (r `containsR` p) && not (r `containsR` p)\r\n=> False\r\n=> Empty `containsR` p\r\n\r\n\u00e2\u02c6\u00b4 (r `Intersect` Complement r) \u00e2\u2030\u00a1 Empty<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>Leaving aside the argument about axioms by definition not requiring proof&#8230; Axiom 3: (r1 `Intersect` (r2 `Union` r3)) `containsR` p => (r1 `containsR` p) &#038;&#038; ((r2 `Union` r3) `containsR` p) => (r1 `containsR` p) &#038;&#038; ((r2 `containsR` p) || (r3 `containsR` p)) => ((r1 `containsR` p) &#038;&#038; (r2 `containsR` p)) || ((r1 `containsR` p) &#038;&#038; [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":[],"categories":[1],"tags":[],"_links":{"self":[{"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=\/wp\/v2\/posts\/37"}],"collection":[{"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=37"}],"version-history":[{"count":0,"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=\/wp\/v2\/posts\/37\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=37"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=37"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=37"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}