That's a good question that i had previously noted for followup, but I never followed up.

slide 50: how does agda check termination.

http://www.seas.upenn.edu/~sweirich/ssgip/main.pdf

http://research.microsoft.com/en-us/news/features/terminator...