		Search-engine friendly clone of the ACL2 documentation.

Introduction-to-the-theorem-prover

Logic-knowledge-taken-for-granted-q3-answer

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

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.