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
|
<html>
<head><title>The_Simplification_of_the_Induction_Conclusion__lparen_Step_9_rparen_.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>the Simplification of the Induction Conclusion (Step 9)</h2>
<p>
<pre>
Subgoal *1/2'
(IMPLIES (AND (CONSP A)
(EQUAL (APP (APP (CDR A) B) C)
(APP (CDR A) (APP B C))))
<a href="The_Simplification_of_the_Induction_Conclusion__lparen_Step_10_rparen_.html">(</a>EQUAL (CONS (CAR A)
(APP (APP (CDR A) B)
C))
<b>(CONS (CAR A)</B>
<b>(APP (CDR A) (APP B C))</B>))).
</pre>
<p>
<img src=green-line.gif><p>
Click on the link above to apply the Axiom that
<code>(EQUAL (CONS x y) (CONS u v))</code> is equal to the conjunction of
<code>(EQUAL x u)</code> and <code>(EQUAL y v)</code>. In this case, <code>(EQUAL x u)</code>
is trivial, <code>(EQUAL (CAR A) (CAR A))</code>.
<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>
|
