Termination checker.

This commit introduces a termination checker. Needless to say, it is
rather primitive. The goal is rather to set up the interfaces, and to
have something that can immediately prove the most obvious cases. The
current `SimpleTerminationChecker` implementation computes
strongly-connected components, and proves that a function `f` terminates
for all inputs if and only if:

  1. `f` has a body
  2. `f` has no precondition
  3. `f` calls only functions that terminate for all inputs or itself
      and, whenever `f` calls itself, it decreases one of its algebraic
      data type arguments.

The astute reader will note that in particular,
`SimpleTerminationChecker` cannot prove anything about:

  1. functions with a precondition
  2. mutually recursive functions
  3. recursive functions that operate on integers only

I am confident that this simple termination checker will pave the way
for future implementations, though, and that we will end up re-inventing
the wheel so many times that we'll be able to equip many trains.