[Agda] termination proof problem

[Sergei Meshveliani]

Can people explain, please, the following subject concerning termination
proof tools?

Having certain 
                   P : ℕ → Set  and   P? : Decidable P,	

one needs to implement

    search :  (n : ℕ) → ∃ \y →  m < y × P y × IsMinimalSuch y

-- find the first  y  after  m  such that  P y.                       

And it is implemented in Agda the function

       bound :  (n : ℕ) → ∃ \b → n < b × P b


(bound n)  gives the counter for `search', for termination proof.
When  m  goes from  n  on,  the value

  counter =  (bound n) ∸ m

decreases at each step. Ans `search' keeps a current witness for  ¬ P y
for all  n < y ≤ m.

All this constitutes a constructive termination proof for `search'.

The problem is that  (bound n)  is expensive to compute at run-time
(while its program is simple).
And the comparison
                   (bound n) ∸ m  ≟  0

is also expensive to check at run-time for many concrete  n and m.

Respectively this counter matching against  0  or  (suc _)
is expensive at run-time.
All other operations cost few.

It is presented	a short and clear constructive bound proof, 
and P? has a small cost. Hence a linear search-through needs to cost
c*b(n),  where  c  is a small constant and  b(n)  is the minimal x after
n such that P x
(we have no idea of where this b(n) resides, besides the condition   
b(n) ≤ bound n).

How to implement `search' with providing a termination proof and
the needed run-time cost property?

Thanks,

------                                                                          
Sergei