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.