Proof-tree-details
Proof tree details not covered elsewhere
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.
