the inductive step of the rev-rev proof -- Answer to Question 2

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
(implies (p (f x))
         (equal (g (h 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.