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

  * A is empty
and we have to prove the conjecture for A.