A stream specification is a set of equations intended to define a stream, that is, an infinite sequence over a given data type. In  a transformation from such a stream specification to a TRS is defined in such a way that termination of the resulting TRS implies that the stream specification admits a unique solution. In this tool description we present how proving such well-definedness of several interesting boolean stream specifications can be done fully automatically using present powerful tools for proving TRS termination.
|Title of host publication
|Algebra and Coalgebra in Computer Science (Third International Conference, CALCO 2009, Udine, Italy, September 7-10, 2009. Proceedings)
|A. Kurz, M. Lenisa, A. Tarlecki
|Place of Publication
|Published - 2009
|Lecture Notes in Computer Science