@*Theory of sequences.
The theory of sequences is built on the theory of stacks. 
The stack theory provides most of the machinery needed for the elementary
operations on lists:  |insert|, |head|, |tail|, and |is_empty|.
The sequence trait includes
additional machinery that allows easy specification of concatenation.
@c
sequence: trait
    imports Stack_theory with [nil for empty_stack,
		cons for push, first for top, rest for pop]
    introduces
         enter: C,E -> C        % adds e to back of c 
         last:  C -> E
         prefix:  C -> C        % c with last deleted 
         #.[#]:C, Card -> E      % indexed selection (starts at 1) 
         append: C,C -> C       % concatenation 

    constrains [C] so that C is generated by [new, insert]
                           C is generated by [new, enter]
                           C is partitioned by [first, rest, isEmpty]
                           C is partitioned by [last, prefix, isEmpty]

      for all [e:E] 
         last(enter(new,e)) = e
         prefix(enter(new,e)) = new

      for all [c:C, e:E] 
         not isEmpty(enter(c,e))
         last(enter(c,e)) = e
         prefix(enter(c,e)) = stk

     for  all [c:C, e, e1: E] 
          insert(new,e) = enter(new,e)
          insert(enter(c,e),e1) = enter(insert(c,e1),e)

       for all [c:C, i:Card] 
          c.[1] = first(c)
          c.[i+1] = rest(c).[i]

      for all [c,c1:C, e:E] 
         append(c,new) = c
         append(c,insert(c1,e)) = insert(append(c,c1), e)

 implies
       converts [insert, first, last, rest, prefix],
                [enter, first, last, rest, prefix],
                [append],
                [isEmpty],
                [size],
                [#.[#]]


      exempts last(new), prefix(new), first(new), rest(new) 
%              for all [c:C], c(0)  

@*Index.