## The Induction Scheme Selected for the App Example

(AND
(IMPLIES (AND (NOT (ENDP A)) ; Induction Step: test
(:P (CDR A) B C)) ; and induction hypothesis
(:P A B C)) ; implies induction conclusion.
(IMPLIES (ENDP A) (:P A B C))) ; Base Case

The formula beginning with this parenthesis is the induction scheme suggested
by `(APP A B)`

applied to `(P A B C)`

.

It is a **conjunction** (`AND`

) of two formulas.

The first is the **induction step** and the second is the **base case**.