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.