PROOF-TREE-DETAILS

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