# 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`.