# LP, the Larch Prover -- The register command

The *register command* provides LP with hints for use in orienting formulas
into terminating sets of rewrite rules.
`<register-command> ::= ``register` <ordering-constraint>
<ordering-constraint> ::= <height-constraint> | <status-constraint>
| <polynomial-constraint>

Note: The first word in the <ordering-constraint> can be
abbreviated.
## Examples

`register height f > g
register status multiset +
register polynomials + x + y + 1, x + 2
`

## Usage

The `register` command adds constraints to a *registry* that LP uses in
conjunction with ordering methods that attempt to orient formulas into a set of
terminating rewrite rules. The height and status constraints are used by LP's
registered orderings, and the polynomial
constraints are used by LP's
polynomial ordering.
When the automatic-registry setting is `on` and the
ordering-method setting is a registered ordering, LP automatically
adds height and status constraints to the registry, as necessary, to orient
equations in order to ensure that the resulting set of rewrite rules is
terminating.

The display ordering command displays the constraints in the
registry. Ordering constraints can be removed from the registry with the
unregister command.