rev-revproof -- 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
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.