LP, the Larch Prover -- Proofs of conjunctions

Proofs of conjunctions can be slow because the operator /\ is associative and commutative, and matching modulo such operators is inherently slow. The command prove t1 /\ ... /\ tn by /\ provides a way to reduce this expense by directing LP to prove each of the conjuncts as a separate subgoal.

The command resume by /\ directs LP to resume the proof of the current conjecture using this method. It is applicable only when the current conjecture has been reduced to a conjunction.

Users should beware that employing this method too early in a proof can result in lengthening the proof considerably, for example, when the same sequence of commands or the same lemma is needed to prove more than one conjunct.