## 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`

.