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

1;

