On Sun, Feb 24, 2013 at 7:09 PM, Roman Cheplyaka <roma@ro-che.info> wrote:

Thus, your
recursion is well-founded — you enter the recursion with the input
strictly smaller than you had in the beginning.

Perhaps you meant /productive/ corecursion? Because the definition "A ::= B A" you gave is codata.

-- Kim-Ee