Suggested Inductions in the Associativity of App Example
To find a plausible induction argument, the system studies the recursions exhibited by the terms in the conjecture.
Roughly speaking, a call of a recursive function ``suggests'' an induction if the argument position decomposed in recursion is occupied by a variable.
In this conjecture, three terms suggest inductions:
(app a b) (app b c) (app a (app b c))
The variable recursively decomposed is indicated in bold.