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.
