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 ConclusionWhen we prove this we can assume
Ais not empty, and that * the associativity conjecture holds for a ``smaller'' version of
Under those hypotheses we have to prove the associativity conjecture