<complete-command> ::= complete
When LP's logical system consists solely of active, nonimmune, quantifier-free equations and rewrite rules, the complete command attempts to transform the logical system into a convergent set of rewrite rules that has the same equational theory. The completion procedure is based on the Peterson and Stickle extension of the Knuth-Bendix completion procedure.
LP terminates the completion procedure if the current conjecture reduces to true.
A convergent rewriting system can be used to prove theorems by normalization using the prove command or to reduce terms to a canonical form using the show normal-form command. The completion-mode setting controls the operation of the completion procedure. You can interrupt and resume the operation of the completion procedure.
See also proofs by consistency.