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

<PRE>
Bag (E, C): <b>trait</b>
  % Common bag operators
  <b>includes</b>
    <A HREF="BagBasics.html">BagBasics</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>
    delete: E, C -&gt; C
    {__}: E -&gt; C
    __\in __, __\notin __: E, C -&gt; Bool
    size: C -&gt; Int
    __\U __, __-__: C, C -&gt; C
  <b>asserts</b>
    <b>forall</b> e, e1, e2: E, b, b1, b2: C
      count(e1, delete(e2, b)) == 
        <b>if</b> e1 = e2 <b>then</b> max(0, count(e1, b) - 1)
        <b>else</b> count(e1, b);
      { e } == insert(e, {});
      e \in b == count(e, b) &gt; 0;
      e \notin b == count(e, b) = 0;
      size({}) == 0;
      size(insert(e, b)) == size(b) + 1;
      count(e, b1 \U b2) ==
        count(e, b1) + count(e, b2);
      count(e, b1 - b2) ==
        max(0, count(e, b1) - count(e, b2));
      b1 \subseteq b2 == b1 - b2 = {};
  <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="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;)
    <b>forall</b> e, e1, e2: E, b, b1, b2: C
      insert(e, b) \neq {};
      count(e, b) &gt;= 0;
      count(e, b) &lt;= size(b);
      b1 \subseteq b2 =&gt; count(e, b1) &lt;= count(e, b2)
    <b>converts</b> count, \in, \notin, {__}, \U, -:C,C-&gt;C,
      delete, size, \subseteq, \supseteq, \subset, \supset
</PRE>

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