# LP, the Larch Prover -- The complete command

The *complete command* provides a method of forward inference that extends
the critical-pairs command.
`<complete-command> ::= ``complete`

## Examples

`complete
`

## Usage

The `complete` command enlarges LP's logical system by adding consequences
of facts already in the system. It operates by computing critical pair
equations between rewrite rules in the system, orienting them into new rewrite
rules, and iterating this procedure until there are no further nontrivial
critical pair equations.
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.