Maude-help mailing list

[Daniel Mahler <dmahler AT gmail.com>]

I am trying to prove the property of a given bit stream transformer that
if the input stream only contains only finitely man 1's
so does the output stream

Is this something that can be done using Circ?

If yes, how? I do not see how to express the property of having finitely many ones in the first place.
If not can anybody suggest tools that may help?

Is maude-help the right place for Circ questions or is there a better place to ask?

thanks
Daniel