PROOF-TREE

proof tree displays 
Major Section:  ACL2 Documentation

A view of ACL2 proofs may be obtained by way of ``proof tree displays.'' The emacs environment is easily customized to provide window-based proof tree displays that assist in traversing and making sense of the proof transcript; see proof-tree-emacs. Proof tree displays may be turned on with the command :start-proof-tree and may be turned off with the command :stop-proof-tree; see start-proof-tree and see stop-proof-tree.

Here is an example of a proof tree display, with comments. Lines marked with ``c'' are considered ``checkpoints,'' i.e., goals whose scrutiny may be of particular value. 
( DEFTHM PLUS-TREE-DEL ...)    ;currently proving PLUS-TREE-DEL
   1 Goal preprocess   ;"Goal" creates 1 subgoal by preprocessing
   2 |  Goal' simp     ;"Goal'" creates 2 subgoals by simplification
c  0 |  |  Subgoal 2 PUSH *1   ;"Subgoal 2" pushes "*1" for INDUCT
++++++++++++++++++++++++++++++ ;first pass thru waterfall completed
c  6 *1 INDUCT                 ;Proof by induction of "*1" has
     |  <5 more subgoals>      ; created 6 top-level subgoals.  At
                               ; this point, one of those 6 has been
                               ; proved, and 5 remain to be proved.
                               ; We are currently working on the
                               ; first of those 5 remaining goals.
See proof-tree-examples for many examples that contain proof tree displays. But first, we summarize the kinds of lines that may appear in a proof tree display. The simplest form of a proof tree display is a header showing the current event, followed by list of lines, each having one of the following forms. 
    n <goal> <process> ...
Says that the indicated goal created n subgoals using the indicated process. Here ``...'' refers to possible additional information. 
c   n <goal> <process> ...
As above, but calls attention to the fact that this goal is a ``checkpoint'' in the sense that it may be of particular interest. Some displays may overwrite ``c'' with ``>'' to indicate the current checkpoint being shown in the proof transcript. 
     |  <goal> ...
     |  |  <k subgoals>
Indicates that the goal just above this line, which is pointed to by the rightmost vertical bar (``|''), has k subgoals, none of which have yet been processed. 
     |  <goal> ...
     |  |  <k more subgoals>
As above, except that some subgoals have already been processed. 
++++++++++++++++++++++++++++++
Separates successive passes through the ``waterfall''. Thus, this ``fencepost'' mark indicates the start of a new proof by induction or of a new forcing round.

See proof-tree-examples for detailed examples. To learn how to turn off proof tree displays or to turn them back on again, see stop-proof-tree and see start-proof-tree, respectively. See checkpoint-forced-goals to learn how to mark goals as checkpoints that force the creation of goals in forcing rounds. Finally, see proof-tree-details for some points not covered elsewhere.