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))