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

<PRE>
Set (E, C): <b>trait</b>
  % Common set operators
  <b>includes</b>
    <A HREF="SetBasics.html">SetBasics</A>,
    <A HREF="Integer.html">Integer</A>,
    <A HREF="DerivedOrders.html">DerivedOrders</A> (C, \subseteq <b>for</b> &lt;=, \supseteq <b>for</b> &gt;=,
                   \subset <b>for</b> &lt;, \supset <b>for</b> &gt;)
  <b>introduces</b>
    __\notin __: E, C -&gt; Bool
    delete: E, C -&gt; C
    {__}: E -&gt; C
    __ \U __, __ \I __, __-__: C, C -&gt; C
    size: C -&gt; Int
  <b>asserts</b>
    <b>forall</b> e, e1, e2: E, s, s1, s2: C
      e \notin s == ~(e \in s);
      { e } == insert(e, {});
      e1 \in delete(e2, s) == e1 \neq e2 /\ e1 \in s;
      e \in (s1 \U s2) == e \in s1 \/ e \in s2;
      e \in (s1 \I s2) == e \in s1 /\ e \in s2;
      e \in (s1 - s2)  == e \in s1 /\ e \notin s2;
      size({}) == 0;
      size(insert(e, s)) ==
        <b>if</b> e \notin s <b>then</b> size(s) + 1 <b>else</b> size(s);
      s1 \subseteq s2 == s1 - s2 = {}
  <b>implies</b>
    <A HREF="AbelianMonoid.html">AbelianMonoid</A> (\U <b>for</b> \circ, {} <b>for</b> unit, C <b>for</b> T), 
    <A HREF="AC.html">AC</A> (\I, C),
    <A HREF="JoinOp.html">JoinOp</A> (\U, {} <b>for</b> empty),
    <A HREF="MemberOp.html">MemberOp</A> ({} <b>for</b> empty),
    <A HREF="PartialOrder.html">PartialOrder</A> (C, \subseteq <b>for</b> &lt;=, \supseteq <b>for</b> &gt;=,
                  \subset <b>for</b> &lt;, \supset <b>for</b> &gt;)
    C <b>generated</b> <b>by</b> {}, {__}, \U
    <b>forall</b> e: E, s, s1, s2: C
      s1 \subseteq s2 =&gt; (e \in s1 =&gt; e \in s2);
      size(s) &gt;= 0
    <b>converts</b>
      \in, \notin, {__}, delete, size, \U, \I, -:C,C-&gt;C,
      \subseteq, \supseteq, \subset, \supset
</PRE>

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