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

<PRE>
ReverseOp: <b>trait</b>
  % An operator on lists commonly used
  % to demonstrate theorem provers.
  <b>assumes</b> <A HREF="List.html">List</A>
  <b>introduces</b> reverse: C -&gt; C
  <b>asserts</b> <b>forall</b> e: E, l, l1, l2: C
    reverse(empty) == empty;
    reverse(e \precat l) == reverse(l) \postcat e
  <b>implies</b> <b>forall</b> e: E, l, l1, l2: C
      reverse(reverse(l)) == l;
      l \neq empty =&gt; head(reverse(l)) = last(l);
      l \neq empty 
        =&gt; tail(reverse(l)) = reverse(init(l));
      len(reverse(l)) == len(l);
      reverse(l1 || l2) == reverse(l2) || reverse(l1)
    <b>converts</b> reverse
</PRE>

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