### POST-INDUCTION-KEY-CHECKPOINTS

reading post-induction key checkpoints
Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER

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 `(MEMBER e x)`

and another is
`(NOT (MEMBER e' x'))`

where `e`

, `x`

, `e'`

, and `x'`

are
possibly complicated expressions.

Is it possible that `e`

and `e'`

are equal and `x`

and `x'`

are
equal? If so, then the two hypotheses are contradictory and the checkpoint
would be proved if you could find rules that would simplify those expressions
to their common forms. So look for theorems about those subexpressions.

Or maybe you can get `e`

and `e'`

to reduce to some common `d`

but
but find that `x`

and `x'`

are really different. Then ask
whether

(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.