\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{}
\@writefile{toc}{\contentsline {subsubsection}{Formalism}{xii}{section*.6}}
\citation{Davis}
\@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}{xiii}{section*.9}}
\@writefile{toc}{\contentsline {subsubsection}{Note Added January 6, 2002}{xiii}{section*.10}}
\newlabel{note2002}{{2}{xiii}{Note Added January 6, 2002\relax }{section*.10}{}}
\expandafter\gdef \csname page@num.note2002\endcsname{xiii}\expandafter\gdef \csname ref@num.note2002\endcsname{2}\expandafter\gdef \csname sectionref@name.note2002\endcsname{}
\@writefile{toc}{\contentsline {subsubsection}{Note Added May 20, 2003}{xiv}{section*.11}}
\newlabel{note2003}{{2}{xiv}{Note Added May 20, 2003\relax }{section*.11}{}}
\expandafter\gdef \csname page@num.note2003\endcsname{xiv}\expandafter\gdef \csname ref@num.note2003\endcsname{2}\expandafter\gdef \csname sectionref@name.note2003\endcsname{}
\@writefile{toc}{\contentsline {subsubsection}{Note Added November 20, 2003}{xv}{section*.12}}
\newlabel{note2003b}{{3}{xv}{Note Added November 20, 2003\relax }{section*.12}{}}
\expandafter\gdef \csname page@num.note2003b\endcsname{xv}\expandafter\gdef \csname ref@num.note2003b\endcsname{3}\expandafter\gdef \csname sectionref@name.note2003b\endcsname{}
\@writefile{toc}{\contentsline {subsubsection}{Note Added April 2, 2004}{xv}{section*.13}}
\newlabel{note2004}{{3}{xv}{Note Added April 2, 2004\relax }{section*.13}{}}
\expandafter\gdef \csname page@num.note2004\endcsname{xv}\expandafter\gdef \csname ref@num.note2004\endcsname{3}\expandafter\gdef \csname sectionref@name.note2004\endcsname{}
\@writefile{toc}{\contentsline {subsubsection}{Note Added May 22, 2004}{xv}{section*.14}}
\newlabel{note2004b}{{3}{xv}{Note Added May 22, 2004\relax }{section*.14}{}}
\expandafter\gdef \csname page@num.note2004b\endcsname{xv}\expandafter\gdef \csname ref@num.note2004b\endcsname{3}\expandafter\gdef \csname sectionref@name.note2004b\endcsname{}
\@writefile{toc}{\contentsline {subsubsection}{Note Added September 14, 2004}{xv}{section*.15}}
\newlabel{note2004c}{{3}{xv}{Note Added September 14, 2004\relax }{section*.15}{}}
\expandafter\gdef \csname page@num.note2004c\endcsname{xv}\expandafter\gdef \csname ref@num.note2004c\endcsname{3}\expandafter\gdef \csname sectionref@name.note2004c\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}
\citation{Landau}
\@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}}
\@writefile{toc}{\contentsline {subsubsection}{A Non-Mathematician's Quest for Truth}{4}{section*.16}}
\citation{Guillen}
\citation{Rucker}
\citation{Solow}
\citation{Davis}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.1.2}Mathematics and the Non-Specialist}{11}{subsection.1.1.2}}
\citation{Edwards}
\citation{Davis}
\citation{Wang}
\citation{deMillo}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.1.3}An Impossible Dream?}{13}{subsection.1.1.3}}
\newlabel{dream}{{1.1.3}{13}{An Impossible Dream?\relax }{subsection.1.1.3}{}}
\expandafter\gdef \csname page@num.dream\endcsname{13}\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}{14}{An Impossible Dream?\relax }{Hfootnote.23}{}}
\expandafter\gdef \csname page@num.bourbaki\endcsname{14}\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}{14}{subsection.1.1.4}}
\citation{deMillo}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.1.5}Simplicity}{15}{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}{17}{subsection.1.1.6}}
\citation{Harrison}
\citation{Albers}
\@writefile{toc}{\contentsline {section}{\numberline {1.2}Computers and Mathematicians}{19}{section.1.2}}
\citation{Tymoczko}
\citation{Swart}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.2.1}Trusting the Computer}{20}{subsection.1.2.1}}
\citation{deMillo}
\citation{deMillo}
\citation{Stark}
\citation{Kramer}
\citation{Davis}
\citation{Enderton}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.2.2}Trusting the Mathematician}{21}{subsection.1.2.2}}
\citation{Enderton}
\citation{Courant}
\citation{Swart}
\citation{Davis}
\citation{PetersonI}
\citation{Wolfram}
\citation{Harrison-thesis}
\@writefile{toc}{\contentsline {section}{\numberline {1.3}The Use of Computers in Mathematics}{23}{section.1.3}}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.3.1}Computer Algebra Systems}{23}{subsection.1.3.1}}
\citation{Tarski}
\citation{Chou}
\citation{Penrose}
\citation{Robinson}
\citation{Wos}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.3.2}Automated Theorem Provers}{24}{subsection.1.3.2}}
\newlabel{theoremprovers}{{1.3.2}{24}{Automated Theorem Provers\relax }{subsection.1.3.2}{}}
\expandafter\gdef \csname page@num.theoremprovers\endcsname{24}\expandafter\gdef \csname ref@num.theoremprovers\endcsname{1.3.2}\expandafter\gdef \csname sectionref@name.theoremprovers\endcsname{subsection.1.3.2}
\citation{Wos}
\citation{Megill}
\citation{Bledsoe}
\citation{Harrison}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.3.3}Proof Verifiers}{26}{subsection.1.3.3}}
\newlabel{proofverifiers}{{1.3.3}{26}{Proof Verifiers\relax }{subsection.1.3.3}{}}
\expandafter\gdef \csname page@num.proofverifiers\endcsname{26}\expandafter\gdef \csname ref@num.proofverifiers\endcsname{1.3.3}\expandafter\gdef \csname sectionref@name.proofverifiers\endcsname{subsection.1.3.3}
\@writefile{toc}{\contentsline {section}{\numberline {1.4}Mathematics and Metamath}{27}{section.1.4}}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.4.1}Standard Mathematics}{27}{subsection.1.4.1}}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.4.2}Other Formal Systems}{27}{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}{28}{subsection.1.4.3}}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.4.4}A History of the Approach Behind Metamath}{28}{subsection.1.4.4}}
\citation{Hindley}
\citation{Kalman}
\citation{Meredith}
\citation{Peterson}
\citation{Megill}
\citation{Robinson}
\citation{Herrlich}
\citation{Blass}
\citation{Megill}
\citation{Monks}
\citation{Leblanc}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.4.5}Metamath and First-Order Logic}{29}{subsection.1.4.5}}
\newlabel{categoryth}{{1.4.5}{29}{Metamath and First-Order Logic\relax }{subsection.1.4.5}{}}
\expandafter\gdef \csname page@num.categoryth\endcsname{29}\expandafter\gdef \csname ref@num.categoryth\endcsname{1.4.5}\expandafter\gdef \csname sectionref@name.categoryth\endcsname{subsection.1.4.5}
\@writefile{toc}{\contentsline {chapter}{\numberline {2}Using the Metamath Program}{31}{chapter.2}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\newlabel{using}{{2}{31}{Using the Metamath Program\relax }{chapter.2}{}}
\expandafter\gdef \csname page@num.using\endcsname{31}\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}{31}{section.2.1}}
\citation{Mendelson}
\citation{Mendelson}
\citation{Mendelson}
\@writefile{toc}{\contentsline {section}{\numberline {2.2}Your First Formal System}{32}{section.2.2}}
\newlabel{start}{{2.2}{32}{Your First Formal System\relax }{section.2.2}{}}
\expandafter\gdef \csname page@num.start\endcsname{32}\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}{32}{subsection.2.2.1}}
\newlabel{startf}{{2.2.1}{32}{From Nothing to Zero\relax }{subsection.2.2.1}{}}
\expandafter\gdef \csname page@num.startf\endcsname{32}\expandafter\gdef \csname ref@num.startf\endcsname{2.2.1}\expandafter\gdef \csname sectionref@name.startf\endcsname{subsection.2.2.1}
\newlabel{zeroproof}{{49}{33}{From Nothing to Zero\relax }{equation.A2}{}}
\expandafter\gdef \csname page@num.zeroproof\endcsname{33}\expandafter\gdef \csname ref@num.zeroproof\endcsname{49}\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}{34}{subsection.2.2.2}}
\newlabel{convert}{{2.2.2}{34}{Converting It to Metamath\relax }{subsection.2.2.2}{}}
\expandafter\gdef \csname page@num.convert\endcsname{34}\expandafter\gdef \csname ref@num.convert\endcsname{2.2.2}\expandafter\gdef \csname sectionref@name.convert\endcsname{subsection.2.2.2}
\newlabel{demo0}{{50}{35}{Converting It to Metamath\relax }{Hfootnote.50}{}}
\expandafter\gdef \csname page@num.demo0\endcsname{35}\expandafter\gdef \csname ref@num.demo0\endcsname{50}\expandafter\gdef \csname sectionref@name.demo0\endcsname{subsection.2.2.2}
\@writefile{toc}{\contentsline {section}{\numberline {2.3}A Trial Run}{38}{section.2.3}}
\newlabel{trialrun}{{2.3}{38}{A Trial Run\relax }{section.2.3}{}}
\expandafter\gdef \csname page@num.trialrun\endcsname{38}\expandafter\gdef \csname ref@num.trialrun\endcsname{2.3}\expandafter\gdef \csname sectionref@name.trialrun\endcsname{section.2.3}
\newlabel{demoproof}{{54}{42}{A Trial Run\relax }{Hfootnote.54}{}}
\expandafter\gdef \csname page@num.demoproof\endcsname{42}\expandafter\gdef \csname ref@num.demoproof\endcsname{54}\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}{43}{subsection.2.3.1}}
\@writefile{toc}{\contentsline {section}{\numberline {2.4}Your First Proof}{44}{section.2.4}}
\@writefile{toc}{\contentsline {section}{\numberline {2.5}A Note About Editing a Data\discretionary {-}{}{}base File}{49}{section.2.5}}
\citation{Barrow}
\@writefile{toc}{\contentsline {chapter}{\numberline {3}Abstract Mathematics Revealed}{51}{chapter.3}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\newlabel{fol}{{3}{51}{Abstract Mathematics Revealed\relax }{chapter.3}{}}
\expandafter\gdef \csname page@num.fol\endcsname{51}\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}{51}{section.3.1}}
\newlabel{logicandsettheory}{{3.1}{51}{Logic and Set Theory\relax }{section.3.1}{}}
\expandafter\gdef \csname page@num.logicandsettheory\endcsname{51}\expandafter\gdef \csname ref@num.logicandsettheory\endcsname{3.1}\expandafter\gdef \csname sectionref@name.logicandsettheory\endcsname{section.3.1}
\newlabel{expandom}{{3.1}{52}{Logic and Set Theory\relax }{Hfootnote.56}{}}
\expandafter\gdef \csname page@num.expandom\endcsname{52}\expandafter\gdef \csname ref@num.expandom\endcsname{3.1}\expandafter\gdef \csname sectionref@name.expandom\endcsname{section.3.1}
\@writefile{toc}{\contentsline {section}{\numberline {3.2}The Axioms for All of Mathematics}{53}{section.3.2}}
\citation{CAMeredith}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.2.1}Propositional Calculus}{54}{subsection.3.2.1}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.2.2}Predicate Calculus}{55}{subsection.3.2.2}}
\citation{Hamilton}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.2.3}Equality}{56}{subsection.3.2.3}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.2.4}Set Theory}{57}{subsection.3.2.4}}
\@writefile{toc}{\contentsline {section}{\numberline {3.3}The Axioms in the Metamath Language}{58}{section.3.3}}
\newlabel{metaaxioms}{{3.3}{58}{The Axioms in the Metamath Language\relax }{section.3.3}{}}
\expandafter\gdef \csname page@num.metaaxioms\endcsname{58}\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}{59}{subsection.3.3.1}}
\newlabel{propcalc}{{3.3.1}{59}{Propositional Calculus\relax }{subsection.3.3.1}{}}
\expandafter\gdef \csname page@num.propcalc\endcsname{59}\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}{59}{Propositional Calculus\relax }{subsection.3.3.1}{}}
\expandafter\gdef \csname page@num.ax1\endcsname{59}\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}{59}{subsection.3.3.2}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.3.3}Equality and Substitution}{60}{subsection.3.3.3}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.3.4}Set Theory}{60}{subsection.3.3.4}}
\newlabel{mmsettheoryaxioms}{{3.3.4}{60}{Set Theory\relax }{subsection.3.3.4}{}}
\expandafter\gdef \csname page@num.mmsettheoryaxioms\endcsname{60}\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}{61}{subsection.3.3.5}}
\@writefile{toc}{\contentsline {section}{\numberline {3.4}A Hierarchy of Definitions}{61}{section.3.4}}
\newlabel{hierarchy}{{3.4}{61}{A Hierarchy of Definitions\relax }{section.3.4}{}}
\expandafter\gdef \csname page@num.hierarchy\endcsname{61}\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}{63}{subsection.3.4.1}}
\newlabel{metadefprop}{{3.4.1}{63}{Definitions for Propositional Calculus\relax }{subsection.3.4.1}{}}
\expandafter\gdef \csname page@num.metadefprop\endcsname{63}\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}{64}{subsection.3.4.2}}
\newlabel{metadefpred}{{3.4.2}{64}{Definitions for Predicate Calculus\relax }{subsection.3.4.2}{}}
\expandafter\gdef \csname page@num.metadefpred\endcsname{64}\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}{65}{subsection.3.4.3}}
\newlabel{setdefinitions}{{3.4.3}{65}{Definitions for Set Theory\relax }{subsection.3.4.3}{}}
\expandafter\gdef \csname page@num.setdefinitions\endcsname{65}\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}{66}{Definitions for Set Theory\relax }{subsection.3.4.3}{}}
\expandafter\gdef \csname page@num.dfclel\endcsname{66}\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}{68}{Definitions for Set Theory\relax }{subsection.3.4.3}{}}
\expandafter\gdef \csname page@num.dfbr\endcsname{68}\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}{69}{Definitions for Set Theory\relax }{subsection.3.4.3}{}}
\expandafter\gdef \csname page@num.dfom\endcsname{69}\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}{71}{Definitions for Set Theory\relax }{subsection.3.4.3}{}}
\expandafter\gdef \csname page@num.dfopr\endcsname{71}\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}{71}{section.3.5}}
\newlabel{tricks}{{3.5}{71}{Tricks of the Trade\relax }{section.3.5}{}}
\expandafter\gdef \csname page@num.tricks\endcsname{71}\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}{72}{section.3.6}}
\newlabel{sometheorems}{{3.6}{72}{A Theorem Sampler\relax }{section.3.6}{}}
\expandafter\gdef \csname page@num.sometheorems\endcsname{72}\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}{75}{section.3.7}}
\newlabel{real}{{3.7}{75}{Axioms for Real and Complex Numbers\relax }{section.3.7}{}}
\expandafter\gdef \csname page@num.real\endcsname{75}\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}{77}{section*.17}}
\@writefile{toc}{\contentsline {section}{\numberline {3.8}Exploring the Set Theory Database}{77}{section.3.8}}
\newlabel{exploring}{{3.8}{77}{Exploring the Set Theory Database\relax }{section.3.8}{}}
\expandafter\gdef \csname page@num.exploring\endcsname{77}\expandafter\gdef \csname ref@num.exploring\endcsname{3.8}\expandafter\gdef \csname sectionref@name.exploring\endcsname{section.3.8}
\citation{Enderton}
\citation{Hamilton}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.8.1}A Note on ``Compact'' Proof Format}{84}{subsection.3.8.1}}
\citation{Russell2}
\@writefile{toc}{\contentsline {chapter}{\numberline {4}The Metamath Language}{87}{chapter.4}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\newlabel{languagespec}{{4}{87}{The Metamath Language\relax }{chapter.4}{}}
\expandafter\gdef \csname page@num.languagespec\endcsname{87}\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}{88}{section.4.1}}
\newlabel{spec}{{4.1}{88}{Specification of the Metamath Language\relax }{section.4.1}{}}
\expandafter\gdef \csname page@num.spec\endcsname{88}\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}{88}{subsection.4.1.1}}
\newlabel{spec1}{{4.1.1}{88}{Preliminaries\relax }{subsection.4.1.1}{}}
\expandafter\gdef \csname page@num.spec1\endcsname{88}\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}{88}{Preliminaries\relax }{subsection.4.1.1}{}}
\expandafter\gdef \csname page@num.spec1chars\endcsname{88}\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}{89}{subsection.4.1.2}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.1.3}Basic Syntax}{89}{subsection.4.1.3}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.1.4}Proof Verification}{90}{subsection.4.1.4}}
\newlabel{spec4}{{4.1.4}{90}{Proof Verification\relax }{subsection.4.1.4}{}}
\expandafter\gdef \csname page@num.spec4\endcsname{90}\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}{91}{section*.18}}
\@writefile{toc}{\contentsline {section}{\numberline {4.2}The Basic Keywords}{91}{section.4.2}}
\newlabel{tut1}{{4.2}{91}{The Basic Keywords\relax }{section.4.2}{}}
\expandafter\gdef \csname page@num.tut1\endcsname{91}\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}}{92}{table.4.1}}
\newlabel{basickeywords}{{4.1}{92}{The Basic Keywords\relax }{table.4.1}{}}
\expandafter\gdef \csname page@num.basickeywords\endcsname{92}\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}}{92}{table.4.2}}
\newlabel{otherkeywords}{{4.2}{92}{The Basic Keywords\relax }{table.4.2}{}}
\expandafter\gdef \csname page@num.otherkeywords\endcsname{92}\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}{93}{subsection.4.2.1}}
\newlabel{dollardollar}{{4.2.1}{93}{User-Defined Tokens\relax }{subsection.4.2.1}{}}
\expandafter\gdef \csname page@num.dollardollar\endcsname{93}\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}{93}{section*.19}}
\@writefile{toc}{\contentsline {subsubsection}{Label Tokens}{94}{section*.20}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.2.2}Constants and Variables}{94}{subsection.4.2.2}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.2.3}The \texttt  {\$c} and \texttt  {\$v} Declaration Statements}{95}{subsection.4.2.3}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.2.4}The \texttt  {\$d} Statement}{95}{subsection.4.2.4}}
\newlabel{dollard}{{4.2.4}{95}{The \texttt {\$d} Statement\relax }{subsection.4.2.4}{}}
\expandafter\gdef \csname page@num.dollard\endcsname{95}\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}{97}{section*.21}}
\citation{Nemeti}
\citation{Megill}
\citation{Megill}
\newlabel{nodd}{{71}{100}{Compound \texttt {\$d} Statements\relax }{section*.21}{}}
\expandafter\gdef \csname page@num.nodd\endcsname{100}\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}{100}{subsection.4.2.5}}
\newlabel{dollaref}{{4.2.5}{100}{The \texttt {\$f} and \texttt {\$e} Statements\relax }{subsection.4.2.5}{}}
\expandafter\gdef \csname page@num.dollaref\endcsname{100}\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)}{102}{subsection.4.2.6}}
\@writefile{toc}{\contentsline {subsubsection}{The \texttt  {\$a} Statement}{102}{section*.22}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.2.7}Frames}{103}{subsection.4.2.7}}
\newlabel{frames}{{4.2.7}{103}{Frames\relax }{subsection.4.2.7}{}}
\expandafter\gdef \csname page@num.frames\endcsname{103}\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}{106}{Frames\relax }{Item.4}{}}
\expandafter\gdef \csname page@num.framelist\endcsname{106}\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  {\$\}})}{107}{subsection.4.2.8}}
\newlabel{scoping}{{4.2.8}{107}{Scoping Statements (\texttt {\$\{} and \texttt {\$\}})\relax }{subsection.4.2.8}{}}
\expandafter\gdef \csname page@num.scoping\endcsname{107}\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}{108}{section*.23}}
\newlabel{redeclaration}{{76}{108}{Redeclaration of Math Symbols\relax }{section*.23}{}}
\expandafter\gdef \csname page@num.redeclaration\endcsname{108}\expandafter\gdef \csname ref@num.redeclaration\endcsname{76}\expandafter\gdef \csname sectionref@name.redeclaration\endcsname{subsection.4.2.8}
\newlabel{redeclarationf}{{13}{108}{Redeclaration of Math Symbols\relax }{Hfootnote.77}{}}
\expandafter\gdef \csname page@num.redeclarationf\endcsname{108}\expandafter\gdef \csname ref@num.redeclarationf\endcsname{13}\expandafter\gdef \csname sectionref@name.redeclarationf\endcsname{subsection.4.2.8}
\@writefile{toc}{\contentsline {subsubsection}{Frames Revisited}{109}{section*.24}}
\newlabel{frameconvert}{{77}{109}{Frames Revisited\relax }{section*.24}{}}
\expandafter\gdef \csname page@num.frameconvert\endcsname{109}\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}{109}{section.4.3}}
\newlabel{proof}{{4.3}{109}{The Anatomy of a Proof\relax }{section.4.3}{}}
\expandafter\gdef \csname page@num.proof\endcsname{109}\expandafter\gdef \csname ref@num.proof\endcsname{4.3}\expandafter\gdef \csname sectionref@name.proof\endcsname{section.4.3}
\newlabel{treeproof}{{79}{112}{The Anatomy of a Proof\relax }{Hfootnote.79}{}}
\expandafter\gdef \csname page@num.treeproof\endcsname{112}\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}{113}{subsection.4.3.1}}
\newlabel{unify}{{4.3.1}{113}{The Concept of Unification\relax }{subsection.4.3.1}{}}
\expandafter\gdef \csname page@num.unify\endcsname{113}\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}{113}{section.4.4}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.4.1}Comments in the Metamath Language}{113}{subsection.4.4.1}}
\newlabel{comments}{{4.4.1}{113}{Comments in the Metamath Language\relax }{subsection.4.4.1}{}}
\expandafter\gdef \csname page@num.comments\endcsname{113}\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}{114}{section*.25}}
\newlabel{mathcomments}{{80}{114}{Math Symbols and Labels Inside Comments\relax }{section*.25}{}}
\expandafter\gdef \csname page@num.mathcomments\endcsname{114}\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}{114}{section*.26}}
\@writefile{toc}{\contentsline {subsubsection}{Label References in Comments}{115}{section*.27}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.4.2}Including Other Files in a Metamath Source File}{115}{subsection.4.4.2}}
\newlabel{include}{{4.4.2}{115}{Including Other Files in a Metamath Source File\relax }{subsection.4.4.2}{}}
\expandafter\gdef \csname page@num.include\endcsname{115}\expandafter\gdef \csname ref@num.include\endcsname{4.4.2}\expandafter\gdef \csname sectionref@name.include\endcsname{subsection.4.4.2}
\newlabel{includef}{{83}{116}{Including Other Files in a Metamath Source File\relax }{Hfootnote.83}{}}
\expandafter\gdef \csname page@num.includef\endcsname{116}\expandafter\gdef \csname ref@num.includef\endcsname{83}\expandafter\gdef \csname sectionref@name.includef\endcsname{subsection.4.4.2}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.4.3}Compressed Proof Format}{116}{subsection.4.4.3}}
\newlabel{compressed1}{{4.4.3}{116}{Compressed Proof Format\relax }{subsection.4.4.3}{}}
\expandafter\gdef \csname page@num.compressed1\endcsname{116}\expandafter\gdef \csname ref@num.compressed1\endcsname{4.4.3}\expandafter\gdef \csname sectionref@name.compressed1\endcsname{subsection.4.4.3}
\citation{Behnke}
\citation{Nemesszeghy}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.4.4}Specifying Unknown Proofs or Subproofs}{117}{subsection.4.4.4}}
\newlabel{unknown}{{4.4.4}{117}{Specifying Unknown Proofs or Subproofs\relax }{subsection.4.4.4}{}}
\expandafter\gdef \csname page@num.unknown\endcsname{117}\expandafter\gdef \csname ref@num.unknown\endcsname{4.4.4}\expandafter\gdef \csname sectionref@name.unknown\endcsname{subsection.4.4.4}
\@writefile{toc}{\contentsline {section}{\numberline {4.5}Appendix: Axioms vs.\ Definitions}{117}{section.4.5}}
\newlabel{definitions}{{4.5}{117}{Appendix: Axioms vs.\ Definitions\relax }{section.4.5}{}}
\expandafter\gdef \csname page@num.definitions\endcsname{117}\expandafter\gdef \csname ref@num.definitions\endcsname{4.5}\expandafter\gdef \csname sectionref@name.definitions\endcsname{section.4.5}
\citation{Lejewski}
\citation{Goodstein}
\citation{Robinsont}
\citation{Quine}
\@writefile{toc}{\contentsline {chapter}{\numberline {5}The Metamath Program}{121}{chapter.5}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\newlabel{commands}{{5}{121}{The Metamath Program\relax }{chapter.5}{}}
\expandafter\gdef \csname page@num.commands\endcsname{121}\expandafter\gdef \csname ref@num.commands\endcsname{5}\expandafter\gdef \csname sectionref@name.commands\endcsname{chapter.5}
\@writefile{toc}{\contentsline {section}{\numberline {5.1}Controlling Metamath}{121}{section.5.1}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.1.1}\texttt  {exit} Command}{121}{subsection.5.1.1}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.1.2}\texttt  {open log} Command}{121}{subsection.5.1.2}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.1.3}\texttt  {close log} Command}{121}{subsection.5.1.3}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.1.4}\texttt  {open tex} Command}{122}{subsection.5.1.4}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.1.5}\texttt  {close tex} Command}{122}{subsection.5.1.5}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.1.6}\texttt  {submit} Command}{122}{subsection.5.1.6}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.1.7}\texttt  {erase} Command}{122}{subsection.5.1.7}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.1.8}Operating System Commands}{122}{subsection.5.1.8}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.1.9}\texttt  {set echo} Command}{123}{subsection.5.1.9}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.1.10}\texttt  {set scroll} Command}{123}{subsection.5.1.10}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.1.11}\texttt  {set screen\_width} Command}{123}{subsection.5.1.11}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.1.12}\texttt  {beep} Command}{123}{subsection.5.1.12}}
\@writefile{toc}{\contentsline {section}{\numberline {5.2}Reading and Writing Files}{123}{section.5.2}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2.1}\texttt  {read} Command}{123}{subsection.5.2.1}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2.2}\texttt  {write source} Command}{124}{subsection.5.2.2}}
\@writefile{toc}{\contentsline {section}{\numberline {5.3}Showing Status and Statements}{124}{section.5.3}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.3.1}\texttt  {show settings} Command}{124}{subsection.5.3.1}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.3.2}\texttt  {show memory} Command}{124}{subsection.5.3.2}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.3.3}\texttt  {show labels} Command}{124}{subsection.5.3.3}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.3.4}\texttt  {show statement} Command}{124}{subsection.5.3.4}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.3.5}\texttt  {search} Command}{125}{subsection.5.3.5}}
\@writefile{toc}{\contentsline {section}{\numberline {5.4}Displaying and Verifying Proofs}{125}{section.5.4}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.4.1}\texttt  {show proof} Command}{125}{subsection.5.4.1}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.4.2}\texttt  {show usage} Command}{126}{subsection.5.4.2}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.4.3}\texttt  {show trace\_back} Command}{126}{subsection.5.4.3}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.4.4}\texttt  {verify proof} Command}{126}{subsection.5.4.4}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.4.5}\texttt  {save proof} Command}{127}{subsection.5.4.5}}
\@writefile{toc}{\contentsline {section}{\numberline {5.5}Changing Label and Symbol Names}{127}{section.5.5}}
\@writefile{toc}{\contentsline {section}{\numberline {5.6}Creating Proofs}{127}{section.5.6}}
\newlabel{pfcommands}{{5.6}{127}{Creating Proofs\relax }{section.5.6}{}}
\expandafter\gdef \csname page@num.pfcommands\endcsname{127}\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}{127}{subsection.5.6.1}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.6.2}\texttt  {set unification\_timeout} Command}{128}{subsection.5.6.2}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.6.3}\texttt  {set empty\_substitution} Command}{128}{subsection.5.6.3}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.6.4}\texttt  {set search\_limit} Command}{128}{subsection.5.6.4}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.6.5}\texttt  {show new\_proof} Command}{128}{subsection.5.6.5}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.6.6}\texttt  {assign} Command}{129}{subsection.5.6.6}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.6.7}\texttt  {match} Command}{129}{subsection.5.6.7}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.6.8}\texttt  {let} Command}{129}{subsection.5.6.8}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.6.9}\texttt  {unify} Command}{130}{subsection.5.6.9}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.6.10}\texttt  {initialize} Command}{130}{subsection.5.6.10}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.6.11}\texttt  {delete} Command}{130}{subsection.5.6.11}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.6.12}\texttt  {improve} Command}{131}{subsection.5.6.12}}
\newlabel{improve}{{5.6.12}{131}{\texttt {improve} Command\relax }{subsection.5.6.12}{}}
\expandafter\gdef \csname page@num.improve\endcsname{131}\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}{131}{subsection.5.6.13}}
\@writefile{toc}{\contentsline {section}{\numberline {5.7}File Utilities}{132}{section.5.7}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.7.1}\texttt  {file type} Command}{132}{subsection.5.7.1}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.7.2}\texttt  {file search} Command}{132}{subsection.5.7.2}}
\@writefile{toc}{\contentsline {section}{\numberline {5.8}Size Limitations in Metamath}{132}{section.5.8}}
\@writefile{toc}{\contentsline {chapter}{\numberline {A}Math Symbol Tokens for Set Theory}{133}{appendix.A}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\newlabel{ASCII}{{A}{133}{Math Symbol Tokens for Set Theory\relax }{appendix.A}{}}
\expandafter\gdef \csname page@num.ASCII\endcsname{133}\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}{137}{appendix.B}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\newlabel{compressed}{{B}{137}{Compressed Proofs\relax }{appendix.B}{}}
\expandafter\gdef \csname page@num.compressed\endcsname{137}\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}{139}{appendix.C}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\newlabel{formalspec}{{C}{139}{Metamath's Formal System\relax }{appendix.C}{}}
\expandafter\gdef \csname page@num.formalspec\endcsname{139}\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}{139}{section.C.1}}
\@writefile{toc}{\contentsline {section}{\numberline {C.2}The Formal Description}{140}{section.C.2}}
\@writefile{toc}{\contentsline {subsection}{\numberline {C.2.1}Preliminaries}{140}{Hfootnote.89}}
\@writefile{toc}{\contentsline {subsection}{\numberline {C.2.2}Constants, Variables, and Expressions}{140}{subsection.C.2.2}}
\@writefile{toc}{\contentsline {subsection}{\numberline {C.2.3}Substitution}{141}{subsection.C.2.3}}
\@writefile{toc}{\contentsline {subsection}{\numberline {C.2.4}Statements}{141}{subsection.C.2.4}}
\citation{Nemeti}
\@writefile{toc}{\contentsline {subsection}{\numberline {C.2.5}Formal Systems}{142}{subsection.C.2.5}}
\@writefile{toc}{\contentsline {section}{\numberline {C.3}Examples of Formal Systems}{143}{section.C.3}}
\newlabel{exampleref}{{C.3}{143}{Examples of Formal Systems\relax }{section.C.3}{}}
\expandafter\gdef \csname page@num.exampleref\endcsname{143}\expandafter\gdef \csname ref@num.exampleref\endcsname{C.3}\expandafter\gdef \csname sectionref@name.exampleref\endcsname{section.C.3}
\citation{Tarski1965}
\citation{Tarski1965}
\@writefile{toc}{\contentsline {subsection}{\numberline {C.3.1}Example\nobreakspace  {}1---Propositional Calculus}{144}{subsection.C.3.1}}
\citation{Tarski1965}
\@writefile{toc}{\contentsline {subsection}{\numberline {C.3.2}Example\nobreakspace  {}2---Predicate Calculus with Equality}{145}{subsection.C.3.2}}
\citation{Tarski1965}
\@writefile{toc}{\contentsline {subsection}{\numberline {C.3.3}Free Variables and Proper Substitution}{147}{subsection.C.3.3}}
\newlabel{effectivelybound}{{C.3.3}{147}{Free Variables and Proper Substitution\relax }{subsection.C.3.3}{}}
\expandafter\gdef \csname page@num.effectivelybound\endcsname{147}\expandafter\gdef \csname ref@num.effectivelybound\endcsname{C.3.3}\expandafter\gdef \csname sectionref@name.effectivelybound\endcsname{subsection.C.3.3}
\citation{Kalish}
\citation{Megill}
\citation{Megill}
\@writefile{toc}{\contentsline {subsection}{\numberline {C.3.4}Metalogical Completeness}{148}{subsection.C.3.4}}
\@writefile{toc}{\contentsline {subsection}{\numberline {C.3.5}Example\nobreakspace  {}3---Metalogically Complete Predicate Calculus with Equality}{148}{subsection.C.3.5}}
\@writefile{toc}{\contentsline {subsection}{\numberline {C.3.6}Example\nobreakspace  {}4---Adding Definitions}{150}{subsection.C.3.6}}
\@writefile{toc}{\contentsline {subsection}{\numberline {C.3.7}Example\nobreakspace  {}5---ZFC Set Theory}{150}{subsection.C.3.7}}
\citation{Takeuti}
\citation{Quine}
\@writefile{toc}{\contentsline {subsection}{\numberline {C.3.8}Example\nobreakspace  {}6---Class Notation in Set Theory}{151}{subsection.C.3.8}}
\newlabel{class}{{C.3.8}{151}{Example~6---Class Notation in Set Theory\relax }{subsection.C.3.8}{}}
\expandafter\gdef \csname page@num.class\endcsname{151}\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}{152}{section.C.4}}
\newlabel{theorymm}{{C.4}{152}{Metamath as a Formal System\relax }{section.C.4}{}}
\expandafter\gdef \csname page@num.theorymm\endcsname{152}\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}{155}{appendix.D}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\newlabel{MIU}{{D}{155}{The MIU System\relax }{appendix.D}{}}
\expandafter\gdef \csname page@num.MIU\endcsname{155}\expandafter\gdef \csname ref@num.MIU\endcsname{D}\expandafter\gdef \csname sectionref@name.MIU\endcsname{chapter.D}
\citation{Hofstadter}
\@writefile{toc}{\contentsline {chapter}{\numberline {E}Software Sources}{159}{appendix.E}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\newlabel{swsources}{{E}{159}{Software Sources\relax }{appendix.E}{}}
\expandafter\gdef \csname page@num.swsources\endcsname{159}\expandafter\gdef \csname ref@num.swsources\endcsname{E}\expandafter\gdef \csname sectionref@name.swsources\endcsname{chapter.E}
\@writefile{toc}{\contentsline {chapter}{\numberline {F}Disclaimer and Trademarks}{161}{appendix.F}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\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}{163}{section*.28}}
\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}{169}{section*.30}}