[Agda] termination proofs

[Serge D. Mechveliani]

On Mon, Sep 24, 2012 at 08:33:58PM +0100, Peter Hancock wrote:
> On 24/09/2012 19:01, Serge D. Mechveliani wrote:
>
>> Does there exist an algorithmic map in  Nat -> Nat  for which there
>> is not any Agda program with a termination proof accepted by Agda ?
> [..]
>
> On countability grounds too, there are uncountably many functions in 
> Nat -> Nat,
> but since Agda is a formal system (isn't it?) there are only countably many
> expressions in it of (formal) type Nat -> Nat. (They are not just countable
> but even computably enumerable.)
> [..]


The countability grounds is not relevant here, because I asked about an 
_algorithmic_ map in  Nat -> Nat.
An algorithm here can be put as 
   any terminating Agda function (program)   f : Nat -> Nat  
   which is applied without the termination check.  
  
But in all the rest -- I see, thanks to peopleя. The imression is that 
the set of provably-terminating Agda programs is large enough.

Regards,

------
Sergei