## The Induction Step in the App Example

This formula is the **Induction Step**. It basically consists of
three parts, a test identifying the inductive case, an induction
hypothesis and an induction conclusion.

(IMPLIES (AND (NOT (ENDP A)) **; Test**
(:P (CDR A) B C)) **; Induction Hypothesis**
(:P A B C)) **; Induction Conclusion**

When we prove this we can assume

* `A`

is not empty, and that
* the associativity conjecture holds for a ``smaller'' version of
`A`

, namely, `(CDR A)`

.

Under those hypotheses we have to prove the associativity conjecture
for `A`

itself.