Streams are infinite sequences over a given data type. A stream

specification is a set of equations intended to define a stream.

In this paper we focus on equality of streams, more precisely,

for a given set of equations two stream terms are said to be

equal if they are equal in every model satisfying the given

equations. We investigate techniques for proving equality of

streams suitable for automation. Apart from techniques that

were already available in the tool CIRC from Lucanu and Rosu,

we also exploit well-definedness of streams, typically proved

by proving productivity. Moreover, our approach does

not restrict to behavioral input format and does not require

termination.

We present a tool Streambox that can prove equality of a

wide range of examples fully automatically.