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
|
<html>
<head><title>The_Theorem_that_App_is_Associative.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>The Theorem that App is Associative</h2>
<p>
<pre>
ACL2!><b>(defthm associativity-of-app</B>
<b>(equal (app (app a b) c)</B>
<b>(app a (app b c))))</B>
</pre>
<p>
The formula above says <code>app</code> is associative. The <code><a href="DEFTHM.html">defthm</a></code> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a>
command instructs ACL2 to prove the formula and to name it
<code>associativity-of-app</code>. Actually, the <code>defthm</code> command also
builds the formula into the data base as a <code><a href="REWRITE.html">rewrite</a></code> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a> rule,
but we won't go into that just yet.<p>
What we will consider is how the ACL2 theorem prover proves this formula.<p>
If you proceed you will find the actual output of ACL2 in response to
the command above. Some of the text is highlighted for the purposes of
the tour. ACL2 does not highlight its output. <p>
You will note that we sometimes highlight a single open parenthesis. This
is our way of drawing your attention to the subformula that begins with
that parenthesis. By clicking on the parenthesis you will get an
explanation of the subformula or its processing.<p>
<a href="The_Proof_of_the_Associativity_of_App.html"><img src=walking.gif></a>
<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>
|