To prove the termination of a functional program there has to be a
well founded order on the product of the function parameters
such that the arguments in each recursive call
are smaller than the corresponding input regarding this order.
We have limited to *structural* orderings.
*foetus* tries to find such
an order by collecting all recursive calls of the given function and
the belonging behaviour of the function arguments. To handle mutually
recursive functions a call graph is constructed and completed.

Section 2 introduces the *foetus* ``body'' (syntax and type
system). Section 3 provides some examples to
intuitively learn the language and see the interpreter and termination
checker work. Then in section 4 we explain the
``heart'' of *foetus*: the call extractor; we also informally introduce
call graph completion and finding of the lexical order: the ``brain'' of
*foetus*. The latter is formally described in section 5.