Recursion induction principle revisited, with L. Kott, in Theoretical Computer Science (TCS) Vol. 22 (1983), 135-173.

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.