LP, the Larch Prover -- The unregister command

The unregister command causes LP to discard information used to control the registered and polynomial orderings.


<unregister-command>   ::= unregister <ordering-information>
<ordering-information> ::= registry | ( bottom | top ) <operator>+[,]
Note: The first word in the <ordering-information> can be abbreviated.


unregister bottom succ
unregister registry


The unregister registry command deletes all information used by the registered and polynomial orderings to orient formulas into rewrite rules.

The unregister top and unregister bottom commands remove the listed operators from the top and bottom of the registry used by the registered orderings.