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

<PRE>
ElementTest (pass, E, C, T): <b>trait</b>
  % filter collects elements accepted by pass
  <b>assumes</b> <A HREF="InsertGenerated.html">InsertGenerated</A>
  <b>introduces</b> 
    pass: E, T -&gt; Bool
    filter: C, T -&gt; C
    allPass: C, T -&gt; Bool
    somePass: C, T -&gt; Bool
  <b>asserts</b> <b>forall</b> c: C, e: E, t: T
    filter(empty, t) == empty;
    filter(insert(e, c), t) == 
       <b>if</b> pass(e, t) <b>then</b> insert(e, filter(c, t))
       <b>else</b> filter(c, t);
    allPass(empty, t);
    allPass(insert(e, c), t) ==
      pass(e, t) /\ allPass(c, t);
    somePass(c, t) == filter(c, t) \neq empty
  <b>implies</b> <b>converts</b> filter, somePass, allPass
</PRE>

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