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

<PRE>
RelationBasics (E, R): <b>trait</b>
  % e1 \langle r \rangle e2 means e1 is related to e2 by r.
  <b>introduces</b> 
    __ \langle __ \rangle __: E, R, E -&gt; Bool
    \bot, \top, I: -&gt; R
    [__, __]: E, E -&gt; R
    -__, __\inv: R -&gt; R
    __ \U __: R, R -&gt; R
  <b>asserts</b>
    R <b>partitioned</b> <b>by</b> __ \langle __ \rangle __
    <b>forall</b> e, e1, e2, e3, e4: E, r, r1, r2: R
      ~(e1 \langle \bot \rangle e2);
      e1 \langle \top \rangle e2;
      e1 \langle I \rangle e2 == e1 = e2;
      e1 \langle [e2, e3] \rangle e4 == e1 = e2 /\ e3 = e4;
      e1 \langle -r \rangle e2 == ~(e1 \langle r \rangle e2);
      e1 \langle r\inv \rangle e2 == e2 \langle r \rangle e1;
      e1 \langle r1 \U r2 \rangle e2 == e1 \langle r1 \rangle e2 \/ e1 \langle r2 \rangle e2
  <b>implies</b>
    <A HREF="AbelianMonoid.html">AbelianMonoid</A> (\bot <b>for</b> unit, \U <b>for</b> \circ, R <b>for</b> T),
    <A HREF="Involutive.html">Involutive</A> (__\inv, R),
    <A HREF="Involutive.html">Involutive</A> (-__, R)
    <b>equations</b>
      -\bot == \top;
      -\top == \bot;
      \bot\inv == \bot;
      \top\inv == \top
    <b>converts</b> \U, -__, __\inv
</PRE>

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