[Agda] How to prove termination for the iterated halving function over the rationals?

[Marko Grdinic]

https://stackoverflow.com/questions/59263530/how-to-prove-that-the-halving-function-over-positive-rationals-always-has-an-exi
<https://stackoverflow.com/questions/59263530/how-to-prove-that-the-halving-function-over-positive-rationals-always-has-an-exi?noredirect=1#comment104751793_59263530>

Sorry for being pushy, but lately I've gotten an interest in rational math
and I really want some input from the experts here regarding how to prove
termination of the above. Implementing the function was easy, but proving
the termination seems impossible so at the very least I need to understand
whether that impression is right or not. Silence as the reply just has too
many possible interpretations to deal with.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20191211/d87b847e/attachment.html>