# LP, the Larch Prover -- The order command

The *order command* directs LP to attempt to orient formulas into rewrite
rules.
`<order-command> ::= ``order` [ <names> ]

## Examples

`order
order nat
`

## Usage

When the automatic-ordering setting is `on`, LP attempts to orient
formulas into rewrite rules automatically. When it is
`off`, LP orients formulas only in response to an explicit `order`
or complete command. If no <names> are specified in an `order`
command, LP attempts to orient all formulas in the system. If <names> are
specified, LP attempts to orient only the named formulas (including any new
formulas that LP generates during the ordering process, for example, as a
result of applying a deduction rule to a newly reduced
fact).
When a formula is an equation `t1 = t2` or `t1 <=> t2`, LP uses the
current ordering-method, if possible, to orient it into the rewrite
rule `t1 -> t2` or into the rewrite rule `t2 -> t1`. When a formula
`f` is not an equation (i.e., when its principal operator is neither `=`
nor `<=>`), LP orients it into the rewrite rule `f -> true` (or into the
rewrite rule `f1 -> false`, if `f` has the form `~f1`).

If the current ordering method is a registered
or polynomial ordering, the `order` command
also attempts to orient the formulas into a provably terminating set of rewrite
rules. If the current ordering method is a
brute-force ordering, the `order`
command may orient the formulas into a nonterminating set of rewrite rules.

Users can interrupt and resume the operation of the
`order` command.