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
41
42
43
44
45
46
47
|
<html>
<head><title>The_Proof_of_the_Associativity_of_App.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>The Proof of the Associativity of App</h2>
<p>
Here is the theorem prover's output when it processes the <b>defthm</B>
command for the associativity of <code>app</code>. We have highlighted text
for which we offer some explanation, and broken the presentation into
several pages. Just follow the Walking Tour after exploring the
explanations.<p>
<img src=green-line.gif><p>
<pre>
ACL2!><b>(defthm associativity-of-app</B>
<b>(equal (app (app a b) c)</B>
<b>(app a (app b c))))</B><p>
Name the formula above <a href="Name_the_Formula_Above.html">*1</a>.<p>
<a href="Perhaps.html">Perhaps</a> we can prove *1 by induction. Three induction schemes are
<a href="Suggested_Inductions_in_the_Associativity_of_App_Example.html">suggested</a> by this conjecture. <a href="Subsumption_of_Induction_Candidates_in_App_Example.html">Subsumption</a> reduces that number to two.
However, one of these is <a href="Flawed_Induction_Candidates_in_App_Example.html">flawed</a> and so we are left with one viable
candidate. <p>
We will induct according to a scheme suggested by (APP A B). If we
let (:P A B C) denote *1 above then the induction scheme we'll use
is
<a href="The_Induction_Scheme_Selected_for_the_App_Example.html">(</a>AND
<a href="The_Induction_Step_in_the_App_Example.html">(</a>IMPLIES (AND (NOT (ENDP A))
(:P (CDR A) B C))
(:P A B C))
<a href="The_Base_Case_in_the_App_Example.html">(</a>IMPLIES (ENDP A) (:P A B C))).
This induction is <a href="The_Justification_of_the_Induction_Scheme.html">justified</a> by the same argument used to admit APP,
namely, the measure (ACL2-COUNT A) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized
by O-P). When <a href="The_Instantiation_of_the_Induction_Scheme.html">applied</a> to the goal at hand the above induction
scheme produces the following two <a href="Nontautological_Subgoals.html">nontautological subgoals</a>.<p>
</pre>
<p>
<a href="Overview_of_the_Simplification_of_the_Induction_Step_to_T.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>
|
