[Agda] termination

[Permjacov Evgeniy]

On 03/03/2011 12:02 PM, Conor McBride wrote:
> 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
>
I do know, how to write similiar program that obviously terminates.
That's a little childish, but it is not fair. And if it is possible
here, it is not neccecary possible in general