LP, the Larch Prover -- The unregister command


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

Syntax

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

Examples

unregister bottom succ
unregister registry

Usage

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.