LP, the Larch Prover -- Proofs of operator theories

LP permits users to prove operator theories as well as assert them. Proving that an operator + is commutative involves proving a single subgoal consisting of the formula x + y = y + x. Proving that an operator is associative-commutative involves proving an additional subgoal consisting of the formula x + (y + z) = (x + y) + z.