LP, the Larch Prover -- Equations

An equation is a formula that consists of a pair of terms separated by an equality operator.


<equation> ::= <term> (= | <=>) <term>
Restriction: The two <term>s in an equation must have the same sort. This sort must be Bool if the equality operator is <=>.


x + 0 = x
x <= y <=> x < y \/ x = y
x | y <=> \E z (y = x*z)


LP treats equations in the same manner as it treats formulas. Indeed, any formula is logically equivalent to an equation: F is logically equivalent to F <=> true.