LP, the Larch Prover -- The unorder command

The unorder command turns rewrite rules back into formulas.


<unorder-command> ::= unorder [ <names> ]


unorder nat


The unorder command causes LP to turn the named rewrite rules back into formulas. If no names are specified, LP unorders all rewrite rules.

Even if the automatic-ordering setting is on, the unordered formulas are not immediately reordered into rewrite rules. This gives users an opportunity to change the ordering-method or the registry. The formulas will be oriented into rewrite rules in response to an explicit order command or in response to some other command that would invoke LP's automatic ordering (for example, the assert command).