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

<PRE>
Sequence (E, C): <b>trait</b>
  % Comparison, subsequences
  <b>assumes</b> <A HREF="StrictPartialOrder.html">StrictPartialOrder</A> (&gt;, E)
  <b>includes</b>
    <A HREF="LexicographicOrder.html">LexicographicOrder</A>,
    <A HREF="String.html">String</A>
  <b>introduces</b>
    isPrefix, isSubstring, isSubsequence: C, C -&gt; Bool
    find: C, C -&gt; Int
  <b>asserts</b> <b>forall</b>  e, e1, e2: E, s, s1, s2: C
    isPrefix(s1, s2) == s1 = prefix(s2, len(s1));
    isSubstring(s1, s2) ==
      isPrefix(s1, s2) \/ isSubstring(s1, tail(s2));
    isSubsequence(empty, s);
    ~isSubsequence(e \precat s, empty);
    isSubsequence(e1 \precat s1, e2 \precat s2) == 
      (e1 = e2 /\ isSubsequence(s1, s2))
        \/ isSubsequence(e1 \precat s1, s2);
    find(empty, empty) == 0;
    find(s1, e -| s2) == 
      <b>if</b> isPrefix(s1, e -| s2) <b>then</b> 0
      <b>else</b> find(s1, s2) + 1
  <b>implies</b>
    <A HREF="IsPO.html">IsPO</A> (isPrefix, C),
    <A HREF="IsPO.html">IsPO</A> (isSubstring, C),
    <A HREF="IsPO.html">IsPO</A> (isSubsequence, C)
    <b>forall</b> s, s1, s2: C, i, n: Int
      isPrefix(prefix(s, n), s);
      isSubstring(substring(s, i, n), s);
      isSubstring(s1, s2) =&gt; isSubsequence(s1, s2)
    <b>converts</b> 
        isPrefix, isSubstring, isSubsequence, find
      exempting <b>forall</b> s: C, e: E  find(e \precat s, empty)
</PRE>

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