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)The variable recursively decomposed is indicated in bold.
(app b c)
(app a (app b c))