Suggested_Inductions_in_the_Associativity_of_App_Example.html -- ACL2 Version 3.1

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.