Conclusion  

We have seen that foetus and its ``brain'', the call graph completion and finding a lexical order on the function arguments, contributes to automated termination proofs. Of course, in its current state it is no more than a toy to gather experience on his subject. Some improvements have to be done: foetus should be able to recognize more kinds of dependencies (see section 4.1).

• Let assignments. The use of let-constructs to save values within functions is discouraged because foetus stores no relations concerning them; it performs no symbolic evaluation during analyzation. For example:

  case list of 
          {Cons pair => let 
                  hd = pair.HD, 
                  tl = pair.TL in ...
  

  foetus does not know that hd ` < ' list and that tl ` < ' list. At least such simple assignments (for code shortening) should be handled.
• Tuple handling. foetus should trace the dependencies not only of the whole tuples but also of their components. At the moment you cannot define functions with one tuple as parameter instead of separate parameters and still expect a termination proof (see example 3.9).
• Function results. The reason that foetus cannot prove termination of div (see example 3.3) is that it does not know x $\not=$0 $\rightarrow$ (y - x = 0$\lor$y - x < y) . But this could be shown for the sub function by induction and result in a dependency foetus could use [BG96].

Furthermore the call graph completion algorithm could be adopted to prove termination of parameter permuting functions like zip (see example 3.8).

If foetus has ``grown older'' in the described manner it could be ``born into'' one of the ``adult'' program verfication systems or theorem provers like ALF, Isabelle, LEGO or MuTTI ;-).