
24 Feb
2013
24 Feb
'13
7:56 a.m.
On Sun, Feb 24, 2013 at 7:47 PM, Roman Cheplyaka
Or perhaps you meant that the production itself, when interpreted as a definition, is corecursive?
I was merely thrown off by your mention of "well-founded" and the assertion that you're left with a "strictly smaller" input. I don't see any of this. That's when I remembered that well-founded recursion (a desirable) is sometimes confused with productive corecursion (another desirable). -- Kim-Ee