[Agda] termination proof problem

[Sergei Meshveliani]

On Tue, 2016-03-29 at 10:21 +0200, Ulf Norell wrote:
> A trick you can use is to skip checking the bound until after a finite
> (but possibly large) number of steps. Basically you write a fast
> search that takes a counter starting at a billion (say) that ignores
> the bound and only when that counter reaches zero do you switch to the
> slow search where you check the bound. For your example:
> 
> 
> https://gist.github.com/UlfNorell/f2d8674b1d6b98172827
> [..]
> 

This looks reasonable. Thank you.

I wonder of whether there is possible a perfect way out.
I have the following question.

1) `search'  has a proved bound  (bound n)  and the counter  cnt  that 
   starts at  1 + (bound n),  moves towards zero, and it is proved in
the program that it never turns zero (say, the pattern 
(search ... zero =)  has  \bottom-elim in RHS, so that `search' stops
earlier).

2) The checker has checked termination by seeing these expressions for
cnt.
   
After this, it is clear that  cnt  is not needed in the program.
It can be rewritten with removing the counter and adding 
{-# TERMINATING #-}, so that the two algorithms are equivalent. 
Right?

Is it possible to introduce some special language construct for
"termination by counter", so that the checker could do this
transformation automatically, in a general and safe way?

Thanks,

------
Sergei