\relax 
\ifx\hyper@anchor\@undefined
\global \let \oldcontentsline\contentsline
\gdef \contentsline#1#2#3#4{\oldcontentsline{#1}{#2}{#3}}
\global \let \oldnewlabel\newlabel
\gdef \newlabel#1#2{\newlabelxx{#1}#2}
\gdef \newlabelxx#1#2#3#4#5#6{\oldnewlabel{#1}{{#2}{#3}}}
\AtEndDocument{\let \contentsline\oldcontentsline
\let \newlabel\oldnewlabel}
\else
\global \let \hyper@last\relax 
\fi

\bibstyle{plain}
\@writefile{toc}{\contentsline {section}{Preface}{ix}{chapter*.2}}
\@writefile{toc}{\contentsline {subsubsection}{Overview}{ix}{section*.3}}
\@writefile{toc}{\contentsline {subsubsection}{Setting Your Expectations}{xi}{section*.4}}
\citation{Barrow}
\@writefile{toc}{\contentsline {subsubsection}{Metamath and Mathematical Literature}{xii}{section*.5}}
\newlabel{envision}{{2}{xii}{Metamath and Mathematical Literature\relax }{section*.5}{}}
\expandafter\gdef \csname page@num.envision\endcsname{xii}\expandafter\gdef \csname ref@num.envision\endcsname{2}\expandafter\gdef \csname sectionref@name.envision\endcsname{}
\citation{Davis}
\@writefile{toc}{\contentsline {subsubsection}{Formalism}{xiii}{section*.6}}
\@writefile{toc}{\contentsline {subsubsection}{A Personal Note}{xiii}{section*.7}}
\@writefile{toc}{\contentsline {subsubsection}{Note on Bibliography and Index}{xiii}{section*.8}}
\@writefile{toc}{\contentsline {subsubsection}{Acknowledgments}{xiv}{section*.9}}
\@writefile{toc}{\contentsline {subsubsection}{Note Added June 22, 2005}{xiv}{section*.10}}
\newlabel{note2002}{{2}{xiv}{Note Added June 22, 2005\relax }{section*.10}{}}
\expandafter\gdef \csname page@num.note2002\endcsname{xiv}\expandafter\gdef \csname ref@num.note2002\endcsname{2}\expandafter\gdef \csname sectionref@name.note2002\endcsname{}
\@writefile{toc}{\contentsline {subsubsection}{Note Added June 24, 2006}{xv}{section*.11}}
\newlabel{note2006}{{3}{xv}{Note Added June 24, 2006\relax }{section*.11}{}}
\expandafter\gdef \csname page@num.note2006\endcsname{xv}\expandafter\gdef \csname ref@num.note2006\endcsname{3}\expandafter\gdef \csname sectionref@name.note2006\endcsname{}
\@writefile{toc}{\contentsline {subsubsection}{Note Added March 10, 2007}{xv}{section*.12}}
\newlabel{note2006b}{{3}{xv}{Note Added March 10, 2007\relax }{section*.12}{}}
\expandafter\gdef \csname page@num.note2006b\endcsname{xv}\expandafter\gdef \csname ref@num.note2006b\endcsname{3}\expandafter\gdef \csname sectionref@name.note2006b\endcsname{}
\citation{Davis}
\@writefile{toc}{\contentsline {chapter}{\numberline {1}Introduction}{1}{chapter.1}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\citation{Munkres}
\citation{Whitehead}
\@writefile{toc}{\contentsline {section}{\numberline {1.1}Mathematics as a Computer Language}{4}{section.1.1}}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.1.1}Is Mathematics ``User-Friendly''?}{4}{subsection.1.1.1}}
\citation{Landau}
\citation{Guillen}
\citation{Rucker}
\@writefile{toc}{\contentsline {subsubsection}{A Non-Mathematician's Quest for Truth}{5}{section*.13}}
\citation{Solow}
\citation{Davis}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.1.2}Mathematics and the Non-Specialist}{12}{subsection.1.1.2}}
\citation{Edwards}
\citation{Davis}
\citation{Wang}
\citation{deMillo}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.1.3}An Impossible Dream?}{14}{subsection.1.1.3}}
\newlabel{dream}{{1.1.3}{14}{An Impossible Dream?\relax }{subsection.1.1.3}{}}
\expandafter\gdef \csname page@num.dream\endcsname{14}\expandafter\gdef \csname ref@num.dream\endcsname{1.1.3}\expandafter\gdef \csname sectionref@name.dream\endcsname{subsection.1.1.3}
\citation{Mathias}
\citation{Moore}
\citation{Russell}
\citation{Davis}
\newlabel{bourbaki}{{23}{15}{An Impossible Dream?\relax }{Hfootnote.23}{}}
\expandafter\gdef \csname page@num.bourbaki\endcsname{15}\expandafter\gdef \csname ref@num.bourbaki\endcsname{23}\expandafter\gdef \csname sectionref@name.bourbaki\endcsname{subsection.1.1.3}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.1.4}Beauty}{15}{subsection.1.1.4}}
\citation{deMillo}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.1.5}Simplicity}{16}{subsection.1.1.5}}
\citation{Anderson}
\citation{MegillBunder}
\citation{Boolos}
\citation{Pavicic}
\citation{Tymoczko}
\citation{Enderton}
\citation{Curry}
\citation{Kline}
\citation{Klinel}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.1.6}Rigor}{18}{subsection.1.1.6}}
\citation{Harrison}
\citation{Albers}
\@writefile{toc}{\contentsline {section}{\numberline {1.2}Computers and Mathematicians}{20}{section.1.2}}
\citation{Tymoczko}
\citation{Swart}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.2.1}Trusting the Computer}{21}{subsection.1.2.1}}
\citation{deMillo}
\citation{deMillo}
\citation{Stark}
\citation{Kramer}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.2.2}Trusting the Mathematician}{22}{subsection.1.2.2}}
\citation{Davis}
\citation{Enderton}
\citation{Enderton}
\citation{Courant}
\citation{Swart}
\citation{Davis}
\citation{PetersonI}
\citation{Wolfram}
\@writefile{toc}{\contentsline {section}{\numberline {1.3}The Use of Computers in Mathematics}{24}{section.1.3}}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.3.1}Computer Algebra Systems}{24}{subsection.1.3.1}}
\citation{Harrison-thesis}
\citation{Tarski}
\citation{Chou}
\citation{Penrose}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.3.2}Automated Theorem Provers}{25}{subsection.1.3.2}}
\newlabel{theoremprovers}{{1.3.2}{25}{Automated Theorem Provers\relax }{subsection.1.3.2}{}}
\expandafter\gdef \csname page@num.theoremprovers\endcsname{25}\expandafter\gdef \csname ref@num.theoremprovers\endcsname{1.3.2}\expandafter\gdef \csname sectionref@name.theoremprovers\endcsname{subsection.1.3.2}
\citation{Robinson}
\citation{Wos}
\citation{Wos}
\citation{Megill}
\citation{Bledsoe}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.3.3}Proof Verifiers}{27}{subsection.1.3.3}}
\newlabel{proofverifiers}{{1.3.3}{27}{Proof Verifiers\relax }{subsection.1.3.3}{}}
\expandafter\gdef \csname page@num.proofverifiers\endcsname{27}\expandafter\gdef \csname ref@num.proofverifiers\endcsname{1.3.3}\expandafter\gdef \csname sectionref@name.proofverifiers\endcsname{subsection.1.3.3}
\citation{Harrison}
\@writefile{toc}{\contentsline {section}{\numberline {1.4}Mathematics and Metamath}{29}{section.1.4}}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.4.1}Standard Mathematics}{29}{subsection.1.4.1}}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.4.2}Other Formal Systems}{29}{subsection.1.4.2}}
\citation{Kline}
\citation{Behnke}
\citation{Shoenfield}
\citation{Davis}
\citation{PM}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.4.3}Metamath and Its Philosophy}{30}{subsection.1.4.3}}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.4.4}A History of the Approach Behind Metamath}{30}{subsection.1.4.4}}
\citation{Hindley}
\citation{Kalman}
\citation{Meredith}
\citation{Peterson}
\citation{Megill}
\citation{Robinson}
\citation{Herrlich}
\citation{Blass}
\citation{Megill}
\citation{Monks}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.4.5}Metamath and First-Order Logic}{31}{subsection.1.4.5}}
\newlabel{categoryth}{{1.4.5}{31}{Metamath and First-Order Logic\relax }{subsection.1.4.5}{}}
\expandafter\gdef \csname page@num.categoryth\endcsname{31}\expandafter\gdef \csname ref@num.categoryth\endcsname{1.4.5}\expandafter\gdef \csname sectionref@name.categoryth\endcsname{subsection.1.4.5}
\citation{Leblanc}
\@writefile{toc}{\contentsline {chapter}{\numberline {2}Using the Metamath Program}{33}{chapter.2}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\newlabel{using}{{2}{33}{Using the Metamath Program\relax }{chapter.2}{}}
\expandafter\gdef \csname page@num.using\endcsname{33}\expandafter\gdef \csname ref@num.using\endcsname{2}\expandafter\gdef \csname sectionref@name.using\endcsname{chapter.2}
\@writefile{toc}{\contentsline {section}{\numberline {2.1}Installation}{33}{section.2.1}}
\citation{Mendelson}
\citation{Mendelson}
\citation{Mendelson}
\@writefile{toc}{\contentsline {section}{\numberline {2.2}Your First Formal System}{34}{section.2.2}}
\newlabel{start}{{2.2}{34}{Your First Formal System\relax }{section.2.2}{}}
\expandafter\gdef \csname page@num.start\endcsname{34}\expandafter\gdef \csname ref@num.start\endcsname{2.2}\expandafter\gdef \csname sectionref@name.start\endcsname{section.2.2}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.2.1}From Nothing to Zero}{34}{subsection.2.2.1}}
\newlabel{startf}{{2.2.1}{34}{From Nothing to Zero\relax }{subsection.2.2.1}{}}
\expandafter\gdef \csname page@num.startf\endcsname{34}\expandafter\gdef \csname ref@num.startf\endcsname{2.2.1}\expandafter\gdef \csname sectionref@name.startf\endcsname{subsection.2.2.1}
\newlabel{zeroproof}{{52}{35}{From Nothing to Zero\relax }{equation.A2}{}}
\expandafter\gdef \csname page@num.zeroproof\endcsname{35}\expandafter\gdef \csname ref@num.zeroproof\endcsname{52}\expandafter\gdef \csname sectionref@name.zeroproof\endcsname{subsection.2.2.1}
\citation{Rucker}
\citation{Hofstadter}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.2.2}Converting It to Metamath}{36}{subsection.2.2.2}}
\newlabel{convert}{{2.2.2}{36}{Converting It to Metamath\relax }{subsection.2.2.2}{}}
\expandafter\gdef \csname page@num.convert\endcsname{36}\expandafter\gdef \csname ref@num.convert\endcsname{2.2.2}\expandafter\gdef \csname sectionref@name.convert\endcsname{subsection.2.2.2}
\newlabel{demo0}{{53}{37}{Converting It to Metamath\relax }{Hfootnote.53}{}}
\expandafter\gdef \csname page@num.demo0\endcsname{37}\expandafter\gdef \csname ref@num.demo0\endcsname{53}\expandafter\gdef \csname sectionref@name.demo0\endcsname{subsection.2.2.2}
\@writefile{toc}{\contentsline {section}{\numberline {2.3}A Trial Run}{40}{section.2.3}}
\newlabel{trialrun}{{2.3}{40}{A Trial Run\relax }{section.2.3}{}}
\expandafter\gdef \csname page@num.trialrun\endcsname{40}\expandafter\gdef \csname ref@num.trialrun\endcsname{2.3}\expandafter\gdef \csname sectionref@name.trialrun\endcsname{section.2.3}
\newlabel{demoproof}{{55}{44}{A Trial Run\relax }{Hfootnote.55}{}}
\expandafter\gdef \csname page@num.demoproof\endcsname{44}\expandafter\gdef \csname ref@num.demoproof\endcsname{55}\expandafter\gdef \csname sectionref@name.demoproof\endcsname{section.2.3}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.3.1}Some Hints for Using the Command Line Interface}{45}{subsection.2.3.1}}
\@writefile{toc}{\contentsline {section}{\numberline {2.4}Your First Proof}{46}{section.2.4}}
\newlabel{frstprf}{{2.4}{46}{Your First Proof\relax }{section.2.4}{}}
\expandafter\gdef \csname page@num.frstprf\endcsname{46}\expandafter\gdef \csname ref@num.frstprf\endcsname{2.4}\expandafter\gdef \csname sectionref@name.frstprf\endcsname{section.2.4}
\@writefile{toc}{\contentsline {section}{\numberline {2.5}A Note About Editing a Data\discretionary {-}{}{}base File}{53}{section.2.5}}
\citation{Barrow}
\@writefile{toc}{\contentsline {chapter}{\numberline {3}Abstract Mathematics Revealed}{55}{chapter.3}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\newlabel{fol}{{3}{55}{Abstract Mathematics Revealed\relax }{chapter.3}{}}
\expandafter\gdef \csname page@num.fol\endcsname{55}\expandafter\gdef \csname ref@num.fol\endcsname{3}\expandafter\gdef \csname sectionref@name.fol\endcsname{chapter.3}
\@writefile{toc}{\contentsline {section}{\numberline {3.1}Logic and Set Theory}{55}{section.3.1}}
\newlabel{logicandsettheory}{{3.1}{55}{Logic and Set Theory\relax }{section.3.1}{}}
\expandafter\gdef \csname page@num.logicandsettheory\endcsname{55}\expandafter\gdef \csname ref@num.logicandsettheory\endcsname{3.1}\expandafter\gdef \csname sectionref@name.logicandsettheory\endcsname{section.3.1}
\newlabel{expandom}{{3.1}{57}{Logic and Set Theory\relax }{Hfootnote.56}{}}
\expandafter\gdef \csname page@num.expandom\endcsname{57}\expandafter\gdef \csname ref@num.expandom\endcsname{3.1}\expandafter\gdef \csname sectionref@name.expandom\endcsname{section.3.1}
\citation{CAMeredith}
\@writefile{toc}{\contentsline {section}{\numberline {3.2}The Axioms for All of Mathematics}{58}{section.3.2}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.2.1}Propositional Calculus}{58}{subsection.3.2.1}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.2.2}Predicate Calculus}{59}{subsection.3.2.2}}
\citation{Hamilton}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.2.3}Equality}{61}{subsection.3.2.3}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.2.4}Set Theory}{61}{subsection.3.2.4}}
\@writefile{toc}{\contentsline {section}{\numberline {3.3}The Axioms in the Metamath Language}{63}{section.3.3}}
\newlabel{metaaxioms}{{3.3}{63}{The Axioms in the Metamath Language\relax }{section.3.3}{}}
\expandafter\gdef \csname page@num.metaaxioms\endcsname{63}\expandafter\gdef \csname ref@num.metaaxioms\endcsname{3.3}\expandafter\gdef \csname sectionref@name.metaaxioms\endcsname{section.3.3}
\citation{Megill}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.3.1}Propositional Calculus}{64}{subsection.3.3.1}}
\newlabel{propcalc}{{3.3.1}{64}{Propositional Calculus\relax }{subsection.3.3.1}{}}
\expandafter\gdef \csname page@num.propcalc\endcsname{64}\expandafter\gdef \csname ref@num.propcalc\endcsname{3.3.1}\expandafter\gdef \csname sectionref@name.propcalc\endcsname{subsection.3.3.1}
\newlabel{ax1}{{3.3.1}{64}{Propositional Calculus\relax }{subsection.3.3.1}{}}
\expandafter\gdef \csname page@num.ax1\endcsname{64}\expandafter\gdef \csname ref@num.ax1\endcsname{3.3.1}\expandafter\gdef \csname sectionref@name.ax1\endcsname{subsection.3.3.1}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.3.2}Pure Predicate Calculus}{64}{subsection.3.3.2}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.3.3}Equality and Substitution}{64}{subsection.3.3.3}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.3.4}Set Theory}{65}{subsection.3.3.4}}
\newlabel{mmsettheoryaxioms}{{3.3.4}{65}{Set Theory\relax }{subsection.3.3.4}{}}
\expandafter\gdef \csname page@num.mmsettheoryaxioms\endcsname{65}\expandafter\gdef \csname ref@num.mmsettheoryaxioms\endcsname{3.3.4}\expandafter\gdef \csname sectionref@name.mmsettheoryaxioms\endcsname{subsection.3.3.4}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.3.5}That's It}{66}{subsection.3.3.5}}
\@writefile{toc}{\contentsline {section}{\numberline {3.4}A Hierarchy of Definitions}{66}{section.3.4}}
\newlabel{hierarchy}{{3.4}{66}{A Hierarchy of Definitions\relax }{section.3.4}{}}
\expandafter\gdef \csname page@num.hierarchy\endcsname{66}\expandafter\gdef \csname ref@num.hierarchy\endcsname{3.4}\expandafter\gdef \csname sectionref@name.hierarchy\endcsname{section.3.4}
\citation{Takeuti}
\citation{Quine}
\citation{Bell}
\citation{Enderton}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.4.1}Definitions for Propositional Calculus}{68}{subsection.3.4.1}}
\newlabel{metadefprop}{{3.4.1}{68}{Definitions for Propositional Calculus\relax }{subsection.3.4.1}{}}
\expandafter\gdef \csname page@num.metadefprop\endcsname{68}\expandafter\gdef \csname ref@num.metadefprop\endcsname{3.4.1}\expandafter\gdef \csname sectionref@name.metadefprop\endcsname{subsection.3.4.1}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.4.2}Definitions for Predicate Calculus}{69}{subsection.3.4.2}}
\newlabel{metadefpred}{{3.4.2}{69}{Definitions for Predicate Calculus\relax }{subsection.3.4.2}{}}
\expandafter\gdef \csname page@num.metadefpred\endcsname{69}\expandafter\gdef \csname ref@num.metadefpred\endcsname{3.4.2}\expandafter\gdef \csname sectionref@name.metadefpred\endcsname{subsection.3.4.2}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.4.3}Definitions for Set Theory}{70}{subsection.3.4.3}}
\newlabel{setdefinitions}{{3.4.3}{70}{Definitions for Set Theory\relax }{subsection.3.4.3}{}}
\expandafter\gdef \csname page@num.setdefinitions\endcsname{70}\expandafter\gdef \csname ref@num.setdefinitions\endcsname{3.4.3}\expandafter\gdef \csname sectionref@name.setdefinitions\endcsname{subsection.3.4.3}
\newlabel{dfclel}{{3.4.3}{71}{Definitions for Set Theory\relax }{subsection.3.4.3}{}}
\expandafter\gdef \csname page@num.dfclel\endcsname{71}\expandafter\gdef \csname ref@num.dfclel\endcsname{3.4.3}\expandafter\gdef \csname sectionref@name.dfclel\endcsname{subsection.3.4.3}
\newlabel{dfbr}{{3.4.3}{73}{Definitions for Set Theory\relax }{subsection.3.4.3}{}}
\expandafter\gdef \csname page@num.dfbr\endcsname{73}\expandafter\gdef \csname ref@num.dfbr\endcsname{3.4.3}\expandafter\gdef \csname sectionref@name.dfbr\endcsname{subsection.3.4.3}
\newlabel{dfom}{{3.4.3}{74}{Definitions for Set Theory\relax }{subsection.3.4.3}{}}
\expandafter\gdef \csname page@num.dfom\endcsname{74}\expandafter\gdef \csname ref@num.dfom\endcsname{3.4.3}\expandafter\gdef \csname sectionref@name.dfom\endcsname{subsection.3.4.3}
\newlabel{dfopr}{{3.4.3}{76}{Definitions for Set Theory\relax }{subsection.3.4.3}{}}
\expandafter\gdef \csname page@num.dfopr\endcsname{76}\expandafter\gdef \csname ref@num.dfopr\endcsname{3.4.3}\expandafter\gdef \csname sectionref@name.dfopr\endcsname{subsection.3.4.3}
\@writefile{toc}{\contentsline {section}{\numberline {3.5}Tricks of the Trade}{76}{section.3.5}}
\newlabel{tricks}{{3.5}{76}{Tricks of the Trade\relax }{section.3.5}{}}
\expandafter\gdef \csname page@num.tricks\endcsname{76}\expandafter\gdef \csname ref@num.tricks\endcsname{3.5}\expandafter\gdef \csname sectionref@name.tricks\endcsname{section.3.5}
\@writefile{toc}{\contentsline {section}{\numberline {3.6}A Theorem Sampler}{78}{section.3.6}}
\newlabel{sometheorems}{{3.6}{78}{A Theorem Sampler\relax }{section.3.6}{}}
\expandafter\gdef \csname page@num.sometheorems\endcsname{78}\expandafter\gdef \csname ref@num.sometheorems\endcsname{3.6}\expandafter\gdef \csname sectionref@name.sometheorems\endcsname{section.3.6}
\@writefile{toc}{\contentsline {section}{\numberline {3.7}Axioms for Real and Complex Numbers}{80}{section.3.7}}
\newlabel{real}{{3.7}{80}{Axioms for Real and Complex Numbers\relax }{section.3.7}{}}
\expandafter\gdef \csname page@num.real\endcsname{80}\expandafter\gdef \csname ref@num.real\endcsname{3.7}\expandafter\gdef \csname sectionref@name.real\endcsname{section.3.7}
\@writefile{toc}{\contentsline {subsubsection}{Complex Number Axioms in Analysis Texts}{82}{section*.14}}
\citation{Enderton}
\@writefile{toc}{\contentsline {section}{\numberline {3.8}Exploring the Set Theory Database}{83}{section.3.8}}
\newlabel{exploring}{{3.8}{83}{Exploring the Set Theory Database\relax }{section.3.8}{}}
\expandafter\gdef \csname page@num.exploring\endcsname{83}\expandafter\gdef \csname ref@num.exploring\endcsname{3.8}\expandafter\gdef \csname sectionref@name.exploring\endcsname{section.3.8}
\citation{Hamilton}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.8.1}A Note on ``Compact'' Proof Format}{89}{subsection.3.8.1}}
\citation{Russell2}
\@writefile{toc}{\contentsline {chapter}{\numberline {4}The Metamath Language}{91}{chapter.4}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\newlabel{languagespec}{{4}{91}{The Metamath Language\relax }{chapter.4}{}}
\expandafter\gdef \csname page@num.languagespec\endcsname{91}\expandafter\gdef \csname ref@num.languagespec\endcsname{4}\expandafter\gdef \csname sectionref@name.languagespec\endcsname{chapter.4}
\citation{deMillo}
\@writefile{toc}{\contentsline {section}{\numberline {4.1}Specification of the Metamath Language}{92}{section.4.1}}
\newlabel{spec}{{4.1}{92}{Specification of the Metamath Language\relax }{section.4.1}{}}
\expandafter\gdef \csname page@num.spec\endcsname{92}\expandafter\gdef \csname ref@num.spec\endcsname{4.1}\expandafter\gdef \csname sectionref@name.spec\endcsname{section.4.1}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.1.1}Preliminaries}{92}{subsection.4.1.1}}
\newlabel{spec1}{{4.1.1}{92}{Preliminaries\relax }{subsection.4.1.1}{}}
\expandafter\gdef \csname page@num.spec1\endcsname{92}\expandafter\gdef \csname ref@num.spec1\endcsname{4.1.1}\expandafter\gdef \csname sectionref@name.spec1\endcsname{subsection.4.1.1}
\newlabel{spec1chars}{{4.1.1}{92}{Preliminaries\relax }{subsection.4.1.1}{}}
\expandafter\gdef \csname page@num.spec1chars\endcsname{92}\expandafter\gdef \csname ref@num.spec1chars\endcsname{4.1.1}\expandafter\gdef \csname sectionref@name.spec1chars\endcsname{subsection.4.1.1}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.1.2}Preprocessing}{93}{subsection.4.1.2}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.1.3}Basic Syntax}{93}{subsection.4.1.3}}
\newlabel{namespace}{{67}{94}{Basic Syntax\relax }{Hfootnote.67}{}}
\expandafter\gdef \csname page@num.namespace\endcsname{94}\expandafter\gdef \csname ref@num.namespace\endcsname{67}\expandafter\gdef \csname sectionref@name.namespace\endcsname{subsection.4.1.3}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.1.4}Proof Verification}{95}{subsection.4.1.4}}
\newlabel{spec4}{{4.1.4}{95}{Proof Verification\relax }{subsection.4.1.4}{}}
\expandafter\gdef \csname page@num.spec4\endcsname{95}\expandafter\gdef \csname ref@num.spec4\endcsname{4.1.4}\expandafter\gdef \csname sectionref@name.spec4\endcsname{subsection.4.1.4}
\@writefile{toc}{\contentsline {subsubsection}{Verifying Disjoint Variable Restrictions}{95}{section*.15}}
\@writefile{toc}{\contentsline {section}{\numberline {4.2}The Basic Keywords}{96}{section.4.2}}
\newlabel{tut1}{{4.2}{96}{The Basic Keywords\relax }{section.4.2}{}}
\expandafter\gdef \csname page@num.tut1\endcsname{96}\expandafter\gdef \csname ref@num.tut1\endcsname{4.2}\expandafter\gdef \csname sectionref@name.tut1\endcsname{section.4.2}
\@writefile{lot}{\contentsline {table}{\numberline {4.1}{\ignorespaces Summary of the basic Metamath keywords}}{96}{table.4.1}}
\newlabel{basickeywords}{{4.1}{96}{The Basic Keywords\relax }{table.4.1}{}}
\expandafter\gdef \csname page@num.basickeywords\endcsname{96}\expandafter\gdef \csname ref@num.basickeywords\endcsname{4.1}\expandafter\gdef \csname sectionref@name.basickeywords\endcsname{section.4.2}
\@writefile{lot}{\contentsline {table}{\numberline {4.2}{\ignorespaces Auxiliary Metamath keywords}}{97}{table.4.2}}
\newlabel{otherkeywords}{{4.2}{97}{The Basic Keywords\relax }{table.4.2}{}}
\expandafter\gdef \csname page@num.otherkeywords\endcsname{97}\expandafter\gdef \csname ref@num.otherkeywords\endcsname{4.2}\expandafter\gdef \csname sectionref@name.otherkeywords\endcsname{section.4.2}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.2.1}User-Defined Tokens}{97}{subsection.4.2.1}}
\newlabel{dollardollar}{{4.2.1}{97}{User-Defined Tokens\relax }{subsection.4.2.1}{}}
\expandafter\gdef \csname page@num.dollardollar\endcsname{97}\expandafter\gdef \csname ref@num.dollardollar\endcsname{4.2.1}\expandafter\gdef \csname sectionref@name.dollardollar\endcsname{subsection.4.2.1}
\@writefile{toc}{\contentsline {subsubsection}{Math Symbol Tokens}{97}{section*.16}}
\@writefile{toc}{\contentsline {subsubsection}{Label Tokens}{98}{section*.17}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.2.2}Constants and Variables}{99}{subsection.4.2.2}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.2.3}The \texttt  {\$c} and \texttt  {\$v} Declaration Statements}{99}{subsection.4.2.3}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.2.4}The \texttt  {\$d} Statement}{100}{subsection.4.2.4}}
\newlabel{dollard}{{4.2.4}{100}{The \texttt {\$d} Statement\relax }{subsection.4.2.4}{}}
\expandafter\gdef \csname page@num.dollard\endcsname{100}\expandafter\gdef \csname ref@num.dollard\endcsname{4.2.4}\expandafter\gdef \csname sectionref@name.dollard\endcsname{subsection.4.2.4}
\@writefile{toc}{\contentsline {subsubsection}{Compound \texttt  {\$d} Statements}{102}{section*.18}}
\citation{Nemeti}
\citation{Megill}
\citation{Megill}
\newlabel{nodd}{{71}{105}{Compound \texttt {\$d} Statements\relax }{section*.18}{}}
\expandafter\gdef \csname page@num.nodd\endcsname{105}\expandafter\gdef \csname ref@num.nodd\endcsname{71}\expandafter\gdef \csname sectionref@name.nodd\endcsname{subsection.4.2.4}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.2.5}The \texttt  {\$f} and \texttt  {\$e} Statements}{105}{subsection.4.2.5}}
\newlabel{dollaref}{{4.2.5}{105}{The \texttt {\$f} and \texttt {\$e} Statements\relax }{subsection.4.2.5}{}}
\expandafter\gdef \csname page@num.dollaref\endcsname{105}\expandafter\gdef \csname ref@num.dollaref\endcsname{4.2.5}\expandafter\gdef \csname sectionref@name.dollaref\endcsname{subsection.4.2.5}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.2.6}Assertions (\texttt  {\$a} and \texttt  {\$p} Statements)}{106}{subsection.4.2.6}}
\@writefile{toc}{\contentsline {subsubsection}{The \texttt  {\$a} Statement}{107}{section*.19}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.2.7}Frames}{108}{subsection.4.2.7}}
\newlabel{frames}{{4.2.7}{108}{Frames\relax }{subsection.4.2.7}{}}
\expandafter\gdef \csname page@num.frames\endcsname{108}\expandafter\gdef \csname ref@num.frames\endcsname{4.2.7}\expandafter\gdef \csname sectionref@name.frames\endcsname{subsection.4.2.7}
\newlabel{framelist}{{4.2.7}{111}{Frames\relax }{Item.4}{}}
\expandafter\gdef \csname page@num.framelist\endcsname{111}\expandafter\gdef \csname ref@num.framelist\endcsname{4.2.7}\expandafter\gdef \csname sectionref@name.framelist\endcsname{subsection.4.2.7}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.2.8}Scoping Statements (\texttt  {\$\{} and \texttt  {\$\}})}{112}{subsection.4.2.8}}
\newlabel{scoping}{{4.2.8}{112}{Scoping Statements (\texttt {\$\{} and \texttt {\$\}})\relax }{subsection.4.2.8}{}}
\expandafter\gdef \csname page@num.scoping\endcsname{112}\expandafter\gdef \csname ref@num.scoping\endcsname{4.2.8}\expandafter\gdef \csname sectionref@name.scoping\endcsname{subsection.4.2.8}
\@writefile{toc}{\contentsline {subsubsection}{Redeclaration of Math Symbols}{113}{section*.20}}
\newlabel{redeclaration}{{76}{113}{Redeclaration of Math Symbols\relax }{section*.20}{}}
\expandafter\gdef \csname page@num.redeclaration\endcsname{113}\expandafter\gdef \csname ref@num.redeclaration\endcsname{76}\expandafter\gdef \csname sectionref@name.redeclaration\endcsname{subsection.4.2.8}
\@writefile{toc}{\contentsline {subsubsection}{Frames Revisited}{114}{section*.21}}
\newlabel{frameconvert}{{77}{114}{Frames Revisited\relax }{section*.21}{}}
\expandafter\gdef \csname page@num.frameconvert\endcsname{114}\expandafter\gdef \csname ref@num.frameconvert\endcsname{77}\expandafter\gdef \csname sectionref@name.frameconvert\endcsname{subsection.4.2.8}
\@writefile{toc}{\contentsline {section}{\numberline {4.3}The Anatomy of a Proof}{114}{section.4.3}}
\newlabel{proof}{{4.3}{114}{The Anatomy of a Proof\relax }{section.4.3}{}}
\expandafter\gdef \csname page@num.proof\endcsname{114}\expandafter\gdef \csname ref@num.proof\endcsname{4.3}\expandafter\gdef \csname sectionref@name.proof\endcsname{section.4.3}
\newlabel{redeclarationf}{{15}{114}{Redeclaration of Math Symbols\relax }{Hfootnote.77}{}}
\expandafter\gdef \csname page@num.redeclarationf\endcsname{114}\expandafter\gdef \csname ref@num.redeclarationf\endcsname{15}\expandafter\gdef \csname sectionref@name.redeclarationf\endcsname{subsection.4.2.8}
\newlabel{treeproof}{{79}{117}{The Anatomy of a Proof\relax }{Hfootnote.79}{}}
\expandafter\gdef \csname page@num.treeproof\endcsname{117}\expandafter\gdef \csname ref@num.treeproof\endcsname{79}\expandafter\gdef \csname sectionref@name.treeproof\endcsname{section.4.3}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.3.1}The Concept of Unification}{118}{subsection.4.3.1}}
\newlabel{unify}{{4.3.1}{118}{The Concept of Unification\relax }{subsection.4.3.1}{}}
\expandafter\gdef \csname page@num.unify\endcsname{118}\expandafter\gdef \csname ref@num.unify\endcsname{4.3.1}\expandafter\gdef \csname sectionref@name.unify\endcsname{subsection.4.3.1}
\@writefile{toc}{\contentsline {section}{\numberline {4.4}Extensions to the Metamath Language}{119}{section.4.4}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.4.1}Comments in the Metamath Language}{119}{subsection.4.4.1}}
\newlabel{comments}{{4.4.1}{119}{Comments in the Metamath Language\relax }{subsection.4.4.1}{}}
\expandafter\gdef \csname page@num.comments\endcsname{119}\expandafter\gdef \csname ref@num.comments\endcsname{4.4.1}\expandafter\gdef \csname sectionref@name.comments\endcsname{subsection.4.4.1}
\@writefile{toc}{\contentsline {subsubsection}{Math Symbols and Labels Inside Comments}{119}{section*.22}}
\newlabel{mathcomments}{{80}{119}{Math Symbols and Labels Inside Comments\relax }{section*.22}{}}
\expandafter\gdef \csname page@num.mathcomments\endcsname{119}\expandafter\gdef \csname ref@num.mathcomments\endcsname{80}\expandafter\gdef \csname sectionref@name.mathcomments\endcsname{subsection.4.4.1}
\@writefile{toc}{\contentsline {subsubsection}{Math Symbols In Comments}{120}{section*.23}}
\@writefile{toc}{\contentsline {subsubsection}{Label References in Comments}{121}{section*.24}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.4.2}Comment Markup Notation for HTML}{121}{subsection.4.4.2}}
\newlabel{htmlmkup}{{4.4.2}{121}{Comment Markup Notation for HTML\relax }{subsection.4.4.2}{}}
\expandafter\gdef \csname page@num.htmlmkup\endcsname{121}\expandafter\gdef \csname ref@num.htmlmkup\endcsname{4.4.2}\expandafter\gdef \csname sectionref@name.htmlmkup\endcsname{subsection.4.4.2}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.4.3}Including Other Files in a Metamath Source File}{122}{subsection.4.4.3}}
\newlabel{include}{{4.4.3}{122}{Including Other Files in a Metamath Source File\relax }{subsection.4.4.3}{}}
\expandafter\gdef \csname page@num.include\endcsname{122}\expandafter\gdef \csname ref@num.include\endcsname{4.4.3}\expandafter\gdef \csname sectionref@name.include\endcsname{subsection.4.4.3}
\newlabel{includef}{{81}{123}{Including Other Files in a Metamath Source File\relax }{Hfootnote.81}{}}
\expandafter\gdef \csname page@num.includef\endcsname{123}\expandafter\gdef \csname ref@num.includef\endcsname{81}\expandafter\gdef \csname sectionref@name.includef\endcsname{subsection.4.4.3}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.4.4}Compressed Proof Format}{123}{subsection.4.4.4}}
\newlabel{compressed1}{{4.4.4}{123}{Compressed Proof Format\relax }{subsection.4.4.4}{}}
\expandafter\gdef \csname page@num.compressed1\endcsname{123}\expandafter\gdef \csname ref@num.compressed1\endcsname{4.4.4}\expandafter\gdef \csname sectionref@name.compressed1\endcsname{subsection.4.4.4}
\citation{Behnke}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.4.5}Specifying Unknown Proofs or Subproofs}{124}{subsection.4.4.5}}
\newlabel{unknown}{{4.4.5}{124}{Specifying Unknown Proofs or Subproofs\relax }{subsection.4.4.5}{}}
\expandafter\gdef \csname page@num.unknown\endcsname{124}\expandafter\gdef \csname ref@num.unknown\endcsname{4.4.5}\expandafter\gdef \csname sectionref@name.unknown\endcsname{subsection.4.4.5}
\citation{Nemesszeghy}
\citation{Lejewski}
\@writefile{toc}{\contentsline {section}{\numberline {4.5}Appendix: Axioms vs.\ Definitions}{125}{section.4.5}}
\newlabel{definitions}{{4.5}{125}{Appendix: Axioms vs.\ Definitions\relax }{section.4.5}{}}
\expandafter\gdef \csname page@num.definitions\endcsname{125}\expandafter\gdef \csname ref@num.definitions\endcsname{4.5}\expandafter\gdef \csname sectionref@name.definitions\endcsname{section.4.5}
\citation{Goodstein}
\citation{Robinsont}
\citation{Quine}
\@writefile{toc}{\contentsline {chapter}{\numberline {5}The Metamath Program}{129}{chapter.5}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\newlabel{commands}{{5}{129}{The Metamath Program\relax }{chapter.5}{}}
\expandafter\gdef \csname page@num.commands\endcsname{129}\expandafter\gdef \csname ref@num.commands\endcsname{5}\expandafter\gdef \csname sectionref@name.commands\endcsname{chapter.5}
\@writefile{toc}{\contentsline {section}{\numberline {5.1}Invoking Metamath}{129}{section.5.1}}
\@writefile{toc}{\contentsline {section}{\numberline {5.2}Controlling Metamath}{130}{section.5.2}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2.1}\texttt  {exit} Command}{131}{subsection.5.2.1}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2.2}\texttt  {open log} Command}{131}{subsection.5.2.2}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2.3}\texttt  {close log} Command}{132}{subsection.5.2.3}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2.4}\texttt  {submit} Command}{132}{subsection.5.2.4}}
\newlabel{sbmt}{{5.2.4}{132}{\texttt {submit} Command\relax }{subsection.5.2.4}{}}
\expandafter\gdef \csname page@num.sbmt\endcsname{132}\expandafter\gdef \csname ref@num.sbmt\endcsname{5.2.4}\expandafter\gdef \csname sectionref@name.sbmt\endcsname{subsection.5.2.4}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2.5}\texttt  {erase} Command}{132}{subsection.5.2.5}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2.6}\texttt  {set echo} Command}{132}{subsection.5.2.6}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2.7}\texttt  {set scroll} Command}{132}{subsection.5.2.7}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2.8}\texttt  {set width} Command}{132}{subsection.5.2.8}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2.9}\texttt  {set height} Command}{133}{subsection.5.2.9}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2.10}\texttt  {beep} Command}{133}{subsection.5.2.10}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2.11}\texttt  {more} Command}{133}{subsection.5.2.11}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2.12}Operating System Commands}{133}{subsection.5.2.12}}
\newlabel{oscmd}{{5.2.12}{133}{Operating System Commands\relax }{subsection.5.2.12}{}}
\expandafter\gdef \csname page@num.oscmd\endcsname{133}\expandafter\gdef \csname ref@num.oscmd\endcsname{5.2.12}\expandafter\gdef \csname sectionref@name.oscmd\endcsname{subsection.5.2.12}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2.13}Size Limitations in Metamath}{134}{subsection.5.2.13}}
\@writefile{toc}{\contentsline {section}{\numberline {5.3}Reading and Writing Files}{134}{section.5.3}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.3.1}\texttt  {read} Command}{134}{subsection.5.3.1}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.3.2}\texttt  {write source} Command}{134}{subsection.5.3.2}}
\@writefile{toc}{\contentsline {section}{\numberline {5.4}Showing Status and Statements}{135}{section.5.4}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.4.1}\texttt  {show settings} Command}{135}{subsection.5.4.1}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.4.2}\texttt  {show memory} Command}{135}{subsection.5.4.2}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.4.3}\texttt  {show labels} Command}{135}{subsection.5.4.3}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.4.4}\texttt  {show statement} Command}{135}{subsection.5.4.4}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.4.5}\texttt  {search} Command}{136}{subsection.5.4.5}}
\@writefile{toc}{\contentsline {section}{\numberline {5.5}Displaying and Verifying Proofs}{136}{section.5.5}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.5.1}\texttt  {show proof} Command}{136}{subsection.5.5.1}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.5.2}\texttt  {show usage} Command}{137}{subsection.5.5.2}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.5.3}\texttt  {show trace\_back} Command}{138}{subsection.5.5.3}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.5.4}\texttt  {verify proof} Command}{138}{subsection.5.5.4}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.5.5}\texttt  {save proof} Command}{138}{subsection.5.5.5}}
\@writefile{toc}{\contentsline {section}{\numberline {5.6}Creating Proofs}{139}{section.5.6}}
\newlabel{pfcommands}{{5.6}{139}{Creating Proofs\relax }{section.5.6}{}}
\expandafter\gdef \csname page@num.pfcommands\endcsname{139}\expandafter\gdef \csname ref@num.pfcommands\endcsname{5.6}\expandafter\gdef \csname sectionref@name.pfcommands\endcsname{section.5.6}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.6.1}\texttt  {prove} Command}{141}{subsection.5.6.1}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.6.2}\texttt  {set unification\_timeout} Command}{141}{subsection.5.6.2}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.6.3}\texttt  {set empty\_substitution} Command}{142}{subsection.5.6.3}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.6.4}\texttt  {set search\_limit} Command}{142}{subsection.5.6.4}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.6.5}\texttt  {show new\_proof} Command}{142}{subsection.5.6.5}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.6.6}\texttt  {assign} Command}{143}{subsection.5.6.6}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.6.7}\texttt  {match} Command}{143}{subsection.5.6.7}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.6.8}\texttt  {let} Command}{143}{subsection.5.6.8}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.6.9}\texttt  {unify} Command}{144}{subsection.5.6.9}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.6.10}\texttt  {initialize} Command}{145}{subsection.5.6.10}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.6.11}\texttt  {delete} Command}{145}{subsection.5.6.11}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.6.12}\texttt  {improve} Command}{145}{subsection.5.6.12}}
\newlabel{improve}{{5.6.12}{145}{\texttt {improve} Command\relax }{subsection.5.6.12}{}}
\expandafter\gdef \csname page@num.improve\endcsname{145}\expandafter\gdef \csname ref@num.improve\endcsname{5.6.12}\expandafter\gdef \csname sectionref@name.improve\endcsname{subsection.5.6.12}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.6.13}\texttt  {save new\_proof} Command}{146}{subsection.5.6.13}}
\@writefile{toc}{\contentsline {section}{\numberline {5.7}Creating \LaTeX  \ Output}{147}{section.5.7}}
\newlabel{texout}{{5.7}{147}{Creating \LaTeX \ Output\relax }{section.5.7}{}}
\expandafter\gdef \csname page@num.texout\endcsname{147}\expandafter\gdef \csname ref@num.texout\endcsname{5.7}\expandafter\gdef \csname sectionref@name.texout\endcsname{section.5.7}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.7.1}\texttt  {open tex} Command}{147}{subsection.5.7.1}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.7.2}\texttt  {close tex} Command}{147}{subsection.5.7.2}}
\@writefile{toc}{\contentsline {section}{\numberline {5.8}Creating HTML Output}{148}{section.5.8}}
\newlabel{htmlout}{{5.8}{148}{Creating HTML Output\relax }{section.5.8}{}}
\expandafter\gdef \csname page@num.htmlout\endcsname{148}\expandafter\gdef \csname ref@num.htmlout\endcsname{5.8}\expandafter\gdef \csname sectionref@name.htmlout\endcsname{section.5.8}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.8.1}The Typesetting Comment (\texttt  {\$t})}{148}{subsection.5.8.1}}
\newlabel{tcomment}{{5.8.1}{148}{The Typesetting Comment (\texttt {\$t})\relax }{subsection.5.8.1}{}}
\expandafter\gdef \csname page@num.tcomment\endcsname{148}\expandafter\gdef \csname ref@num.tcomment\endcsname{5.8.1}\expandafter\gdef \csname sectionref@name.tcomment\endcsname{subsection.5.8.1}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.8.2}\texttt  {write theorem\_list} Command}{150}{subsection.5.8.2}}
\newlabel{wrbib}{{5.8.3}{151}{\texttt {write bibliography}\label {wrbib} Command\relax }{subsection.5.8.3}{}}
\expandafter\gdef \csname page@num.wrbib\endcsname{151}\expandafter\gdef \csname ref@num.wrbib\endcsname{5.8.3}\expandafter\gdef \csname sectionref@name.wrbib\endcsname{subsection.5.8.3}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.8.3}\texttt  {write bibliography} Command}{151}{subsection.5.8.3}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.8.4}\texttt  {write recent\_additions} Command}{151}{subsection.5.8.4}}
\@writefile{toc}{\contentsline {section}{\numberline {5.9}Text File Utilities}{151}{section.5.9}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.9.1}\texttt  {tools} Command}{151}{subsection.5.9.1}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.9.2}\texttt  {help} Command (in \texttt  {tools})}{152}{subsection.5.9.2}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.9.3}Using \texttt  {tools} to Build Metamath \texttt  {submit} Scripts}{152}{subsection.5.9.3}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.9.4}Example of a \texttt  {tools} Session}{153}{subsection.5.9.4}}
\@writefile{toc}{\contentsline {chapter}{\numberline {A}Math Symbol Tokens for Set Theory}{155}{appendix.A}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\newlabel{ASCII}{{A}{155}{Math Symbol Tokens for Set Theory\relax }{appendix.A}{}}
\expandafter\gdef \csname page@num.ASCII\endcsname{155}\expandafter\gdef \csname ref@num.ASCII\endcsname{A}\expandafter\gdef \csname sectionref@name.ASCII\endcsname{chapter.A}
\@writefile{toc}{\contentsline {chapter}{\numberline {B}Compressed Proofs}{159}{appendix.B}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\newlabel{compressed}{{B}{159}{Compressed Proofs\relax }{appendix.B}{}}
\expandafter\gdef \csname page@num.compressed\endcsname{159}\expandafter\gdef \csname ref@num.compressed\endcsname{B}\expandafter\gdef \csname sectionref@name.compressed\endcsname{chapter.B}
\citation{Campbell}
\citation{Munkres}
\citation{Tarski1965}
\@writefile{toc}{\contentsline {chapter}{\numberline {C}Metamath's Formal System}{161}{appendix.C}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\newlabel{formalspec}{{C}{161}{Metamath's Formal System\relax }{appendix.C}{}}
\expandafter\gdef \csname page@num.formalspec\endcsname{161}\expandafter\gdef \csname ref@num.formalspec\endcsname{C}\expandafter\gdef \csname sectionref@name.formalspec\endcsname{chapter.C}
\@writefile{toc}{\contentsline {section}{\numberline {C.1}Introduction}{161}{section.C.1}}
\@writefile{toc}{\contentsline {section}{\numberline {C.2}The Formal Description}{162}{section.C.2}}
\@writefile{toc}{\contentsline {subsection}{\numberline {C.2.1}Preliminaries}{162}{Hfootnote.86}}
\@writefile{toc}{\contentsline {subsection}{\numberline {C.2.2}Constants, Variables, and Expressions}{162}{subsection.C.2.2}}
\@writefile{toc}{\contentsline {subsection}{\numberline {C.2.3}Substitution}{163}{subsection.C.2.3}}
\@writefile{toc}{\contentsline {subsection}{\numberline {C.2.4}Statements}{163}{subsection.C.2.4}}
\citation{Nemeti}
\@writefile{toc}{\contentsline {subsection}{\numberline {C.2.5}Formal Systems}{165}{subsection.C.2.5}}
\@writefile{toc}{\contentsline {section}{\numberline {C.3}Examples of Formal Systems}{166}{section.C.3}}
\newlabel{exampleref}{{C.3}{166}{Examples of Formal Systems\relax }{section.C.3}{}}
\expandafter\gdef \csname page@num.exampleref\endcsname{166}\expandafter\gdef \csname ref@num.exampleref\endcsname{C.3}\expandafter\gdef \csname sectionref@name.exampleref\endcsname{section.C.3}
\@writefile{toc}{\contentsline {subsection}{\numberline {C.3.1}Example\nobreakspace  {}1---Propositional Calculus}{166}{subsection.C.3.1}}
\citation{Tarski1965}
\citation{Tarski1965}
\citation{Tarski1965}
\@writefile{toc}{\contentsline {subsection}{\numberline {C.3.2}Example\nobreakspace  {}2---Predicate Calculus with Equality}{168}{subsection.C.3.2}}
\citation{Tarski1965}
\@writefile{toc}{\contentsline {subsection}{\numberline {C.3.3}Free Variables and Proper Substitution}{170}{subsection.C.3.3}}
\newlabel{effectivelybound}{{C.3.3}{170}{Free Variables and Proper Substitution\relax }{subsection.C.3.3}{}}
\expandafter\gdef \csname page@num.effectivelybound\endcsname{170}\expandafter\gdef \csname ref@num.effectivelybound\endcsname{C.3.3}\expandafter\gdef \csname sectionref@name.effectivelybound\endcsname{subsection.C.3.3}
\@writefile{toc}{\contentsline {subsection}{\numberline {C.3.4}Metalogical Completeness}{170}{subsection.C.3.4}}
\citation{Kalish}
\citation{Megill}
\citation{Megill}
\@writefile{toc}{\contentsline {subsection}{\numberline {C.3.5}Example\nobreakspace  {}3---Metalogically Complete Predicate Calculus with Equality}{171}{subsection.C.3.5}}
\@writefile{toc}{\contentsline {subsection}{\numberline {C.3.6}Example\nobreakspace  {}4---Adding Definitions}{172}{subsection.C.3.6}}
\@writefile{toc}{\contentsline {subsection}{\numberline {C.3.7}Example\nobreakspace  {}5---ZFC Set Theory}{173}{subsection.C.3.7}}
\citation{Takeuti}
\citation{Quine}
\@writefile{toc}{\contentsline {subsection}{\numberline {C.3.8}Example\nobreakspace  {}6---Class Notation in Set Theory}{174}{subsection.C.3.8}}
\newlabel{class}{{C.3.8}{174}{Example~6---Class Notation in Set Theory\relax }{subsection.C.3.8}{}}
\expandafter\gdef \csname page@num.class\endcsname{174}\expandafter\gdef \csname ref@num.class\endcsname{C.3.8}\expandafter\gdef \csname sectionref@name.class\endcsname{subsection.C.3.8}
\@writefile{toc}{\contentsline {section}{\numberline {C.4}Metamath as a Formal System}{175}{section.C.4}}
\newlabel{theorymm}{{C.4}{175}{Metamath as a Formal System\relax }{section.C.4}{}}
\expandafter\gdef \csname page@num.theorymm\endcsname{175}\expandafter\gdef \csname ref@num.theorymm\endcsname{C.4}\expandafter\gdef \csname sectionref@name.theorymm\endcsname{section.C.4}
\@writefile{toc}{\contentsline {chapter}{\numberline {D}The MIU System}{177}{appendix.D}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\newlabel{MIU}{{D}{177}{The MIU System\relax }{appendix.D}{}}
\expandafter\gdef \csname page@num.MIU\endcsname{177}\expandafter\gdef \csname ref@num.MIU\endcsname{D}\expandafter\gdef \csname sectionref@name.MIU\endcsname{chapter.D}
\citation{Hofstadter}
\bibdata{metamath}
\bibcite{Albers}{1}
\bibcite{Anderson}{2}
\bibcite{Barrow}{3}
\bibcite{Behnke}{4}
\bibcite{Bell}{5}
\bibcite{Blass}{6}
\bibcite{Bledsoe}{7}
\bibcite{Boolos}{8}
\bibcite{Campbell}{9}
\bibcite{Chou}{10}
\@writefile{toc}{\contentsline {chapter}{Bibliography}{181}{section*.25}}
\bibcite{Courant}{11}
\bibcite{Curry}{12}
\bibcite{Davis}{13}
\bibcite{deMillo}{14}
\bibcite{Edwards}{15}
\bibcite{Enderton}{16}
\bibcite{Goodstein}{17}
\bibcite{Guillen}{18}
\bibcite{Hamilton}{19}
\bibcite{Harrison}{20}
\bibcite{Harrison-thesis}{21}
\bibcite{Herrlich}{22}
\bibcite{Hindley}{23}
\bibcite{Hofstadter}{24}
\bibcite{Kalish}{25}
\bibcite{Kalman}{26}
\bibcite{Kline}{27}
\bibcite{Klinel}{28}
\bibcite{Kramer}{29}
\bibcite{Landau}{30}
\bibcite{Leblanc}{31}
\bibcite{Lejewski}{32}
\bibcite{Mathias}{33}
\bibcite{Megill}{34}
\bibcite{MegillBunder}{35}
\bibcite{Mendelson}{36}
\bibcite{CAMeredith}{37}
\bibcite{Meredith}{38}
\bibcite{Monks}{39}
\bibcite{Moore}{40}
\bibcite{Munkres}{41}
\bibcite{Nemesszeghy}{42}
\bibcite{Nemeti}{43}
\bibcite{Pavicic}{44}
\bibcite{Penrose}{45}
\bibcite{PetersonI}{46}
\bibcite{Peterson}{47}
\bibcite{Quine}{48}
\bibcite{Robinson}{49}
\bibcite{Robinsont}{50}
\bibcite{Rucker}{51}
\bibcite{Russell2}{52}
\bibcite{Russell}{53}
\bibcite{Shoenfield}{54}
\bibcite{Solow}{55}
\bibcite{Stark}{56}
\bibcite{Swart}{57}
\bibcite{Takeuti}{58}
\bibcite{Tarski}{59}
\bibcite{Tarski1965}{60}
\bibcite{Tymoczko}{61}
\bibcite{Wang}{62}
\bibcite{Whitehead}{63}
\bibcite{PM}{64}
\bibcite{Wolfram}{65}
\bibcite{Wos}{66}
\@writefile{toc}{\contentsline {chapter}{Index}{187}{section*.27}}