The Coq mailing list

[Wojciech Jedynak <wjedynak AT gmail.com>]

Hello,

> Is it possible use this result to prove theorem tak_terminates? In some
> simple way? Or more general question? Is it possible to prove termination 
> (similarly to the problem) if I have > corresponding function with all 
> required recursive equations proved?

yes! I actually tried this approach two days ago and succeded, but now
I'm waiting for the proof market to accept solutions again. I'm not so
sure about the simple part, though -- I found a nice measure by
analyzing relation between the depth of the recursion  and the inputs.
I didn't use the _dec functions in the def. of tak0, but instead
relied on e.g. <=?, so that could simplify my proof.

Best,
Wojciech