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.


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


set rewriting-limit 50


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).