Partial correctness with defined_f predicates

[vkuncak]

If a function is annotated with @partial we can introduce a predicate that guards the case when it is equal to its recursive case. The function is always equal to the part of the body that contains calls to functions not proven terminating. For functions to be defined, the functions it calls should also be defined.

This seems more efficient encoding into formulas than the Option monad, but it should be sematically equivalent.
One could, however, first implement an option monad.