(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
(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.