# LP, the Larch Prover -- Operator theories

An operator theory is logically equivalent to a set of equations involving a single operator. At present, LP supports two operator theories:
• the commutative theory, which is axiomatized by the commutative law x + y = y + x
• the associative-commutative (ac) theory, which is axiomatized by the commutative law together with the associative law x + (y + z) = (x + y) + z.
LP uses operator theories to circumvent problems with nonterminating rewriting systems. Because the commutative law cannot be oriented into a terminating rewrite rule, LP uses equational term-rewriting to match and unify terms modulo the ac and commutative operator theories.

## Syntax

```<operator-theory> ::= (ac | commutative) <operator>
```

```ac +
commutative gcd
```

## Usage

Users can assert or prove operator theories.

LP hardwires the logical connectives /\, \/, and <=> as associative-commutative operators. It hardwires the equality operator =:S,S->Bool as a commutative operator when the sort S is not Bool.

The fact ac op normalizes the fact commutative op to true.

To display the operator theories in LP's logical system, type display operator-theories (or disp o-t for short).