LP, the Larch Prover -- Equations

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

Syntax

<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 <=>.

Examples

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

Usage

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.