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.
