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
It is a conjunction (and
The first is the induction step and the second is the base case.