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
|
<html>
<head><title>ACL2-PC_colon__colon_DEMOTE.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h3>ACL2-PC::DEMOTE</h3>(primitive)
<code> </code>move top-level hypotheses to the conclusion
<pre>Major Section: <a href="PROOF-CHECKER-COMMANDS.html">PROOF-CHECKER-COMMANDS</a>
</pre><p>
<pre>
Examples:
demote -- demote all top-level hypotheses
(demote 3 5) -- demote hypotheses 3 and 5
</pre>
For example, if the top-level hypotheses are <code>x</code> and <code>y</code> and the
conclusion is <code>z</code>, then after execution of <code>demote</code>, the conclusion will
be <code>(implies (and x y) z)</code> and there will be no (top-level)
hypotheses.
<p>
<pre>
General Form:
(demote &rest hyps-indices)
</pre>
Eliminate the indicated (top-level) hypotheses, but replace the
conclusion <code>conc</code> with <code>(implies hyps conc)</code> where <code>hyps</code> is the
conjunction of the hypotheses that were eliminated. If no arguments
are supplied, then all hypotheses are demoted, i.e. <code>demote</code> is the
same as <code>(demote 1 2 ... n)</code> where <code>n</code> is the number of top-level
hypotheses.<p>
<strong>Note</strong>: You must be at the top of the conclusion in order to use
this command. Otherwise, first invoke <code>top</code>. Also, <code>demote</code> fails if
there are no top-level hypotheses or if indices are supplied that
are out of range.
<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>
|
