Abstract:
We present a new version of the recursion induction principle, with an effective and mechanizable flavour. Furthermore we obtain a measure of complexity of equivalences (or inequalities) between recursive programs, and also of the difficulty of their proof.