\indexentry{Metamath|hyperpage}{ix}
\indexentry{formal system|hyperpage}{ix}
\indexentry{theorem|hyperpage}{ix}
\indexentry{axiom|hyperpage}{ix}
\indexentry{rule|hyperpage}{ix}
\indexentry{well-formed formula (wff)|hyperpage}{ix}
\indexentry{Metamath|hyperpage}{x}
\indexentry{computer program bugs|hyperpage}{x}
\indexentry{computer program bugs|hyperpage}{x}
\indexentry{G\"{o}del's incompleteness theorem|hyperpage}{xi}
\indexentry{formal system|hyperpage}{xi}
\indexentry{Proof Assistant|hyperpage}{xi}
\indexentry{Metamath|hyperpage}{xi}
\indexentry{latex@{\LaTeX}|hyperpage}{xi}
\indexentry{Metamath|hyperpage}{xi}
\indexentry{Metamath|hyperpage}{xii}
\indexentry{constant|hyperpage}{xii}
\indexentry{variable|hyperpage}{xii}
\indexentry{substitution!variable|hyperpage}{xii}
\indexentry{variable substitution|hyperpage}{xii}
\indexentry{formal proof|hyperpage}{xii}
\indexentry{Bourbaki, Nicholaus|hyperpage}{xiii}
\indexentry{Barrow, John D.|hyperpage}{xiii}
\indexentry{Metamath|hyperpage}{xiii}
\indexentry{Euclidean geometry|hyperpage}{xiii}
\indexentry{Pasch's axiom|hyperpage}{xiii}
\indexentry{Purinton, Josh|hyperpage}{xiv}
\indexentry{Levien, Raph|hyperpage}{xiv}
\indexentry{Ghilbert|hyperpage}{xiv}
\indexentry{Solovay, Robert|hyperpage}{xiv}
\indexentry{category theory|hyperpage}{xiv}
\indexentry{cardinal, inaccessible|hyperpage}{xiv}
\indexentry{Grothendieck, Alexander|hyperpage}{xiv}
\indexentry{Mac Lane, Saunders|hyperpage}{xiv}
\indexentry{Feferman, Solomon|hyperpage}{xiv}
\indexentry{Mizar|hyperpage}{xv}
\indexentry{Williams, Anthony|hyperpage}{xv}
\indexentry{Davis, Phillip J.|hyperpage}{1}
\indexentry{Metamath|hyperpage}{2}
\indexentry{Metamath|hyperpage}{2}
\indexentry{formal system|hyperpage}{2}
\indexentry{metalanguage|hyperpage}{2}
\indexentry{axiom|hyperpage}{2}
\indexentry{logic|hyperpage}{2}
\indexentry{set theory|hyperpage}{2}
\indexentry{number theory|hyperpage}{2}
\indexentry{group theory|hyperpage}{3}
\indexentry{abstract algebra|hyperpage}{3}
\indexentry{analysis|hyperpage}{3}
\indexentry{real and complex numbers|hyperpage}{3}
\indexentry{topology|hyperpage}{3}
\indexentry{quantum logic|hyperpage}{3}
\indexentry{quantum mechanics|hyperpage}{3}
\indexentry{Metamath|hyperpage}{3}
\indexentry{Metamath!representation of numbers|hyperpage}{3}
\indexentry{computer algebra system|hyperpage}{3}
\indexentry{macsyma@{\sc macsyma}|hyperpage}{3}
\indexentry{Mathematica|hyperpage}{3}
\indexentry{Maple|hyperpage}{3}
\indexentry{Munkres, James R.|hyperpage}{3}
\indexentry{Metamath|hyperpage}{4}
\indexentry{Whitehead, Alfred North|hyperpage}{4}
\indexentry{Landau, Edmund|hyperpage}{5}
\indexentry{Auden, W.\ H.|hyperpage}{5}
\indexentry{Guillen, Michael|hyperpage}{5}
\indexentry{G\"{o}del's incompleteness theorem|hyperpage}{5}
\indexentry{Rucker, Rudy|hyperpage}{6}
\indexentry{computer program bugs|hyperpage}{8}
\indexentry{Solow, Daniel|hyperpage}{8}
\indexentry{computer program bugs|hyperpage}{8}
\indexentry{Zermelo-Fraenkel set theory|hyperpage}{9}
\indexentry{Russell's paradox|hyperpage}{9}
\indexentry{Russell's paradox|hyperpage}{10}
\indexentry{first-order logic|hyperpage}{11}
\indexentry{deduction theorem|hyperpage}{11}
\indexentry{substitution theorem|hyperpage}{11}
\indexentry{first-order logic!completeness|hyperpage}{11}
\indexentry{formal proof|hyperpage}{12}
\indexentry{metatheorem|hyperpage}{12}
\indexentry{computer program bugs|hyperpage}{12}
\indexentry{Davis, Phillip J.|hyperpage}{12}
\indexentry{informal proof|hyperpage}{13}
\indexentry{formal proof|hyperpage}{13}
\indexentry{hierarchy|hyperpage}{13}
\indexentry{cranks|hyperpage}{13}
\indexentry{Fermat's Last Theorem|hyperpage}{13}
\indexentry{Edwards, Robert E.|hyperpage}{14}
\indexentry{Davis, Phillip J.|hyperpage}{14}
\indexentry{Wang, Hao|hyperpage}{14}
\indexentry{de Millo, Richard|hyperpage}{15}
\indexentry{Metamath|hyperpage}{15}
\indexentry{formal proof|hyperpage}{15}
\indexentry{informal proof|hyperpage}{15}
\indexentry{proof length|hyperpage}{15}
\indexentry{definition|hyperpage}{15}
\indexentry{G\"{o}del's incompleteness theorem|hyperpage}{15}
\indexentry{Boolos, George S.|hyperpage}{15}
\indexentry{Mathias, Adrian R. D.|hyperpage}{15}
\indexentry{Bourbaki, Nicholaus|hyperpage}{15}
\indexentry{hierarchy|hyperpage}{15}
\indexentry{Metamath|hyperpage}{15}
\indexentry{Hilbert, David|hyperpage}{15}
\indexentry{Russell, Bertrand|hyperpage}{15}
\indexentry{Millay, Edna|hyperpage}{16}
\indexentry{Metamath|hyperpage}{16}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{16}
\indexentry{Bible|hyperpage}{16}
\indexentry{Kronecker, Leopold|hyperpage}{16}
\indexentry{Hilbert, David|hyperpage}{16}
\indexentry{Metamath|hyperpage}{16}
\indexentry{Metamath|hyperpage}{17}
\indexentry{foundations of mathematics|hyperpage}{17}
\indexentry{metalanguage|hyperpage}{17}
\indexentry{object language|hyperpage}{17}
\indexentry{weak logic|hyperpage}{17}
\indexentry{Anderson, Alan Ross|hyperpage}{17}
\indexentry{Megill, Norman|hyperpage}{17}
\indexentry{Bunder, Martin|hyperpage}{17}
\indexentry{modal logic|hyperpage}{17}
\indexentry{Boolos, George S.|hyperpage}{17}
\indexentry{quantum logic|hyperpage}{17}
\indexentry{Pavi{\v{c}}i{\'{c}}, M.|hyperpage}{17}
\indexentry{Metamath|hyperpage}{17}
\indexentry{intuitionism|hyperpage}{17}
\indexentry{constructivism|hyperpage}{17}
\indexentry{axiom|hyperpage}{17}
\indexentry{rule|hyperpage}{17}
\indexentry{intuitionism|hyperpage}{17}
\indexentry{\texttt{show trace{\char`\_}back} command|hyperpage}{17}
\indexentry{Tymoczko, Thomas|hyperpage}{17}
\indexentry{Axiom of Choice|hyperpage}{17}
\indexentry{Enderton, Herbert B.|hyperpage}{17}
\indexentry{Quine, Willard Van Orman|hyperpage}{17}
\indexentry{Kline, Morris|hyperpage}{18}
\indexentry{G\"{o}del's incompleteness theorem|hyperpage}{18}
\indexentry{consistent theory|hyperpage}{18}
\indexentry{Russell's paradox|hyperpage}{18}
\indexentry{Frege, Gottlob|hyperpage}{18}
\indexentry{Kline, Morris|hyperpage}{18}
\indexentry{certainty|hyperpage}{18}
\indexentry{Curry, Haskell B.|hyperpage}{18}
\indexentry{formal logic|hyperpage}{19}
\indexentry{gaps in proofs|hyperpage}{19}
\indexentry{formal proof|hyperpage}{19}
\indexentry{set theory|hyperpage}{19}
\indexentry{hierarchy|hyperpage}{19}
\indexentry{formal logic|hyperpage}{19}
\indexentry{formal proof|hyperpage}{19}
\indexentry{well-formed formula (wff)|hyperpage}{19}
\indexentry{automated proof verification|hyperpage}{19}
\indexentry{computer program bugs|hyperpage}{19}
\indexentry{formal system|hyperpage}{19}
\indexentry{syntax rules|hyperpage}{19}
\indexentry{axiom|hyperpage}{19}
\indexentry{theorem|hyperpage}{19}
\indexentry{Metamath|hyperpage}{19}
\indexentry{formal system|hyperpage}{19}
\indexentry{Metamath|hyperpage}{20}
\indexentry{constructive language|hyperpage}{20}
\indexentry{first-order logic|hyperpage}{20}
\indexentry{higher-order logic|hyperpage}{20}
\indexentry{weak logic|hyperpage}{20}
\indexentry{well-formed formula (wff)|hyperpage}{20}
\indexentry{Metamath!self-description|hyperpage}{20}
\indexentry{Harrison, John|hyperpage}{20}
\indexentry{reflection principle|hyperpage}{20}
\indexentry{formal proof|hyperpage}{20}
\indexentry{automated proof verification|hyperpage}{20}
\indexentry{Halmos, Paul|hyperpage}{21}
\indexentry{computers and pure mathematics|hyperpage}{21}
\indexentry{computer algebra system|hyperpage}{21}
\indexentry{automated theorem proving|hyperpage}{21}
\indexentry{computer program bugs|hyperpage}{21}
\indexentry{Tymoczko, Thomas|hyperpage}{21}
\indexentry{four-color theorem|hyperpage}{21}
\indexentry{proof length|hyperpage}{21}
\indexentry{Swart, E. R.|hyperpage}{21}
\indexentry{trusting computers|hyperpage}{21}
\indexentry{Metamath|hyperpage}{22}
\indexentry{computer program bugs|hyperpage}{22}
\indexentry{Hume, David|hyperpage}{22}
\indexentry{Ulam, Stanislaw|hyperpage}{22}
\indexentry{errors in proofs|hyperpage}{22}
\indexentry{Fermat's Last Theorem|hyperpage}{23}
\indexentry{Stark, Harold M|hyperpage}{23}
\indexentry{Miyaoka, Yoichi|hyperpage}{23}
\indexentry{Wiles, Andrew|hyperpage}{23}
\indexentry{Euclidean geometry|hyperpage}{23}
\indexentry{Pasch's axiom|hyperpage}{23}
\indexentry{Schr\"{o}der-Berstein theorem|hyperpage}{23}
\indexentry{Enderton, Herbert B.|hyperpage}{23}
\indexentry{Hilbert, David|hyperpage}{23}
\indexentry{continuum hypothesis|hyperpage}{23}
\indexentry{Cohen, Paul|hyperpage}{23}
\indexentry{infinity|hyperpage}{23}
\indexentry{cardinal, transfinite|hyperpage}{23}
\indexentry{cardinality|hyperpage}{23}
\indexentry{Cantor, Georg|hyperpage}{23}
\indexentry{four-color theorem|hyperpage}{23}
\indexentry{Kempe, A. B.|hyperpage}{23}
\indexentry{Courant, Richard|hyperpage}{23}
\indexentry{Appel, K.|hyperpage}{23}
\indexentry{Haken, W.|hyperpage}{23}
\indexentry{Koch, K.|hyperpage}{23}
\indexentry{set|hyperpage}{23}
\indexentry{function|hyperpage}{23}
\indexentry{mapping|hyperpage}{23}
\indexentry{domain|hyperpage}{23}
\indexentry{Coxeter, H. S. M.|hyperpage}{24}
\indexentry{Poincar\'{e} conjecture|hyperpage}{24}
\indexentry{Rourke, Colin|hyperpage}{24}
\indexentry{R\^{e}go, Eduardo|hyperpage}{24}
\indexentry{Clifford algebras|hyperpage}{24}
\indexentry{Lounesto, Pertti|hyperpage}{24}
\indexentry{Metamath|hyperpage}{24}
\indexentry{errors in proofs|hyperpage}{24}
\indexentry{Metamath|hyperpage}{24}
\indexentry{computer algebra system|hyperpage}{24}
\indexentry{Mathematica|hyperpage}{24}
\indexentry{theorem|hyperpage}{25}
\indexentry{proof|hyperpage}{25}
\indexentry{Mathematica and proofs|hyperpage}{25}
\indexentry{computer program bugs|hyperpage}{25}
\indexentry{Harrison, John|hyperpage}{25}
\indexentry{decidable theory|hyperpage}{25}
\indexentry{Euclidean geometry|hyperpage}{25}
\indexentry{Tarski, Alfred|hyperpage}{25}
\indexentry{Wen-ts{\"{u}}n, Wu|hyperpage}{25}
\indexentry{Fermat's Last Theorem|hyperpage}{25}
\indexentry{Maple|hyperpage}{25}
\indexentry{Chou, Shang-Ching|hyperpage}{25}
\indexentry{Penrose, Roger|hyperpage}{26}
\indexentry{automated theorem proving|hyperpage}{26}
\indexentry{Robinson's resolution principle|hyperpage}{26}
\indexentry{hierarchy|hyperpage}{26}
\indexentry{first-order logic|hyperpage}{26}
\indexentry{Wos, Larry|hyperpage}{26}
\indexentry{Robbins algebra|hyperpage}{26}
\indexentry{Boolean algebra|hyperpage}{26}
\indexentry{Huntington, E. V.|hyperpage}{26}
\indexentry{Robbins, Herbert|hyperpage}{26}
\indexentry{Tarski, Alfred|hyperpage}{26}
\indexentry{Metamath|hyperpage}{27}
\indexentry{Isabelle|hyperpage}{27}
\indexentry{hol@{\sc hol}|hyperpage}{27}
\indexentry{otter@{\sc otter}|hyperpage}{27}
\indexentry{Wos, Larry|hyperpage}{27}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{27}
\indexentry{Megill, Norman|hyperpage}{27}
\indexentry{Bledsoe, W. W.|hyperpage}{27}
\indexentry{automated theorem proving|hyperpage}{27}
\indexentry{dummy variable!eliminating|hyperpage}{27}
\indexentry{qed project@{\sc qed} project|hyperpage}{28}
\indexentry{Mizar|hyperpage}{28}
\indexentry{lcf@{\sc lcf}|hyperpage}{28}
\indexentry{hol@{\sc hol}|hyperpage}{28}
\indexentry{Metamath|hyperpage}{29}
\indexentry{set theory|hyperpage}{29}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{29}
\indexentry{analysis|hyperpage}{29}
\indexentry{real and complex numbers|hyperpage}{29}
\indexentry{theorem|hyperpage}{29}
\indexentry{axiom|hyperpage}{29}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{29}
\indexentry{formal system|hyperpage}{29}
\indexentry{Metamath|hyperpage}{29}
\indexentry{formal system|hyperpage}{29}
\indexentry{modal logic|hyperpage}{29}
\indexentry{intuitionism|hyperpage}{29}
\indexentry{higher-order logic|hyperpage}{29}
\indexentry{quantum logic|hyperpage}{29}
\indexentry{category theory|hyperpage}{29}
\indexentry{Hofstadter, Douglas R.|hyperpage}{29}
\indexentry{MIU-system|hyperpage}{29}
\indexentry{Hilbert, David|hyperpage}{29}
\indexentry{metalanguage|hyperpage}{29}
\indexentry{Metamath|hyperpage}{29}
\indexentry{finitary proof|hyperpage}{29}
\indexentry{weak logic|hyperpage}{29}
\indexentry{formal system|hyperpage}{29}
\indexentry{model theory|hyperpage}{29}
\indexentry{proof theory|hyperpage}{29}
\indexentry{Metamath|hyperpage}{30}
\indexentry{formalism|hyperpage}{30}
\indexentry{Hilbert, David|hyperpage}{30}
\indexentry{Kline, Morris|hyperpage}{30}
\indexentry{Behnke, H.|hyperpage}{30}
\indexentry{metamathematics|hyperpage}{30}
\indexentry{finitary proof|hyperpage}{30}
\indexentry{Shoenfield, Joseph R.|hyperpage}{30}
\indexentry{Davis, Phillip J.|hyperpage}{30}
\indexentry{Metamath|hyperpage}{30}
\indexentry{Whitehead, Alfred North|hyperpage}{30}
\indexentry{Russell, Bertrand|hyperpage}{30}
\indexentry{principia mathematica@{\em Principia Mathematica}|hyperpage}{30}
\indexentry{condensed detachment|hyperpage}{31}
\indexentry{Hindley, J. Roger|hyperpage}{31}
\indexentry{Kalman, J. A.|hyperpage}{31}
\indexentry{Meredith, C. A.|hyperpage}{31}
\indexentry{Peterson, Jeremy George|hyperpage}{31}
\indexentry{axiom|hyperpage}{31}
\indexentry{rule|hyperpage}{31}
\indexentry{theorem|hyperpage}{31}
\indexentry{substitution!variable|hyperpage}{31}
\indexentry{variable substitution|hyperpage}{31}
\indexentry{propositional calculus|hyperpage}{31}
\indexentry{first-order logic|hyperpage}{31}
\indexentry{Megill, Norman|hyperpage}{31}
\indexentry{condensed detachment!and first-order logic|hyperpage}{31}
\indexentry{unification|hyperpage}{31}
\indexentry{substitution!variable|hyperpage}{31}
\indexentry{variable substitution|hyperpage}{31}
\indexentry{Robinson's resolution principle|hyperpage}{31}
\indexentry{first-order logic|hyperpage}{31}
\indexentry{first-order logic|hyperpage}{31}
\indexentry{category theory|hyperpage}{31}
\indexentry{cardinal, inaccessible|hyperpage}{31}
\indexentry{Metamath|hyperpage}{31}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{31}
\indexentry{Herrlich, Horst|hyperpage}{31}
\indexentry{Blass, Andrea|hyperpage}{31}
\indexentry{metatheorem|hyperpage}{32}
\indexentry{metalogical completeness|hyperpage}{32}
\indexentry{Megill, Norman|hyperpage}{32}
\indexentry{Monk, J. Donald|hyperpage}{32}
\indexentry{Tarski, Alfred|hyperpage}{32}
\indexentry{distinct variables|hyperpage}{32}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{32}
\indexentry{formal proof|hyperpage}{32}
\indexentry{free variable|hyperpage}{32}
\indexentry{bound variable|hyperpage}{32}
\indexentry{proper substitution|hyperpage}{32}
\indexentry{substitution!proper|hyperpage}{32}
\indexentry{implicit axiom|hyperpage}{32}
\indexentry{empty domain|hyperpage}{32}
\indexentry{free logic|hyperpage}{32}
\indexentry{Leblanc, Hugues|hyperpage}{32}
\indexentry{Zermelo-Fraenkel set theory|hyperpage}{32}
\indexentry{Axiom of the Null Set|hyperpage}{32}
\indexentry{Axiom of Infinity|hyperpage}{32}
\indexentry{Metamath!installation|hyperpage}{33}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{33}
\indexentry{text editor|hyperpage}{33}
\indexentry{ascii@{\sc ascii}|hyperpage}{33}
\indexentry{word processor|hyperpage}{33}
\indexentry{Word (Microsoft)|hyperpage}{33}
\indexentry{plain text|hyperpage}{33}
\indexentry{printers|hyperpage}{33}
\indexentry{monospaced font|hyperpage}{33}
\indexentry{Courier font|hyperpage}{33}
\indexentry{Monaco font|hyperpage}{33}
\indexentry{latex@{\LaTeX}|hyperpage}{34}
\indexentry{Metamath|hyperpage}{34}
\indexentry{number theory|hyperpage}{34}
\indexentry{Mendelson, Elliot|hyperpage}{34}
\indexentry{formal proof|hyperpage}{34}
\indexentry{axiom|hyperpage}{34}
\indexentry{syntax rules|hyperpage}{34}
\indexentry{term|hyperpage}{34}
\indexentry{metavariable|hyperpage}{34}
\indexentry{well-formed formula (wff)|hyperpage}{34}
\indexentry{implication ($\rightarrow$)|hyperpage}{34}
\indexentry{axiom|hyperpage}{34}
\indexentry{theorem|hyperpage}{34}
\indexentry{operator precedence|hyperpage}{35}
\indexentry{axiom|hyperpage}{35}
\indexentry{axiom scheme|hyperpage}{35}
\indexentry{theorem|hyperpage}{35}
\indexentry{inference rule|hyperpage}{35}
\indexentry{modus ponens|hyperpage}{35}
\indexentry{proof|hyperpage}{35}
\indexentry{reverse Polish notation (RPN)|hyperpage}{35}
\indexentry{Metamath|hyperpage}{35}
\indexentry{theorem scheme|hyperpage}{35}
\indexentry{proof scheme|hyperpage}{35}
\indexentry{axiom|hyperpage}{36}
\indexentry{rule|hyperpage}{36}
\indexentry{modus ponens|hyperpage}{36}
\indexentry{theorem|hyperpage}{36}
\indexentry{axiom|hyperpage}{36}
\indexentry{formal proof|hyperpage}{36}
\indexentry{Mendelson, Elliot|hyperpage}{36}
\indexentry{formal proof|hyperpage}{36}
\indexentry{Rucker, Rudy|hyperpage}{36}
\indexentry{Hofstadter, Douglas R.|hyperpage}{36}
\indexentry{formal proof|hyperpage}{36}
\indexentry{axiom|hyperpage}{36}
\indexentry{term|hyperpage}{37}
\indexentry{Metamath|hyperpage}{37}
\indexentry{well-formed formula (wff)|hyperpage}{37}
\indexentry{axiom|hyperpage}{37}
\indexentry{formal proof|hyperpage}{37}
\indexentry{proof step|hyperpage}{37}
\indexentry{substitution!variable|hyperpage}{37}
\indexentry{variable substitution|hyperpage}{37}
\indexentry{\texttt{show proof} command|hyperpage}{37}
\indexentry{Metamath|hyperpage}{37}
\indexentry{metavariable|hyperpage}{37}
\indexentry{metavariable|hyperpage}{38}
\indexentry{database|hyperpage}{38}
\indexentry{Metamath|hyperpage}{38}
\indexentry{token|hyperpage}{38}
\indexentry{keyword|hyperpage}{38}
\indexentry{\texttt{\$(} and \texttt{\$)} auxiliary keywords|hyperpage}{38}
\indexentry{\texttt{\$c} statement|hyperpage}{38}
\indexentry{\texttt{\$v} statement|hyperpage}{38}
\indexentry{\texttt{\$e} statement|hyperpage}{38}
\indexentry{\texttt{\$f} statement|hyperpage}{38}
\indexentry{\texttt{\$a} statement|hyperpage}{38}
\indexentry{\texttt{\$p} statement|hyperpage}{38}
\indexentry{\texttt{\$.}\ keyword|hyperpage}{38}
\indexentry{constant declaration|hyperpage}{38}
\indexentry{variable declaration|hyperpage}{38}
\indexentry{math symbol|hyperpage}{38}
\indexentry{turnstile ({$\,\vdash$})|hyperpage}{38}
\indexentry{axiom|hyperpage}{38}
\indexentry{theorem|hyperpage}{38}
\indexentry{constant|hyperpage}{38}
\indexentry{variable|hyperpage}{39}
\indexentry{constant declaration|hyperpage}{39}
\indexentry{variable declaration|hyperpage}{39}
\indexentry{metavariable|hyperpage}{39}
\indexentry{substitution!variable|hyperpage}{39}
\indexentry{variable substitution|hyperpage}{39}
\indexentry{\texttt{\$c} statement|hyperpage}{39}
\indexentry{\texttt{\$v} statement|hyperpage}{39}
\indexentry{math symbol|hyperpage}{39}
\indexentry{redeclaration of symbols|hyperpage}{39}
\indexentry{\texttt{\$f} statement|hyperpage}{39}
\indexentry{\texttt{\$e} statement|hyperpage}{39}
\indexentry{hypothesis|hyperpage}{39}
\indexentry{variable-type hypothesis|hyperpage}{39}
\indexentry{logical hypothesis|hyperpage}{39}
\indexentry{floating hypothesis|hyperpage}{39}
\indexentry{essential hypothesis|hyperpage}{39}
\indexentry{\texttt{\$a} statement|hyperpage}{39}
\indexentry{axiomatic assertion|hyperpage}{39}
\indexentry{\texttt{\$p} statement|hyperpage}{39}
\indexentry{provable assertion|hyperpage}{39}
\indexentry{label|hyperpage}{39}
\indexentry{assertion|hyperpage}{39}
\indexentry{mandatory hypothesis|hyperpage}{39}
\indexentry{\texttt{\$f} statement|hyperpage}{39}
\indexentry{\texttt{\$e} statement|hyperpage}{39}
\indexentry{\texttt{show statement} command|hyperpage}{39}
\indexentry{\texttt{\$\char`\{} and \texttt{\$\char`\}} keywords|hyperpage}{39}
\indexentry{block|hyperpage}{39}
\indexentry{\texttt{\$p} statement|hyperpage}{39}
\indexentry{assertion|hyperpage}{39}
\indexentry{math symbol|hyperpage}{39}
\indexentry{\texttt{\$=} keyword|hyperpage}{39}
\indexentry{\texttt{\$.}\ keyword|hyperpage}{39}
\indexentry{hypothesis label|hyperpage}{40}
\indexentry{push|hyperpage}{40}
\indexentry{stack|hyperpage}{40}
\indexentry{RPN stack|hyperpage}{40}
\indexentry{assertion label|hyperpage}{40}
\indexentry{pop|hyperpage}{40}
\indexentry{substitution!variable|hyperpage}{40}
\indexentry{variable substitution|hyperpage}{40}
\indexentry{Metamath|hyperpage}{40}
\indexentry{assertion|hyperpage}{40}
\indexentry{constant|hyperpage}{40}
\indexentry{variable|hyperpage}{40}
\indexentry{Metamath|hyperpage}{40}
\indexentry{command line interface (CLI)|hyperpage}{40}
\indexentry{compressed proof|hyperpage}{40}
\indexentry{proof!compressed|hyperpage}{40}
\indexentry{normal proof|hyperpage}{40}
\indexentry{proof!normal|hyperpage}{40}
\indexentry{Metamath|hyperpage}{41}
\indexentry{command keyword|hyperpage}{41}
\indexentry{\texttt{read} command|hyperpage}{41}
\indexentry{Macintosh file names|hyperpage}{41}
\indexentry{file names!Macintosh|hyperpage}{41}
\indexentry{\texttt{verify proof} command|hyperpage}{41}
\indexentry{Unix file names|hyperpage}{41}
\indexentry{file names!Unix|hyperpage}{41}
\indexentry{label|hyperpage}{42}
\indexentry{\texttt{show labels} command|hyperpage}{42}
\indexentry{command qualifier|hyperpage}{42}
\indexentry{\texttt{show statement} command|hyperpage}{42}
\indexentry{mandatory hypothesis|hyperpage}{42}
\indexentry{RPN order|hyperpage}{42}
\indexentry{formal proof|hyperpage}{42}
\indexentry{\texttt{show proof} command|hyperpage}{42}
\indexentry{Lemmon-style proof|hyperpage}{43}
\indexentry{proof!Lemmon-style|hyperpage}{43}
\indexentry{tree-style proof|hyperpage}{43}
\indexentry{proof!tree-style|hyperpage}{43}
\indexentry{math symbol|hyperpage}{44}
\indexentry{formal proof|hyperpage}{44}
\indexentry{\texttt{\$f} statement|hyperpage}{45}
\indexentry{\texttt{show proof} command|hyperpage}{45}
\indexentry{\texttt{exit} command|hyperpage}{45}
\indexentry{Metamath|hyperpage}{45}
\indexentry{command line interface (CLI)|hyperpage}{45}
\indexentry{command keyword|hyperpage}{45}
\indexentry{\texttt{read} command|hyperpage}{45}
\indexentry{\texttt{submit} command|hyperpage}{45}
\indexentry{command keyword|hyperpage}{45}
\indexentry{label|hyperpage}{45}
\indexentry{math symbol|hyperpage}{45}
\indexentry{token|hyperpage}{45}
\indexentry{\texttt{help} command|hyperpage}{45}
\indexentry{\texttt{]}@\texttt{?}\ in command lines|hyperpage}{46}
\indexentry{token|hyperpage}{46}
\indexentry{Proof Assistant|hyperpage}{46}
\indexentry{source buffer|hyperpage}{46}
\indexentry{\texttt{read} command|hyperpage}{46}
\indexentry{\texttt{write source} command|hyperpage}{46}
\indexentry{\texttt{]}@\texttt{?}\ inside proofs|hyperpage}{46}
\indexentry{\texttt{\$=} keyword|hyperpage}{46}
\indexentry{\texttt{\$.}\ keyword|hyperpage}{46}
\indexentry{Metamath|hyperpage}{46}
\indexentry{formal proof|hyperpage}{46}
\indexentry{\texttt{show proof} command|hyperpage}{46}
\indexentry{Proof Assistant|hyperpage}{47}
\indexentry{theorem|hyperpage}{47}
\indexentry{substitution!variable|hyperpage}{47}
\indexentry{variable substitution|hyperpage}{47}
\indexentry{unification|hyperpage}{47}
\indexentry{\texttt{prove} command|hyperpage}{47}
\indexentry{Proof Assistant|hyperpage}{47}
\indexentry{\texttt{show new{\char`\_}proof} command|hyperpage}{47}
\indexentry{\texttt{assign} command|hyperpage}{48}
\indexentry{temporary variable|hyperpage}{48}
\indexentry{Proof Assistant|hyperpage}{48}
\indexentry{formal proof|hyperpage}{48}
\indexentry{MIU-system|hyperpage}{49}
\indexentry{\texttt{set empty{\char`\_}substitution} command|hyperpage}{49}
\indexentry{ambiguous unification|hyperpage}{49}
\indexentry{unification!ambiguous|hyperpage}{49}
\indexentry{substitution!variable|hyperpage}{49}
\indexentry{variable substitution|hyperpage}{49}
\indexentry{Proof Assistant|hyperpage}{51}
\indexentry{\texttt{save new{\char`\_}proof} command|hyperpage}{52}
\indexentry{normal proof|hyperpage}{52}
\indexentry{proof!normal|hyperpage}{52}
\indexentry{compressed proof|hyperpage}{52}
\indexentry{proof!compressed|hyperpage}{52}
\indexentry{\texttt{show proof} command|hyperpage}{52}
\indexentry{Proof Assistant|hyperpage}{52}
\indexentry{mandatory hypothesis|hyperpage}{53}
\indexentry{\texttt{show statement} command|hyperpage}{53}
\indexentry{\texttt{minimize{\char`\_}with} command|hyperpage}{53}
\indexentry{Rucker, Rudy|hyperpage}{55}
\indexentry{axiom|hyperpage}{55}
\indexentry{theorem|hyperpage}{55}
\indexentry{Metamath|hyperpage}{55}
\indexentry{propositional calculus|hyperpage}{56}
\indexentry{sentential logic|hyperpage}{56}
\indexentry{first-order logic|hyperpage}{56}
\indexentry{quantifier theory|hyperpage}{56}
\indexentry{predicate calculus|hyperpage}{56}
\indexentry{Zermelo-Fraenkel set theory|hyperpage}{56}
\indexentry{set theory|hyperpage}{56}
\indexentry{axioms of logic|hyperpage}{56}
\indexentry{variable!in predicate calculus|hyperpage}{56}
\indexentry{propositional calculus|hyperpage}{56}
\indexentry{predicate calculus|hyperpage}{56}
\indexentry{set theory|hyperpage}{56}
\indexentry{empty set|hyperpage}{56}
\indexentry{integer|hyperpage}{56}
\indexentry{set union|hyperpage}{56}
\indexentry{set intersection|hyperpage}{56}
\indexentry{infinite set|hyperpage}{56}
\indexentry{natural number|hyperpage}{56}
\indexentry{brace notation|hyperpage}{56}
\indexentry{class abstraction|hyperpage}{56}
\indexentry{abstraction class|hyperpage}{56}
\indexentry{stylized epsilon ($\in$)|hyperpage}{57}
\indexentry{omega ($\omega$)|hyperpage}{57}
\indexentry{integer|hyperpage}{57}
\indexentry{rational number|hyperpage}{57}
\indexentry{real number|hyperpage}{57}
\indexentry{variable!in set theory|hyperpage}{57}
\indexentry{axiom|hyperpage}{57}
\indexentry{theorem|hyperpage}{57}
\indexentry{axioms for mathematics|hyperpage}{58}
\indexentry{Metamath|hyperpage}{58}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{58}
\indexentry{propositional calculus|hyperpage}{58}
\indexentry{well-formed formula (wff)|hyperpage}{58}
\indexentry{implication ($\rightarrow$)|hyperpage}{58}
\indexentry{negation ($\lnot$)|hyperpage}{58}
\indexentry{axioms of propositional calculus|hyperpage}{58}
\indexentry{well-formed formula (wff)|hyperpage}{58}
\indexentry{Meredith, C. A.|hyperpage}{58}
\indexentry{axiom scheme|hyperpage}{59}
\indexentry{theorem|hyperpage}{59}
\indexentry{rule|hyperpage}{59}
\indexentry{modus ponens|hyperpage}{59}
\indexentry{theorem|hyperpage}{59}
\indexentry{Metamath|hyperpage}{59}
\indexentry{tautology|hyperpage}{59}
\indexentry{truth table|hyperpage}{59}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{59}
\indexentry{predicate calculus|hyperpage}{59}
\indexentry{variable!in predicate calculus|hyperpage}{59}
\indexentry{individual variable|hyperpage}{59}
\indexentry{universal quantifier ($\forall$)|hyperpage}{60}
\indexentry{equality ($=$)|hyperpage}{60}
\indexentry{stylized epsilon ($\in$)|hyperpage}{60}
\indexentry{Metamath|hyperpage}{60}
\indexentry{metavariable|hyperpage}{60}
\indexentry{math symbol|hyperpage}{60}
\indexentry{well-formed formula (wff)|hyperpage}{60}
\indexentry{axioms of predicate calculus|hyperpage}{60}
\indexentry{well-formed formula (wff)|hyperpage}{60}
\indexentry{Metamath|hyperpage}{60}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{60}
\indexentry{free variable|hyperpage}{60}
\indexentry{proper substitution|hyperpage}{60}
\indexentry{substitution!proper|hyperpage}{60}
\indexentry{Hamilton, Alan G.|hyperpage}{60}
\indexentry{theorem|hyperpage}{61}
\indexentry{rule of generalization|hyperpage}{61}
\indexentry{decision procedure|hyperpage}{61}
\indexentry{automated theorem proving|hyperpage}{61}
\indexentry{axioms of equality|hyperpage}{61}
\indexentry{equality ($=$)|hyperpage}{61}
\indexentry{free variable|hyperpage}{61}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{61}
\indexentry{Zermelo-Fraenkel set theory|hyperpage}{61}
\indexentry{set theory|hyperpage}{61}
\indexentry{Metamath|hyperpage}{61}
\indexentry{variable!in set theory|hyperpage}{61}
\indexentry{object|hyperpage}{61}
\indexentry{set|hyperpage}{61}
\indexentry{element|hyperpage}{61}
\indexentry{collection|hyperpage}{61}
\indexentry{family|hyperpage}{61}
\indexentry{member|hyperpage}{61}
\indexentry{subset|hyperpage}{62}
\indexentry{Venn diagram|hyperpage}{62}
\indexentry{axioms of set theory|hyperpage}{62}
\indexentry{Axiom of Extensionality|hyperpage}{62}
\indexentry{Axiom of Pairing|hyperpage}{62}
\indexentry{Axiom of Power Sets|hyperpage}{62}
\indexentry{Axiom of the Null Set|hyperpage}{62}
\indexentry{Axiom of Union|hyperpage}{62}
\indexentry{Axiom of Regularity|hyperpage}{62}
\indexentry{Axiom of Infinity|hyperpage}{62}
\indexentry{Axiom of Separation|hyperpage}{62}
\indexentry{Axiom of Replacement|hyperpage}{62}
\indexentry{disjoint sets|hyperpage}{62}
\indexentry{Axiom of Choice|hyperpage}{62}
\indexentry{ZFC set theory|hyperpage}{63}
\indexentry{axiom scheme|hyperpage}{63}
\indexentry{well-formed formula (wff)|hyperpage}{63}
\indexentry{Metamath|hyperpage}{63}
\indexentry{free variable|hyperpage}{63}
\indexentry{proper substitution|hyperpage}{63}
\indexentry{substitution!proper|hyperpage}{63}
\indexentry{Metamath|hyperpage}{63}
\indexentry{substitution!variable|hyperpage}{63}
\indexentry{variable substitution|hyperpage}{63}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{63}
\indexentry{\texttt{show statement} command|hyperpage}{63}
\indexentry{disjoint variables|hyperpage}{63}
\indexentry{\texttt{\$d} statement|hyperpage}{63}
\indexentry{distinct variables|hyperpage}{63}
\indexentry{substitution!variable|hyperpage}{63}
\indexentry{variable substitution|hyperpage}{63}
\indexentry{function!in predicate calculus|hyperpage}{63}
\indexentry{constant!in predicate calculus|hyperpage}{63}
\indexentry{metalogic|hyperpage}{64}
\indexentry{axioms in \texttt{set.mm}|hyperpage}{64}
\indexentry{Megill, Norman|hyperpage}{64}
\indexentry{axioms of propositional calculus|hyperpage}{64}
\indexentry{modus ponens|hyperpage}{64}
\indexentry{axioms of predicate calculus|hyperpage}{64}
\indexentry{rule of generalization|hyperpage}{64}
\indexentry{axioms of equality|hyperpage}{64}
\indexentry{\texttt{\$d} statement|hyperpage}{65}
\indexentry{distinct variables|hyperpage}{65}
\indexentry{\texttt{\$d} statement|hyperpage}{65}
\indexentry{distinct variables|hyperpage}{65}
\indexentry{axioms of set theory|hyperpage}{65}
\indexentry{conjunction ($\wedge$)|hyperpage}{65}
\indexentry{logical {\sc and} ($\wedge$)|hyperpage}{65}
\indexentry{logical equivalence ($\leftrightarrow$)|hyperpage}{65}
\indexentry{biconditional ($\leftrightarrow$)|hyperpage}{65}
\indexentry{existential quantifier ($\exists$)|hyperpage}{65}
\indexentry{distinct variables|hyperpage}{65}
\indexentry{\texttt{\$d} statement|hyperpage}{65}
\indexentry{Axiom of Extensionality|hyperpage}{65}
\indexentry{Axiom of Replacement|hyperpage}{65}
\indexentry{Axiom of Union|hyperpage}{65}
\indexentry{Axiom of Power Sets|hyperpage}{65}
\indexentry{Axiom of Regularity|hyperpage}{65}
\indexentry{Axiom of Infinity|hyperpage}{66}
\indexentry{Axiom of Choice|hyperpage}{66}
\indexentry{definition|hyperpage}{66}
\indexentry{omega ($\omega$)|hyperpage}{66}
\indexentry{natural number|hyperpage}{66}
\indexentry{natural number|hyperpage}{66}
\indexentry{Peano's postulates|hyperpage}{66}
\indexentry{creative definition|hyperpage}{67}
\indexentry{definition!creative|hyperpage}{67}
\indexentry{definition!eliminability|hyperpage}{67}
\indexentry{definiendum|hyperpage}{67}
\indexentry{definiens|hyperpage}{67}
\indexentry{dummy variable!in definitions|hyperpage}{67}
\indexentry{effectively bound variable|hyperpage}{67}
\indexentry{qualifying expression|hyperpage}{67}
\indexentry{logical equivalence ($\leftrightarrow$)|hyperpage}{67}
\indexentry{biconditional ($\leftrightarrow$)|hyperpage}{67}
\indexentry{equality ($=$)|hyperpage}{67}
\indexentry{class|hyperpage}{67}
\indexentry{Axiom of Extensionality|hyperpage}{67}
\indexentry{\texttt{show statement} command|hyperpage}{68}
\indexentry{Takeuti, Gaisi|hyperpage}{68}
\indexentry{Quine, Willard Van Orman|hyperpage}{68}
\indexentry{Bell, J. L.|hyperpage}{68}
\indexentry{Enderton, Herbert B.|hyperpage}{68}
\indexentry{connective|hyperpage}{68}
\indexentry{constant|hyperpage}{68}
\indexentry{logical equivalence ($\leftrightarrow$)|hyperpage}{68}
\indexentry{biconditional ($\leftrightarrow$)|hyperpage}{68}
\indexentry{disjunction ($\vee$)|hyperpage}{69}
\indexentry{logical {\sc or} ($\vee$)|hyperpage}{69}
\indexentry{conjunction ($\wedge$)|hyperpage}{69}
\indexentry{logical {\sc and} ($\wedge$)|hyperpage}{69}
\indexentry{existential quantifier ($\exists$)|hyperpage}{69}
\indexentry{proper substitution|hyperpage}{69}
\indexentry{substitution!proper|hyperpage}{69}
\indexentry{postfix connective|hyperpage}{69}
\indexentry{infix connective|hyperpage}{69}
\indexentry{existential uniqueness quantifier ($\exists "!$)|hyperpage}{70}
\indexentry{class|hyperpage}{70}
\indexentry{abstraction class|hyperpage}{70}
\indexentry{class abstraction|hyperpage}{70}
\indexentry{proper class|hyperpage}{70}
\indexentry{class!proper|hyperpage}{70}
\indexentry{abstraction class|hyperpage}{70}
\indexentry{class abstraction|hyperpage}{70}
\indexentry{prefix connective|hyperpage}{70}
\indexentry{Polish notation|hyperpage}{70}
\indexentry{class equality|hyperpage}{71}
\indexentry{Axiom of Extensionality|hyperpage}{71}
\indexentry{class membership|hyperpage}{71}
\indexentry{universal quantifier ($\forall$)!restricted|hyperpage}{71}
\indexentry{existential quantifier ($\exists$)!restricted|hyperpage}{71}
\indexentry{universal class ($V$)|hyperpage}{71}
\indexentry{subclass|hyperpage}{72}
\indexentry{subset|hyperpage}{72}
\indexentry{union|hyperpage}{72}
\indexentry{intersection|hyperpage}{72}
\indexentry{class difference|hyperpage}{72}
\indexentry{set difference|hyperpage}{72}
\indexentry{empty set|hyperpage}{72}
\indexentry{null set|hyperpage}{72}
\indexentry{power set|hyperpage}{72}
\indexentry{power class|hyperpage}{72}
\indexentry{singleton|hyperpage}{72}
\indexentry{unordered pair|hyperpage}{72}
\indexentry{pair|hyperpage}{72}
\indexentry{unordered triple|hyperpage}{72}
\indexentry{Kuratowski, Kazimierz|hyperpage}{72}
\indexentry{ordered pair|hyperpage}{72}
\indexentry{union|hyperpage}{73}
\indexentry{intersection|hyperpage}{73}
\indexentry{transitive class|hyperpage}{73}
\indexentry{transitive set|hyperpage}{73}
\indexentry{binary relation|hyperpage}{73}
\indexentry{abstraction class!of ordered pairs|hyperpage}{73}
\indexentry{epsilon relation|hyperpage}{73}
\indexentry{founded relation|hyperpage}{73}
\indexentry{iff|hyperpage}{73}
\indexentry{well-ordering|hyperpage}{73}
\indexentry{ordinal predicate|hyperpage}{74}
\indexentry{ordinal number|hyperpage}{74}
\indexentry{limit ordinal|hyperpage}{74}
\indexentry{successor|hyperpage}{74}
\indexentry{natural number|hyperpage}{74}
\indexentry{omega ($\omega$)|hyperpage}{74}
\indexentry{cross product|hyperpage}{74}
\indexentry{domain|hyperpage}{74}
\indexentry{range|hyperpage}{74}
\indexentry{restriction|hyperpage}{75}
\indexentry{image|hyperpage}{75}
\indexentry{composition|hyperpage}{75}
\indexentry{relation|hyperpage}{75}
\indexentry{function|hyperpage}{75}
\indexentry{one-to-one function|hyperpage}{75}
\indexentry{onto function|hyperpage}{75}
\indexentry{function value|hyperpage}{76}
\indexentry{operation|hyperpage}{76}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{76}
\indexentry{turnstile ({$\,\vdash$})|hyperpage}{76}
\indexentry{effectively not free|hyperpage}{76}
\indexentry{substitution!implicit|hyperpage}{77}
\indexentry{Axiom of Separation|hyperpage}{78}
\indexentry{Aussonderung|hyperpage}{78}
\indexentry{Axiom of the Null Set|hyperpage}{78}
\indexentry{Axiom of Pairing|hyperpage}{78}
\indexentry{Russell's paradox|hyperpage}{78}
\indexentry{Cantor's theorem|hyperpage}{79}
\indexentry{Burali-Forti paradox|hyperpage}{79}
\indexentry{Peano's postulates|hyperpage}{79}
\indexentry{successor|hyperpage}{79}
\indexentry{finite induction|hyperpage}{79}
\indexentry{mathematical induction|hyperpage}{79}
\indexentry{transfinite recursion|hyperpage}{79}
\indexentry{natural number|hyperpage}{80}
\indexentry{omega ($\omega$)|hyperpage}{80}
\indexentry{Axiom of Infinity|hyperpage}{80}
\indexentry{real and complex numbers!axioms for|hyperpage}{80}
\indexentry{operation|hyperpage}{80}
\indexentry{binary relation|hyperpage}{80}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{83}
\indexentry{well-formed formula (wff)|hyperpage}{83}
\indexentry{\texttt{\$f} statement|hyperpage}{83}
\indexentry{Metamath|hyperpage}{83}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{83}
\indexentry{command keyword|hyperpage}{83}
\indexentry{\texttt{read} command|hyperpage}{83}
\indexentry{Enderton, Herbert B.|hyperpage}{84}
\indexentry{\texttt{search} command|hyperpage}{84}
\indexentry{\texttt{search} command|hyperpage}{84}
\indexentry{\texttt{show statement} command|hyperpage}{84}
\indexentry{latex@{\LaTeX}|hyperpage}{85}
\indexentry{\texttt{show statement} command|hyperpage}{85}
\indexentry{optional variable|hyperpage}{85}
\indexentry{optional hypothesis|hyperpage}{85}
\indexentry{scope|hyperpage}{85}
\indexentry{dummy variable|hyperpage}{85}
\indexentry{\texttt{show proof} command|hyperpage}{85}
\indexentry{Hamilton, Alan G.|hyperpage}{86}
\indexentry{substitution!variable|hyperpage}{86}
\indexentry{variable substitution|hyperpage}{86}
\indexentry{\texttt{show proof} command|hyperpage}{86}
\indexentry{substitution!variable|hyperpage}{87}
\indexentry{variable substitution|hyperpage}{87}
\indexentry{conjunction ($\wedge$)|hyperpage}{87}
\indexentry{logical {\sc and} ($\wedge$)|hyperpage}{87}
\indexentry{\texttt{search} command|hyperpage}{88}
\indexentry{axiom|hyperpage}{88}
\indexentry{definition|hyperpage}{88}
\indexentry{hierarchy|hyperpage}{88}
\indexentry{\texttt{show trace{\char`\_}back} command|hyperpage}{88}
\indexentry{axiom vs.\ definition|hyperpage}{88}
\indexentry{axiom|hyperpage}{88}
\indexentry{definition|hyperpage}{88}
\indexentry{labels in \texttt{set.mm}|hyperpage}{88}
\indexentry{\texttt{\$a} statement|hyperpage}{89}
\indexentry{proof length|hyperpage}{89}
\indexentry{\texttt{show usage} command|hyperpage}{89}
\indexentry{Metamath!limitations of version 0.07.30|hyperpage}{89}
\indexentry{compact proof|hyperpage}{89}
\indexentry{local label|hyperpage}{90}
\indexentry{\texttt{save proof} command|hyperpage}{90}
\indexentry{Russell, Bertrand|hyperpage}{91}
\indexentry{Metamath|hyperpage}{91}
\indexentry{Metamath|hyperpage}{91}
\indexentry{Metamath|hyperpage}{91}
\indexentry{parsing Metamath|hyperpage}{92}
\indexentry{Metamath!specification|hyperpage}{92}
\indexentry{Hardy, G. H.|hyperpage}{92}
\indexentry{database|hyperpage}{92}
\indexentry{ascii@{\sc ascii}|hyperpage}{92}
\indexentry{special characters|hyperpage}{92}
\indexentry{token|hyperpage}{92}
\indexentry{white space|hyperpage}{92}
\indexentry{keyword|hyperpage}{92}
\indexentry{auxiliary keyword|hyperpage}{92}
\indexentry{Metamath!limitations of version 0.07.30|hyperpage}{92}
\indexentry{label|hyperpage}{93}
\indexentry{math symbol|hyperpage}{93}
\indexentry{\texttt{\$(} and \texttt{\$)} auxiliary keywords|hyperpage}{93}
\indexentry{comment|hyperpage}{93}
\indexentry{\texttt{\$[} and \texttt{\$]} auxiliary keywords|hyperpage}{93}
\indexentry{included file|hyperpage}{93}
\indexentry{file inclusion|hyperpage}{93}
\indexentry{scoping statement|hyperpage}{93}
\indexentry{block|hyperpage}{93}
\indexentry{block!outermost|hyperpage}{93}
\indexentry{\texttt{\$v} statement|hyperpage}{93}
\indexentry{\texttt{\$c} statement|hyperpage}{93}
\indexentry{declaration|hyperpage}{93}
\indexentry{variable!Metamath|hyperpage}{93}
\indexentry{constant|hyperpage}{93}
\indexentry{active math symbol|hyperpage}{93}
\indexentry{redeclaration of symbols|hyperpage}{94}
\indexentry{\texttt{\$f} statement|hyperpage}{94}
\indexentry{\texttt{\$e} statement|hyperpage}{94}
\indexentry{hypothesis|hyperpage}{94}
\indexentry{\texttt{\$d} statement!simple|hyperpage}{94}
\indexentry{\texttt{\$d} statement!compound|hyperpage}{94}
\indexentry{disjoint-variable restriction|hyperpage}{94}
\indexentry{\texttt{\$a} statement|hyperpage}{94}
\indexentry{\texttt{\$p} statement|hyperpage}{94}
\indexentry{assertion|hyperpage}{94}
\indexentry{active statement|hyperpage}{94}
\indexentry{mandatory variable|hyperpage}{94}
\indexentry{mandatory hypothesis|hyperpage}{94}
\indexentry{mandatory disjoint-variable restriction|hyperpage}{94}
\indexentry{proof!Metamath|hyperpage}{95}
\indexentry{expression|hyperpage}{95}
\indexentry{substitution map|hyperpage}{95}
\indexentry{substitution!variable|hyperpage}{95}
\indexentry{variable substitution|hyperpage}{95}
\indexentry{stack|hyperpage}{95}
\indexentry{RPN stack|hyperpage}{95}
\indexentry{compressed proof|hyperpage}{95}
\indexentry{proof!compressed|hyperpage}{95}
\indexentry{\texttt{\$d} statement|hyperpage}{95}
\indexentry{Metamath|hyperpage}{96}
\indexentry{source file|hyperpage}{96}
\indexentry{ascii@{\sc ascii}|hyperpage}{96}
\indexentry{token|hyperpage}{96}
\indexentry{white space|hyperpage}{96}
\indexentry{printable character|hyperpage}{96}
\indexentry{database|hyperpage}{96}
\indexentry{keyword|hyperpage}{96}
\indexentry{label|hyperpage}{96}
\indexentry{math symbol|hyperpage}{96}
\indexentry{symbol|hyperpage}{96}
\indexentry{basic keyword|hyperpage}{96}
\indexentry{\texttt{\$c} statement|hyperpage}{96}
\indexentry{\texttt{\$v} statement|hyperpage}{96}
\indexentry{\texttt{\$e} statement|hyperpage}{96}
\indexentry{\texttt{\$f} statement|hyperpage}{96}
\indexentry{\texttt{\$d} statement|hyperpage}{96}
\indexentry{\texttt{\$a} statement|hyperpage}{96}
\indexentry{\texttt{\$p} statement|hyperpage}{96}
\indexentry{\texttt{\$=} keyword|hyperpage}{96}
\indexentry{\texttt{\$.}\ keyword|hyperpage}{96}
\indexentry{\texttt{\$\char`\{} and \texttt{\$\char`\}} keywords|hyperpage}{96}
\indexentry{basic language|hyperpage}{96}
\indexentry{auxiliary keyword|hyperpage}{96}
\indexentry{Metamath|hyperpage}{97}
\indexentry{extended language|hyperpage}{97}
\indexentry{source file|hyperpage}{97}
\indexentry{\texttt{\$(} and \texttt{\$)} auxiliary keywords|hyperpage}{97}
\indexentry{\texttt{\$[} and \texttt{\$]} auxiliary keywords|hyperpage}{97}
\indexentry{keyword|hyperpage}{97}
\indexentry{token|hyperpage}{97}
\indexentry{keyword|hyperpage}{97}
\indexentry{Metamath|hyperpage}{97}
\indexentry{token|hyperpage}{97}
\indexentry{math symbol|hyperpage}{97}
\indexentry{Metamath|hyperpage}{97}
\indexentry{turnstile ({$\,\vdash$})|hyperpage}{98}
\indexentry{axiom|hyperpage}{98}
\indexentry{definition|hyperpage}{98}
\indexentry{\texttt{\$a} statement|hyperpage}{98}
\indexentry{token|hyperpage}{98}
\indexentry{math symbol|hyperpage}{98}
\indexentry{\texttt{open tex} command|hyperpage}{98}
\indexentry{latex@{\LaTeX}|hyperpage}{98}
\indexentry{\texttt{\$t} comment|hyperpage}{98}
\indexentry{typesetting comment|hyperpage}{98}
\indexentry{token|hyperpage}{98}
\indexentry{label|hyperpage}{98}
\indexentry{Metamath|hyperpage}{98}
\indexentry{label declaration|hyperpage}{98}
\indexentry{\texttt{\$e} statement|hyperpage}{98}
\indexentry{\texttt{\$f} statement|hyperpage}{98}
\indexentry{\texttt{\$a} statement|hyperpage}{98}
\indexentry{\texttt{\$p} statement|hyperpage}{98}
\indexentry{label reference|hyperpage}{98}
\indexentry{\texttt{\$=} keyword|hyperpage}{98}
\indexentry{\texttt{\$.}\ keyword|hyperpage}{98}
\indexentry{label sequence|hyperpage}{98}
\indexentry{proof|hyperpage}{98}
\indexentry{constant|hyperpage}{99}
\indexentry{variable|hyperpage}{99}
\indexentry{expression|hyperpage}{99}
\indexentry{Metamath|hyperpage}{99}
\indexentry{basic language|hyperpage}{99}
\indexentry{math symbol|hyperpage}{99}
\indexentry{constant|hyperpage}{99}
\indexentry{variable|hyperpage}{99}
\indexentry{substitution!variable|hyperpage}{99}
\indexentry{variable substitution|hyperpage}{99}
\indexentry{variable type|hyperpage}{99}
\indexentry{type|hyperpage}{99}
\indexentry{metavariable|hyperpage}{99}
\indexentry{\texttt{\$c} statement|hyperpage}{99}
\indexentry{constant declaration|hyperpage}{99}
\indexentry{\texttt{\$v} statement|hyperpage}{99}
\indexentry{variable declaration|hyperpage}{99}
\indexentry{constant declaration|hyperpage}{99}
\indexentry{\texttt{\$c} statement|hyperpage}{99}
\indexentry{variable declaration|hyperpage}{99}
\indexentry{\texttt{\$v} statement|hyperpage}{99}
\indexentry{simple declaration|hyperpage}{99}
\indexentry{token|hyperpage}{99}
\indexentry{math symbol|hyperpage}{99}
\indexentry{compound declaration|hyperpage}{100}
\indexentry{\texttt{\$c} statement|hyperpage}{100}
\indexentry{\texttt{\$v} statement|hyperpage}{100}
\indexentry{\texttt{\$d} statement|hyperpage}{100}
\indexentry{active math symbol|hyperpage}{100}
\indexentry{scope|hyperpage}{100}
\indexentry{distinct variables|hyperpage}{100}
\indexentry{non-trivial theory|hyperpage}{100}
\indexentry{free vs.\ bound variable|hyperpage}{100}
\indexentry{proper substitution|hyperpage}{100}
\indexentry{substitution!proper|hyperpage}{100}
\indexentry{free variable|hyperpage}{100}
\indexentry{bound variable|hyperpage}{100}
\indexentry{\texttt{\$d} statement|hyperpage}{101}
\indexentry{disjoint variables|hyperpage}{101}
\indexentry{\texttt{\$d} statement|hyperpage}{101}
\indexentry{empty substitution|hyperpage}{101}
\indexentry{variable|hyperpage}{101}
\indexentry{variable!in ordinary mathematics|hyperpage}{101}
\indexentry{metavariable|hyperpage}{101}
\indexentry{\texttt{\$d} statement|hyperpage}{102}
\indexentry{\texttt{\$d} statement|hyperpage}{102}
\indexentry{Metamath|hyperpage}{103}
\indexentry{label|hyperpage}{103}
\indexentry{distinct variables|hyperpage}{103}
\indexentry{\texttt{\$d} statement|hyperpage}{104}
\indexentry{\texttt{\$a} statement|hyperpage}{104}
\indexentry{\texttt{\$d} statement|hyperpage}{105}
\indexentry{dummy variable!eliminating|hyperpage}{105}
\indexentry{Andr{\'{e}}ka, H.|hyperpage}{105}
\indexentry{Megill, Norman|hyperpage}{105}
\indexentry{\texttt{\$e} statement|hyperpage}{105}
\indexentry{\texttt{\$f} statement|hyperpage}{105}
\indexentry{floating hypothesis|hyperpage}{105}
\indexentry{essential hypothesis|hyperpage}{105}
\indexentry{variable-type hypothesis|hyperpage}{105}
\indexentry{logical hypothesis|hyperpage}{105}
\indexentry{hypothesis|hyperpage}{105}
\indexentry{\texttt{\$f} statement|hyperpage}{105}
\indexentry{\texttt{\$d} statement|hyperpage}{105}
\indexentry{floating hypothesis|hyperpage}{105}
\indexentry{essential hypothesis|hyperpage}{105}
\indexentry{\texttt{\$e} statement|hyperpage}{105}
\indexentry{\texttt{\$f} statement|hyperpage}{105}
\indexentry{label|hyperpage}{105}
\indexentry{variable type|hyperpage}{105}
\indexentry{type|hyperpage}{105}
\indexentry{theorem|hyperpage}{106}
\indexentry{free variable|hyperpage}{106}
\indexentry{inference|hyperpage}{106}
\indexentry{Metamath|hyperpage}{106}
\indexentry{\texttt{\$p} statement|hyperpage}{106}
\indexentry{\texttt{\$e} statement|hyperpage}{106}
\indexentry{\texttt{\$f} statement|hyperpage}{106}
\indexentry{turnstile ({$\,\vdash$})|hyperpage}{106}
\indexentry{assertion|hyperpage}{106}
\indexentry{\texttt{\$a} statement|hyperpage}{106}
\indexentry{\texttt{\$p} statement|hyperpage}{106}
\indexentry{assertion|hyperpage}{106}
\indexentry{axiomatic assertion|hyperpage}{106}
\indexentry{provable assertion|hyperpage}{106}
\indexentry{\texttt{\$a} statement|hyperpage}{106}
\indexentry{\texttt{\$a} statement|hyperpage}{107}
\indexentry{\texttt{\$p} statement|hyperpage}{107}
\indexentry{\texttt{\$=} keyword|hyperpage}{107}
\indexentry{label|hyperpage}{107}
\indexentry{axiom|hyperpage}{107}
\indexentry{definition|hyperpage}{107}
\indexentry{\texttt{\$a} statement|hyperpage}{107}
\indexentry{\texttt{\$p} statement|hyperpage}{107}
\indexentry{axiom|hyperpage}{107}
\indexentry{Metamath|hyperpage}{107}
\indexentry{formal logic|hyperpage}{107}
\indexentry{\texttt{\$a} statement|hyperpage}{107}
\indexentry{axiom vs.\ definition|hyperpage}{107}
\indexentry{axiom|hyperpage}{107}
\indexentry{definition|hyperpage}{107}
\indexentry{label|hyperpage}{108}
\indexentry{\texttt{\$a} statement|hyperpage}{108}
\indexentry{axiom|hyperpage}{108}
\indexentry{rule|hyperpage}{108}
\indexentry{proper definition|hyperpage}{108}
\indexentry{definition!proper|hyperpage}{108}
\indexentry{\texttt{\$a} statement|hyperpage}{108}
\indexentry{frame|hyperpage}{108}
\indexentry{mandatory variable|hyperpage}{109}
\indexentry{mandatory hypothesis|hyperpage}{110}
\indexentry{RPN order|hyperpage}{110}
\indexentry{dummy variable|hyperpage}{110}
\indexentry{extended frame|hyperpage}{110}
\indexentry{optional variable|hyperpage}{110}
\indexentry{optional hypothesis|hyperpage}{110}
\indexentry{optional disjoint-variable restriction|hyperpage}{110}
\indexentry{\texttt{\$\char`\{} and \texttt{\$\char`\}} keywords|hyperpage}{111}
\indexentry{\texttt{\$\char`\{} and \texttt{\$\char`\}} keywords|hyperpage}{112}
\indexentry{scoping statement|hyperpage}{112}
\indexentry{block|hyperpage}{112}
\indexentry{\texttt{\$\char`\{} and \texttt{\$\char`\}} keywords|hyperpage}{112}
\indexentry{block|hyperpage}{112}
\indexentry{nested block|hyperpage}{112}
\indexentry{non-scoping statement|hyperpage}{112}
\indexentry{recursive definition|hyperpage}{112}
\indexentry{nesting level|hyperpage}{112}
\indexentry{\texttt{\$\char`\{} and \texttt{\$\char`\}} keywords|hyperpage}{112}
\indexentry{outermost block|hyperpage}{112}
\indexentry{active statement|hyperpage}{113}
\indexentry{\texttt{\$c} statement|hyperpage}{113}
\indexentry{\texttt{\$d} statement|hyperpage}{113}
\indexentry{\texttt{\$e} statement|hyperpage}{113}
\indexentry{\texttt{\$f} statement|hyperpage}{113}
\indexentry{\texttt{\$v} statement|hyperpage}{113}
\indexentry{\texttt{\$a} statement|hyperpage}{113}
\indexentry{\texttt{\$p} statement|hyperpage}{113}
\indexentry{outermost block|hyperpage}{113}
\indexentry{global statement|hyperpage}{113}
\indexentry{scope|hyperpage}{113}
\indexentry{math symbol|hyperpage}{113}
\indexentry{constant|hyperpage}{113}
\indexentry{variable|hyperpage}{113}
\indexentry{active math symbol|hyperpage}{113}
\indexentry{\texttt{\$c} statement|hyperpage}{113}
\indexentry{\texttt{\$v} statement|hyperpage}{113}
\indexentry{redeclaration of symbols|hyperpage}{113}
\indexentry{local variable|hyperpage}{113}
\indexentry{frames and scoping statements|hyperpage}{114}
\indexentry{proof!Metamath, description of|hyperpage}{114}
\indexentry{\texttt{\$p} statement|hyperpage}{114}
\indexentry{proof|hyperpage}{114}
\indexentry{\texttt{\$=} keyword|hyperpage}{114}
\indexentry{basic language|hyperpage}{114}
\indexentry{label sequence|hyperpage}{114}
\indexentry{\texttt{\$p} statement|hyperpage}{114}
\indexentry{\texttt{\$=} keyword|hyperpage}{114}
\indexentry{\texttt{verify proof} command|hyperpage}{114}
\indexentry{label reference|hyperpage}{114}
\indexentry{assertion|hyperpage}{114}
\indexentry{\texttt{\$a} statement|hyperpage}{114}
\indexentry{\texttt{\$f} statement|hyperpage}{114}
\indexentry{\texttt{\$e} statement|hyperpage}{114}
\indexentry{label|hyperpage}{115}
\indexentry{\texttt{\$a} statement|hyperpage}{115}
\indexentry{\texttt{\$p} statement|hyperpage}{115}
\indexentry{\texttt{\$f} statement|hyperpage}{115}
\indexentry{mandatory hypothesis|hyperpage}{115}
\indexentry{reverse Polish notation (RPN)|hyperpage}{115}
\indexentry{hypothesis label|hyperpage}{115}
\indexentry{assertion label|hyperpage}{115}
\indexentry{stack|hyperpage}{115}
\indexentry{RPN stack|hyperpage}{115}
\indexentry{push|hyperpage}{115}
\indexentry{mandatory hypothesis|hyperpage}{115}
\indexentry{substitution!variable|hyperpage}{115}
\indexentry{variable substitution|hyperpage}{115}
\indexentry{pop|hyperpage}{115}
\indexentry{well-formed formula (wff)|hyperpage}{116}
\indexentry{\texttt{\$p} statement|hyperpage}{117}
\indexentry{mandatory hypothesis|hyperpage}{117}
\indexentry{\texttt{show proof} command|hyperpage}{117}
\indexentry{tree-style proof|hyperpage}{117}
\indexentry{proof!tree-style|hyperpage}{117}
\indexentry{hypothesis association|hyperpage}{118}
\indexentry{label|hyperpage}{118}
\indexentry{\texttt{show proof} command|hyperpage}{118}
\indexentry{\texttt{\$d} statement|hyperpage}{118}
\indexentry{mandatory \texttt{\$d} statement|hyperpage}{118}
\indexentry{substitution!variable|hyperpage}{118}
\indexentry{variable substitution|hyperpage}{118}
\indexentry{Metamath|hyperpage}{118}
\indexentry{assertion label|hyperpage}{118}
\indexentry{mandatory hypothesis|hyperpage}{118}
\indexentry{stack|hyperpage}{118}
\indexentry{RPN stack|hyperpage}{118}
\indexentry{substitution!variable|hyperpage}{118}
\indexentry{variable substitution|hyperpage}{118}
\indexentry{unification|hyperpage}{118}
\indexentry{Proof Assistant|hyperpage}{119}
\indexentry{ambiguous unification|hyperpage}{119}
\indexentry{unification!ambiguous|hyperpage}{119}
\indexentry{extended language|hyperpage}{119}
\indexentry{white space|hyperpage}{119}
\indexentry{token|hyperpage}{119}
\indexentry{\texttt{\$(} and \texttt{\$)} auxiliary keywords|hyperpage}{119}
\indexentry{comment|hyperpage}{119}
\indexentry{\texttt{`} inside comments|hyperpage}{119}
\indexentry{\texttt{\char`\~} inside comments|hyperpage}{119}
\indexentry{markup notation|hyperpage}{119}
\indexentry{comments!markup notation|hyperpage}{119}
\indexentry{token|hyperpage}{119}
\indexentry{grave accent (\texttt{`})|hyperpage}{119}
\indexentry{latex@{\LaTeX}|hyperpage}{119}
\indexentry{\texttt{\$t} comment|hyperpage}{119}
\indexentry{typesetting comment|hyperpage}{119}
\indexentry{math mode|hyperpage}{119}
\indexentry{tilde (\texttt{\char`\~})|hyperpage}{119}
\indexentry{white space|hyperpage}{119}
\indexentry{Metamath!limitations of version 0.07.30|hyperpage}{119}
\indexentry{label mode|hyperpage}{120}
\indexentry{math symbol|hyperpage}{120}
\indexentry{math mode|hyperpage}{120}
\indexentry{grave accent (\texttt{`})|hyperpage}{120}
\indexentry{Metamath|hyperpage}{120}
\indexentry{white space|hyperpage}{120}
\indexentry{\texttt{\$t} comment|hyperpage}{120}
\indexentry{typesetting comment|hyperpage}{120}
\indexentry{Pierce's axiom|hyperpage}{120}
\indexentry{token|hyperpage}{120}
\indexentry{white space|hyperpage}{120}
\indexentry{Metamath!using as a math editor|hyperpage}{120}
\indexentry{label mode|hyperpage}{121}
\indexentry{tilde (\texttt{\char`\~})|hyperpage}{121}
\indexentry{Metamath|hyperpage}{121}
\indexentry{token|hyperpage}{121}
\indexentry{white space|hyperpage}{121}
\indexentry{\texttt{`} inside comments|hyperpage}{121}
\indexentry{\texttt{\char`\~} inside comments|hyperpage}{121}
\indexentry{markup notation|hyperpage}{121}
\indexentry{comments!markup notation|hyperpage}{121}
\indexentry{html generation@{\sc html} generation|hyperpage}{121}
\indexentry{\texttt{\char`\[}\ldots\texttt{]} inside comments|hyperpage}{121}
\indexentry{\texttt{\$t} comment|hyperpage}{121}
\indexentry{typesetting comment|hyperpage}{121}
\indexentry{\texttt{\char`\_} inside comments|hyperpage}{121}
\indexentry{error checking|hyperpage}{122}
\indexentry{\texttt{\$[} and \texttt{\$]} auxiliary keywords|hyperpage}{122}
\indexentry{included file|hyperpage}{122}
\indexentry{file inclusion|hyperpage}{122}
\indexentry{Metamath|hyperpage}{122}
\indexentry{source file|hyperpage}{122}
\indexentry{token|hyperpage}{122}
\indexentry{Macintosh file names|hyperpage}{123}
\indexentry{file names!Macintosh|hyperpage}{123}
\indexentry{outermost block|hyperpage}{123}
\indexentry{compressed proof|hyperpage}{123}
\indexentry{proof!compressed|hyperpage}{123}
\indexentry{normal proof|hyperpage}{123}
\indexentry{proof!normal|hyperpage}{123}
\indexentry{Metamath|hyperpage}{123}
\indexentry{\texttt{\$=} keyword|hyperpage}{124}
\indexentry{mandatory hypothesis|hyperpage}{124}
\indexentry{white space|hyperpage}{124}
\indexentry{\texttt{save proof} command|hyperpage}{124}
\indexentry{\texttt{]}@\texttt{?}\ inside proofs|hyperpage}{124}
\indexentry{Proof Assistant|hyperpage}{124}
\indexentry{\texttt{save new{\char`\_}proof} command|hyperpage}{124}
\indexentry{\texttt{\$p} statement|hyperpage}{124}
\indexentry{\texttt{\$=} keyword|hyperpage}{124}
\indexentry{\texttt{]}@\texttt{?}\ inside proofs|hyperpage}{124}
\indexentry{\texttt{verify proof} command|hyperpage}{124}
\indexentry{compressed proof|hyperpage}{124}
\indexentry{proof!compressed|hyperpage}{124}
\indexentry{Metamath|hyperpage}{125}
\indexentry{axiom vs.\ definition|hyperpage}{125}
\indexentry{axiom|hyperpage}{125}
\indexentry{definition|hyperpage}{125}
\indexentry{\texttt{\$a} statement|hyperpage}{125}
\indexentry{theorem|hyperpage}{125}
\indexentry{Behnke, H.|hyperpage}{125}
\indexentry{proper definition|hyperpage}{125}
\indexentry{definition!proper|hyperpage}{125}
\indexentry{creative definition|hyperpage}{125}
\indexentry{definition!creative|hyperpage}{125}
\indexentry{Nemesszeghy, E. Z.|hyperpage}{125}
\indexentry{Le\'{s}niewski, S.|hyperpage}{125}
\indexentry{Lejewski, Czeslaw|hyperpage}{125}
\indexentry{disjunction ($\vee$)|hyperpage}{125}
\indexentry{well-formed formula (wff)|hyperpage}{125}
\indexentry{definition|hyperpage}{126}
\indexentry{axiom vs.\ definition|hyperpage}{126}
\indexentry{axiom|hyperpage}{126}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{126}
\indexentry{Goodstein, R. L.|hyperpage}{126}
\indexentry{intuitionism|hyperpage}{126}
\indexentry{Quine, Willard Van Orman|hyperpage}{126}
\indexentry{metalogic|hyperpage}{126}
\indexentry{successor|hyperpage}{126}
\indexentry{recursive definition|hyperpage}{126}
\indexentry{Robinson, T. Thacher|hyperpage}{126}
\indexentry{natural number|hyperpage}{127}
\indexentry{addition|hyperpage}{127}
\indexentry{recursive definition|hyperpage}{127}
\indexentry{ordinal addition|hyperpage}{127}
\indexentry{ordinal addition|hyperpage}{127}
\indexentry{addition!of ordinals|hyperpage}{127}
\indexentry{abstraction class!of nested ordered pairs|hyperpage}{127}
\indexentry{recursion operator|hyperpage}{127}
\indexentry{Metamath!commands|hyperpage}{129}
\indexentry{Unix file names|hyperpage}{129}
\indexentry{file names!Unix|hyperpage}{129}
\indexentry{Unix file names|hyperpage}{129}
\indexentry{file names!Unix|hyperpage}{129}
\indexentry{\texttt{exit} command|hyperpage}{131}
\indexentry{Proof Assistant|hyperpage}{131}
\indexentry{\texttt{open log} command|hyperpage}{131}
\indexentry{Metamath!bugs|hyperpage}{131}
\indexentry{\texttt{close log} command|hyperpage}{132}
\indexentry{\texttt{submit} command|hyperpage}{132}
\indexentry{\texttt{erase} command|hyperpage}{132}
\indexentry{\texttt{set echo} command|hyperpage}{132}
\indexentry{\texttt{set scroll} command|hyperpage}{132}
\indexentry{\texttt{set width} command|hyperpage}{132}
\indexentry{latex@{\LaTeX}!characters per line|hyperpage}{133}
\indexentry{\texttt{set height} command|hyperpage}{133}
\indexentry{\texttt{beep} command|hyperpage}{133}
\indexentry{\texttt{more} command|hyperpage}{133}
\indexentry{operating system command|hyperpage}{133}
\indexentry{Metamath!memory limits|hyperpage}{134}
\indexentry{token|hyperpage}{134}
\indexentry{\texttt{read} command|hyperpage}{134}
\indexentry{Unix file names|hyperpage}{134}
\indexentry{file names!Unix|hyperpage}{134}
\indexentry{\texttt{write source} command|hyperpage}{134}
\indexentry{database|hyperpage}{134}
\indexentry{source file|hyperpage}{134}
\indexentry{Metamath!limitations of version 0.07.30|hyperpage}{134}
\indexentry{\texttt{\$[} and \texttt{\$]} auxiliary keywords|hyperpage}{135}
\indexentry{\texttt{show settings} command|hyperpage}{135}
\indexentry{\texttt{show memory} command|hyperpage}{135}
\indexentry{Metamath!memory usage|hyperpage}{135}
\indexentry{\texttt{show labels} command|hyperpage}{135}
\indexentry{\texttt{tools} command|hyperpage}{135}
\indexentry{\texttt{show statement} command|hyperpage}{135}
\indexentry{\texttt{\$f} statement|hyperpage}{135}
\indexentry{\texttt{\$e} statement|hyperpage}{135}
\indexentry{\texttt{\$a} statement|hyperpage}{135}
\indexentry{\texttt{\$p} statement|hyperpage}{135}
\indexentry{html generation@{\sc html} generation|hyperpage}{136}
\indexentry{\texttt{search} command|hyperpage}{136}
\indexentry{\texttt{show proof} command|hyperpage}{136}
\indexentry{\texttt{\$p} statement|hyperpage}{136}
\indexentry{\texttt{\$f} statement|hyperpage}{137}
\indexentry{latex@{\LaTeX}|hyperpage}{137}
\indexentry{\texttt{show usage} command|hyperpage}{137}
\indexentry{\texttt{show        trace{\char`\_}back} command|hyperpage}{138}
\indexentry{\texttt{\$p} statement|hyperpage}{138}
\indexentry{\texttt{\$e} statement|hyperpage}{138}
\indexentry{\texttt{verify proof} command|hyperpage}{138}
\indexentry{\texttt{save proof} command|hyperpage}{138}
\indexentry{source buffer|hyperpage}{138}
\indexentry{basic language|hyperpage}{138}
\indexentry{Proof Assistant|hyperpage}{139}
\indexentry{\texttt{minimize{\char`\_}with} command|hyperpage}{141}
\indexentry{\texttt{prove} command|hyperpage}{141}
\indexentry{Proof Assistant|hyperpage}{141}
\indexentry{Metamath!limitations of version 0.07.30|hyperpage}{141}
\indexentry{\texttt{\$d} statement|hyperpage}{141}
\indexentry{\texttt{set unification{\char`\_}timeout} command|hyperpage}{141}
\indexentry{Proof Assistant|hyperpage}{141}
\indexentry{temporary variable|hyperpage}{141}
\indexentry{\texttt{set empty{\char`\_}substitution} command|hyperpage}{142}
\indexentry{Proof Assistant|hyperpage}{142}
\indexentry{substitution!variable|hyperpage}{142}
\indexentry{variable substitution|hyperpage}{142}
\indexentry{empty substitution|hyperpage}{142}
\indexentry{formal system|hyperpage}{142}
\indexentry{ambiguous unification|hyperpage}{142}
\indexentry{unification!ambiguous|hyperpage}{142}
\indexentry{MIU-system|hyperpage}{142}
\indexentry{\texttt{set search{\char`\_}limit} command|hyperpage}{142}
\indexentry{Proof Assistant|hyperpage}{142}
\indexentry{\texttt{show new{\char`\_}proof} command|hyperpage}{142}
\indexentry{\texttt{assign} command|hyperpage}{143}
\indexentry{\texttt{match} command|hyperpage}{143}
\indexentry{\texttt{\$e} statement|hyperpage}{143}
\indexentry{\texttt{let} command|hyperpage}{143}
\indexentry{Proof Assistant|hyperpage}{144}
\indexentry{temporary variable|hyperpage}{144}
\indexentry{\texttt{unify} command|hyperpage}{144}
\indexentry{\texttt{initialize} command|hyperpage}{145}
\indexentry{Proof Assistant|hyperpage}{145}
\indexentry{\texttt{delete} command|hyperpage}{145}
\indexentry{\texttt{\$f} statement|hyperpage}{145}
\indexentry{\texttt{improve} command|hyperpage}{145}
\indexentry{Proof Assistant|hyperpage}{146}
\indexentry{\texttt{\$f} statement|hyperpage}{146}
\indexentry{\texttt{\$e} statement|hyperpage}{146}
\indexentry{\texttt{\$d} statement|hyperpage}{146}
\indexentry{\texttt{save new{\char`\_}proof} command|hyperpage}{146}
\indexentry{source buffer|hyperpage}{146}
\indexentry{ambiguous unification|hyperpage}{146}
\indexentry{unification!ambiguous|hyperpage}{146}
\indexentry{basic language|hyperpage}{146}
\indexentry{latex@{\LaTeX}|hyperpage}{147}
\indexentry{\texttt{open tex} command|hyperpage}{147}
\indexentry{latex@{\LaTeX}|hyperpage}{147}
\indexentry{\texttt{close tex} command|hyperpage}{147}
\indexentry{latex@{\LaTeX}|hyperpage}{148}
\indexentry{error checking|hyperpage}{148}
\indexentry{\texttt{\$t} comment|hyperpage}{148}
\indexentry{typesetting comment|hyperpage}{148}
\indexentry{Metamath!limitations of version 0.07.30|hyperpage}{148}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{148}
\indexentry{\texttt{htmldef} statement|hyperpage}{148}
\indexentry{\texttt{htmltitle} statement|hyperpage}{149}
\indexentry{\texttt{htmlhome} statement|hyperpage}{149}
\indexentry{\texttt{htmlvarcolors} statement|hyperpage}{149}
\indexentry{\texttt{htmlbibliography} statement|hyperpage}{149}
\indexentry{\texttt{\char`\[}\ldots\texttt{]} inside comments|hyperpage}{149}
\indexentry{\texttt{althtmldef} statement|hyperpage}{149}
\indexentry{\texttt{htmldir} statement|hyperpage}{149}
\indexentry{\texttt{althtmldir} statement|hyperpage}{149}
\indexentry{\texttt{exthtmltitle} statement|hyperpage}{150}
\indexentry{\texttt{exthtmlhome} statement|hyperpage}{150}
\indexentry{\texttt{exthtmlbibliography} statement|hyperpage}{150}
\indexentry{\texttt{exthtmllabel} statement|hyperpage}{150}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{150}
\indexentry{\texttt{write theorem{\char`\_}list} command|hyperpage}{150}
\indexentry{Metamath!limitations of version 0.07.30|hyperpage}{150}
\indexentry{\texttt{write bibliography} command|hyperpage}{151}
\indexentry{\texttt{write recent{\char`\_}additions} command|hyperpage}{151}
\indexentry{\texttt{tools} command|hyperpage}{151}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{155}
\indexentry{\texttt{\$t} comment|hyperpage}{155}
\indexentry{typesetting comment|hyperpage}{155}
\indexentry{latex definitions@\LaTeX\ definitions|hyperpage}{155}
\indexentry{\texttt{latexdef} statement|hyperpage}{155}
\indexentry{Metamath!limitations of version 0.07.30|hyperpage}{155}
\indexentry{\texttt{htmldef} statement|hyperpage}{156}
\indexentry{\texttt{althtmldef} statement|hyperpage}{156}
\indexentry{html generation@{\sc html} generation|hyperpage}{156}
\indexentry{compressed proof|hyperpage}{159}
\indexentry{proof!compressed|hyperpage}{159}
\indexentry{RPN order|hyperpage}{160}
\indexentry{Metamath!as a formal system|hyperpage}{161}
\indexentry{de Saint-Exupery, Antoine|hyperpage}{161}
\indexentry{Munkres, James R.|hyperpage}{161}
\indexentry{simple infinite sequence|hyperpage}{162}
\indexentry{term|hyperpage}{162}
\indexentry{finite $n$-termed sequence|hyperpage}{162}
\indexentry{length of a sequence ({$"|\ "|$})|hyperpage}{162}
\indexentry{concatenation|hyperpage}{162}
\indexentry{symbol!in a formal system|hyperpage}{162}
\indexentry{constant!in a formal system|hyperpage}{162}
\indexentry{variable!in a formal system|hyperpage}{162}
\indexentry{Tarski, Alfred|hyperpage}{162}
\indexentry{expression!in a formal system|hyperpage}{163}
\indexentry{constant-prefixed expression|hyperpage}{163}
\indexentry{constant-variable pair|hyperpage}{163}
\indexentry{substitution!variable|hyperpage}{163}
\indexentry{variable substitution|hyperpage}{163}
\indexentry{substitution map|hyperpage}{163}
\indexentry{pre-statement!in a formal system|hyperpage}{164}
\indexentry{disjoint-variable restriction!in a formal system|hyperpage}{164}
\indexentry{variable-type hypothesis!in a formal system|hyperpage}{164}
\indexentry{logical hypothesis!in a formal system|hyperpage}{164}
\indexentry{assertion!in a formal system|hyperpage}{164}
\indexentry{mandatory variable-type hypothesis!in a formal system|hyperpage}{164}
\indexentry{mandatory disjoint-variable restriction!in a formal system|hyperpage}{164}
\indexentry{mandatory hypothesis!in a formal system|hyperpage}{164}
\indexentry{reduct!in a formal system|hyperpage}{164}
\indexentry{statement!in a formal system|hyperpage}{164}
\indexentry{Andr{\'{e}}ka, H.|hyperpage}{164}
\indexentry{formal system|hyperpage}{165}
\indexentry{axiomatic statement!in a formal system|hyperpage}{165}
\indexentry{closure|hyperpage}{165}
\indexentry{provable statement!in a formal system|hyperpage}{165}
\indexentry{universe of a formal system|hyperpage}{165}
\indexentry{Purinton, Josh|hyperpage}{165}
\indexentry{propositional calculus|hyperpage}{166}
\indexentry{inference|hyperpage}{167}
\indexentry{predicate calculus|hyperpage}{168}
\indexentry{individual metavariable|hyperpage}{168}
\indexentry{free variable|hyperpage}{170}
\indexentry{proper substitution|hyperpage}{170}
\indexentry{substitution!proper|hyperpage}{170}
\indexentry{effectively not free|hyperpage}{170}
\indexentry{metalogical completeness|hyperpage}{170}
\indexentry{effectively not free|hyperpage}{170}
\indexentry{simple metatheorem|hyperpage}{171}
\indexentry{metalogical completeness|hyperpage}{171}
\indexentry{Megill, Norman|hyperpage}{171}
\indexentry{metalogical completeness|hyperpage}{171}
\indexentry{definition|hyperpage}{172}
\indexentry{logical equivalence ($\leftrightarrow$)|hyperpage}{173}
\indexentry{biconditional ($\leftrightarrow$)|hyperpage}{173}
\indexentry{conjunction ($\wedge$)|hyperpage}{173}
\indexentry{disjunction ($\vee$)|hyperpage}{173}
\indexentry{existential quantifier ($\exists$)|hyperpage}{173}
\indexentry{ZFC set theory|hyperpage}{173}
\indexentry{Axiom of Extensionality|hyperpage}{174}
\indexentry{Axiom of Replacement|hyperpage}{174}
\indexentry{Axiom of Union|hyperpage}{174}
\indexentry{Axiom of Power Sets|hyperpage}{174}
\indexentry{Axiom of Regularity|hyperpage}{174}
\indexentry{Axiom of Infinity|hyperpage}{174}
\indexentry{Axiom of Choice|hyperpage}{174}
\indexentry{class abstraction|hyperpage}{174}
\indexentry{abstraction class|hyperpage}{174}
\indexentry{Takeuti, Gaisi|hyperpage}{174}
\indexentry{Quine, Willard Van Orman|hyperpage}{174}
\indexentry{proper class|hyperpage}{174}
\indexentry{class!proper|hyperpage}{174}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{174}
\indexentry{class variable|hyperpage}{174}
\indexentry{empty set|hyperpage}{175}
\indexentry{union|hyperpage}{175}
\indexentry{unordered pair|hyperpage}{175}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{176}
\indexentry{formal system|hyperpage}{177}
\indexentry{MIU-system|hyperpage}{177}
\indexentry{well-formed formula (wff)|hyperpage}{179}
\indexentry{Hofstadter, Douglas R.|hyperpage}{179}