Conjectures can often be simplified by dividing a proof into cases. When a conjecture reduces to

The command `prove F by cases F1, ..., Fn` directs LP to prove a formula
`F` by division into `n` cases defined by the formulas `F1`, ...,
`Fn` (or into two cases, `F1` and `~F1` if `n = 1`). The command
`resume by cases F1, ..., Fn` directs LP to resume the proof of the current
conjecture by division into cases.

A proof by cases involves `n+1` subgoals. If `n > 1`, the first subgoal
involves proving `F1 \/ ... \/ Fn` to show that the cases exhaust all
possibilities. If `n = 1`, LP generates a default second case of `~F1`,
but does not generate a disjunction as the first subgoal. Then, for each case
`i`, LP generates a subgoal `F'` and an additional hypothesis `Fi'` by
substituting new constants for the free variables of `Fi`
in both `F` and `Fi`. If an inconsistency results
from adding a case hypothesis, that case is impossible and the subgoal is
vacuously true. Otherwise the subgoal must be shown to follow from the axioms
supplemented by the case hypothesis. The names of the case hypotheses have the
form <simpleId>`CaseHyp.`<number>, where <simpleId> is the current
value of the name-prefix setting.

In each case of a proof by cases, LP first adds the case hypothesis without
using it to reduce the other rewrite rules in the system. Only if this action
fails to reduce the desired conclusion to `true` does LP use the case
hypothesis to reduce the other rewrite rules.