LP, the Larch Prover -- The rewriting-limit setting

The rewriting-limit setting sets an upper bound on the number of reductions that LP will perform when normalizing a term with respect to a rewriting system that is not guaranteed to terminate.

Syntax

<set-rewriting-limit-command> ::= set rewriting-limit <number>

Examples

set rewriting-limit 50

Usage

The rewriting-limit setting is local to the current proof context. Its default value is 1000.

If LP exceeds the rewriting limit when normalizing a formula, rewrite rule, or deduction rule, it immunizes that fact. If it exceeds the rewriting limit when attempting to prove a conjecture by normalization or rewriting, the user can continue normalizing the conjecture by typing resume (after raising the rewriting limit, if desired).