Termination analysis
--------------------

This analysis assigns `True` to an operation `f` if all its evaluations
on ground argument terms are finite.

The current method used in this analysis is quite simple.
It checks whether the arguments in all recursive
calls of an operation are smaller than the arguments passed to
the operation. Indirect calls are not considered.
Therefore, the operation

    length []     = 0
    length (x:xs) = 1 + length xs

is classified as terminating, whereas the semantically equivalent operation

    length []     = 0
    length (x:xs) = incLength xs
    
    incLength xs = 1 + length xs

is classified as possibly non-terminating.

Operations containing free variables in their definitions are
also classified as possibly non-terminating since a free variable
might reduce to arbitrarily large constructor terms (in case of
recursive data types).