[Agda] termination example

[Serge D. Mechveliani]

Please,
why the checker does not prove termination of the function 
`power' in the attached program?
(about 140 lines in the attached  Main.zip). 

The last clause of `power' has the first argument
                                   suc (suc (suc cnt)),

and `power' is recursively called in the RHS with the first 
argument
                           cnt'' = suc (suc cnt).

So, the checker must decide that `power' terminates.
But it does not decide.

It this an error in the checker?

Thank you in advance for explanation,

------
Sergei
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Main.zip
Type: application/zip
Size: 2159 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20130930/5d113531/Main.zip