The Base Case in the App Example
This formula is the Base Case. It consists of two parts, a test identifying the non-inductive case and the conjecture to prove.
(IMPLIES (ENDP A) ; Test (:P A B C)) ; Conjecture
When we prove this we can assume
and we have to prove the conjecture for