[<A HREF="Boolean.ps">PostScript</A>]

<PRE>
Boolean: <b>trait</b>
  % This trait is given for documentation only.
  % It is implicit in LSL.
  <b>introduces</b>
    true, false: -&gt; Bool
    ~__: Bool -&gt; Bool
    __/\ __, __\/__, __=&gt;__: Bool, Bool -&gt; Bool
  <b>asserts</b>
    Bool <b>generated</b> <b>by</b> true, false
    <b>forall</b> b: Bool
      ~ true == false;
      ~ false == true;
      true /\ b == b;
      false /\ b == false;
      true \/ b == true;
      false \/ b == b;
      true =&gt; b == b;
      false =&gt; b == true
  <b>implies</b>
    <A HREF="AC.html">AC</A> (/\ , Bool),
    <A HREF="AC.html">AC</A> (\/, Bool),
    <A HREF="Distributive.html">Distributive</A> (\/ <b>for</b> +, /\ <b>for</b> *, Bool <b>for</b> T),
    <A HREF="Distributive.html">Distributive</A> (/\ <b>for</b> +, \/ <b>for</b> *, Bool <b>for</b> T),
    <A HREF="Involutive.html">Involutive</A> (~__, Bool),
    <A HREF="Transitive.html">Transitive</A> (=&gt; <b>for</b> \rel, Bool <b>for</b> T)
    <b>forall</b> b1, b2, b3: Bool
      ~(b1 /\ b2) == ~b1 \/ ~b2;
      ~(b1 \/ b2) == ~b1 /\ ~b2;
      b1 \/ (b1 /\ b2) == b1;
      b1 /\ (b1 \/ b2) == b1;
      b2 \/ ~b2;
      (b1 = b2) \/ (b1 = b3) \/ (b2 = b3);
      b1 =&gt; b2 == ~b1 \/ b2
</PRE>

[<A HREF="toc.html">Table of Contents</A>] [<A HREF="index.html">Index</A>]