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

<PRE>
ListStructureOps (A, E, C): <b>trait</b>
  % Operators frequently used in
  % theorem proving demonstrations.
  <b>assumes</b> <A HREF="ListStructure.html">ListStructure</A>
  <b>introduces</b>
    flatten, reverseAll: C -&gt; C
    countAtoms: C -&gt; Int
  <b>asserts</b> <b>forall</b> a: A, l, l1, l2: C
    flatten(empty) == empty;
    flatten(atom(a) \precat l) == atom(a) \precat flatten(l);
    flatten(list(l1) \precat l2) ==
      flatten(l1) || flatten(l2);
    reverseAll(empty) == empty;
    reverseAll(atom(a) \precat l) ==
      reverseAll(l) \postcat atom(a);
    reverseAll(list(l1) \precat l2) ==
      reverseAll(l2) \postcat list(reverseAll(l1));
    countAtoms(l) == len(flatten(l))
  <b>implies</b>
    <b>forall</b> l, l1, l2: C
      flatten(l1 || l2) == flatten(l1) || flatten(l2);
      flatten(flatten(l)) == flatten(l);
      reverseAll(l1 || l2) ==
        reverseAll(l2) || reverseAll(l1);
      reverseAll(flatten(l)) ==
        flatten(reverseAll(l));
      reverseAll(reverseAll(l)) == l;
      countAtoms(l1 || l2) ==
        countAtoms(l1) + countAtoms(l2);
      countAtoms(flatten(l)) == countAtoms(l);
      countAtoms(reverseAll(l)) == countAtoms(l)
    <b>converts</b> flatten, reverseAll, countAtoms
</PRE>

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