# LaTeX2HTML 96.1 (Feb 5, 1996)
# Associate contents original text with physical files.

$key = q/0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '0%:%newlib.html%:%The LEGO library' unless ($toc_section_info{$key}); 
$key = q/0 0 0 13 6 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node30.html%:%Square Roots' unless ($toc_section_info{$key}); 
$key = q/0 0 0 22 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node73.html%:%Imperative programs' unless ($toc_section_info{$key}); 
$key = q/0 0 0 6 3 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node14.html%:%Setoids' unless ($toc_section_info{$key}); 
$key = q/0 0 0 9 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node17.html%:%The Booleans' unless ($toc_section_info{$key}); 
$key = q/0 0 0 14 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node42.html%:%List Definitions' unless ($toc_section_info{$key}); 
$key = q/0 0 0 18 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node59.html%:%Relations' unless ($toc_section_info{$key}); 
$key = q/0 0 0 14 7 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node48.html%:%Lists and products' unless ($toc_section_info{$key}); 
$key = q/0 0 0 23 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node84.html%:%Basic properties' unless ($toc_section_info{$key}); 
$key = q/0 0 0 27 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node91.html%:%Other work' unless ($toc_section_info{$key}); 
$key = q/0 0 0 20 3 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node66.html%:%Basic Lemmas' unless ($toc_section_info{$key}); 
$key = q/0 0 0 22 1 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '5%:%node76.html%:%Updating' unless ($toc_section_info{$key}); 
$key = q/0 0 0 6 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node8.html%:%Logic' unless ($toc_section_info{$key}); 
$key = q/0 0 0 7 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node15.html%:%The Empty Type' unless ($toc_section_info{$key}); 
$key = q/0 0 0 13 14 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node38.html%:%All order relations' unless ($toc_section_info{$key}); 
$key = q/0 0 0 6 2 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '5%:%node11.html%:%Paulin-Mohring's Inductive Equality' unless ($toc_section_info{$key}); 
$key = q/0 0 0 13 5 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node29.html%:%Theorems about multiplication' unless ($toc_section_info{$key}); 
$key = q/0 0 0 22 5 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node80.html%:%Example' unless ($toc_section_info{$key}); 
$key = q/0 0 0 14 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node41.html%:%List' unless ($toc_section_info{$key}); 
$key = q/0 0 0 23 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node83.html%:%Pure Martin L&#246;f type theory' unless ($toc_section_info{$key}); 
$key = q/0 0 0 14 6 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node47.html%:%Other list functions' unless ($toc_section_info{$key}); 
$key = q/0 0 0 13 10 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node34.html%:%Propositional Relations' unless ($toc_section_info{$key}); 
$key = q/0 0 0 5 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node5.html%:%Basic Library Files' unless ($toc_section_info{$key}); 
$key = q/0 0 0 20 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node65.html%:%The Integers--Definitions' unless ($toc_section_info{$key}); 
$key = q/0 0 0 19 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node62.html%:%Set theory' unless ($toc_section_info{$key}); 
$key = q/0 0 0 28 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node92.html%:%References' unless ($toc_section_info{$key}); 
$key = q/0 0 0 20 8 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node71.html%:%Max and min on integers' unless ($toc_section_info{$key}); 
$key = q/0 0 0 14 10 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node51.html%:%Distinctness' unless ($toc_section_info{$key}); 
$key = q/0 0 0 16 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node57.html%:%Vector Basics' unless ($toc_section_info{$key}); 
$key = q/0 0 0 13 4 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node28.html%:%Theorems about Plus' unless ($toc_section_info{$key}); 
$key = q/0 0 0 3 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node3.html%:%Conventions' unless ($toc_section_info{$key}); 
$key = q/0 0 0 22 4 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node79.html%:%Hoare logic: Inversion' unless ($toc_section_info{$key}); 
$key = q/0 0 0 9 3 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node20.html%:%Boolean Theorems' unless ($toc_section_info{$key}); 
$key = q/0 0 0 10 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node21.html%:%Product Types' unless ($toc_section_info{$key}); 
$key = q/0 0 0 13 15 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node39.html%:%The predicate Even' unless ($toc_section_info{$key}); 
$key = q/0 0 0 14 5 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node46.html%:%Length-like list functions' unless ($toc_section_info{$key}); 
$key = q/0 0 0 15 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node54.html%:%Finite Sets' unless ($toc_section_info{$key}); 
$key = q/0 0 0 20 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node64.html%:%Extra lemmas for integers' unless ($toc_section_info{$key}); 
$key = q/0 0 0 24 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node86.html%:%Library files for eliminating over <TT>Type</TT>' unless ($toc_section_info{$key}); 
$key = q/0 0 0 20 7 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node70.html%:%Propositional relations on integers' unless ($toc_section_info{$key}); 
$key = q/0 0 0 6 2 3 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '5%:%node12.html%:%Martin-L&#246;f's Inductive Equality' unless ($toc_section_info{$key}); 
$key = q/0 0 0 22 5 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '5%:%node82.html%:%The correctness proof' unless ($toc_section_info{$key}); 
$key = q/0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node1.html%:%Contents' unless ($toc_section_info{$key}); 
$key = q/0 0 0 16 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node56.html%:%Vector Definitions' unless ($toc_section_info{$key}); 
$key = q/0 0 0 9 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node18.html%:%Boolean Definition' unless ($toc_section_info{$key}); 
$key = q/0 0 0 13 11 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node35.html%:%Iteration Principles' unless ($toc_section_info{$key}); 
$key = q/0 0 0 22 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '5%:%node75.html%:%Basic defintion of locations' unless ($toc_section_info{$key}); 
$key = q/0 0 0 29 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node93.html%:%  About this document ... ' unless ($toc_section_info{$key}); 
$key = q/0 0 0 13 3 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node27.html%:%Theorems about Minus' unless ($toc_section_info{$key}); 
$key = q/0 0 0 13 9 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node33.html%:%Propositional Strict Inequality' unless ($toc_section_info{$key}); 
$key = q/0 0 0 14 11 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node52.html%:%Permutation' unless ($toc_section_info{$key}); 
$key = q/0 0 0 22 3 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node78.html%:%Hoare logic' unless ($toc_section_info{$key}); 
$key = q/0 0 0 26 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node90.html%:%Number Theory' unless ($toc_section_info{$key}); 
$key = q/0 0 0 14 4 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node45.html%:%Partial List functions' unless ($toc_section_info{$key}); 
$key = q/0 0 0 6 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node9.html%:%Equality' unless ($toc_section_info{$key}); 
$key = q/0 0 0 8 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node16.html%:%The Unit Type' unless ($toc_section_info{$key}); 
$key = q/0 0 0 11 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node22.html%:%Sum Types' unless ($toc_section_info{$key}); 
$key = q/0 0 0 20 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node63.html%:%The Integers' unless ($toc_section_info{$key}); 
$key = q/0 0 0 13 16 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node40.html%:%Max and Min' unless ($toc_section_info{$key}); 
$key = q/0 0 0 20 6 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node69.html%:%Boolean valued functions on the integers' unless ($toc_section_info{$key}); 
$key = q/0 0 0 16 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node55.html%:%Vectors' unless ($toc_section_info{$key}); 
$key = q/0 0 0 25 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node87.html%:%Library files for elimination over <TT>Prop</TT>' unless ($toc_section_info{$key}); 
$key = q/0 0 0 13 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node26.html%:%Theorems about Successor' unless ($toc_section_info{$key}); 
$key = q/0 0 0 6 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node7.html%:%Providing logic and equality' unless ($toc_section_info{$key}); 
$key = q/0 0 0 5 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node6.html%:%Parameters' unless ($toc_section_info{$key}); 
$key = q/0 0 0 13 8 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node32.html%:%Propositional Inequality' unless ($toc_section_info{$key}); 
$key = q/0 0 0 22 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node77.html%:%An imperative programming language' unless ($toc_section_info{$key}); 
$key = q/0 0 0 13 12 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node36.html%:%Induction Principles' unless ($toc_section_info{$key}); 
$key = q/0 0 0 26 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node89.html%:%The Rationals' unless ($toc_section_info{$key}); 
$key = q/0 0 0 14 3 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node44.html%:%List functions with booleans' unless ($toc_section_info{$key}); 
$key = q/0 0 0 18 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node61.html%:%Relation closures' unless ($toc_section_info{$key}); 
$key = q/0 0 0 6 2 4 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '5%:%node13.html%:%Altenkirch-Streicher Elimination Rule' unless ($toc_section_info{$key}); 
$key = q/0 0 0 14 9 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node50.html%:%Membership' unless ($toc_section_info{$key}); 
$key = q/0 0 0 14 12 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node53.html%:%Sorted Lists' unless ($toc_section_info{$key}); 
$key = q/0 0 0 20 5 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node68.html%:%Some integer facts for number theory' unless ($toc_section_info{$key}); 
$key = q/0 0 0 12 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node23.html%:%Inductive Sigma' unless ($toc_section_info{$key}); 
$key = q/0 0 0 4 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node4.html%:%Customizing the Library' unless ($toc_section_info{$key}); 
$key = q/0 0 0 21 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node72.html%:%Specification and development of functional programs' unless ($toc_section_info{$key}); 
$key = q/0 0 0 22 5 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '5%:%node81.html%:%The marker phase of a garbage collection algorithm' unless ($toc_section_info{$key}); 
$key = q/0 0 0 13 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node25.html%:%Natural Numbers: Basic Definitions' unless ($toc_section_info{$key}); 
$key = q/0 0 0 17 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node58.html%:%Quotient Types' unless ($toc_section_info{$key}); 
$key = q/0 0 0 13 7 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node31.html%:%Order relations' unless ($toc_section_info{$key}); 
$key = q/0 0 0 22 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node74.html%:%Locations' unless ($toc_section_info{$key}); 
$key = q/0 0 0 26 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node88.html%:%Example Proof developments' unless ($toc_section_info{$key}); 
$key = q/0 0 0 6 2 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '5%:%node10.html%:%Leibniz Equality' unless ($toc_section_info{$key}); 
$key = q/0 0 0 14 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node43.html%:%List Basics' unless ($toc_section_info{$key}); 
$key = q/0 0 0 18 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node60.html%:%Definitions' unless ($toc_section_info{$key}); 
$key = q/0 0 0 14 8 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node49.html%:%The Relation Adjoin' unless ($toc_section_info{$key}); 
$key = q/0 0 0 23 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node85.html%:%Natural Numbers: Basic theorems' unless ($toc_section_info{$key}); 
$key = q/0 0 0 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node2.html%:%Introduction' unless ($toc_section_info{$key}); 
$key = q/0 0 0 9 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node19.html%:%Boolean Functions' unless ($toc_section_info{$key}); 
$key = q/0 0 0 13 13 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node37.html%:%Boolean-valued Relations' unless ($toc_section_info{$key}); 
$key = q/0 0 0 20 4 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node67.html%:%Some theorems about Modulo' unless ($toc_section_info{$key}); 
$key = q/0 0 0 13 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node24.html%:%The Natural Numbers' unless ($toc_section_info{$key}); 

1;

