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

<PRE>
SetBasics (E, C): <b>trait</b>
  % Essential finite-set operators
  <b>introduces</b>
    {}: -&gt; C
    insert: E, C -&gt; C
    __\in __: E, C -&gt; Bool
  <b>asserts</b>
    C <b>generated</b> <b>by</b> {}, insert
    C <b>partitioned</b> <b>by</b> \in
    <b>forall</b> s: C, e, e1, e2: E
      ~(e \in {});
      e1 \in insert(e2, s) == e1 = e2 \/ e1 \in s
  <b>implies</b>
    <A HREF="InsertGenerated.html">InsertGenerated</A> ({} <b>for</b> empty)
    <b>forall</b> e, e1, e2: E, s: C
      insert(e, s) \neq {};
      insert(e, insert(e, s)) == insert(e, s);
      insert(e1, insert(e2, s)) ==
        insert(e2, insert(e1, s))
    <b>converts</b> \in
</PRE>

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