Major Section: PROOF-TREE
See proof-tree for an introduction to proof trees, and for a list of related topics. Here we present some details not covered elsewhere.
1. When proof tree display is enabled (because the command
:stop-proof-tree has not been executed, or has been superseded by a
later :start-proof-tree command), then time summaries will include
the time for proof tree display. This time includes the time spent computing
with proof trees, such as the pruning process described briefly above. Even
when proof trees are not displayed, such as when their display is turned off
in the middle of a proof, this time will be printed if it is not 0.
2. When a goal is given a :bye in a proof (see hints), it is treated
for the purpose of proof tree display just as though it had been proved.
3. Several state global variables affect proof tree display.
(@ proof-tree-indent) is initially the string "| ": it is
the string that is laid down the appropriate number of times to effect
indentation. (@ proof-tree-buffer-width) is initially the value of
(fmt-soft-right-margin state), and is used to prevent printing of the
annotation ``(forced ...)'' in any greater column than this value.
However, (assign proof-tree-buffer-width nil) to avoid any such
suppression. Finally, (@ checkpoint-processors) is a list of processors
from the constant list *preprocess-clause-ledge*, together with
:induct. You may remove elements of (@ checkpoint-processors) to
limit which processes are considered checkpoints, but note that this can
affect what is printed by gag-mode (see set-gag-mode).
4. When :otf-flg is not set to t in a proof, and the prover
then decides to revert to the original goal and prove it by induction, the
proof tree display will reflect this fact as shown here:
c 0 | | Subgoal 2 PUSH (reverting)
5. The usual failure message is printed as part of the prooftree display when a proof has failed.
