* algebra/boolean.spad.pamphlet (PropositionalLogic): New category.

	(Boolean): Assert as belonging to PropositionalLogic.
	Update cached Lisp translation.
	* algebra/Makefile.pamphlet (axiom_algebra_layer_0): Add
	PROPLOG.o
	* src/algebra: Update databases.

3 files changed, 182 insertions, 258 deletions

diff --git a/src/algebra/Makefile.in b/src/algebra/Makefile.in
index a974ad21..7fe8dd8f 100644
--- a/src/algebra/Makefile.in
+++ b/src/algebra/Makefile.in
@@ -377,7 +377,7 @@ axiom_algebra_layer_0 = \
   KOERCE.o  KONVERT.o MSYSCMD.o ODEIFTBL.o \
   OM.o      OMCONN.o  OMDEV.o   OUT.o      \
   PRIMCAT.o PRINT.o   PTRANFN.o SPFCAT.o   \
-  TYPE.o    UTYPE.o
+  TYPE.o    UTYPE.o   PROPLOG.o
 
 axiom_algebra_layer_0_nrlibs = \
 	$(axiom_algebra_layer_0:.$(OBJEXT)=.NRLIB/code.$(OBJEXT))
diff --git a/src/algebra/Makefile.pamphlet b/src/algebra/Makefile.pamphlet
index 45f1f2bd..70a3f05c 100644
--- a/src/algebra/Makefile.pamphlet
+++ b/src/algebra/Makefile.pamphlet
@@ -205,7 +205,7 @@ axiom_algebra_layer_0 = \
   KOERCE.o  KONVERT.o MSYSCMD.o ODEIFTBL.o \
   OM.o      OMCONN.o  OMDEV.o   OUT.o      \
   PRIMCAT.o PRINT.o   PTRANFN.o SPFCAT.o   \
-  TYPE.o    UTYPE.o
+  TYPE.o    UTYPE.o   PROPLOG.o
 
 axiom_algebra_layer_0_nrlibs = \
 	$(axiom_algebra_layer_0:.$(OBJEXT)=.NRLIB/code.$(OBJEXT))
diff --git a/src/algebra/boolean.spad.pamphlet b/src/algebra/boolean.spad.pamphlet
index 84632fa5..85b2c056 100644
--- a/src/algebra/boolean.spad.pamphlet
+++ b/src/algebra/boolean.spad.pamphlet
@@ -1,14 +1,39 @@
 \documentclass{article}
 \usepackage{axiom}
+
+\title{src/algebra boolean.spad}
+\author{Stephen M. Watt, Michael Monagan, Gabriel Dos~Reis}
+
 \begin{document}
-\title{\$SPAD/src/algebra boolean.spad}
-\author{Stephen M. Watt, Michael Monagan}
 \maketitle
 \begin{abstract}
 \end{abstract}
-\eject
+
 \tableofcontents
 \eject
+
+\section{category PROPLOG PropositionalLogic}
+<<category PROPLOG PropositionalLogic>>=
+)abbrev category PROPLOG PropositionalLogic
+++ Author: Gabriel Dos Reis
+++ Date Created: Januray 14, 2008
+++ Date Last Modified: January 14, 2008
+++ Description: This category declares the connectives of
+++ Propositional Logic.
+PropositionalLogic(): Category == with
+  "not": % -> %
+    ++ not p returns the logical negation of `p'.
+  "and": (%, %) -> %
+    ++ p and q returns the logical conjunction of `p', `q'.
+  "or": (%, %) -> %
+    ++ p or q returns the logical disjunction of `p', `q'.
+  implies: (%,%) -> %
+    ++ implies(p,q) returns the logical implication of `q' by `p'.
+  equiv: (%,%) -> %
+    ++ equiv(p,q) returns the logical equivalence of `p', `q'.
+@
+
+
 \section{domain REF Reference}
 <<domain REF Reference>>=
 )abbrev domain REF Reference
@@ -131,20 +156,13 @@ Logic: Category == BasicType with
 ++ Description:  \spadtype{Boolean} is the elementary logic with 2 values:
 ++ true and false
 
-Boolean(): Join(OrderedSet, Finite, Logic, ConvertibleTo InputForm) with
+Boolean(): Join(OrderedSet, Finite, Logic, PropositionalLogic, ConvertibleTo InputForm) with
     true   : constant -> %
       ++ true is a logical constant.
     false  : constant -> %
       ++ false is a logical constant.
     _^    : % -> %
       ++ ^ n returns the negation of n.
-    _not : % -> %
-      ++ not n returns the negation of n.
-    _and  : (%, %) -> %
-      ++ a and b  returns the logical {\em and} of Boolean \spad{a} and b.
-    _or  : (%, %) -> %
-      ++ a or b returns the logical inclusive {\em or}
-      ++ of Boolean \spad{a} and b.
     xor    : (%, %) -> %
       ++ xor(a,b) returns the logical exclusive {\em or}
       ++ of Boolean \spad{a} and b.
@@ -152,9 +170,6 @@ Boolean(): Join(OrderedSet, Finite, Logic, ConvertibleTo InputForm) with
       ++ nand(a,b) returns the logical negation of \spad{a} and b.
     nor    : (%, %) -> %
       ++ nor(a,b) returns the logical negation of \spad{a} or b.
-    implies: (%, %) -> %
-      ++ implies(a,b) returns the logical implication
-      ++ of Boolean \spad{a} and b.
     test: % -> Boolean
       ++ test(b) returns b and is provided for compatibility with the new compiler.
   == add
@@ -178,6 +193,7 @@ Boolean(): Join(OrderedSet, Finite, Logic, ConvertibleTo InputForm) with
     nand(a, b)    == (test a => nt b; true)
     a = b         == BooleanEquality(a, b)$Lisp
     implies(a, b) == (test a => b; true)
+    equiv(a,b)    == BooleanEquality(a, b)$Lisp
     a < b         == (test b => not(test a);false)
 
     size()        == 2
@@ -212,250 +228,157 @@ code and copy the {\bf BOOLEAN.o} file to the {\bf OUT} directory.
 This is eventually forcibly replaced by a recompiled version. 
 <<BOOLEAN.lsp BOOTSTRAP>>=
 
-(|/VERSIONCHECK| 2) 
+(/VERSIONCHECK 2) 
+
+(PUT '|BOOLEAN;test;$B;1| '|SPADreplace| '(XLAM (|a|) |a|)) 
+
+(DEFUN |BOOLEAN;test;$B;1| (|a| $) |a|) 
+
+(DEFUN |BOOLEAN;nt| (|b| $) (COND (|b| 'NIL) ('T 'T))) 
+
+(PUT '|BOOLEAN;true;$;3| '|SPADreplace| '(XLAM NIL 'T)) 
+
+(DEFUN |BOOLEAN;true;$;3| ($) 'T) 
+
+(PUT '|BOOLEAN;false;$;4| '|SPADreplace| '(XLAM NIL NIL)) 
+
+(DEFUN |BOOLEAN;false;$;4| ($) NIL) 
+
+(DEFUN |BOOLEAN;not;2$;5| (|b| $) (COND (|b| 'NIL) ('T 'T))) 
+
+(DEFUN |BOOLEAN;^;2$;6| (|b| $) (COND (|b| 'NIL) ('T 'T))) 
+
+(DEFUN |BOOLEAN;~;2$;7| (|b| $) (COND (|b| 'NIL) ('T 'T))) 
+
+(DEFUN |BOOLEAN;and;3$;8| (|a| |b| $) (COND (|a| |b|) ('T 'NIL))) 
+
+(DEFUN |BOOLEAN;/\\;3$;9| (|a| |b| $) (COND (|a| |b|) ('T 'NIL))) 
+
+(DEFUN |BOOLEAN;or;3$;10| (|a| |b| $) (COND (|a| 'T) ('T |b|))) 
+
+(DEFUN |BOOLEAN;\\/;3$;11| (|a| |b| $) (COND (|a| 'T) ('T |b|))) 
+
+(DEFUN |BOOLEAN;xor;3$;12| (|a| |b| $)
+  (COND (|a| (|BOOLEAN;nt| |b| $)) ('T |b|))) 
 
-(PUT 
-  (QUOTE |BOOLEAN;test;2$;1|) 
-  (QUOTE |SPADreplace|) 
-  (QUOTE (XLAM (|a|) |a|))) 
-
-(DEFUN |BOOLEAN;test;2$;1| (|a| |$|) |a|) 
-
-(DEFUN |BOOLEAN;nt| (|b| |$|) 
-  (COND (|b| (QUOTE NIL)) 
-  ((QUOTE T) (QUOTE T)))) 
-
-(PUT 
-  (QUOTE |BOOLEAN;true;$;3|) 
-  (QUOTE |SPADreplace|) 
-  (QUOTE (XLAM NIL (QUOTE T)))) 
-
-(DEFUN |BOOLEAN;true;$;3| (|$|) 
-  (QUOTE T)) 
-
-(PUT 
-  (QUOTE |BOOLEAN;false;$;4|) 
-  (QUOTE |SPADreplace|) 
-  (QUOTE (XLAM NIL NIL))) 
-
-(DEFUN |BOOLEAN;false;$;4| (|$|) NIL) 
-
-(DEFUN |BOOLEAN;not;2$;5| (|b| |$|) 
-  (COND 
-    (|b| (QUOTE NIL)) 
-    ((QUOTE T) (QUOTE T)))) 
-
-(DEFUN |BOOLEAN;^;2$;6| (|b| |$|) 
-  (COND 
-    (|b| (QUOTE NIL)) 
-    ((QUOTE T) (QUOTE T)))) 
-
-(DEFUN |BOOLEAN;~;2$;7| (|b| |$|) 
-  (COND 
-    (|b| (QUOTE NIL)) 
-    ((QUOTE T) (QUOTE T)))) 
-
-(DEFUN |BOOLEAN;and;3$;8| (|a| |b| |$|) 
-  (COND 
-    (|a| |b|) 
-    ((QUOTE T) (QUOTE NIL)))) 
-
-(DEFUN |BOOLEAN;/\\;3$;9| (|a| |b| |$|) 
-  (COND 
-    (|a| |b|) 
-    ((QUOTE T) (QUOTE NIL)))) 
-
-(DEFUN |BOOLEAN;or;3$;10| (|a| |b| |$|) 
-  (COND 
-    (|a| (QUOTE T)) 
-    ((QUOTE T) |b|))) 
-
-(DEFUN |BOOLEAN;\\/;3$;11| (|a| |b| |$|) 
-  (COND 
-    (|a| (QUOTE T)) 
-    ((QUOTE T) |b|))) 
-
-(DEFUN |BOOLEAN;xor;3$;12| (|a| |b| |$|) 
-  (COND 
-    (|a| (|BOOLEAN;nt| |b| |$|)) 
-    ((QUOTE T) |b|))) 
-
-(DEFUN |BOOLEAN;nor;3$;13| (|a| |b| |$|) 
-  (COND 
-    (|a| (QUOTE NIL)) 
-    ((QUOTE T) (|BOOLEAN;nt| |b| |$|)))) 
-
-(DEFUN |BOOLEAN;nand;3$;14| (|a| |b| |$|) 
-  (COND 
-    (|a| (|BOOLEAN;nt| |b| |$|)) 
-    ((QUOTE T) (QUOTE T)))) 
-
-(PUT 
-  (QUOTE |BOOLEAN;=;3$;15|) 
-  (QUOTE |SPADreplace|) 
-  (QUOTE |BooleanEquality|)) 
-
-(DEFUN |BOOLEAN;=;3$;15| (|a| |b| |$|) 
-  (|BooleanEquality| |a| |b|)) 
-
-(DEFUN |BOOLEAN;implies;3$;16| (|a| |b| |$|) 
-  (COND 
-    (|a| |b|) 
-    ((QUOTE T) (QUOTE T)))) 
-
-(DEFUN |BOOLEAN;<;3$;17| (|a| |b| |$|) 
-  (COND 
-    (|b| 
-      (COND 
-        (|a| (QUOTE NIL))
-        ((QUOTE T) (QUOTE T)))) 
-    ((QUOTE T) (QUOTE NIL)))) 
-
-(PUT 
-  (QUOTE |BOOLEAN;size;Nni;18|) 
-  (QUOTE |SPADreplace|) 
-  (QUOTE (XLAM NIL 2))) 
-
-(DEFUN |BOOLEAN;size;Nni;18| (|$|) 2) 
-
-(DEFUN |BOOLEAN;index;Pi$;19| (|i| |$|) 
-  (COND 
-    ((SPADCALL |i| (QREFELT |$| 26)) (QUOTE NIL))
-    ((QUOTE T) (QUOTE T)))) 
-
-(DEFUN |BOOLEAN;lookup;$Pi;20| (|a| |$|) 
-  (COND 
-    (|a| 1) 
-    ((QUOTE T) 2))) 
-
-(DEFUN |BOOLEAN;random;$;21| (|$|) 
-  (COND 
-    ((SPADCALL (|random|) (QREFELT |$| 26)) (QUOTE NIL)) 
-    ((QUOTE T) (QUOTE T)))) 
-
-(DEFUN |BOOLEAN;convert;$If;22| (|x| |$|) 
-  (COND 
-    (|x| (SPADCALL (SPADCALL "true" (QREFELT |$| 33)) (QREFELT |$| 35)))
-    ((QUOTE T) 
-      (SPADCALL (SPADCALL "false" (QREFELT |$| 33)) (QREFELT |$| 35))))) 
-
-(DEFUN |BOOLEAN;coerce;$Of;23| (|x| |$|) 
-  (COND 
-    (|x| (SPADCALL "true" (QREFELT |$| 38)))
-    ((QUOTE T) (SPADCALL "false" (QREFELT |$| 38))))) 
-
-(DEFUN |Boolean| NIL 
-  (PROG NIL 
-    (RETURN 
-      (PROG (#1=#:G82461) 
-        (RETURN 
-          (COND 
-            ((LETT #1# 
-                (HGET |$ConstructorCache| (QUOTE |Boolean|))
-                |Boolean|)
-              (|CDRwithIncrement| (CDAR #1#)))
-             ((QUOTE T) 
-               (|UNWIND-PROTECT| 
-                 (PROG1 
-                   (CDDAR 
-                     (HPUT 
-                       |$ConstructorCache| 
-                       (QUOTE |Boolean|) 
-                       (LIST (CONS NIL (CONS 1 (|Boolean;|))))))
-                   (LETT #1# T |Boolean|))
-                 (COND 
-                   ((NOT #1#) 
-                     (HREM |$ConstructorCache| (QUOTE |Boolean|)))))))))))) 
-
-(DEFUN |Boolean;| NIL 
-  (PROG (|dv$| |$| |pv$|) 
-    (RETURN 
-      (PROGN 
-        (LETT |dv$| (QUOTE (|Boolean|)) . #1=(|Boolean|))
-        (LETT |$| (GETREFV 41) . #1#)
-        (QSETREFV |$| 0 |dv$|)
-        (QSETREFV |$| 3 (LETT |pv$| (|buildPredVector| 0 0 NIL) . #1#))
-        (|haddProp| |$ConstructorCache| (QUOTE |Boolean|) NIL (CONS 1 |$|))
-        (|stuffDomainSlots| |$|) |$|)))) 
-
-(MAKEPROP 
-  (QUOTE |Boolean|) 
-  (QUOTE |infovec|) 
-    (LIST 
-      (QUOTE 
-        #(NIL NIL NIL NIL NIL NIL 
-          (|Boolean|)
-          |BOOLEAN;test;2$;1| 
-          (CONS IDENTITY 
-            (FUNCALL (|dispatchFunction| |BOOLEAN;true;$;3|) |$|))
-          (CONS IDENTITY 
-            (FUNCALL (|dispatchFunction| |BOOLEAN;false;$;4|) |$|))
-          |BOOLEAN;not;2$;5| 
-          |BOOLEAN;^;2$;6| 
-          |BOOLEAN;~;2$;7| 
-          |BOOLEAN;and;3$;8| 
-          |BOOLEAN;/\\;3$;9| 
-          |BOOLEAN;or;3$;10| 
-          |BOOLEAN;\\/;3$;11| 
-          |BOOLEAN;xor;3$;12| 
-          |BOOLEAN;nor;3$;13| 
-          |BOOLEAN;nand;3$;14| 
-          |BOOLEAN;=;3$;15| 
-          |BOOLEAN;implies;3$;16| 
-          |BOOLEAN;<;3$;17| 
-          (|NonNegativeInteger|) 
-          |BOOLEAN;size;Nni;18| 
-          (|Integer|) 
-          (0 . |even?|) 
-          (|PositiveInteger|) 
-          |BOOLEAN;index;Pi$;19| 
-          |BOOLEAN;lookup;$Pi;20| 
-          |BOOLEAN;random;$;21| 
-          (|String|) 
-          (|Symbol|)
-          (5 . |coerce|)
-          (|InputForm|)
-          (10 . |convert|)
-          |BOOLEAN;convert;$If;22| 
-          (|OutputForm|) 
-          (15 . |message|) 
-          |BOOLEAN;coerce;$Of;23| 
-          (|SingleInteger|)))
-      (QUOTE 
-         #(|~=| 20 |~| 26 |xor| 31 |true| 37 |test| 41 |size| 46 |random| 50 
-           |or| 54 |not| 60 |nor| 65 |nand| 71 |min| 77 |max| 83 |lookup| 89 
-           |latex| 94 |index| 99 |implies| 104 |hash| 110 |false| 115 
-           |convert| 119 |coerce| 124 |and| 129 |^| 135 |\\/| 140 |>=| 146 
-           |>| 152 |=| 158 |<=| 164 |<| 170 |/\\| 176))
-      (QUOTE NIL)
-      (CONS 
-        (|makeByteWordVec2| 1 (QUOTE (0 0 0 0 0 0 0)))
-        (CONS 
-          (QUOTE 
-            #(|OrderedSet&| NIL |Logic&| |SetCategory&| NIL |BasicType&| NIL))
-          (CONS 
-            (QUOTE 
-              #((|OrderedSet|) 
-                (|Finite|)
-                (|Logic|)
-                (|SetCategory|)
-                (|ConvertibleTo| 34)
-                (|BasicType|)
-                (|CoercibleTo| 37)))
-            (|makeByteWordVec2| 
-              40 
-              (QUOTE 
-                (1 25 6 0 26 1 32 0 31 33 1 34 0 32 35 1 37 0 31 38 2 0 6 0 0 
-                 1 1 0 0 0 12 2 0 0 0 0 17 0 0 0 8 1 0 6 0 7 0 0 23 24 0 0 0 
-                 30 2 0 0 0 0 15 1 0 0 0 10 2 0 0 0 0 18 2 0 0 0 0 19 2 0 0 0 
-                 0 1 2 0 0 0 0 1 1 0 27 0 29 1 0 31 0 1 1 0 0 27 28 2 0 0 0 0
-                 21 1 0 40 0 1 0 0 0 9 1 0 34 0 36 1 0 37 0 39 2 0 0 0 0 13 1
-                 0 0 0 11 2 0 0 0 0 16 2 0 6 0 0 1 2 0 6 0 0 1 2 0 6 0 0 20 2
-                 0 6 0 0 1 2 0 6 0 0 22 2 0 0 0 0 14))))))
-      (QUOTE |lookupComplete|))) 
-
-(MAKEPROP (QUOTE |Boolean|) (QUOTE NILADIC) T) 
+(DEFUN |BOOLEAN;nor;3$;13| (|a| |b| $)
+  (COND (|a| 'NIL) ('T (|BOOLEAN;nt| |b| $)))) 
 
+(DEFUN |BOOLEAN;nand;3$;14| (|a| |b| $)
+  (COND (|a| (|BOOLEAN;nt| |b| $)) ('T 'T))) 
+
+(PUT '|BOOLEAN;=;2$B;15| '|SPADreplace| '|BooleanEquality|) 
+
+(DEFUN |BOOLEAN;=;2$B;15| (|a| |b| $) (|BooleanEquality| |a| |b|)) 
+
+(DEFUN |BOOLEAN;implies;3$;16| (|a| |b| $) (COND (|a| |b|) ('T 'T))) 
+
+(PUT '|BOOLEAN;equiv;3$;17| '|SPADreplace| '|BooleanEquality|) 
+
+(DEFUN |BOOLEAN;equiv;3$;17| (|a| |b| $) (|BooleanEquality| |a| |b|)) 
+
+(DEFUN |BOOLEAN;<;2$B;18| (|a| |b| $)
+  (COND (|b| (SPADCALL |a| (QREFELT $ 23))) ('T 'NIL))) 
+
+(PUT '|BOOLEAN;size;Nni;19| '|SPADreplace| '(XLAM NIL 2)) 
+
+(DEFUN |BOOLEAN;size;Nni;19| ($) 2) 
+
+(DEFUN |BOOLEAN;index;Pi$;20| (|i| $)
+  (COND ((SPADCALL |i| (QREFELT $ 28)) 'NIL) ('T 'T))) 
+
+(DEFUN |BOOLEAN;lookup;$Pi;21| (|a| $) (COND (|a| 1) ('T 2))) 
+
+(DEFUN |BOOLEAN;random;$;22| ($)
+  (COND ((SPADCALL (|random|) (QREFELT $ 28)) 'NIL) ('T 'T))) 
+
+(DEFUN |BOOLEAN;convert;$If;23| (|x| $)
+  (COND
+    (|x| (SPADCALL (SPADCALL "true" (QREFELT $ 35)) (QREFELT $ 37)))
+    ('T (SPADCALL (SPADCALL "false" (QREFELT $ 35)) (QREFELT $ 37))))) 
+
+(DEFUN |BOOLEAN;coerce;$Of;24| (|x| $)
+  (COND
+    (|x| (SPADCALL "true" (QREFELT $ 40)))
+    ('T (SPADCALL "false" (QREFELT $ 40))))) 
+
+(DEFUN |Boolean| ()
+  (PROG ()
+    (RETURN
+      (PROG (#0=#:G1458)
+        (RETURN
+          (COND
+            ((LETT #0# (HGET |$ConstructorCache| '|Boolean|) |Boolean|)
+             (|CDRwithIncrement| (CDAR #0#)))
+            ('T
+             (UNWIND-PROTECT
+               (PROG1 (CDDAR (HPUT |$ConstructorCache| '|Boolean|
+                                   (LIST
+                                    (CONS NIL (CONS 1 (|Boolean;|))))))
+                 (LETT #0# T |Boolean|))
+               (COND
+                 ((NOT #0#) (HREM |$ConstructorCache| '|Boolean|))))))))))) 
+
+(DEFUN |Boolean;| ()
+  (PROG (|dv$| $ |pv$|)
+    (RETURN
+      (PROGN
+        (LETT |dv$| '(|Boolean|) . #0=(|Boolean|))
+        (LETT $ (GETREFV 43) . #0#)
+        (QSETREFV $ 0 |dv$|)
+        (QSETREFV $ 3 (LETT |pv$| (|buildPredVector| 0 0 NIL) . #0#))
+        (|haddProp| |$ConstructorCache| '|Boolean| NIL (CONS 1 $))
+        (|stuffDomainSlots| $)
+        $)))) 
+
+(MAKEPROP '|Boolean| '|infovec|
+    (LIST '#(NIL NIL NIL NIL NIL NIL (|Boolean|) |BOOLEAN;test;$B;1|
+             (CONS IDENTITY
+                   (FUNCALL (|dispatchFunction| |BOOLEAN;true;$;3|) $))
+             (CONS IDENTITY
+                   (FUNCALL (|dispatchFunction| |BOOLEAN;false;$;4|) $))
+             |BOOLEAN;not;2$;5| |BOOLEAN;^;2$;6| |BOOLEAN;~;2$;7|
+             |BOOLEAN;and;3$;8| |BOOLEAN;/\\;3$;9| |BOOLEAN;or;3$;10|
+             |BOOLEAN;\\/;3$;11| |BOOLEAN;xor;3$;12|
+             |BOOLEAN;nor;3$;13| |BOOLEAN;nand;3$;14|
+             |BOOLEAN;=;2$B;15| |BOOLEAN;implies;3$;16|
+             |BOOLEAN;equiv;3$;17| (0 . |not|) |BOOLEAN;<;2$B;18|
+             (|NonNegativeInteger|) |BOOLEAN;size;Nni;19| (|Integer|)
+             (5 . |even?|) (|PositiveInteger|) |BOOLEAN;index;Pi$;20|
+             |BOOLEAN;lookup;$Pi;21| |BOOLEAN;random;$;22| (|String|)
+             (|Symbol|) (10 . |coerce|) (|InputForm|) (15 . |convert|)
+             |BOOLEAN;convert;$If;23| (|OutputForm|) (20 . |message|)
+             |BOOLEAN;coerce;$Of;24| (|SingleInteger|))
+          '#(~= 25 ~ 31 |xor| 36 |true| 42 |test| 46 |size| 51 |random|
+             55 |or| 59 |not| 65 |nor| 70 |nand| 76 |min| 82 |max| 88
+             |lookup| 94 |latex| 99 |index| 104 |implies| 109 |hash|
+             115 |false| 120 |equiv| 124 |convert| 130 |coerce| 135
+             |and| 140 ^ 146 |\\/| 151 >= 157 > 163 = 169 <= 175 < 181
+             |/\\| 187)
+          'NIL
+          (CONS (|makeByteWordVec2| 1 '(0 0 0 0 0 0 0 0))
+                (CONS '#(|OrderedSet&| NIL |Logic&| |SetCategory&| NIL
+                         NIL |BasicType&| NIL)
+                      (CONS '#((|OrderedSet|) (|Finite|) (|Logic|)
+                               (|SetCategory|) (|ConvertibleTo| 36)
+                               (|PropositionalLogic|) (|BasicType|)
+                               (|CoercibleTo| 39))
+                            (|makeByteWordVec2| 42
+                                '(1 6 0 0 23 1 27 6 0 28 1 34 0 33 35 1
+                                  36 0 34 37 1 39 0 33 40 2 0 6 0 0 1 1
+                                  0 0 0 12 2 0 0 0 0 17 0 0 0 8 1 0 6 0
+                                  7 0 0 25 26 0 0 0 32 2 0 0 0 0 15 1 0
+                                  0 0 10 2 0 0 0 0 18 2 0 0 0 0 19 2 0
+                                  0 0 0 1 2 0 0 0 0 1 1 0 29 0 31 1 0
+                                  33 0 1 1 0 0 29 30 2 0 0 0 0 21 1 0
+                                  42 0 1 0 0 0 9 2 0 0 0 0 22 1 0 36 0
+                                  38 1 0 39 0 41 2 0 0 0 0 13 1 0 0 0
+                                  11 2 0 0 0 0 16 2 0 6 0 0 1 2 0 6 0 0
+                                  1 2 0 6 0 0 20 2 0 6 0 0 1 2 0 6 0 0
+                                  24 2 0 0 0 0 14)))))
+          '|lookupComplete|)) 
+
+(MAKEPROP '|Boolean| 'NILADIC T) 
 @
 \section{domain IBITS IndexedBits}
 <<domain IBITS IndexedBits>>=
@@ -579,6 +502,7 @@ Bits(): Exports == Implementation where
 <<domain BOOLEAN Boolean>>
 <<domain IBITS IndexedBits>>
 <<domain BITS Bits>>
+<<category PROPLOG PropositionalLogic>>
 @
 \eject
 \begin{thebibliography}{99}