LP, the Larch Prover -- Equations
An equation is a formula that consists of a pair of terms separated by an
Restriction: The two <term>s in an equation must have the same sort. This
sort must be Bool if the equality operator is <=>.
<equation> ::= <term> (= | <=>) <term>
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.