[Agda] termination proofs

[Serge D. Mechveliani]

I thank people for userful responses on my question on termination 
proofs.

Nils Anders Danielsson  writes

On Mon, Sep 24, 2012 at 04:20:58PM +0200, Nils Anders Danielsson wrote:
> On 2012-09-24 13:36, Serge D. Mechveliani wrote:
>> Where it is specified in the Language which functions are considered
>> as provably terminating?
>
> A conservative approximation of the criterion used in Agda is described
> in Section 2.5 of "Subtyping, Declaratively"
> (http://www.cse.chalmers.se/~nad/publications/danielsson-altenkirch-
subtyping.html).
>
>> Now: how to make a  termination proof  as explicit as possible?
>
> You can represent termination proofs explicitly in many different ways.
> I believe that the paper "Partiality and Recursion in Interactive
> Theorem Provers ??? An Overview" by Bove, Krauss and Sozeau
> (http://mattam.org/research/publications/drafts/Partiality_and_Recursion_in_Interactive_Theorem_Provers_-_An_Overview.pdf)
> lists some of them.


I see.
In my newbie impression, Agda looks very good.

Does there exist an algorithmic map in  Nat -> Nat  for which there
is not any Agda program with a termination proof accepted by Agda ?

Regards,

------
Sergei