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
|
<html>
<head><title>The_Induction_Step_in_the_App_Example.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>The Induction Step in the App Example</h2>
<p>
This formula is the <b>Induction Step</B>. It basically consists of
three parts, a test identifying the inductive case, an induction
hypothesis and an induction conclusion.<p>
<pre>
(IMPLIES (AND (NOT (ENDP A)) <b>; Test</B>
(:P (CDR A) B C)) <b>; Induction Hypothesis</B>
(:P A B C)) <b>; Induction Conclusion</B>
</pre>
When we prove this we can assume<p>
<pre>
* <code>A</code> is not empty, and that<p>
* the associativity conjecture holds for a ``smaller'' version of
<code>A</code>, namely, <code>(CDR A)</code>.
</pre>
<p>
Under those hypotheses we have to prove the associativity conjecture
for <code>A</code> itself.
<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>
|
