LP, the Larch Prover -- Hints on orienting formulas into rewrite rules

If you put some well-selected ordering constraints in the registry, LP will orient formulas more quickly and with fewer surprises. Put the generators for a sort, such as 0 and s for Nat, at the bottom of the registry. Enter defining formulas, such as P(x) = P1(x) /\ P2(x), with the term being defined on the left side of the equality sign.

When a proof fails unexpectedly, look at the rewrite rules to see if any are oriented in surprising directions. If so, there are several potentially useful things to try.

Set automatic-registry off, instruct LP to order only the offending formula, and choose one of the presented suggestions that order the formula as desired. Then add register commands corresponding to that suggestion to your command file and try running the proof again.
Alternatively, rerun the proof at a trace-level (e.g., 2) that prints out extensions to the registry; then use a text editor and the .lplog file to locate extensions dealing with operators appearing in the offending rewrite rule. This may suggest a set of register commands that will force the formulas to be ordered as desired.
Alternatively, rerun the proof with automatic-registry off to find a set of suggestions that will order things the way you want them. Then add register commands with the appropriate suggestions to your command file, and execute it again with automatic-registry on. This last step is important because proof scripts with automatic-registry off are not usually robust.

Occasionally, LP will fail to orient a set of formulas for which a terminating set of rewrite rules does indeed exist. At this point you should consider changing the ordering to use a more powerful ordering strategy (e.g., the dsmpos ordering rather than noeq-dsmpos) or an ordering strategy that makes no attempt to check termination (e.g., left-to-right). It is also worth keeping in mind that although LP will not automatically give operators equal height when using noeq-dsmpos, the register command can be used to do so explicitly.