1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
|
<html>
<head><title>PROOF-TREE-DETAILS.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>PROOF-TREE-DETAILS</h2>proof tree details not covered elsewhere
<pre>Major Section: <a href="PROOF-TREE.html">PROOF-TREE</a>
</pre><p>
See <a href="PROOF-TREE.html">proof-tree</a> for an introduction to proof trees, and for a
list of related topics. Here we present some details not covered
elsewhere.
<p>
1. When proof tree display is enabled (because the command
<code>:</code><code><a href="STOP-PROOF-TREE.html">stop-proof-tree</a></code> has not been executed, or has been superseded by a
later <code>:</code><code><a href="START-PROOF-TREE.html">start-proof-tree</a></code> 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.<p>
2. When a goal is given a <code>:bye</code> in a proof (see <a href="HINTS.html">hints</a>), it is
treated for the purpose of proof tree display just as though it had
been proved.<p>
3. Several <a href="STATE.html">state</a> global variables affect proof tree display.
<code>(@ proof-tree-indent)</code> is initially the string <code>"| "</code>: it is
the string that is laid down the appropriate number of times to
effect indentation. <code>(@ proof-tree-buffer-width)</code> is initially the
value of <code>(fmt-soft-right-margin state)</code>, and is used to prevent
printing of the annotation ``(<a href="FORCE.html">force</a>d ...)'' in any greater column
than this value. However, <code>(assign proof-tree-buffer-width nil)</code>
to avoid any such suppression. Finally,
<code>(@ checkpoint-processors)</code> is a list of processors from the
constant list <code>*preprocess-clause-ledge*</code>, together with
<code>:induct</code>. You may remove elements of <code>(@ checkpoint-processors)</code>
to limit which processes are considered checkpoints.<p>
4. When <code>:</code><code><a href="OTF-FLG.html">otf-flg</a></code> is not set to <code>t</code> 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:
<pre>
c 0 | | Subgoal 2 PUSH (reverting)
</pre>
5. <code><a href="PROOF-TREE.html">Proof-tree</a></code> display is turned off during calls of
<code><a href="CERTIFY-BOOK.html">certify-book</a></code>.<p>
6. The usual <a href="FAILURE.html">failure</a> message is printed as part of the prooftree
display when a proof has failed.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
