1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
<html>
<head><title>The_WARNING_about_the_Trivial_Consequence.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>The WARNING about the Trivial Consequence</h2>
<p>
This <b>Warning</B> alerts us to the fact that when treated as a
<b>rewrite</B> rule, the new rule <code>TRIVIAL-CONSEQUENCE</code>, rewrites
terms of the same form as a rule we have already proved, namely
<code>ASSOCIATIVITY-OF-APP</code>.<p>
When you see this warning you should <b>think about your rules</B>!<p>
In the current case, it would be a good idea <b>not</B> to make
<code>TRIVIAL-CONSEQUENCE</code> a rule at all. We could do this with
:<code><a href="RULE-CLASSES.html">rule-classes</a></code> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a> nil.<p>
ACL2 proceeds to try to prove the theorem, even though it printed
some warnings. The basic assumption in ACL2 is that the <b>user</B>
<b>understands what he or she is doing</B> but may need a little reminding
just to manage a complicated set of facts.
<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>
|
