# LP, the Larch Prover -- Formulas

A *formula* is boolean-valued term.
`<formula> ::= <term>
`

Restriction: the sort of the <term> must be `Bool`.
## Examples

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

## Usage

Users can assert formulas, prove them, or derive them from
other formulas by forward inference.
Operationally, LP uses formulas by orienting them
(if possible) into a terminating set of rewrite rules.
LP also automatically reduces all nonimmune
formulas to normal form.

LP automatically rewrites formulas of the form `~p` to `p = false` and
formulas of the form `~p = false` to `p`. Furthermore, it uses the
following hardwired deduction rules to derive new
formulas from existing formulas and rewrite rules.

`lp_and_is_true: when p /\ q yield p, q
lp_or_is_false: when ~(p \/ q) yield ~p, ~q
`

LP uses the names of these deduction rules when it reports their application,
but they cannot be entered by the user when naming objects.
To display the formulas that LP has not converted into rewrite rules,
type `display formulas` (or `dis fo` for short).