Hints on proofs by recursion induction
J. Michael Brady · The Computer Journal · 1977
In 1963 John McCarthy proposed a formalism based on conditional expression and recursion for use in the emergent theory of computation. Included in his proposals was a proof technique, known as recursive induction, which could be used to establish the equivalence of recursively defined functions. This paper shows that the discovery of an equations to serve in a proof by recursive induction does not have to rely on luck or inspiration, but can be developed rationally hand in hand with the development of the proof.