[Agda] termination by contradiction

[Sergei Meshveliani]

People,

is it possible in Agda to prove termination of a function by programming
a 
      negation of non-termination             -- call it  method  (M)

(deriving an absurd from assuming an infinite work of the algorithm)
?

A.A.Markov wrote that this provides a wider class of constructive
objects, and that this is intuitive enough.

My current termination proofs in Agda use only a simple approach by
providing an upper bound for a certain counter. And I have an impression
that (M) gives something wider.

Consider the following attempt.
For a recursive function        f : Nat -> Nat,  
define  
       g : Nat -> Nat -> State,  

such that   g x n  is the `state' of the computation of  f x  
at the step  n.
Then the type
              (n : Nat) ->  \neg (isFinalState (g x n))          (NT)

expresses a non-termination at x, and      

          ((n : Nat) ->  \neg (isFinalState (g x n)))  ->  \bottom

will express termination by (M).
Right?

How to express this in Agda ?  Needs it to be expressed?

Thanks,

------
Sergei