rev-rev proof -- Answer to Question 2
Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER
The correct answer to Question 3 in logic-knowledge-taken-for-granted is that you need to prove
Subgoal to Relieve Hyp 1:
(implies (and (q (f a))
(r a))
(p (f a)))
in order to use
Theorem:
(implies (p (f x))
(equal (g (h x))
x))
to rewrite the target (g (h a)) to a in
Goal Conjecture:
(implies (and (q (f a))
(r a))
(s (g (h a))))
If you don't see why, re-read the discussion of rewriting again. Forgetting about the need to relieve hypotheses is a common mistake in informal proofs. ACL2 won't forget to relieve them. But if you forget about the need to do it, you may be confused when ACL2 doesn't see the ``proof'' you see!
Now use your browser's Back Button to return to the end of quiz in logic-knowledge-taken-for-granted.
