Reading post-induction key checkpoints
Each post-induction key checkpoint is a theorem if and only if the original conjecture was a theorem. The reason is that each subgoal produced by induction concludes with the original formula and simplification preserves equivalence.
So if you see a post-induction key checkpoint that is not a theorem, stop looking at the checkpoints! Your original conjecture is not a theorem! Fix it.
If you're convinced all the post-induction conjectures are theorems, ask whether each has the hypotheses you'd need to prove it. If the case analysis feels inappropriate or induction hypotheses seem to be missing, then ACL2 might have done the wrong induction. Find the induction scheme it did by reading the first induction message printed after the conjecture was submitted. If it is wrong, then extend ACL2's induction analysis or tell ACL2 what induction to do, as explained shortly.
But before you decide the induction hypothesis is missing, look closely for
contradictions among the hypotheses of the checkpoint formula. For example,
perhaps one of the hypotheses is
Is it possible that
Or maybe you can get
(implies (member d x) (member d x'))
If you could prove that, the key checkpoint would be proved. Of course, you may need other hypotheses from the checkpoint to state your theorems.
If you have been working your way through the tutorial introduction to the theorem prover, use your browser's Back Button now to introduction-to-key-checkpoints.