### LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-BASE-CASE

a brief explanation of base cases
Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER

According to the sentence, the conjecture being proved is
``reversing the reverse of a `true-listp`

yields the original list.''
The formula corresponding to this conjecture is:

(implies (true-listp z)
(equal (rev (rev z)) z)).

We're also told that this is an inductive proof. Evidently we're doing an
induction on the structure of the list `z`

. Then the
*Base Case* is the formula:
(implies (endp z)
(implies (true-listp z)
(equal (rev (rev z)) z))).

Now use your browser's **Back Button** to return to the example proof
in logic-knowledge-taken-for-granted.