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

<PRE>
MemberOp: <b>trait</b>
  <b>assumes</b> <A HREF="InsertGenerated.html">InsertGenerated</A>
  <b>introduces</b>
    __ \in __, __ \notin __: E, C -&gt; Bool
  <b>asserts</b> <b>forall</b> e, e1, e2: E, c: C
    e \notin c == ~(e \in c);
    e \notin empty;
    e1 \in insert(e2, c) == e1 = e2 \/ e1 \in c
  <b>implies</b> <b>converts</b> \in, \notin
</PRE>

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