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.
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.
Proof-tree display is turned off during calls of
certify-book.
6. The usual failure message is printed as part of the prooftree
display when a proof has failed.