- 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*0 (*y*-*x*= 0*y*-*x*<*y*) . But this could be shown for the`sub`function by induction and result in a dependency*foetus*could use [BG96].

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 **;-)**.