### LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-Q3-ANSWER

the inductive step of the `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.