# LP, the Larch Prover -- The ordering-method setting

The *ordering-method setting* specifies the method used to orient formulas
into rewrite rules.
`<set-ordering-method-command> ::= ``set ordering-method` <ordering>
<ordering> ::= <registered-ordering>
| `either-way` | `left-to-right`
| `manual` | `polynomial` [ <number> ]
<registered-ordering> ::= `dsmpos` | `noeq-dsmpos`

Note: The <ordering> can be abbreviated.
## Examples

`set ordering dsmpos
set ordering polynomial 2
`

## Usage

The `set ordering-method` command sets the method used to orient formulas
into rewrite rules in the current proof context. The methods based on the
registered and
polynomial orderings attempt to guarantee that
the resulting set of rewrite rules is terminating. The other
brute-force orderings give users more control
over the direction in which equations are oriented into rewrite rules, but they
do not guarantee termination. The registered orderings are the easiest to use.
The default ordering method is `noeq-dsmpos`.
When a set of rewrite rules is known to terminate (because of the ordering used
to orient them), but the new ordering does not establish termination, LP issues
a warning that the termination proof will be lost when the next rewrite rule is
added to the system.