Proofs by cases Conjectures can often be simplified by dividing a proof into cases. When a conjecture reduces to true in all cases, it is a theorem.
Case analysis has two primary uses.
If a conjecture is a theorem, a proof by cases may circumvent a lack of completeness in the rewrite rules. If a conjecture is not a theorem, an attempted proof by cases may simplify the conjecture and make it easier to understand why the proof is not succeeding. 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.