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
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
|
<html>
<head><title>Pages_Written_Especially_for_the_Tours.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h1>Pages Written Especially for the Tours</h1>Pages Written Especially for the Tours
<pre>Major Section: <a href="acl2-doc-major-topics.html">ACL2 Documentation</a>
</pre><p>
The ACL2 Home Page is generated from ACL2's online documentation strings.
(How else could we achieve the total integration of ACL2's online
documentation with the home page?) This page is just an artifact of the
structure of our documentation strings: each string must belong to a ``major
section'' of the documentation database. This page is not structured to be
used by a person browsing via the Web. It contains, in an arbitrary order,
the pages written specificially for the Web user.<p>
Furthermore, browsing the pages below via the ACL2 :DOC command or
via TexInfo is often unsatisfying because those browsers do not
support gif files and the notion of going ``back'' to a node just
visited. If you wish to look at the pages below, we strongly
recommend that you do so via a HTML-based Web browser. Indeed, you
should simply visit ACL2's Home Page and take one of the Tours.
<p>
<ul>
<li><h3><a href="A_Flying_Tour_of_ACL2.html">A Flying Tour of ACL2</a> -- A Flying Tour of ACL2
</h3>
</li>
<li><h3><a href="A_Sketch_of_How_the_Rewriter_Works.html">A Sketch of How the Rewriter Works</a> -- A Sketch of How the Rewriter Works
</h3>
</li>
<li><h3><a href="A_Tiny_Warning_Sign.html">A Tiny Warning Sign</a> -- A Tiny Warning Sign
</h3>
</li>
<li><h3><a href="A_Trivial_Proof.html">A Trivial Proof</a> -- A Trivial Proof
</h3>
</li>
<li><h3><a href="A_Typical_State.html">A Typical State</a> -- A Typical State
</h3>
</li>
<li><h3><a href="A_Walking_Tour_of_ACL2.html">A Walking Tour of ACL2</a> -- A Walking Tour of ACL2
</h3>
</li>
<li><h3><a href="ACL2_Characters.html">ACL2 Characters</a> -- ACL2 Characters
</h3>
</li>
<li><h3><a href="ACL2_Conses_or_Ordered_Pairs.html">ACL2 Conses or Ordered Pairs</a> -- ACL2 Conses or Ordered Pairs
</h3>
</li>
<li><h3><a href="ACL2_Strings.html">ACL2 Strings</a> -- ACL2 Strings
</h3>
</li>
<li><h3><a href="ACL2_Symbols.html">ACL2 Symbols</a> -- ACL2 Symbols
</h3>
</li>
<li><h3><a href="ACL2_System_Architecture.html">ACL2 System Architecture</a> -- ACL2 System Architecture
</h3>
</li>
<li><h3><a href="ACL2_as_an_Interactive_Theorem_Prover.html">ACL2 as an Interactive Theorem Prover</a> -- ACL2 as an Interactive Theorem Prover
</h3>
</li>
<li><h3><a href="ACL2_as_an_Interactive_Theorem_Prover__lparen_cont_rparen_.html">ACL2 as an Interactive Theorem Prover (cont)</a> -- ACL2 as an Interactive Theorem Prover (cont)
</h3>
</li>
<li><h3><a href="ACL2_is_an_Untyped_Language.html">ACL2 is an Untyped Language</a> -- ACL2 is an Untyped Language
</h3>
</li>
<li><h3><a href="About_Models.html">About Models</a> -- About Models
</h3>
</li>
<li><h3><a href="About_Types.html">About Types</a> -- About Types
</h3>
</li>
<li><h3><a href="About_the_ACL2_Home_Page.html">About the ACL2 Home Page</a> -- About the ACL2 Home Page
</h3>
</li>
<li><h3><a href="About_the_Admission_of_Recursive_Definitions.html">About the Admission of Recursive Definitions</a> -- About the Admission of Recursive Definitions
</h3>
</li>
<li><h3><a href="About_the_Prompt.html">About the Prompt</a> -- About the Prompt
</h3>
</li>
<li><h3><a href="An_Example_Common_Lisp_Function_Definition.html">An Example Common Lisp Function Definition</a> -- An Example Common Lisp Function Definition
</h3>
</li>
<li><h3><a href="An_Example_of_ACL2_in_Use.html">An Example of ACL2 in Use</a> -- An Example of ACL2 in Use
</h3>
</li>
<li><h3><a href="Analyzing_Common_Lisp_Models.html">Analyzing Common Lisp Models</a> -- Analyzing Common Lisp Models
</h3>
</li>
<li><h3><a href="Common_Lisp.html">Common Lisp</a> -- Common Lisp
</h3>
</li>
<li><h3><a href="Common_Lisp_as_a_Modeling_Language.html">Common Lisp as a Modeling Language</a> -- Common Lisp as a Modeling Language
</h3>
</li>
<li><h3><a href="Conversion.html">Conversion</a> -- Conversion to Uppercase
</h3>
</li>
<li><h3><a href="Corroborating_Models.html">Corroborating Models</a> -- Corroborating Models
</h3>
</li>
<li><h3><a href="Evaluating_App_on_Sample_Input.html">Evaluating App on Sample Input</a> -- Evaluating App on Sample Input
</h3>
</li>
<li><h3><a href="Flawed_Induction_Candidates_in_App_Example.html">Flawed Induction Candidates in App Example</a> -- Flawed Induction Candidates in App Example
</h3>
</li>
<li><h3><a href="Free_Variables_in_Top-Level_Input.html">Free Variables in Top-Level Input</a> -- Free Variables in Top-Level Input
</h3>
</li>
<li><h3><a href="Functions_for_Manipulating_these_Objects.html">Functions for Manipulating these Objects</a> -- Functions for Manipulating these Objects
</h3>
</li>
<li><h3><a href="Guards.html">Guards</a> -- Guards
</h3>
</li>
<li><h3><a href="Guessing_the_Type_of_a_Newly_Admitted_Function.html">Guessing the Type of a Newly Admitted Function</a> -- Guessing the Type of a Newly Admitted Function
</h3>
</li>
<li><h3><a href="Guiding_the_ACL2_Theorem_Prover.html">Guiding the ACL2 Theorem Prover</a> -- Guiding the ACL2 Theorem Prover
</h3>
</li>
<li><h3><a href="Hey_Wait_bang___Is_ACL2_Typed_or_Untyped_lparen_Q_rparen_.html">Hey Wait! Is ACL2 Typed or Untyped(Q)</a> -- Hey Wait! Is ACL2 Typed or Untyped?
</h3>
</li>
<li><h3><a href="How_Long_Does_It_Take_to_Become_an_Effective_User_lparen_Q_rparen_.html">How Long Does It Take to Become an Effective User(Q)</a> -- How Long Does It Take to Become an Effective User?
</h3>
</li>
<li><h3><a href="How_To_Find_Out_about_ACL2_Functions.html">How To Find Out about ACL2 Functions</a> -- How To Find Out about ACL2 Functions
</h3>
</li>
<li><h3><a href="How_To_Find_Out_about_ACL2_Functions__lparen_cont_rparen_.html">How To Find Out about ACL2 Functions (cont)</a> -- How To Find Out about ACL2 Functions (cont)
</h3>
</li>
<li><h3><a href="Modeling_in_ACL2.html">Modeling in ACL2</a> -- Modeling in ACL2
</h3>
</li>
<li><h3><a href="Models_in_Engineering.html">Models in Engineering</a> -- Models in Engineering
</h3>
</li>
<li><h3><a href="Models_of_Computer_Hardware_and_Software.html">Models of Computer Hardware and Software</a> -- Models of Computer Hardware and Software
</h3>
</li>
<li><h3><a href="Name_the_Formula_Above.html">Name the Formula Above</a> -- Name the Formula Above
</h3>
</li>
<li><h3><a href="Nontautological_Subgoals.html">Nontautological Subgoals</a> -- Prover output omits some details
</h3>
</li>
<li><h3><a href="Numbers_in_ACL2.html">Numbers in ACL2</a> -- Numbers in ACL2
</h3>
</li>
<li><h3><a href="On_the_Naming_of_Subgoals.html">On the Naming of Subgoals</a> -- On the Naming of Subgoals
</h3>
</li>
<li><h3><a href="Other_Requirements.html">Other Requirements</a> -- Other Requirements
</h3>
</li>
<li><h3><a href="Overview_of_the_Expansion_of_ENDP_in_the_Base_Case.html">Overview of the Expansion of ENDP in the Base Case</a> -- Overview of the Expansion of ENDP in the Base Case
</h3>
</li>
<li><h3><a href="Overview_of_the_Expansion_of_ENDP_in_the_Induction_Step.html">Overview of the Expansion of ENDP in the Induction Step</a> -- Overview of the Expansion of ENDP in the Induction Step
</h3>
</li>
<li><h3><a href="Overview_of_the_Final_Simplification_in_the_Base_Case.html">Overview of the Final Simplification in the Base Case</a> -- Overview of the Final Simplification in the Base Case
</h3>
</li>
<li><h3><a href="Overview_of_the_Proof_of_a_Trivial_Consequence.html">Overview of the Proof of a Trivial Consequence</a> -- Overview of the Proof of a Trivial Consequence
</h3>
</li>
<li><h3><a href="Overview_of_the_Simplification_of_the_Base_Case_to_T.html">Overview of the Simplification of the Base Case to T</a> -- Overview of the Simplification of the Base Case to T
</h3>
</li>
<li><h3><a href="Overview_of_the_Simplification_of_the_Induction_Conclusion.html">Overview of the Simplification of the Induction Conclusion</a> -- Overview of the Simplification of the Induction Conclusion
</h3>
</li>
<li><h3><a href="Overview_of_the_Simplification_of_the_Induction_Step_to_T.html">Overview of the Simplification of the Induction Step to T</a> -- Overview of the Simplification of the Induction Step to T
</h3>
</li>
<li><h3><a href="Perhaps.html">Perhaps</a> -- Perhaps
</h3>
</li>
<li><h3><a href="Popping_out_of_an_Inductive_Proof.html">Popping out of an Inductive Proof</a> -- Popping out of an Inductive Proof
</h3>
</li>
<li><h3><a href="Proving_Theorems_about_Models.html">Proving Theorems about Models</a> -- Proving Theorems about Models
</h3>
</li>
<li><h3><a href="Revisiting_the_Admission_of_App.html">Revisiting the Admission of App</a> -- Revisiting the Admission of App
</h3>
</li>
<li><h3><a href="Rewrite_Rules_are_Generated_from_DEFTHM_Events.html">Rewrite Rules are Generated from DEFTHM Events</a> -- Rewrite Rules are Generated from DEFTHM Events
</h3>
</li>
<li><h3><a href="Running_Models.html">Running Models</a> -- Running Models
</h3>
</li>
<li><h3><a href="Subsumption_of_Induction_Candidates_in_App_Example.html">Subsumption of Induction Candidates in App Example</a> -- Subsumption of Induction Candidates in App Example
</h3>
</li>
<li><h3><a href="Suggested_Inductions_in_the_Associativity_of_App_Example.html">Suggested Inductions in the Associativity of App Example</a> -- Suggested Inductions in the Associativity of App Example
</h3>
</li>
<li><h3><a href="Symbolic_Execution_of_Models.html">Symbolic Execution of Models</a> -- Symbolic Execution of Models
</h3>
</li>
<li><h3><a href="The_Admission_of_App.html">The Admission of App</a> -- The Admission of App
</h3>
</li>
<li><h3><a href="The_Associativity_of_App.html">The Associativity of App</a> -- The Associativity of App
</h3>
</li>
<li><h3><a href="The_Base_Case_in_the_App_Example.html">The Base Case in the App Example</a> -- The Base Case in the App Example
</h3>
</li>
<li><h3><a href="The_End_of_the_Flying_Tour.html">The End of the Flying Tour</a> -- The End of the Flying Tour
</h3>
</li>
<li><h3><a href="The_End_of_the_Proof_of_the_Associativity_of_App.html">The End of the Proof of the Associativity of App</a> -- The End of the Proof of the Associativity of App
</h3>
</li>
<li><h3><a href="The_End_of_the_Walking_Tour.html">The End of the Walking Tour</a> -- The End of the Walking Tour
</h3>
</li>
<li><h3><a href="The_Event_Summary.html">The Event Summary</a> -- The Event Summary
</h3>
</li>
<li><h3><a href="The_Expansion_of_ENDP_in_the_Induction_Step__lparen_Step_0_rparen_.html">The Expansion of ENDP in the Induction Step (Step 0)</a> -- The Expansion of ENDP in the Induction Step (Step 0)
</h3>
</li>
<li><h3><a href="The_Expansion_of_ENDP_in_the_Induction_Step__lparen_Step_1_rparen_.html">The Expansion of ENDP in the Induction Step (Step 1)</a> -- The Expansion of ENDP in the Induction Step (Step 1)
</h3>
</li>
<li><h3><a href="The_Expansion_of_ENDP_in_the_Induction_Step__lparen_Step_2_rparen_.html">The Expansion of ENDP in the Induction Step (Step 2)</a> -- The Expansion of ENDP in the Induction Step (Step 2)
</h3>
</li>
<li><h3><a href="The_Falling_Body_Model.html">The Falling Body Model</a> -- The Falling Body Model
</h3>
</li>
<li><h3><a href="The_Final_Simplification_in_the_Base_Case__lparen_Step_0_rparen_.html">The Final Simplification in the Base Case (Step 0)</a> -- the Final Simplification in the Base Case (Step 0)
</h3>
</li>
<li><h3><a href="The_Final_Simplification_in_the_Base_Case__lparen_Step_1_rparen_.html">The Final Simplification in the Base Case (Step 1)</a> -- the Final Simplification in the Base Case (Step 1)
</h3>
</li>
<li><h3><a href="The_Final_Simplification_in_the_Base_Case__lparen_Step_2_rparen_.html">The Final Simplification in the Base Case (Step 2)</a> -- the Final Simplification in the Base Case (Step 2)
</h3>
</li>
<li><h3><a href="The_Final_Simplification_in_the_Base_Case__lparen_Step_3_rparen_.html">The Final Simplification in the Base Case (Step 3)</a> -- the Final Simplification in the Base Case (Step 3)
</h3>
</li>
<li><h3><a href="The_First_Application_of_the_Associativity_Rule.html">The First Application of the Associativity Rule</a> -- The First Application of the Associativity Rule
</h3>
</li>
<li><h3><a href="The_Induction_Scheme_Selected_for_the_App_Example.html">The Induction Scheme Selected for the App Example</a> -- The Induction Scheme Selected for the App Example
</h3>
</li>
<li><h3><a href="The_Induction_Step_in_the_App_Example.html">The Induction Step in the App Example</a> -- The Induction Step in the App Example
</h3>
</li>
<li><h3><a href="The_Instantiation_of_the_Induction_Scheme.html">The Instantiation of the Induction Scheme</a> -- The Instantiation of the Induction Scheme
</h3>
</li>
<li><h3><a href="The_Justification_of_the_Induction_Scheme.html">The Justification of the Induction Scheme</a> -- The Justification of the Induction Scheme
</h3>
</li>
<li><h3><a href="The_Proof_of_the_Associativity_of_App.html">The Proof of the Associativity of App</a> -- The Proof of the Associativity of App
</h3>
</li>
<li><h3><a href="The_Q.E.D._Message.html">The Q.E.D. Message</a> -- The Q.E.D. Message
</h3>
</li>
<li><h3><a href="The_Rules_used_in_the_Associativity_of_App_Proof.html">The Rules used in the Associativity of App Proof</a> -- The Rules used in the Associativity of App Proof
</h3>
</li>
<li><h3><a href="The_Simplification_of_the_Induction_Conclusion__lparen_Step_0_rparen_.html">The Simplification of the Induction Conclusion (Step 0)</a> -- the Simplification of the Induction Conclusion (Step 0)
</h3>
</li>
<li><h3><a href="The_Simplification_of_the_Induction_Conclusion__lparen_Step_1_rparen_.html">The Simplification of the Induction Conclusion (Step 1)</a> -- the Simplification of the Induction Conclusion (Step 1)
</h3>
</li>
<li><h3><a href="The_Simplification_of_the_Induction_Conclusion__lparen_Step_10_rparen_.html">The Simplification of the Induction Conclusion (Step 10)</a> -- the Simplification of the Induction Conclusion (Step 10)
</h3>
</li>
<li><h3><a href="The_Simplification_of_the_Induction_Conclusion__lparen_Step_11_rparen_.html">The Simplification of the Induction Conclusion (Step 11)</a> -- the Simplification of the Induction Conclusion (Step 11)
</h3>
</li>
<li><h3><a href="The_Simplification_of_the_Induction_Conclusion__lparen_Step_12_rparen_.html">The Simplification of the Induction Conclusion (Step 12)</a> -- the Simplification of the Induction Conclusion (Step 12)
</h3>
</li>
<li><h3><a href="The_Simplification_of_the_Induction_Conclusion__lparen_Step_2_rparen_.html">The Simplification of the Induction Conclusion (Step 2)</a> -- the Simplification of the Induction Conclusion (Step 2)
</h3>
</li>
<li><h3><a href="The_Simplification_of_the_Induction_Conclusion__lparen_Step_3_rparen_.html">The Simplification of the Induction Conclusion (Step 3)</a> -- the Simplification of the Induction Conclusion (Step 3)
</h3>
</li>
<li><h3><a href="The_Simplification_of_the_Induction_Conclusion__lparen_Step_4_rparen_.html">The Simplification of the Induction Conclusion (Step 4)</a> -- the Simplification of the Induction Conclusion (Step 4)
</h3>
</li>
<li><h3><a href="The_Simplification_of_the_Induction_Conclusion__lparen_Step_5_rparen_.html">The Simplification of the Induction Conclusion (Step 5)</a> -- the Simplification of the Induction Conclusion (Step 5)
</h3>
</li>
<li><h3><a href="The_Simplification_of_the_Induction_Conclusion__lparen_Step_6_rparen_.html">The Simplification of the Induction Conclusion (Step 6)</a> -- the Simplification of the Induction Conclusion (Step 6)
</h3>
</li>
<li><h3><a href="The_Simplification_of_the_Induction_Conclusion__lparen_Step_7_rparen_.html">The Simplification of the Induction Conclusion (Step 7)</a> -- the Simplification of the Induction Conclusion (Step 7)
</h3>
</li>
<li><h3><a href="The_Simplification_of_the_Induction_Conclusion__lparen_Step_8_rparen_.html">The Simplification of the Induction Conclusion (Step 8)</a> -- the Simplification of the Induction Conclusion (Step 8)
</h3>
</li>
<li><h3><a href="The_Simplification_of_the_Induction_Conclusion__lparen_Step_9_rparen_.html">The Simplification of the Induction Conclusion (Step 9)</a> -- the Simplification of the Induction Conclusion (Step 9)
</h3>
</li>
<li><h3><a href="The_Summary_of_the_Proof_of_the_Trivial_Consequence.html">The Summary of the Proof of the Trivial Consequence</a> -- The Summary of the Proof of the Trivial Consequence
</h3>
</li>
<li><h3><a href="The_Theorem_that_App_is_Associative.html">The Theorem that App is Associative</a> -- The Theorem that App is Associative
</h3>
</li>
<li><h3><a href="The_Time_Taken_to_do_the_Associativity_of_App_Proof.html">The Time Taken to do the Associativity of App Proof</a> -- The Time Taken to do the Associativity of App Proof
</h3>
</li>
<li><h3><a href="The_Tours.html">The Tours</a> -- The Tours
</h3>
</li>
<li><h3><a href="The_WARNING_about_the_Trivial_Consequence.html">The WARNING about the Trivial Consequence</a> -- The WARNING about the Trivial Consequence
</h3>
</li>
<li><h3><a href="Undocumented_Topic.html">Undocumented Topic</a> -- Undocumented Topic
</h3>
</li>
<li><h3><a href="Using_the_Associativity_of_App_to_Prove_a_Trivial_Consequence.html">Using the Associativity of App to Prove a Trivial Consequence</a> -- Using the Associativity of App to Prove a Trivial Consequence
</h3>
</li>
<li><h3><a href="What_Is_ACL2_lparen_Q_rparen_.html">What Is ACL2(Q)</a> -- What Is ACL2?
</h3>
</li>
<li><h3><a href="What_is_Required_of_the_User_lparen_Q_rparen_.html">What is Required of the User(Q)</a> -- What is Required of the User?
</h3>
</li>
<li><h3><a href="What_is_a_Mathematical_Logic_lparen_Q_rparen_.html">What is a Mathematical Logic(Q)</a> -- What is a Mathematical Logic?
</h3>
</li>
<li><h3><a href="What_is_a_Mechanical_Theorem_Prover_lparen_Q_rparen_.html">What is a Mechanical Theorem Prover(Q)</a> -- What is a Mechanical Theorem Prover?
</h3>
</li>
<li><h3><a href="What_is_a_Mechanical_Theorem_Prover_lparen_Q_rparen___lparen_cont_rparen_.html">What is a Mechanical Theorem Prover(Q) (cont)</a> -- What is a Mechanical Theorem Prover? (cont)
</h3>
</li>
<li><h3><a href="You_Must_Think_about_the_Use_of_a_Formula_as_a_Rule.html">You Must Think about the Use of a Formula as a Rule</a> -- You Must Think about the Use of a Formula as a Rule
</h3>
</li>
</ul>
Generally, the topics listed above will not be of use to the ACL2 user.
<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>
|
