[Agda] termination

[Conor McBride]

Hi

On 2 Mar 2011, at 23:03, Permjacov Evgeniy wrote:

> Consider the code (this is attempt to formalize base-2 arithmetics)
>
>
> How to prove, that it WILL terminate?

You, like so many others before you, are asking the question that
leads to pain.

The question that leads to less pain is

   How can I write a different but adequate program, which obviously
     terminates?

May I respectfully suggest that you consider implementing instead
addition-with-carry?

All the best

Conor