\indexentry{Moore, J Strother (*1947)}{1}
\indexentry{Wirth, Claus-Peter (*1963)}{1}
\indexentry{destructor elimination}{1}
\indexentry{simplification}{1}
\indexentry{generalization}{1}
\indexentry{destructor elimination}{1}
\indexentry{cross-fertilization}{1}
\indexentry{elimination of irrelevance}{1}
\indexentry{Boyer--Moore waterfall}{1}
\indexentry{Boyer, Robert S. (*1946)}{1}
\indexentry{Moore, J Strother (*1947)}{1}
\indexentry{Waldmeister@{\sc  Wald\discretionary {-}{}{}Meister}}{1}
\indexentry{Hillenbrand, Thomas}{1}
\indexentry{Hillenbrand, Thomas}{1}
\indexentry{Loechner, Bernd (*1967)@{L\"ochner, Bernd (*1967)}}{1}
\indexentry{Leo-II@{\sc  Leo-II}}{1}
\indexentry{Benzmueller, Christoph (*1968)@{Benzm\"uller, Christoph\ (*1968)}}{1}
\indexentry{Satallax@{\sc  Satallax}}{1}
\indexentry{Boyer, Robert S. (*1946)}{2}
\indexentry{Moore, J Strother (*1947)}{2}
\indexentry{Boyer, Robert S. (*1946)}{2}
\indexentry{Moore, J Strother (*1947)}{2}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{2}
\indexentry{LISP@{\sc  LISP}}{2}
\indexentry{Boyer--Moore waterfall}{2}
\indexentry{Boyer, Robert S. (*1946)}{2}
\indexentry{Moore, J Strother (*1947)}{2}
\indexentry{Boyer, Robert S. (*1946)}{2}
\indexentry{Moore, J Strother (*1947)}{2}
\indexentry{Bledsoe, W. W. (1921--1995)}{3}
\indexentry{Hope Park}{3}
\indexentry{Hope Park}{3}
\indexentry{Burstall, Rod M. (*1934)}{3}
\indexentry{Kowalski, Robert A. (*1941)}{3}
\indexentry{Boyer, Robert S. (*1946)}{3}
\indexentry{Moore, J Strother (*1947)}{3}
\indexentry{Meltzer, Bernard (1916?--2008)}{3}
\indexentry{Michie, Donald (1923--2007)}{3}
\indexentry{Meltzer, Bernard (1916?--2008)}{3}
\indexentry{Burstall, Rod M. (*1934)}{3}
\indexentry{Kowalski, Robert A. (*1941)}{3}
\indexentry{Hayes, Pat(rick) J. (*1944)}{3}
\indexentry{Moore, J Strother (*1947)}{3}
\indexentry{Gordon, Mike J. C. (*1948)}{3}
\indexentry{Boyer, Robert S. (*1946)}{3}
\indexentry{Bundy, Alan (*1947)}{3}
\indexentry{Milner, Robin (1934--2010)}{3}
\indexentry{Meltzer, Bernard (1916?--2008)}{3}
\indexentry{Michie, Donald (1923--2007)}{3}
\indexentry{Meltzer, Bernard (1916?--2008)}{3}
\indexentry{Kowalski, Robert A. (*1941)}{3}
\indexentry{Hayes, Pat(rick) J. (*1944)}{4}
\indexentry{Moore, J Strother (*1947)}{4}
\indexentry{Gordon, Mike J. C. (*1948)}{4}
\indexentry{Boyer, Robert S. (*1946)}{4}
\indexentry{Bundy, Alan (*1947)}{4}
\indexentry{Milner, Robin (1934--2010)}{4}
\indexentry{Hope Park}{4}
\indexentry{Robinson, J. Alan (*1930?)}{4}
\indexentry{McCarthy, John (1927--2011)}{4}
\indexentry{Bledsoe, W. W. (1921--1995)}{4}
\indexentry{Scott, Dana S. (*1932)}{4}
\indexentry{Robinson, J. Alan (*1930?)}{4}
\indexentry{Boyer, Robert S. (*1946)}{4}
\indexentry{Moore, J Strother (*1947)}{4}
\indexentry{Boyer, Robert S. (*1946)}{4}
\indexentry{Moore, J Strother (*1947)}{4}
\indexentry{linear resolution}{4}
\indexentry{LISP@{\sc  LISP}}{4}
\indexentry{Moore, J Strother (*1947)}{4}
\indexentry{LISP@{\sc  LISP}}{4}
\indexentry{LISP@{\sc  LISP}}{4}
\indexentry{LISP@{\sc  LISP}}{4}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{4}
\indexentry{LISP@{\sc  LISP}}{4}
\indexentry{Hope Park}{4}
\indexentry{Hope Park}{4}
\indexentry{Boyer, Robert S. (*1946)}{5}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{5}
\indexentry{LISP@{\sc  LISP}}{5}
\indexentry{Hope Park}{5}
\indexentry{Walther, Christoph (*1950)}{5}
\indexentry{Bundy, Alan (*1947)}{5}
\indexentry{Moore, J Strother (*1947)}{5}
\indexentry{Kowalski, Robert A. (*1941)}{5}
\indexentry{Burstall, Rod M. (*1934)}{5}
\indexentry{Hope Park}{5}
\indexentry{Boyer, Robert S. (*1946)}{5}
\indexentry{Moore, J Strother (*1947)}{5}
\indexentry{Moore, J Strother (*1947)}{5}
\indexentry{Simonyi, Charles}{5}
\indexentry{Boyer--Moore theorem provers}{6}
\indexentry{Boyer, Robert S. (*1946)}{6}
\indexentry{Moore, J Strother (*1947)}{6}
\indexentry{LISP@{\sc  LISP}}{6}
\indexentry{Boyer--Moore theorem provers}{6}
\indexentry{Boyer, Robert S. (*1946)}{6}
\indexentry{Moore, J Strother (*1947)}{6}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{6}
\indexentry{LISP@{\sc  LISP}}{6}
\indexentry{Thm@{\sc  Thm}}{6}
\indexentry{Nqthm@{\sc  Nqthm}}{6}
\indexentry{ACL2@{\sc  ACL2}}{6}
\indexentry{LISP@{\sc  LISP}}{6}
\indexentry{LISP@{\sc  LISP}}{6}
\indexentry{LISP@{\sc  LISP}}{6}
\indexentry{LISP@{\sc  LISP}}{6}
\indexentry{LISP@{\sc  LISP}}{6}
\indexentry{LISP@{\sc  LISP}}{6}
\indexentry{LISP@{\sc  LISP}}{6}
\indexentry{LISP@{\sc  LISP}}{6}
\indexentry{LISP@{\sc  LISP}}{6}
\indexentry{LISP@{\sc  LISP}}{6}
\indexentry{LISP@{\sc  LISP}}{6}
\indexentry{Kowalski, Robert A. (*1941)}{6}
\indexentry{Hayes, Pat(rick) J. (*1944)}{6}
\indexentry{LISP@{\sc  LISP}}{6}
\indexentry{LISP@{\sc  LISP}}{6}
\indexentry{Common Lisp@{\sc  Common Lisp}}{6}
\indexentry{Boyer, Robert S. (*1946)}{6}
\indexentry{Moore, J Strother (*1947)}{6}
\indexentry{Moore, J Strother (*1947)}{6}
\indexentry{LISP@{\sc  LISP}}{7}
\indexentry{ml@{\sc  ml}}{7}
\indexentry{Haskell@{\sc  Haskell}}{7}
\indexentry{LISP@{\sc  LISP}}{7}
\indexentry{ml@{\sc  ml}}{7}
\indexentry{Haskell@{\sc  Haskell}}{7}
\indexentry{Wirth, Claus-Peter (*1963)}{7}
\indexentry{Gramlich, Bernhard (*1959)}{7}
\indexentry{Wirth, Claus-Peter (*1963)}{7}
\indexentry{constructor variables}{7}
\indexentry{Common Lisp@{\sc  Common Lisp}}{7}
\indexentry{ACL2@{\sc  ACL2}}{7}
\indexentry{ACL2@{\sc  ACL2}}{7}
\indexentry{Boyer--Moore machines}{7}
\indexentry{Boyer, Robert S. (*1946)}{7}
\indexentry{Moore, J Strother (*1947)}{7}
\indexentry{Haskell@{\sc  Haskell}}{7}
\indexentry{ml@{\sc  ml}}{7}
\indexentry{LCF@{\sc  LCF}}{7}
\indexentry{Scott, Dana S. (*1932)}{7}
\indexentry{Gordon, Mike J. C. (*1948)}{7}
\indexentry{Wirth, Claus-Peter (*1963)}{7}
\indexentry{Gramlich, Bernhard (*1959)}{7}
\indexentry{Wirth, Claus-Peter (*1963)}{7}
\indexentry{LISP@{\sc  LISP}}{8}
\indexentry{LISP@{\sc  LISP}}{8}
\indexentry{Boyer--Moore theorem provers}{8}
\indexentry{Boyer, Robert S. (*1946)}{8}
\indexentry{Moore, J Strother (*1947)}{8}
\indexentry{LISP@{\sc  LISP}}{8}
\indexentry{LISP@{\sc  LISP}}{8}
\indexentry{LISP@{\sc  LISP}}{8}
\indexentry{LISP@{\sc  LISP}}{8}
\indexentry{LISP@{\sc  LISP}}{8}
\indexentry{LISP@{\sc  LISP}}{8}
\indexentry{LISP@{\sc  LISP}}{8}
\indexentry{Boyer--Moore theorem provers}{8}
\indexentry{Boyer, Robert S. (*1946)}{8}
\indexentry{Moore, J Strother (*1947)}{8}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{8}
\indexentry{LISP@{\sc  LISP}}{8}
\indexentry{Thm@{\sc  Thm}}{8}
\indexentry{Nqthm@{\sc  Nqthm}}{8}
\indexentry{ACL2@{\sc  ACL2}}{8}
\indexentry{Wirth, Claus-Peter (*1963)}{8}
\indexentry{Boyer, Robert S. (*1946)}{8}
\indexentry{Moore, J Strother (*1947)}{8}
\indexentry{Moore, J Strother (*1947)}{8}
\indexentry{Boyer, Robert S. (*1946)}{8}
\indexentry{Moore, J Strother (*1947)}{8}
\indexentry{Walther, Christoph (*1950)}{8}
\indexentry{Bundy, Alan (*1947)}{8}
\indexentry{Kaufmann, Matt (*1952)}{8}
\indexentry{shells}{8}
\indexentry{Aristotle (384--322\,{\sc  b.c.})}{9}
\indexentry{Euclid}{9}
\indexentry{Kant, Immanuel (1724--1804)}{9}
\indexentry{Hippasus of Metapontum (ca.\,550\,{\sc  b.c.})}{9}
\indexentry{descente infinie}{9}
\indexentry{induction!structural}{9}
\indexentry{Plato (427--347\,{\sc  b.c.})}{9}
\indexentry{Euclid}{9}
\indexentry{descente infinie}{9}
\indexentry{induction!structural}{9}
\indexentry{induction!structural}{9}
\indexentry{Gerson, Levi ben (1288--1344)}{9}
\indexentry{induction!structural}{9}
\indexentry{Maurolico, Francesco (1494--1575)}{9}
\indexentry{Pascal, Blaise (1623--1662)}{9}
\indexentry{descente infinie}{9}
\indexentry{Fermat, Pierre (160?--1665)}{9}
\indexentry{Acerbi, Fabio}{9}
\indexentry{descente infinie}{9}
\indexentry{induction!structural}{9}
\indexentry{Acerbi, Fabio}{9}
\indexentry{Wirth, Claus-Peter (*1963)}{9}
\indexentry{well-foundedness}{10}
\indexentry{termination}{10}
\indexentry{choice!Axiom of Choice}{10}
\indexentry{choice!Axiom of Choice}{10}
\indexentry{induction!Noetherian}{10}
\indexentry{induction!Noetherian}{10}
\indexentry{induction!Noetherian}{10}
\indexentry{Fermat, Pierre (160?--1665)}{10}
\indexentry{Barner, Klaus}{10}
\indexentry{Fermat, Pierre (160?--1665)}{10}
\indexentry{Goldstein, Catherine (*1958)}{10}
\indexentry{Fermat, Pierre (160?--1665)}{10}
\indexentry{descente infinie}{10}
\indexentry{Wirth, Claus-Peter (*1963)}{10}
\indexentry{Wirth, Claus-Peter (*1963)}{10}
\indexentry{Wirth, Claus-Peter (*1963)}{10}
\indexentry{choice!Principle of Dependent Choice}{10}
\indexentry{Noether, Emmy (1882--1935)}{11}
\indexentry{Bourbaki, Nicolas (pseudonym)}{11}
\indexentry{Bourbaki, Nicolas (pseudonym)}{11}
\indexentry{Bourbaki, Nicolas (pseudonym)}{11}
\indexentry{Bourbaki, Nicolas (pseudonym)}{11}
\indexentry{induction!Noetherian}{11}
\indexentry{induction!Noetherian}{11}
\indexentry{induction!Noetherian}{11}
\indexentry{induction!course-of-values}{11}
\indexentry{induction!complete}{11}
\indexentry{induction!structural}{11}
\indexentry{Bourbaki, Nicolas (pseudonym)}{11}
\indexentry{Bourbaki, Nicolas (pseudonym)}{11}
\indexentry{choice!Axiom of Choice}{12}
\indexentry{induction!Noetherian}{12}
\indexentry{choice!Axiom of Choice}{12}
\indexentry{choice!Axiom of Choice}{12}
\indexentry{constructor function symbols}{12}
\indexentry{induction!structural}{12}
\indexentry{Dedekind, Richard (1831--1916)}{13}
\indexentry{induction!structural}{13}
\indexentry{Dedekind, Richard (1831--1916)}{13}
\indexentry{constructor style}{13}
\indexentry{destructor style}{13}
\indexentry{linear terms}{13}
\indexentry{Ackermann function}{13}
\indexentry{Aristotelian logic}{13}
\indexentry{induction!structural}{13}
\indexentry{Fries, Jakob Friedrich (1773--1843)}{13}
\indexentry{Dedekind, Richard (1831--1916)}{13}
\indexentry{induction!complete}{13}
\indexentry{Heijenoort, Jean van (1912--1986)}{13}
\indexentry{Hilbert, David (1862--1943)}{13}
\indexentry{Bernays, Paul (1888--1977)}{13}
\indexentry{constructor style}{13}
\indexentry{destructor style}{13}
\indexentry{P\'eter, R\'osza (1905--1977)}{13}
\indexentry{Ackermann, Wilhelm (1896--1962)}{13}
\indexentry{Ackermann, Wilhelm (1896--1962)}{13}
\indexentry{Ackermann function}{13}
\indexentry{Peano, Guiseppe (1858--1932)}{14}
\indexentry{Pieri, Mario (1860--1913)}{14}
\indexentry{induction!structural}{14}
\indexentry{induction!structural}{14}
\indexentry{Ackermann function}{14}
\indexentry{Wirth, Claus-Peter (*1963)}{14}
\indexentry{Pieri, Mario (1860--1913)}{14}
\indexentry{Peano axioms}{14}
\indexentry{Peano, Guiseppe (1858--1932)}{14}
\indexentry{Padoa, Alessandro (1868--1937)}{14}
\indexentry{Smith, James T.}{14}
\indexentry{Pieri, Mario (1860--1913)}{14}
\indexentry{Pieri, Mario (1860--1913)}{16}
\indexentry{Pieri, Mario (1860--1913)}{16}
\indexentry{Peano, Guiseppe (1858--1932)}{16}
\indexentry{Pieri, Mario (1860--1913)}{16}
\indexentry{Pieri, Mario (1860--1913)}{16}
\indexentry{Pieri, Mario (1860--1913)}{16}
\indexentry{shells}{16}
\indexentry{shell principle}{16}
\indexentry{Boyer, Robert S. (*1946)}{16}
\indexentry{Moore, J Strother (*1947)}{16}
\indexentry{shell principle}{16}
\indexentry{constructor style}{17}
\indexentry{destructor style}{17}
\indexentry{lexicographic combination}{17}
\indexentry{measured positions}{17}
\indexentry{Wirth, Claus-Peter (*1963)}{17}
\indexentry{induction!structural}{18}
\indexentry{induction!Noetherian}{18}
\indexentry{Pieri, Mario (1860--1913)}{18}
\indexentry{induction!Noetherian}{18}
\indexentry{Peano, Guiseppe (1858--1932)}{18}
\indexentry{induction!structural}{18}
\indexentry{Hilbert, David (1862--1943)}{18}
\indexentry{Bernays, Paul (1888--1977)}{18}
\indexentry{confluence}{18}
\indexentry{Gramlich, Bernhard (*1959)}{18}
\indexentry{Wirth, Claus-Peter (*1963)}{18}
\indexentry{Wirth, Claus-Peter (*1963)}{18}
\indexentry{Hilbert, David (1862--1943)}{18}
\indexentry{Bernays, Paul (1888--1977)}{18}
\indexentry{consistency}{18}
\indexentry{Ackermann, Wilhelm (1896--1962)}{18}
\indexentry{descente infinie}{19}
\indexentry{Fermat, Pierre (160?--1665)}{19}
\indexentry{Fermat, Pierre (160?--1665)}{19}
\indexentry{descente infinie}{19}
\indexentry{descente infinie}{19}
\indexentry{Fermat, Pierre (160?--1665)}{19}
\indexentry{descente infinie}{19}
\indexentry{induction!Noetherian}{19}
\indexentry{descente infinie}{19}
\indexentry{Wirth, Claus-Peter (*1963)}{19}
\indexentry{Fermat, Pierre (160?--1665)}{19}
\indexentry{Huygens, Christiaan (1629--1695)}{19}
\indexentry{descente infinie}{19}
\indexentry{Wirth, Claus-Peter (*1963)}{19}
\indexentry{descente infinie}{19}
\indexentry{Fermat, Pierre (160?--1665)}{19}
\indexentry{induction!Noetherian}{19}
\indexentry{Wirth, Claus-Peter (*1963)}{19}
\indexentry{descente infinie}{19}
\indexentry{descente infinie}{19}
\indexentry{Wirth, Claus-Peter (*1963)}{19}
\indexentry{Wirth, Claus-Peter (*1963)}{19}
\indexentry{descente infinie}{20}
\indexentry{descente infinie}{20}
\indexentry{induction!Noetherian}{20}
\indexentry{descente infinie}{20}
\indexentry{Autexier, Serge (*1971)}{20}
\indexentry{descente infinie}{21}
\indexentry{induction!Noetherian}{21}
\indexentry{descente infinie}{21}
\indexentry{induction!Noetherian}{22}
\indexentry{induction!explicit|(}{22}
\indexentry{induction!Noetherian}{22}
\indexentry{induction!Noetherian}{22}
\indexentry{induction rule}{22}
\indexentry{induction!Noetherian}{22}
\indexentry{induction rule}{22}
\indexentry{induction rule}{23}
\indexentry{induction!Noetherian}{23}
\indexentry{induction rule}{23}
\indexentry{induction!Noetherian}{23}
\indexentry{Boyer--Moore waterfall}{23}
\indexentry{Boyer, Robert S. (*1946)}{23}
\indexentry{Moore, J Strother (*1947)}{23}
\indexentry{induction rule}{23}
\indexentry{induction rule}{23}
\indexentry{induction!explicit}{23}
\indexentry{induction rule}{23}
\indexentry{induction!Noetherian}{23}
\indexentry{induction!Noetherian}{23}
\indexentry{induction!Noetherian}{23}
\indexentry{induction rule}{23}
\indexentry{induction!explicit}{23}
\indexentry{induction rule}{24}
\indexentry{induction rule}{24}
\indexentry{induction rule}{24}
\indexentry{induction rule}{24}
\indexentry{Boyer--Moore theorem provers}{24}
\indexentry{Boyer, Robert S. (*1946)}{24}
\indexentry{Moore, J Strother (*1947)}{24}
\indexentry{induction rule}{24}
\indexentry{Walther, Christoph (*1950)}{24}
\indexentry{descente infinie}{24}
\indexentry{induction rule}{24}
\indexentry{induction!explicit}{24}
\indexentry{induction rule}{24}
\indexentry{induction!explicit}{24}
\indexentry{induction rule}{24}
\indexentry{induction!structural}{24}
\indexentry{induction rule}{24}
\indexentry{Boyer--Moore theorem provers}{24}
\indexentry{Boyer, Robert S. (*1946)}{24}
\indexentry{Moore, J Strother (*1947)}{24}
\indexentry{induction rule}{24}
\indexentry{cross-fertilization}{24}
\indexentry{Boyer--Moore waterfall}{24}
\indexentry{Boyer, Robert S. (*1946)}{24}
\indexentry{Moore, J Strother (*1947)}{24}
\indexentry{Walther, Christoph (*1950)}{24}
\indexentry{induction rule}{24}
\indexentry{induction rule}{24}
\indexentry{Boyer--Moore waterfall}{24}
\indexentry{Boyer, Robert S. (*1946)}{24}
\indexentry{Moore, J Strother (*1947)}{24}
\indexentry{induction rule}{25}
\indexentry{induction!structural}{25}
\indexentry{induction rule}{25}
\indexentry{Boyer--Moore theorem provers}{25}
\indexentry{Boyer, Robert S. (*1946)}{25}
\indexentry{Moore, J Strother (*1947)}{25}
\indexentry{descente infinie}{25}
\indexentry{Boyer--Moore waterfall}{25}
\indexentry{Boyer, Robert S. (*1946)}{25}
\indexentry{Moore, J Strother (*1947)}{25}
\indexentry{descente infinie}{25}
\indexentry{induction rule}{25}
\indexentry{induction!explicit}{25}
\indexentry{Boyer--Moore theorem provers}{25}
\indexentry{Boyer, Robert S. (*1946)}{25}
\indexentry{Moore, J Strother (*1947)}{25}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{25}
\indexentry{LISP@{\sc  LISP}}{25}
\indexentry{induction!explicit|)}{25}
\indexentry{induction!explicit}{25}
\indexentry{Peano, Guiseppe (1858--1932)}{25}
\indexentry{Pieri, Mario (1860--1913)}{25}
\indexentry{descente infinie}{25}
\indexentry{Newman, Max(well) H. A. (1897--1984)}{25}
\indexentry{Wirth, Claus-Peter (*1963)}{25}
\indexentry{confluence}{25}
\indexentry{induction rule}{25}
\indexentry{induction!explicit}{25}
\indexentry{confluence}{25}
\indexentry{Church--Rosser property}{25}
\indexentry{Newman Lemma}{25}
\indexentry{Church--Rosser Theorem}{25}
\indexentry{confluence}{25}
\indexentry{Boyer--Moore theorem provers}{25}
\indexentry{Boyer, Robert S. (*1946)}{25}
\indexentry{Moore, J Strother (*1947)}{25}
\indexentry{Shankar, Natarajan}{25}
\indexentry{Newman Lemma}{25}
\indexentry{induction!structural}{25}
\indexentry{Boyer--Moore theorem provers}{26}
\indexentry{Boyer, Robert S. (*1946)}{26}
\indexentry{Moore, J Strother (*1947)}{26}
\indexentry{induction rule}{26}
\indexentry{induction!Noetherian}{26}
\indexentry{induction!explicit}{26}
\indexentry{induction rule}{26}
\indexentry{induction!explicit}{26}
\indexentry{induction!Noetherian}{26}
\indexentry{Boyer--Moore waterfall}{26}
\indexentry{Boyer, Robert S. (*1946)}{26}
\indexentry{Moore, J Strother (*1947)}{26}
\indexentry{induction rule}{26}
\indexentry{induction rule}{26}
\indexentry{induction!explicit}{26}
\indexentry{induction variables}{26}
\indexentry{constructor substitutions}{26}
\indexentry{induction variables}{26}
\indexentry{induction rule}{26}
\indexentry{induction!explicit}{26}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{26}
\indexentry{LISP@{\sc  LISP}}{26}
\indexentry{induction variables}{26}
\indexentry{induction!structural}{26}
\indexentry{constructor substitutions}{26}
\indexentry{constructor style}{26}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{26}
\indexentry{LISP@{\sc  LISP}}{26}
\indexentry{Thm@{\sc  Thm}}{26}
\indexentry{generalization|(}{27}
\indexentry{induction!explicit}{27}
\indexentry{Boyer--Moore theorem provers}{27}
\indexentry{Boyer, Robert S. (*1946)}{27}
\indexentry{Moore, J Strother (*1947)}{27}
\indexentry{elimination of irrelevance}{27}
\indexentry{Boyer--Moore waterfall}{27}
\indexentry{Boyer, Robert S. (*1946)}{27}
\indexentry{Moore, J Strother (*1947)}{27}
\indexentry{Aubin, Raymond}{27}
\indexentry{induction!explicit}{28}
\indexentry{induction rule}{28}
\indexentry{induction!explicit}{28}
\indexentry{induction!explicit}{28}
\indexentry{induction!explicit}{28}
\indexentry{Boyer--Moore theorem provers}{28}
\indexentry{Boyer, Robert S. (*1946)}{28}
\indexentry{Moore, J Strother (*1947)}{28}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{28}
\indexentry{LISP@{\sc  LISP}}{28}
\indexentry{Wirth, Claus-Peter (*1963)}{28}
\indexentry{generalization|)}{28}
\indexentry{induction!explicit}{28}
\indexentry{Fermat, Pierre (160?--1665)}{29}
\indexentry{descente infinie}{29}
\indexentry{induction!explicit}{29}
\indexentry{consistency}{29}
\indexentry{recursion}{30}
\indexentry{induction!explicit}{30}
\indexentry{rewrite relation}{30}
\indexentry{ground terms}{30}
\indexentry{confluence|(}{30}
\indexentry{confluence}{30}
\indexentry{consistency}{30}
\indexentry{confluence}{30}
\indexentry{Wirth, Claus-Peter (*1963)}{30}
\indexentry{Church--Rosser property}{30}
\indexentry{confluence}{30}
\indexentry{Boyer--Moore theorem provers}{31}
\indexentry{Boyer, Robert S. (*1946)}{31}
\indexentry{Moore, J Strother (*1947)}{31}
\indexentry{confluence}{31}
\indexentry{LISP@{\sc  LISP}}{31}
\indexentry{Boyer--Moore theorem provers}{31}
\indexentry{Boyer, Robert S. (*1946)}{31}
\indexentry{Moore, J Strother (*1947)}{31}
\indexentry{LISP@{\sc  LISP}}{31}
\indexentry{LISP@{\sc  LISP}}{31}
\indexentry{Boyer, Robert S. (*1946)}{31}
\indexentry{Moore, J Strother (*1947)}{31}
\indexentry{Boyer, Robert S. (*1946)}{31}
\indexentry{Moore, J Strother (*1947)}{31}
\indexentry{constructor style}{31}
\indexentry{destructor style}{31}
\indexentry{constructor style}{31}
\indexentry{destructor style}{31}
\indexentry{destructor style}{31}
\indexentry{Boyer--Moore theorem provers}{31}
\indexentry{Boyer, Robert S. (*1946)}{31}
\indexentry{Moore, J Strother (*1947)}{31}
\indexentry{Boyer, Robert S. (*1946)}{31}
\indexentry{Moore, J Strother (*1947)}{31}
\indexentry{confluence}{31}
\indexentry{Moore, J Strother (*1947)}{31}
\indexentry{Boyer, Robert S. (*1946)}{31}
\indexentry{Moore, J Strother (*1947)}{31}
\indexentry{LISP@{\sc  LISP}}{31}
\indexentry{LISP@{\sc  LISP}}{31}
\indexentry{LISP@{\sc  LISP}}{31}
\indexentry{LISP@{\sc  LISP}}{31}
\indexentry{confluence}{32}
\indexentry{confluence}{32}
\indexentry{confluence}{32}
\indexentry{Wirth, Claus-Peter (*1963)}{32}
\indexentry{Boyer--Moore theorem provers}{32}
\indexentry{Boyer, Robert S. (*1946)}{32}
\indexentry{Moore, J Strother (*1947)}{32}
\indexentry{confluence}{32}
\indexentry{confluence|)}{32}
\indexentry{Boyer--Moore theorem provers}{32}
\indexentry{Boyer, Robert S. (*1946)}{32}
\indexentry{Moore, J Strother (*1947)}{32}
\indexentry{termination}{32}
\indexentry{reducibility}{32}
\indexentry{Boyer--Moore theorem provers}{32}
\indexentry{Boyer, Robert S. (*1946)}{32}
\indexentry{Moore, J Strother (*1947)}{32}
\indexentry{LISP@{\sc  LISP}}{32}
\indexentry{constructor variables}{32}
\indexentry{confluence}{32}
\indexentry{consistency}{32}
\indexentry{confluence}{32}
\indexentry{Wirth, Claus-Peter (*1963)}{32}
\indexentry{constructor variables}{32}
\indexentry{Boyer, Robert S. (*1946)}{32}
\indexentry{Moore, J Strother (*1947)}{32}
\indexentry{Wirth, Claus-Peter (*1963)}{32}
\indexentry{Gramlich, Bernhard (*1959)}{32}
\indexentry{Wirth, Claus-Peter (*1963)}{32}
\indexentry{Boyer--Moore theorem provers}{33}
\indexentry{Boyer, Robert S. (*1946)}{33}
\indexentry{Moore, J Strother (*1947)}{33}
\indexentry{LISP@{\sc  LISP}}{33}
\indexentry{Boyer--Moore theorem provers}{33}
\indexentry{Boyer, Robert S. (*1946)}{33}
\indexentry{Moore, J Strother (*1947)}{33}
\indexentry{Moore, J Strother (*1947)}{33}
\indexentry{confluence}{33}
\indexentry{Russell's Paradox}{33}
\indexentry{confluence}{33}
\indexentry{consistency}{33}
\indexentry{consistency}{33}
\indexentry{constructor variables}{33}
\indexentry{constructor function symbols}{33}
\indexentry{constructor variables}{33}
\indexentry{consistency}{33}
\indexentry{constructor variables}{33}
\indexentry{LISP@{\sc  LISP}}{33}
\indexentry{LISP@{\sc  LISP}}{33}
\indexentry{constructor variables}{33}
\indexentry{Moore, J Strother (*1947)}{33}
\indexentry{confluence}{33}
\indexentry{constructor variables}{33}
\indexentry{constructor variables}{33}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{33}
\indexentry{LISP@{\sc  LISP}}{33}
\indexentry{Moore, J Strother (*1947)}{33}
\indexentry{constructor variables}{33}
\indexentry{Wirth, Claus-Peter (*1963)}{33}
\indexentry{Wirth, Claus-Peter (*1963)}{33}
\indexentry{Gramlich, Bernhard (*1959)}{33}
\indexentry{Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}{33}
\indexentry{Wirth, Claus-Peter (*1963)}{33}
\indexentry{Wirth, Claus-Peter (*1963)}{33}
\indexentry{Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}{33}
\indexentry{Schmidt-Samoa, Tobias (*1973)}{33}
\indexentry{Wirth, Claus-Peter (*1963)}{33}
\indexentry{Gramlich, Bernhard (*1959)}{33}
\indexentry{Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}{33}
\indexentry{Wirth, Claus-Peter (*1963)}{33}
\indexentry{Boyer--Moore theorem provers}{34}
\indexentry{Boyer, Robert S. (*1946)}{34}
\indexentry{Moore, J Strother (*1947)}{34}
\indexentry{termination|(}{34}
\indexentry{induction templates|(}{34}
\indexentry{LISP@{\sc  LISP}}{34}
\indexentry{confluence}{34}
\indexentry{induction!explicit}{34}
\indexentry{Boyer--Moore theorem provers}{34}
\indexentry{Boyer, Robert S. (*1946)}{34}
\indexentry{Moore, J Strother (*1947)}{34}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{34}
\indexentry{LISP@{\sc  LISP}}{34}
\indexentry{Thm@{\sc  Thm}}{34}
\indexentry{Boyer, Robert S. (*1946)}{34}
\indexentry{Moore, J Strother (*1947)}{34}
\indexentry{induction!explicit}{34}
\indexentry{induction rule}{34}
\indexentry{induction!explicit}{34}
\indexentry{relational descriptions}{34}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{34}
\indexentry{LISP@{\sc  LISP}}{34}
\indexentry{LISP@{\sc  LISP}}{34}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{34}
\indexentry{LISP@{\sc  LISP}}{34}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{34}
\indexentry{LISP@{\sc  LISP}}{34}
\indexentry{Boyer, Robert S. (*1946)}{34}
\indexentry{Moore, J Strother (*1947)}{34}
\indexentry{relational descriptions}{34}
\indexentry{Walther, Christoph (*1950)}{34}
\indexentry{destructor style}{35}
\indexentry{relational descriptions}{35}
\indexentry{relational descriptions}{35}
\indexentry{relational descriptions}{35}
\indexentry{measured positions}{35}
\indexentry{relational descriptions}{35}
\indexentry{measured positions}{35}
\indexentry{relational descriptions}{35}
\indexentry{relational descriptions}{35}
\indexentry{relational descriptions}{35}
\indexentry{measured positions}{35}
\indexentry{relational descriptions}{35}
\indexentry{Ackermann function}{35}
\indexentry{measured positions}{35}
\indexentry{relational descriptions}{36}
\indexentry{destructor style}{36}
\indexentry{constructor variables}{36}
\indexentry{Wirth, Claus-Peter (*1963)}{36}
\indexentry{Wirth, Claus-Peter (*1963)}{36}
\indexentry{Wirth, Claus-Peter (*1963)}{36}
\indexentry{termination|)}{37}
\indexentry{induction!explicit}{37}
\indexentry{measured positions}{37}
\indexentry{changeable positions}{37}
\indexentry{changeable positions}{37}
\indexentry{measured positions}{37}
\indexentry{relational descriptions}{37}
\indexentry{measured positions}{37}
\indexentry{changeable positions}{37}
\indexentry{induction rule}{37}
\indexentry{induction rule}{37}
\indexentry{induction!explicit}{37}
\indexentry{changeable positions}{37}
\indexentry{changeable positions}{37}
\indexentry{Boyer, Robert S. (*1946)}{37}
\indexentry{Moore, J Strother (*1947)}{37}
\indexentry{changeable positions}{38}
\indexentry{changeable positions}{38}
\indexentry{relational descriptions}{38}
\indexentry{constructor substitutions}{38}
\indexentry{changeable positions}{38}
\indexentry{constructor substitutions}{38}
\indexentry{induction templates|)}{38}
\indexentry{induction schemes|(}{38}
\indexentry{relational descriptions}{38}
\indexentry{induction templates}{38}
\indexentry{induction templates}{38}
\indexentry{induction templates}{38}
\indexentry{induction rule}{38}
\indexentry{induction!explicit}{38}
\indexentry{constructor substitutions}{38}
\indexentry{changeable positions}{38}
\indexentry{induction templates}{38}
\indexentry{measured positions}{38}
\indexentry{changeable positions}{38}
\indexentry{changeable positions}{38}
\indexentry{changeable positions}{38}
\indexentry{changeable positions}{38}
\indexentry{measured positions}{39}
\indexentry{induction!explicit}{39}
\indexentry{induction!lazy}{39}
\indexentry{position sets}{39}
\indexentry{induction variables}{39}
\indexentry{changeable positions}{39}
\indexentry{induction templates}{39}
\indexentry{step-case descriptions}{39}
\indexentry{relational descriptions}{39}
\indexentry{step-case descriptions}{39}
\indexentry{hitting ratio}{39}
\indexentry{Boyer, Robert S. (*1946)}{39}
\indexentry{Moore, J Strother (*1947)}{39}
\indexentry{Wirth, Claus-Peter (*1963)}{39}
\indexentry{induction templates}{39}
\indexentry{position sets}{40}
\indexentry{induction rule}{40}
\indexentry{induction!explicit}{40}
\indexentry{induction variables}{40}
\indexentry{induction templates}{40}
\indexentry{changeable positions}{40}
\indexentry{relational descriptions}{40}
\indexentry{induction templates}{40}
\indexentry{step-case descriptions}{40}
\indexentry{relational descriptions}{40}
\indexentry{constructor substitutions}{40}
\indexentry{changeable positions}{40}
\indexentry{relational descriptions}{40}
\indexentry{constructor substitutions}{40}
\indexentry{hitting ratio}{40}
\indexentry{step-case descriptions}{40}
\indexentry{induction schemes|)}{40}
\indexentry{induction!explicit|(}{41}
\indexentry{ACL2@{\sc  ACL2}}{42}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{42}
\indexentry{LISP@{\sc  LISP}}{42}
\indexentry{Boyer, Robert S. (*1946)}{42}
\indexentry{Moore, J Strother (*1947)}{42}
\indexentry{Thm@{\sc  Thm}}{42}
\indexentry{Boyer, Robert S. (*1946)}{42}
\indexentry{Moore, J Strother (*1947)}{42}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{42}
\indexentry{LISP@{\sc  LISP}}{42}
\indexentry{Boyer, Robert S. (*1946)}{42}
\indexentry{Moore, J Strother (*1947)}{42}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{42}
\indexentry{LISP@{\sc  LISP}}{42}
\indexentry{Moore, J Strother (*1947)}{42}
\indexentry{Boyer, Robert S. (*1946)}{42}
\indexentry{Moore, J Strother (*1947)}{42}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{42}
\indexentry{LISP@{\sc  LISP}}{42}
\indexentry{Burstall, Rod M. (*1934)}{42}
\indexentry{Burstall, Rod M. (*1934)}{42}
\indexentry{Bledsoe, W. W. (1921--1995)}{42}
\indexentry{induction!structural}{42}
\indexentry{Boyer--Moore waterfall}{43}
\indexentry{Boyer, Robert S. (*1946)}{43}
\indexentry{Moore, J Strother (*1947)}{43}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{43}
\indexentry{LISP@{\sc  LISP}}{43}
\indexentry{Boyer--Moore theorem provers}{43}
\indexentry{Boyer, Robert S. (*1946)}{43}
\indexentry{Moore, J Strother (*1947)}{43}
\indexentry{Thm@{\sc  Thm}}{43}
\indexentry{Bledsoe, W. W. (1921--1995)}{43}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{43}
\indexentry{LISP@{\sc  LISP}}{43}
\indexentry{Moore, J Strother (*1947)}{43}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{43}
\indexentry{LISP@{\sc  LISP}}{43}
\indexentry{Bledsoe, W. W. (1921--1995)}{43}
\indexentry{induction!explicit}{43}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{43}
\indexentry{LISP@{\sc  LISP}}{43}
\indexentry{LISP@{\sc  LISP}}{43}
\indexentry{Moore, J Strother (*1947)}{43}
\indexentry{Wirth, Claus-Peter (*1963)}{43}
\indexentry{Bledsoe, W. W. (1921--1995)}{44}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{44}
\indexentry{LISP@{\sc  LISP}}{44}
\indexentry{Moore, J Strother (*1947)}{44}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{44}
\indexentry{LISP@{\sc  LISP}}{44}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{44}
\indexentry{LISP@{\sc  LISP}}{44}
\indexentry{Moore, J Strother (*1947)}{44}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{44}
\indexentry{LISP@{\sc  LISP}}{44}
\indexentry{induction!structural}{44}
\indexentry{Boyer--Moore theorem provers}{44}
\indexentry{Boyer, Robert S. (*1946)}{44}
\indexentry{Moore, J Strother (*1947)}{44}
\indexentry{Burstall, Rod M. (*1934)}{44}
\indexentry{Bledsoe, W. W. (1921--1995)}{44}
\indexentry{Burstall, Rod M. (*1934)}{44}
\indexentry{Moore, J Strother (*1947)}{44}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{45}
\indexentry{LISP@{\sc  LISP}}{45}
\indexentry{constructor variables}{45}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{45}
\indexentry{LISP@{\sc  LISP}}{45}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{45}
\indexentry{LISP@{\sc  LISP}}{45}
\indexentry{LISP@{\sc  LISP}}{45}
\indexentry{LISP@{\sc  LISP}}{45}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{45}
\indexentry{LISP@{\sc  LISP}}{45}
\indexentry{LISP@{\sc  LISP}}{45}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{45}
\indexentry{LISP@{\sc  LISP}}{45}
\indexentry{Boyer--Moore waterfall}{45}
\indexentry{Boyer, Robert S. (*1946)}{45}
\indexentry{Moore, J Strother (*1947)}{45}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{45}
\indexentry{LISP@{\sc  LISP}}{45}
\indexentry{simplification|(}{45}
\indexentry{Boyer--Moore waterfall}{45}
\indexentry{Boyer, Robert S. (*1946)}{45}
\indexentry{Moore, J Strother (*1947)}{45}
\indexentry{normalation}{45}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{45}
\indexentry{LISP@{\sc  LISP}}{45}
\indexentry{LISP@{\sc  LISP}}{45}
\indexentry{confluence}{45}
\indexentry{Wirth, Claus-Peter (*1963)}{45}
\indexentry{Moore, J Strother (*1947)}{45}
\indexentry{Moore, J Strother (*1947)}{45}
\indexentry{LISP@{\sc  LISP}}{46}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{46}
\indexentry{LISP@{\sc  LISP}}{46}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{46}
\indexentry{LISP@{\sc  LISP}}{46}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{46}
\indexentry{LISP@{\sc  LISP}}{46}
\indexentry{LISP@{\sc  LISP}}{46}
\indexentry{LISP@{\sc  LISP}}{46}
\indexentry{constructor function symbols}{46}
\indexentry{Boyer--Moore waterfall}{46}
\indexentry{Boyer, Robert S. (*1946)}{46}
\indexentry{Moore, J Strother (*1947)}{46}
\indexentry{cross-fertilization}{46}
\indexentry{LISP@{\sc  LISP}}{47}
\indexentry{Boyer--Moore waterfall}{47}
\indexentry{Boyer, Robert S. (*1946)}{47}
\indexentry{Moore, J Strother (*1947)}{47}
\indexentry{Boyer--Moore theorem provers}{47}
\indexentry{Boyer, Robert S. (*1946)}{47}
\indexentry{Moore, J Strother (*1947)}{47}
\indexentry{induction rule}{47}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{47}
\indexentry{LISP@{\sc  LISP}}{47}
\indexentry{induction rule}{47}
\indexentry{induction rule}{47}
\indexentry{Moore, J Strother (*1947)}{47}
\indexentry{Boyer--Moore theorem provers}{47}
\indexentry{Boyer, Robert S. (*1946)}{47}
\indexentry{Moore, J Strother (*1947)}{47}
\indexentry{QuodLibet@{\sc  Quod\discretionary {-}{}{}Libet}}{47}
\indexentry{Schmidt-Samoa, Tobias (*1973)}{47}
\indexentry{induction rule}{47}
\indexentry{destructor elimination}{47}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{47}
\indexentry{LISP@{\sc  LISP}}{47}
\indexentry{induction!explicit}{48}
\indexentry{recursion analysis}{48}
\indexentry{Boyer--Moore theorem provers}{48}
\indexentry{Boyer, Robert S. (*1946)}{48}
\indexentry{Moore, J Strother (*1947)}{48}
\indexentry{simplification|)}{48}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{48}
\indexentry{LISP@{\sc  LISP}}{48}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{48}
\indexentry{LISP@{\sc  LISP}}{48}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{48}
\indexentry{LISP@{\sc  LISP}}{48}
\indexentry{cross-fertilization|(}{48}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{48}
\indexentry{LISP@{\sc  LISP}}{48}
\indexentry{Moore, J Strother (*1947)}{48}
\indexentry{Moore, J Strother (*1947)}{48}
\indexentry{induction rule}{48}
\indexentry{Boyer--Moore theorem provers}{48}
\indexentry{Boyer, Robert S. (*1946)}{48}
\indexentry{Moore, J Strother (*1947)}{48}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{48}
\indexentry{LISP@{\sc  LISP}}{48}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{49}
\indexentry{LISP@{\sc  LISP}}{49}
\indexentry{Boyer--Moore theorem provers}{49}
\indexentry{Boyer, Robert S. (*1946)}{49}
\indexentry{Moore, J Strother (*1947)}{49}
\indexentry{cross-fertilization|)}{49}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{49}
\indexentry{LISP@{\sc  LISP}}{49}
\indexentry{generalization|(}{49}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{49}
\indexentry{LISP@{\sc  LISP}}{49}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{49}
\indexentry{LISP@{\sc  LISP}}{49}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{49}
\indexentry{LISP@{\sc  LISP}}{49}
\indexentry{generalization|)}{49}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{49}
\indexentry{LISP@{\sc  LISP}}{49}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{49}
\indexentry{LISP@{\sc  LISP}}{49}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{49}
\indexentry{LISP@{\sc  LISP}}{49}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{49}
\indexentry{LISP@{\sc  LISP}}{49}
\indexentry{induction rule}{49}
\indexentry{induction!explicit}{49}
\indexentry{Boyer--Moore theorem provers}{49}
\indexentry{Boyer, Robert S. (*1946)}{49}
\indexentry{Moore, J Strother (*1947)}{49}
\indexentry{induction schemes}{49}
\indexentry{induction rule}{49}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{49}
\indexentry{LISP@{\sc  LISP}}{49}
\indexentry{Moore, J Strother (*1947)}{49}
\indexentry{Moore, J Strother (*1947)}{49}
\indexentry{induction rule}{50}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{50}
\indexentry{LISP@{\sc  LISP}}{50}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{50}
\indexentry{LISP@{\sc  LISP}}{50}
\indexentry{induction!explicit}{50}
\indexentry{induction rule}{50}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{50}
\indexentry{LISP@{\sc  LISP}}{50}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{50}
\indexentry{LISP@{\sc  LISP}}{50}
\indexentry{destructor style}{50}
\indexentry{constructor style}{50}
\indexentry{induction templates}{50}
\indexentry{induction variables}{50}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{50}
\indexentry{LISP@{\sc  LISP}}{50}
\indexentry{induction variables}{50}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{50}
\indexentry{LISP@{\sc  LISP}}{50}
\indexentry{Boyer--Moore theorem provers}{50}
\indexentry{Boyer, Robert S. (*1946)}{50}
\indexentry{Moore, J Strother (*1947)}{50}
\indexentry{Moore, J Strother (*1947)}{50}
\indexentry{induction!explicit}{51}
\indexentry{induction!explicit}{51}
\indexentry{Boyer, Robert S. (*1946)}{51}
\indexentry{Moore, J Strother (*1947)}{51}
\indexentry{induction rule}{51}
\indexentry{induction!explicit}{51}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{51}
\indexentry{LISP@{\sc  LISP}}{51}
\indexentry{destructor style}{51}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{51}
\indexentry{LISP@{\sc  LISP}}{51}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{51}
\indexentry{LISP@{\sc  LISP}}{51}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{51}
\indexentry{LISP@{\sc  LISP}}{51}
\indexentry{induction!explicit}{51}
\indexentry{induction!structural}{51}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{51}
\indexentry{LISP@{\sc  LISP}}{51}
\indexentry{Boyer--Moore waterfall}{51}
\indexentry{Boyer, Robert S. (*1946)}{51}
\indexentry{Moore, J Strother (*1947)}{51}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{52}
\indexentry{LISP@{\sc  LISP}}{52}
\indexentry{induction rule}{52}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{52}
\indexentry{LISP@{\sc  LISP}}{52}
\indexentry{induction rule}{52}
\indexentry{induction!explicit}{52}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{52}
\indexentry{LISP@{\sc  LISP}}{52}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{52}
\indexentry{LISP@{\sc  LISP}}{52}
\indexentry{induction!structural}{52}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{52}
\indexentry{LISP@{\sc  LISP}}{52}
\indexentry{recursion analysis}{52}
\indexentry{Boyer--Moore theorem provers}{52}
\indexentry{Boyer, Robert S. (*1946)}{52}
\indexentry{Moore, J Strother (*1947)}{52}
\indexentry{recursion analysis}{52}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{52}
\indexentry{LISP@{\sc  LISP}}{52}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{52}
\indexentry{LISP@{\sc  LISP}}{52}
\indexentry{measured positions}{52}
\indexentry{Ackermann function}{52}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{52}
\indexentry{LISP@{\sc  LISP}}{52}
\indexentry{Thm@{\sc  Thm}}{52}
\indexentry{induction!explicit}{52}
\indexentry{recursion analysis}{52}
\indexentry{induction!explicit}{52}
\indexentry{Thm@{\sc  Thm}}{52}
\indexentry{Thm@{\sc  Thm}|(}{52}
\indexentry{Thm@{\sc  Thm}}{52}
\indexentry{Boyer, Robert S. (*1946)}{52}
\indexentry{Moore, J Strother (*1947)}{52}
\indexentry{Boyer, Robert S. (*1946)}{52}
\indexentry{Moore, J Strother (*1947)}{52}
\indexentry{Boyer--Moore theorem provers}{52}
\indexentry{Boyer, Robert S. (*1946)}{52}
\indexentry{Moore, J Strother (*1947)}{52}
\indexentry{induction rule}{52}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{52}
\indexentry{LISP@{\sc  LISP}}{52}
\indexentry{Moore, J Strother (*1947)}{52}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{52}
\indexentry{LISP@{\sc  LISP}}{52}
\indexentry{ACL2@{\sc  ACL2}}{53}
\indexentry{Thm@{\sc  Thm}}{53}
\indexentry{Qthm@{\sc  Qthm}}{53}
\indexentry{Thm@{\sc  Thm}}{53}
\indexentry{Nqthm@{\sc  Nqthm}}{53}
\indexentry{Thm@{\sc  Thm}}{53}
\indexentry{Qthm@{\sc  Qthm}}{53}
\indexentry{Nqthm@{\sc  Nqthm}}{53}
\indexentry{Qthm@{\sc  Qthm}}{53}
\indexentry{Thm@{\sc  Thm}}{53}
\indexentry{Nqthm@{\sc  Nqthm}}{53}
\indexentry{Nqthm@{\sc  Nqthm}}{53}
\indexentry{Boyer, Robert S. (*1946)}{53}
\indexentry{Moore, J Strother (*1947)}{53}
\indexentry{Kaufmann, Matt (*1952)}{53}
\indexentry{Nqthm@{\sc  Nqthm}}{53}
\indexentry{Nqthm@{\sc  Nqthm}}{53}
\indexentry{Boyer, Robert S. (*1946)}{53}
\indexentry{Moore, J Strother (*1947)}{53}
\indexentry{Nqthm@{\sc  Nqthm}}{53}
\indexentry{Boyer, Robert S. (*1946)}{53}
\indexentry{Moore, J Strother (*1947)}{53}
\indexentry{Moore, J Strother (*1947)}{53}
\indexentry{Boyer, Robert S. (*1946)}{53}
\indexentry{Moore, J Strother (*1947)}{53}
\indexentry{Nqthm@{\sc  Nqthm}}{53}
\indexentry{Boyer, Robert S. (*1946)}{53}
\indexentry{Moore, J Strother (*1947)}{53}
\indexentry{Nqthm@{\sc  Nqthm}}{53}
\indexentry{Thm@{\sc  Thm}}{53}
\indexentry{Boyer, Robert S. (*1946)}{53}
\indexentry{Moore, J Strother (*1947)}{53}
\indexentry{Boyer, Robert S. (*1946)}{53}
\indexentry{Moore, J Strother (*1947)}{53}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{53}
\indexentry{LISP@{\sc  LISP}}{53}
\indexentry{Thm@{\sc  Thm}}{53}
\indexentry{Nqthm@{\sc  Nqthm}}{53}
\indexentry{Boyer, Robert S. (*1946)}{53}
\indexentry{Moore, J Strother (*1947)}{53}
\indexentry{Boyer, Robert S. (*1946)}{53}
\indexentry{Moore, J Strother (*1947)}{53}
\indexentry{Boyer, Robert S. (*1946)}{53}
\indexentry{Moore, J Strother (*1947)}{53}
\indexentry{Moore, J Strother (*1947)}{53}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{53}
\indexentry{LISP@{\sc  LISP}}{53}
\indexentry{Boyer, Robert S. (*1946)}{53}
\indexentry{Moore, J Strother (*1947)}{53}
\indexentry{LISP@{\sc  LISP}}{53}
\indexentry{Moore, J Strother (*1947)}{53}
\indexentry{Boyer, Robert S. (*1946)}{53}
\indexentry{Moore, J Strother (*1947)}{53}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{53}
\indexentry{LISP@{\sc  LISP}}{53}
\indexentry{Boyer, Robert S. (*1946)}{53}
\indexentry{Boyer, Robert S. (*1946)}{53}
\indexentry{Moore, J Strother (*1947)}{53}
\indexentry{Boyer, Robert S. (*1946)}{53}
\indexentry{Moore, J Strother (*1947)}{53}
\indexentry{Boyer, Robert S. (*1946)}{53}
\indexentry{Thm@{\sc  Thm}}{54}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{54}
\indexentry{LISP@{\sc  LISP}}{54}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{54}
\indexentry{LISP@{\sc  LISP}}{54}
\indexentry{Thm@{\sc  Thm}}{54}
\indexentry{induction schemes}{54}
\indexentry{induction schemes}{54}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{54}
\indexentry{LISP@{\sc  LISP}}{54}
\indexentry{Thm@{\sc  Thm}}{54}
\indexentry{shell principle}{54}
\indexentry{shells}{54}
\indexentry{shells}{54}
\indexentry{shells}{54}
\indexentry{Boyer, Robert S. (*1946)}{54}
\indexentry{Moore, J Strother (*1947)}{54}
\indexentry{Boyer, Robert S. (*1946)}{54}
\indexentry{Moore, J Strother (*1947)}{54}
\indexentry{LISP@{\sc  LISP}}{54}
\indexentry{Boyer, Robert S. (*1946)}{54}
\indexentry{Moore, J Strother (*1947)}{54}
\indexentry{Boyer, Robert S. (*1946)}{54}
\indexentry{Moore, J Strother (*1947)}{54}
\indexentry{accessor functions}{54}
\indexentry{recognizer functions}{54}
\indexentry{shell principle}{55}
\indexentry{shells}{55}
\indexentry{shells}{55}
\indexentry{shell principle}{55}
\indexentry{shells}{55}
\indexentry{shells}{55}
\indexentry{Boyer, Robert S. (*1946)}{55}
\indexentry{Moore, J Strother (*1947)}{55}
\indexentry{Boyer, Robert S. (*1946)}{55}
\indexentry{Moore, J Strother (*1947)}{55}
\indexentry{Boyer, Robert S. (*1946)}{55}
\indexentry{Moore, J Strother (*1947)}{55}
\indexentry{Boyer, Robert S. (*1946)}{55}
\indexentry{Moore, J Strother (*1947)}{55}
\indexentry{shells}{56}
\indexentry{shells}{56}
\indexentry{shells}{56}
\indexentry{shells}{56}
\indexentry{shells}{56}
\indexentry{shell principle}{56}
\indexentry{shells}{56}
\indexentry{Thm@{\sc  Thm}}{56}
\indexentry{Thm@{\sc  Thm}}{56}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{56}
\indexentry{LISP@{\sc  LISP}}{56}
\indexentry{Thm@{\sc  Thm}}{56}
\indexentry{Boyer--Moore waterfall}{56}
\indexentry{Boyer, Robert S. (*1946)}{56}
\indexentry{Moore, J Strother (*1947)}{56}
\indexentry{Thm@{\sc  Thm}}{56}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{56}
\indexentry{LISP@{\sc  LISP}}{56}
\indexentry{Boyer, Robert S. (*1946)}{56}
\indexentry{Moore, J Strother (*1947)}{56}
\indexentry{Thm@{\sc  Thm}}{57}
\indexentry{simplification|(}{57}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{57}
\indexentry{LISP@{\sc  LISP}}{57}
\indexentry{Thm@{\sc  Thm}}{57}
\indexentry{Boyer, Robert S. (*1946)}{57}
\indexentry{Moore, J Strother (*1947)}{57}
\indexentry{Thm@{\sc  Thm}}{57}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{57}
\indexentry{LISP@{\sc  LISP}}{57}
\indexentry{shells}{57}
\indexentry{LISP@{\sc  LISP}}{57}
\indexentry{Thm@{\sc  Thm}}{57}
\indexentry{Thm@{\sc  Thm}}{57}
\indexentry{Thm@{\sc  Thm}}{57}
\indexentry{Boyer, Robert S. (*1946)}{57}
\indexentry{Moore, J Strother (*1947)}{57}
\indexentry{Thm@{\sc  Thm}}{57}
\indexentry{Thm@{\sc  Thm}}{57}
\indexentry{Kaufmann, Matt (*1952)}{57}
\indexentry{Boyer, Robert S. (*1946)}{57}
\indexentry{Moore, J Strother (*1947)}{57}
\indexentry{Thm@{\sc  Thm}}{57}
\indexentry{Pieri, Mario (1860--1913)}{57}
\indexentry{Thm@{\sc  Thm}}{57}
\indexentry{Thm@{\sc  Thm}}{57}
\indexentry{Boyer, Robert S. (*1946)}{57}
\indexentry{Moore, J Strother (*1947)}{57}
\indexentry{LISP@{\sc  LISP}}{58}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{58}
\indexentry{LISP@{\sc  LISP}}{58}
\indexentry{LISP@{\sc  LISP}}{58}
\indexentry{LISP@{\sc  LISP}}{58}
\indexentry{Boyer, Robert S. (*1946)}{58}
\indexentry{Moore, J Strother (*1947)}{58}
\indexentry{Boyer, Robert S. (*1946)}{58}
\indexentry{Moore, J Strother (*1947)}{58}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{58}
\indexentry{LISP@{\sc  LISP}}{58}
\indexentry{Thm@{\sc  Thm}}{58}
\indexentry{Boyer--Moore theorem provers}{58}
\indexentry{Boyer, Robert S. (*1946)}{58}
\indexentry{Moore, J Strother (*1947)}{58}
\indexentry{Thm@{\sc  Thm}}{59}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{59}
\indexentry{LISP@{\sc  LISP}}{59}
\indexentry{Thm@{\sc  Thm}}{59}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{59}
\indexentry{LISP@{\sc  LISP}}{59}
\indexentry{Thm@{\sc  Thm}}{59}
\indexentry{destructor style}{59}
\indexentry{measured positions}{59}
\indexentry{induction templates}{59}
\indexentry{measured positions}{59}
\indexentry{Boyer, Robert S. (*1946)}{59}
\indexentry{Moore, J Strother (*1947)}{59}
\indexentry{Thm@{\sc  Thm}}{60}
\indexentry{Thm@{\sc  Thm}}{60}
\indexentry{Boyer--Moore theorem provers}{60}
\indexentry{Boyer, Robert S. (*1946)}{60}
\indexentry{Moore, J Strother (*1947)}{60}
\indexentry{Thm@{\sc  Thm}}{60}
\indexentry{Schmidt-Samoa, Tobias (*1973)}{60}
\indexentry{Thm@{\sc  Thm}}{60}
\indexentry{Thm@{\sc  Thm}}{60}
\indexentry{simplification|)}{60}
\indexentry{Kaufmann, Matt (*1952)}{60}
\indexentry{Moore, J Strother (*1947)}{60}
\indexentry{ACL2@{\sc  ACL2}}{60}
\indexentry{Boyer, Robert S. (*1946)}{60}
\indexentry{Moore, J Strother (*1947)}{60}
\indexentry{Boyer, Robert S. (*1946)}{60}
\indexentry{Moore, J Strother (*1947)}{60}
\indexentry{Boyer--Moore theorem provers}{60}
\indexentry{Boyer, Robert S. (*1946)}{60}
\indexentry{Moore, J Strother (*1947)}{60}
\indexentry{LISP@{\sc  LISP}}{60}
\indexentry{ACL2@{\sc  ACL2}}{60}
\indexentry{LISP@{\sc  LISP}}{60}
\indexentry{Nqthm@{\sc  Nqthm}}{60}
\indexentry{Boyer, Robert S. (*1946)}{60}
\indexentry{Moore, J Strother (*1947)}{60}
\indexentry{Boyer, Robert S. (*1946)}{60}
\indexentry{Moore, J Strother (*1947)}{60}
\indexentry{Thm@{\sc  Thm}}{61}
\indexentry{destructor elimination|(}{61}
\indexentry{Thm@{\sc  Thm}}{61}
\indexentry{destructor style}{61}
\indexentry{destructor style}{61}
\indexentry{destructor style}{61}
\indexentry{destructor elimination}{62}
\indexentry{destructor elimination}{62}
\indexentry{cross-fertilization}{62}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{62}
\indexentry{LISP@{\sc  LISP}}{62}
\indexentry{Thm@{\sc  Thm}}{62}
\indexentry{destructor elimination}{62}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{62}
\indexentry{LISP@{\sc  LISP}}{62}
\indexentry{destructor elimination}{62}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{62}
\indexentry{LISP@{\sc  LISP}}{62}
\indexentry{Thm@{\sc  Thm}}{62}
\indexentry{induction rule}{62}
\indexentry{induction!explicit}{62}
\indexentry{destructor style}{62}
\indexentry{constructor style}{62}
\indexentry{destructor style}{62}
\indexentry{induction!explicit}{62}
\indexentry{Thm@{\sc  Thm}}{62}
\indexentry{destructor elimination}{62}
\indexentry{induction schemes}{62}
\indexentry{Boyer, Robert S. (*1946)}{62}
\indexentry{Moore, J Strother (*1947)}{62}
\indexentry{destructor elimination}{62}
\indexentry{cross-fertilization}{62}
\indexentry{Boyer, Robert S. (*1946)}{62}
\indexentry{Moore, J Strother (*1947)}{62}
\indexentry{destructor elimination}{63}
\indexentry{constructor style}{63}
\indexentry{destructor style}{63}
\indexentry{destructor elimination}{63}
\indexentry{Thm@{\sc  Thm}}{63}
\indexentry{destructor elimination}{63}
\indexentry{destructor elimination}{63}
\indexentry{Boyer, Robert S. (*1946)}{63}
\indexentry{Moore, J Strother (*1947)}{63}
\indexentry{destructor elimination}{64}
\indexentry{Thm@{\sc  Thm}}{64}
\indexentry{destructor elimination}{64}
\indexentry{destructor elimination}{64}
\indexentry{destructor elimination}{64}
\indexentry{destructor elimination}{64}
\indexentry{destructor elimination}{64}
\indexentry{destructor elimination}{64}
\indexentry{destructor elimination}{64}
\indexentry{destructor elimination|)}{64}
\indexentry{Thm@{\sc  Thm}}{64}
\indexentry{Thm@{\sc  Thm}}{64}
\indexentry{Thm@{\sc  Thm}}{64}
\indexentry{destructor elimination}{64}
\indexentry{Thm@{\sc  Thm}}{64}
\indexentry{Thm@{\sc  Thm}}{64}
\indexentry{Thm@{\sc  Thm}}{64}
\indexentry{Thm@{\sc  Thm}}{64}
\indexentry{Boyer, Robert S. (*1946)}{64}
\indexentry{Moore, J Strother (*1947)}{64}
\indexentry{destructor elimination}{64}
\indexentry{Thm@{\sc  Thm}}{64}
\indexentry{Boyer, Robert S. (*1946)}{64}
\indexentry{Moore, J Strother (*1947)}{64}
\indexentry{Thm@{\sc  Thm}}{65}
\indexentry{cross-fertilization|(}{65}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{65}
\indexentry{LISP@{\sc  LISP}}{65}
\indexentry{Thm@{\sc  Thm}}{65}
\indexentry{cross-fertilization|)}{65}
\indexentry{Thm@{\sc  Thm}}{65}
\indexentry{generalization|(}{65}
\indexentry{Thm@{\sc  Thm}}{65}
\indexentry{destructor elimination}{65}
\indexentry{destructor elimination}{65}
\indexentry{Thm@{\sc  Thm}}{65}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{65}
\indexentry{LISP@{\sc  LISP}}{65}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{65}
\indexentry{LISP@{\sc  LISP}}{65}
\indexentry{Thm@{\sc  Thm}}{65}
\indexentry{generalization|)}{65}
\indexentry{Boyer, Robert S. (*1946)}{65}
\indexentry{Moore, J Strother (*1947)}{65}
\indexentry{Boyer, Robert S. (*1946)}{65}
\indexentry{Moore, J Strother (*1947)}{65}
\indexentry{Boyer, Robert S. (*1946)}{65}
\indexentry{Moore, J Strother (*1947)}{65}
\indexentry{Thm@{\sc  Thm}}{66}
\indexentry{elimination of irrelevance|(}{66}
\indexentry{Thm@{\sc  Thm}}{66}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{66}
\indexentry{LISP@{\sc  LISP}}{66}
\indexentry{induction schemes}{66}
\indexentry{Thm@{\sc  Thm}}{66}
\indexentry{constructor function symbols}{66}
\indexentry{shells}{66}
\indexentry{elimination of irrelevance|)}{66}
\indexentry{Boyer, Robert S. (*1946)}{66}
\indexentry{Moore, J Strother (*1947)}{66}
\indexentry{Wirth, Claus-Peter (*1963)}{66}
\indexentry{Thm@{\sc  Thm}}{66}
\indexentry{Thm@{\sc  Thm}}{67}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{67}
\indexentry{LISP@{\sc  LISP}}{67}
\indexentry{recursion analysis|(}{67}
\indexentry{recursion analysis}{67}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{67}
\indexentry{LISP@{\sc  LISP}}{67}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{67}
\indexentry{LISP@{\sc  LISP}}{67}
\indexentry{Thm@{\sc  Thm}}{67}
\indexentry{recursion analysis}{67}
\indexentry{induction rule}{67}
\indexentry{recursion analysis}{67}
\indexentry{Thm@{\sc  Thm}}{67}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{67}
\indexentry{LISP@{\sc  LISP}}{67}
\indexentry{recursion analysis}{67}
\indexentry{Thm@{\sc  Thm}}{67}
\indexentry{Thm@{\sc  Thm}}{67}
\indexentry{recursion analysis}{67}
\indexentry{Thm@{\sc  Thm}}{67}
\indexentry{induction rule}{67}
\indexentry{Thm@{\sc  Thm}}{67}
\indexentry{induction templates}{67}
\indexentry{induction templates}{67}
\indexentry{destructor style}{67}
\indexentry{destructor style}{67}
\indexentry{Thm@{\sc  Thm}}{67}
\indexentry{Thm@{\sc  Thm}}{67}
\indexentry{descente infinie}{67}
\indexentry{recursion analysis}{67}
\indexentry{induction!explicit}{67}
\indexentry{induction templates}{68}
\indexentry{measured positions}{68}
\indexentry{relational descriptions}{68}
\indexentry{relational descriptions}{68}
\indexentry{Ackermann function}{68}
\indexentry{induction templates}{68}
\indexentry{measured positions}{68}
\indexentry{Thm@{\sc  Thm}}{68}
\indexentry{relational descriptions}{68}
\indexentry{induction templates}{68}
\indexentry{Thm@{\sc  Thm}}{68}
\indexentry{induction templates}{68}
\indexentry{Thm@{\sc  Thm}}{68}
\indexentry{destructor style}{68}
\indexentry{shells}{68}
\indexentry{Thm@{\sc  Thm}}{68}
\indexentry{shells}{68}
\indexentry{shells}{68}
\indexentry{induction templates}{68}
\indexentry{Thm@{\sc  Thm}}{68}
\indexentry{Thm@{\sc  Thm}}{68}
\indexentry{Boyer, Robert S. (*1946)}{68}
\indexentry{Moore, J Strother (*1947)}{68}
\indexentry{Boyer, Robert S. (*1946)}{68}
\indexentry{Moore, J Strother (*1947)}{68}
\indexentry{Thm@{\sc  Thm}}{68}
\indexentry{Thm@{\sc  Thm}}{68}
\indexentry{Thm@{\sc  Thm}}{69}
\indexentry{induction rule}{69}
\indexentry{induction templates}{69}
\indexentry{induction templates}{69}
\indexentry{induction schemes}{69}
\indexentry{hitting ratio}{69}
\indexentry{induction schemes}{69}
\indexentry{hitting ratio}{69}
\indexentry{induction schemes}{69}
\indexentry{induction schemes}{69}
\indexentry{hitting ratio}{69}
\indexentry{induction rule}{69}
\indexentry{induction templates}{69}
\indexentry{measured positions}{69}
\indexentry{changeable positions}{69}
\indexentry{destructor style}{69}
\indexentry{induction templates}{69}
\indexentry{induction schemes}{69}
\indexentry{induction schemes}{69}
\indexentry{induction templates}{69}
\indexentry{relational descriptions}{69}
\indexentry{induction schemes}{69}
\indexentry{position sets}{69}
\indexentry{step-case descriptions}{69}
\indexentry{induction variables}{69}
\indexentry{hitting ratio}{69}
\indexentry{induction templates}{69}
\indexentry{destructor style}{69}
\indexentry{hitting ratio}{69}
\indexentry{measured positions}{69}
\indexentry{induction templates}{69}
\indexentry{recursion analysis}{69}
\indexentry{Thm@{\sc  Thm}}{69}
\indexentry{Boyer, Robert S. (*1946)}{69}
\indexentry{Moore, J Strother (*1947)}{69}
\indexentry{induction schemes}{70}
\indexentry{position sets}{70}
\indexentry{induction variables}{70}
\indexentry{hitting ratio}{70}
\indexentry{induction schemes}{70}
\indexentry{induction schemes}{70}
\indexentry{hitting ratio}{70}
\indexentry{induction variables}{70}
\indexentry{induction schemes}{70}
\indexentry{position sets}{70}
\indexentry{induction schemes}{70}
\indexentry{induction schemes}{70}
\indexentry{step-case descriptions}{70}
\indexentry{induction schemes}{70}
\indexentry{step-case descriptions}{70}
\indexentry{induction schemes}{70}
\indexentry{induction schemes}{70}
\indexentry{step-case descriptions}{70}
\indexentry{step-case descriptions}{70}
\indexentry{induction schemes}{70}
\indexentry{induction schemes}{70}
\indexentry{position sets}{70}
\indexentry{hitting ratio}{70}
\indexentry{Boyer, Robert S. (*1946)}{70}
\indexentry{Moore, J Strother (*1947)}{70}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{71}
\indexentry{LISP@{\sc  LISP}}{71}
\indexentry{Thm@{\sc  Thm}}{71}
\indexentry{induction schemes}{71}
\indexentry{step-case descriptions}{71}
\indexentry{induction schemes}{71}
\indexentry{induction schemes}{71}
\indexentry{step-case descriptions}{71}
\indexentry{induction schemes}{71}
\indexentry{step-case descriptions}{71}
\indexentry{step-case descriptions}{71}
\indexentry{induction schemes}{71}
\indexentry{step-case descriptions}{71}
\indexentry{induction schemes}{71}
\indexentry{induction schemes}{71}
\indexentry{induction variables}{71}
\indexentry{step-case descriptions}{71}
\indexentry{induction schemes}{71}
\indexentry{induction schemes}{71}
\indexentry{induction variables}{71}
\indexentry{LISP@{\sc  LISP}}{72}
\indexentry{Thm@{\sc  Thm}}{72}
\indexentry{Boyer--Moore waterfall}{72}
\indexentry{Boyer, Robert S. (*1946)}{72}
\indexentry{Moore, J Strother (*1947)}{72}
\indexentry{destructor elimination}{72}
\indexentry{destructor elimination}{72}
\indexentry{destructor elimination}{72}
\indexentry{descente infinie}{72}
\indexentry{induction!explicit}{72}
\indexentry{Thm@{\sc  Thm}}{72}
\indexentry{induction schemes}{72}
\indexentry{induction templates}{72}
\indexentry{induction schemes}{72}
\indexentry{step-case descriptions}{72}
\indexentry{induction schemes}{72}
\indexentry{induction schemes}{72}
\indexentry{induction schemes}{72}
\indexentry{induction schemes}{72}
\indexentry{induction schemes}{72}
\indexentry{induction schemes}{72}
\indexentry{induction schemes}{72}
\indexentry{induction variables}{72}
\indexentry{induction schemes}{72}
\indexentry{induction schemes}{72}
\indexentry{induction schemes}{72}
\indexentry{Thm@{\sc  Thm}}{72}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{72}
\indexentry{LISP@{\sc  LISP}}{72}
\indexentry{recursion analysis|)}{72}
\indexentry{Boyer, Robert S. (*1946)}{72}
\indexentry{Moore, J Strother (*1947)}{72}
\indexentry{Boyer, Robert S. (*1946)}{72}
\indexentry{Moore, J Strother (*1947)}{72}
\indexentry{Boyer, Robert S. (*1946)}{72}
\indexentry{Moore, J Strother (*1947)}{72}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{72}
\indexentry{LISP@{\sc  LISP}}{72}
\indexentry{Thm@{\sc  Thm}}{73}
\indexentry{Thm@{\sc  Thm}}{73}
\indexentry{induction schemes}{73}
\indexentry{induction schemes}{73}
\indexentry{Thm@{\sc  Thm}}{73}
\indexentry{induction schemes}{73}
\indexentry{induction schemes}{73}
\indexentry{induction schemes}{73}
\indexentry{induction schemes}{73}
\indexentry{Thm@{\sc  Thm}}{73}
\indexentry{induction!explicit}{73}
\indexentry{Thm@{\sc  Thm}}{73}
\indexentry{Nqthm@{\sc  Nqthm}}{73}
\indexentry{ACL2@{\sc  ACL2}}{73}
\indexentry{induction!explicit}{73}
\indexentry{induction schemes}{73}
\indexentry{induction schemes}{73}
\indexentry{induction!explicit}{73}
\indexentry{Walther, Christoph (*1950)}{73}
\indexentry{Walther, Christoph (*1950)}{73}
\indexentry{Bundy, Alan (*1947)}{73}
\indexentry{Thm@{\sc  Thm}}{74}
\indexentry{induction!explicit}{74}
\indexentry{Thm@{\sc  Thm}}{74}
\indexentry{Thm@{\sc  Thm}}{74}
\indexentry{Nqthm@{\sc  Nqthm}}{74}
\indexentry{Thm@{\sc  Thm}}{74}
\indexentry{Thm@{\sc  Thm}}{74}
\indexentry{induction templates}{74}
\indexentry{induction schemes}{74}
\indexentry{Thm@{\sc  Thm}|)}{74}
\indexentry{Nqthm@{\sc  Nqthm}}{75}
\indexentry{induction schemes}{75}
\indexentry{Nqthm@{\sc  Nqthm}}{75}
\indexentry{ACL2@{\sc  ACL2}}{75}
\indexentry{Thm@{\sc  Thm}}{75}
\indexentry{Thm@{\sc  Thm}}{75}
\indexentry{Nqthm@{\sc  Nqthm}}{75}
\indexentry{Nqthm@{\sc  Nqthm}}{75}
\indexentry{induction templates}{75}
\indexentry{Boyer, Robert S. (*1946)}{75}
\indexentry{Moore, J Strother (*1947)}{75}
\indexentry{Thm@{\sc  Thm}}{75}
\indexentry{LISP@{\sc  LISP}}{75}
\indexentry{Thm@{\sc  Thm}}{75}
\indexentry{LISP@{\sc  LISP}}{75}
\indexentry{Boyer, Robert S. (*1946)}{75}
\indexentry{Moore, J Strother (*1947)}{75}
\indexentry{Boyer, Robert S. (*1946)}{75}
\indexentry{Moore, J Strother (*1947)}{75}
\indexentry{Nqthm@{\sc  Nqthm}}{75}
\indexentry{Boyer, Robert S. (*1946)}{75}
\indexentry{Moore, J Strother (*1947)}{75}
\indexentry{LISP@{\sc  LISP}}{75}
\indexentry{LISP@{\sc  LISP}}{75}
\indexentry{LISP@{\sc  LISP}}{75}
\indexentry{LISP@{\sc  LISP}}{75}
\indexentry{Nqthm@{\sc  Nqthm}}{75}
\indexentry{Nqthm@{\sc  Nqthm}}{75}
\indexentry{Nqthm@{\sc  Nqthm}}{75}
\indexentry{linear arithmetic}{75}
\indexentry{Boyer, Robert S. (*1946)}{75}
\indexentry{Moore, J Strother (*1947)}{75}
\indexentry{linear arithmetic}{75}
\indexentry{linear arithmetic}{75}
\indexentry{Presburger, Moj\unprotectedzwithdot es{}z (1904--1943?)}{75}
\indexentry{Presburger, Moj\unprotectedzwithdot es{}z (1904--1943?)}{75}
\indexentry{Nqthm@{\sc  Nqthm}}{76}
\indexentry{Thm@{\sc  Thm}}{76}
\indexentry{Hunt, Warren A.}{76}
\indexentry{Boyer, Robert S. (*1946)}{76}
\indexentry{Moore, J Strother (*1947)}{76}
\indexentry{ACL2@{\sc  ACL2}}{76}
\indexentry{LISP@{\sc  LISP}}{76}
\indexentry{Nqthm@{\sc  Nqthm}}{76}
\indexentry{LISP@{\sc  LISP}}{76}
\indexentry{Thm@{\sc  Thm}}{76}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{76}
\indexentry{LISP@{\sc  LISP}}{76}
\indexentry{Nqthm@{\sc  Nqthm}}{76}
\indexentry{Nqthm@{\sc  Nqthm}}{76}
\indexentry{LISP@{\sc  LISP}}{76}
\indexentry{Nqthm@{\sc  Nqthm}}{76}
\indexentry{Boyer, Robert S. (*1946)}{76}
\indexentry{Moore, J Strother (*1947)}{76}
\indexentry{Nqthm@{\sc  Nqthm}}{76}
\indexentry{Common Lisp@{\sc  Common Lisp}}{76}
\indexentry{LISP@{\sc  LISP}}{76}
\indexentry{Nqthm@{\sc  Nqthm}}{76}
\indexentry{ACL2@{\sc  ACL2}}{76}
\indexentry{ACL2@{\sc  ACL2}}{76}
\indexentry{Kaufmann, Matt (*1952)}{76}
\indexentry{Shankar, Natarajan}{76}
\indexentry{Shankar, Natarajan}{76}
\indexentry{Nqthm@{\sc  Nqthm}}{76}
\indexentry{Boyer--Moore theorem provers}{76}
\indexentry{Boyer, Robert S. (*1946)}{76}
\indexentry{Moore, J Strother (*1947)}{76}
\indexentry{Moore, J Strother (*1947)}{76}
\indexentry{Hunt, Warren A.}{76}
\indexentry{Boyer, Robert S. (*1946)}{76}
\indexentry{Nqthm@{\sc  Nqthm}}{77}
\indexentry{ACL2@{\sc  ACL2}}{77}
\indexentry{ACL2@{\sc  ACL2}}{77}
\indexentry{ACL2@{\sc  ACL2}}{77}
\indexentry{induction templates}{77}
\indexentry{Nqthm@{\sc  Nqthm}}{77}
\indexentry{ACL2@{\sc  ACL2}}{77}
\indexentry{Boyer, Robert S. (*1946)}{77}
\indexentry{Moore, J Strother (*1947)}{77}
\indexentry{Kaufmann, Matt (*1952)}{77}
\indexentry{ACL2@{\sc  ACL2}}{77}
\indexentry{ACL2@{\sc  ACL2}}{77}
\indexentry{Hunt, Warren A.}{77}
\indexentry{Moore, J Strother (*1947)}{77}
\indexentry{ACL2@{\sc  ACL2}}{77}
\indexentry{ACL2@{\sc  ACL2}}{77}
\indexentry{Hunt, Warren A.}{77}
\indexentry{Hunt, Warren A.}{77}
\indexentry{Moore, J Strother (*1947)}{77}
\indexentry{ACL2@{\sc  ACL2}}{77}
\indexentry{ACL2@{\sc  ACL2}}{77}
\indexentry{ACL2@{\sc  ACL2}}{77}
\indexentry{ACL2@{\sc  ACL2}}{78}
\indexentry{Boyer--Moore theorem provers}{78}
\indexentry{Boyer, Robert S. (*1946)}{78}
\indexentry{Moore, J Strother (*1947)}{78}
\indexentry{Boyer--Moore theorem provers}{78}
\indexentry{Boyer, Robert S. (*1946)}{78}
\indexentry{Moore, J Strother (*1947)}{78}
\indexentry{ACL2@{\sc  ACL2}}{78}
\indexentry{ACL2@{\sc  ACL2}}{78}
\indexentry{Isabelle/HOL}{78}
\indexentry{HOL@{\sc  HOL}}{78}
\indexentry{Coq@{\sc  Coq}}{78}
\indexentry{PVS@{\sc  PVS}}{78}
\indexentry{IsaPlanner@{\sc  IsaPlanner}}{78}
\indexentry{Rrl@{\sc  Rrl}}{78}
\indexentry{Rrl@{\sc  Rrl}}{78}
\indexentry{Rrl@{\sc  Rrl}}{78}
\indexentry{Rrl@{\sc  Rrl}}{78}
\indexentry{Inka@{\sc  Inka}}{78}
\indexentry{induction!explicit}{78}
\indexentry{Inka@{\sc  Inka}}{78}
\indexentry{Walther, Christoph (*1950)}{78}
\indexentry{Walther, Christoph (*1950)}{78}
\indexentry{Walther, Christoph (*1950)}{78}
\indexentry{Hutter, Dieter (*1959)}{78}
\indexentry{rippling}{78}
\indexentry{Bundy, Alan (*1947)}{78}
\indexentry{Protzen, Martin (*1962)}{78}
\indexentry{induction!explicit}{79}
\indexentry{induction!lazy}{79}
\indexentry{Protzen, Martin (*1962)}{79}
\indexentry{Inka@{\sc  Inka}}{79}
\indexentry{Inka@{\sc  Inka}}{79}
\indexentry{Boyer--Moore theorem provers}{79}
\indexentry{Boyer, Robert S. (*1946)}{79}
\indexentry{Moore, J Strother (*1947)}{79}
\indexentry{Inka@{\sc  Inka}}{79}
\indexentry{Autexier, Serge (*1971)}{79}
\indexentry{Nqthm@{\sc  Nqthm}}{79}
\indexentry{Inka@{\sc  Inka}}{79}
\indexentry{Inka@{\sc  Inka}}{79}
\indexentry{Hutter, Dieter (*1959)}{79}
\indexentry{Autexier, Serge (*1971)}{79}
\indexentry{Inka@{\sc  Inka}}{79}
\indexentry{Boyer, Robert S. (*1946)}{79}
\indexentry{Moore, J Strother (*1947)}{79}
\indexentry{Inka@{\sc  Inka}}{79}
\indexentry{Autexier, Serge (*1971)}{79}
\indexentry{Inka@{\sc  Inka}}{79}
\indexentry{Inka@{\sc  Inka}}{79}
\indexentry{Boyer, Robert S. (*1946)}{79}
\indexentry{Moore, J Strother (*1947)}{79}
\indexentry{Hutter, Dieter (*1959)}{79}
\indexentry{rippling}{79}
\indexentry{Oyster/CLAM@{{\sc  Oyster}/{\rm  CL\kern -.36em\raise .39ex\hbox {\sc  a}\kern -.15emM}}}{79}
\indexentry{Oyster/CLAM@{{\sc  Oyster}/{\rm  CL\kern -.36em\raise .39ex\hbox {\sc  a}\kern -.15emM}}}{79}
\indexentry{Bundy, Alan (*1947)}{79}
\indexentry{Nuprl@{\sc  Nuprl}}{79}
\indexentry{induction!structural}{79}
\indexentry{Peano, Guiseppe (1858--1932)}{79}
\indexentry{Hutter, Dieter (*1959)}{79}
\indexentry{Bundy, Alan (*1947)}{79}
\indexentry{Nqthm@{\sc  Nqthm}}{79}
\indexentry{Inka@{\sc  Inka}}{79}
\indexentry{Hutter, Dieter (*1959)}{79}
\indexentry{Oyster/CLAM@{{\sc  Oyster}/{\rm  CL\kern -.36em\raise .39ex\hbox {\sc  a}\kern -.15emM}}}{79}
\indexentry{Bundy, Alan (*1947)}{79}
\indexentry{QuodLibet@{\sc  Quod\discretionary {-}{}{}Libet}}{79}
\indexentry{Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}{79}
\indexentry{Oyster/CLAM@{{\sc  Oyster}/{\rm  CL\kern -.36em\raise .39ex\hbox {\sc  a}\kern -.15emM}}}{79}
\indexentry{ACL2@{\sc  ACL2}}{79}
\indexentry{Bundy, Alan (*1947)}{79}
\indexentry{Oyster/CLAM@{{\sc  Oyster}/{\rm  CL\kern -.36em\raise .39ex\hbox {\sc  a}\kern -.15emM}}}{79}
\indexentry{Bundy, Alan (*1947)}{79}
\indexentry{Bundy, Alan (*1947)}{79}
\indexentry{rippling}{80}
\indexentry{Oyster/CLAM@{{\sc  Oyster}/{\rm  CL\kern -.36em\raise .39ex\hbox {\sc  a}\kern -.15emM}}}{80}
\indexentry{rippling}{80}
\indexentry{Bundy, Alan (*1947)}{80}
\indexentry{recursion analysis}{80}
\indexentry{ripple analysis}{80}
\indexentry{Bundy, Alan (*1947)}{80}
\indexentry{Bundy, Alan (*1947)}{80}
\indexentry{induction!explicit|)}{80}
\indexentry{induction!explicit}{80}
\indexentry{induction!explicit}{80}
\indexentry{proof planning}{80}
\indexentry{rippling}{80}
\indexentry{induction!explicit}{80}
\indexentry{Boyer, Robert S. (*1946)}{80}
\indexentry{Moore, J Strother (*1947)}{80}
\indexentry{induction!explicit}{80}
\indexentry{induction!implicit}{80}
\indexentry{induction!explicit}{80}
\indexentry{Rrl@{\sc  Rrl}}{80}
\indexentry{QuodLibet@{\sc  Quod\discretionary {-}{}{}Libet}}{80}
\indexentry{proof planning}{80}
\indexentry{Bundy, Alan (*1947)}{80}
\indexentry{Bundy, Alan (*1947)}{80}
\indexentry{rippling}{81}
\indexentry{Aubin, Raymond}{81}
\indexentry{rippling}{81}
\indexentry{Bundy, Alan (*1947)}{81}
\indexentry{rippling}{81}
\indexentry{Bundy, Alan (*1947)}{81}
\indexentry{recursion analysis}{81}
\indexentry{rippling}{81}
\indexentry{Bundy, Alan (*1947)}{81}
\indexentry{rippling}{81}
\indexentry{induction!explicit}{81}
\indexentry{induction!explicit}{81}
\indexentry{descente infinie}{81}
\indexentry{Bundy, Alan (*1947)}{81}
\indexentry{Aubin, Raymond}{81}
\indexentry{rippling}{81}
\indexentry{Aubin, Raymond}{81}
\indexentry{Bundy, Alan (*1947)}{81}
\indexentry{Aubin, Raymond}{81}
\indexentry{rippling}{81}
\indexentry{Hutter, Dieter (*1959)}{81}
\indexentry{Bundy, Alan (*1947)}{81}
\indexentry{Bundy, Alan (*1947)}{81}
\indexentry{induction!implicit}{82}
\indexentry{induction!explicit}{82}
\indexentry{induction!implicit}{82}
\indexentry{Boyer, Robert S. (*1946)}{82}
\indexentry{Moore, J Strother (*1947)}{82}
\indexentry{induction!implicit}{82}
\indexentry{induction!implicit}{82}
\indexentry{Boyer, Robert S. (*1946)}{82}
\indexentry{Moore, J Strother (*1947)}{82}
\indexentry{induction!explicit}{82}
\indexentry{induction!implicit}{82}
\indexentry{proof by consistency}{82}
\indexentry{consistency}{82}
\indexentry{Boyer, Robert S. (*1946)}{82}
\indexentry{Moore, J Strother (*1947)}{82}
\indexentry{Boyer, Robert S. (*1946)}{82}
\indexentry{Moore, J Strother (*1947)}{82}
\indexentry{Boyer, Robert S. (*1946)}{82}
\indexentry{Moore, J Strother (*1947)}{82}
\indexentry{Boyer, Robert S. (*1946)}{82}
\indexentry{Aubin, Raymond}{82}
\indexentry{Aubin, Raymond}{82}
\indexentry{Gramlich, Bernhard (*1959)}{82}
\indexentry{proof by consistency}{82}
\indexentry{Unicom@{\sc  Unicom}}{82}
\indexentry{Gramlich, Bernhard (*1959)}{82}
\indexentry{proof by consistency}{83}
\indexentry{proof by consistency}{83}
\indexentry{induction!explicit}{83}
\indexentry{QuodLibet@{\sc  Quod\discretionary {-}{}{}Libet}}{83}
\indexentry{induction!implicit}{83}
\indexentry{Wirth, Claus-Peter (*1963)}{83}
\indexentry{induction!lazy}{83}
\indexentry{descente infinie}{83}
\indexentry{induction!explicit}{83}
\indexentry{induction rule}{83}
\indexentry{induction!implicit}{83}
\indexentry{induction rule}{83}
\indexentry{induction!explicit}{83}
\indexentry{Gramlich, Bernhard (*1959)}{83}
\indexentry{Wirth, Claus-Peter (*1963)}{83}
\indexentry{QuodLibet@{\sc  Quod\discretionary {-}{}{}Libet}}{83}
\indexentry{Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}{83}
\indexentry{induction!inductionless}{83}
\indexentry{induction!implicit}{83}
\indexentry{induction rule}{83}
\indexentry{induction!implicit}{84}
\indexentry{induction!implicit}{84}
\indexentry{descente infinie}{84}
\indexentry{Protzen, Martin (*1962)}{84}
\indexentry{induction!lazy}{84}
\indexentry{descente infinie}{84}
\indexentry{Wirth, Claus-Peter (*1963)}{84}
\indexentry{proof by consistency}{84}
\indexentry{induction!explicit}{84}
\indexentry{descente infinie}{84}
\indexentry{induction!explicit}{84}
\indexentry{QuodLibet@{\sc  Quod\discretionary {-}{}{}Libet}}{84}
\indexentry{QuodLibet@{\sc  Quod\discretionary {-}{}{}Libet}}{84}
\indexentry{induction!explicit}{84}
\indexentry{Nqthm@{\sc  Nqthm}}{84}
\indexentry{Inka@{\sc  Inka}}{84}
\indexentry{induction!implicit}{84}
\indexentry{Unicom@{\sc  Unicom}}{84}
\indexentry{Gramlich, Bernhard (*1959)}{84}
\indexentry{Rrl@{\sc  Rrl}}{84}
\indexentry{Wirth, Claus-Peter (*1963)}{84}
\indexentry{Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}{84}
\indexentry{Unicom@{\sc  Unicom}}{84}
\indexentry{descente infinie}{84}
\indexentry{induction!implicit}{84}
\indexentry{Unicom@{\sc  Unicom}}{84}
\indexentry{QuodLibet@{\sc  Quod\discretionary {-}{}{}Libet}}{84}
\indexentry{Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}{84}
\indexentry{Unicom@{\sc  Unicom}}{84}
\indexentry{Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}{84}
\indexentry{Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}{84}
\indexentry{induction!explicit}{85}
\indexentry{Wirth, Claus-Peter (*1963)}{85}
\indexentry{Wirth, Claus-Peter (*1963)}{85}
\indexentry{Gramlich, Bernhard (*1959)}{85}
\indexentry{constructor variables}{85}
\indexentry{Wirth, Claus-Peter (*1963)}{85}
\indexentry{Wirth, Claus-Peter (*1963)}{85}
\indexentry{Gramlich, Bernhard (*1959)}{85}
\indexentry{confluence}{85}
\indexentry{QuodLibet@{\sc  Quod\discretionary {-}{}{}Libet}}{85}
\indexentry{consistency}{85}
\indexentry{Wirth, Claus-Peter (*1963)}{85}
\indexentry{QuodLibet@{\sc  Quod\discretionary {-}{}{}Libet}}{85}
\indexentry{QuodLibet@{\sc  Quod\discretionary {-}{}{}Libet}}{85}
\indexentry{Loechner, Bernd (*1967)@{L\"ochner, Bernd (*1967)}}{85}
\indexentry{QuodLibet@{\sc  Quod\discretionary {-}{}{}Libet}}{85}
\indexentry{Wirth, Claus-Peter (*1963)}{85}
\indexentry{Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}{85}
\indexentry{QuodLibet@{\sc  Quod\discretionary {-}{}{}Libet}}{85}
\indexentry{Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}{85}
\indexentry{Wirth, Claus-Peter (*1963)}{85}
\indexentry{consistency}{85}
\indexentry{QuodLibet@{\sc  Quod\discretionary {-}{}{}Libet}}{85}
\indexentry{Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}{85}
\indexentry{Wirth, Claus-Peter (*1963)}{85}
\indexentry{Wirth, Claus-Peter (*1963)}{85}
\indexentry{consistency}{85}
\indexentry{Wirth, Claus-Peter (*1963)}{85}
\indexentry{Gramlich, Bernhard (*1959)}{85}
\indexentry{QuodLibet@{\sc  Quod\discretionary {-}{}{}Libet}}{85}
\indexentry{Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}{85}
\indexentry{Wirth, Claus-Peter (*1963)}{85}
\indexentry{induction!implicit}{85}
\indexentry{Loechner, Bernd (*1967)@{L\"ochner, Bernd (*1967)}}{86}
\indexentry{QuodLibet@{\sc  Quod\discretionary {-}{}{}Libet}}{86}
\indexentry{Loechner, Bernd (*1967)@{L\"ochner, Bernd (*1967)}}{86}
\indexentry{QuodLibet@{\sc  Quod\discretionary {-}{}{}Libet}}{86}
\indexentry{descente infinie}{86}
\indexentry{Wirth, Claus-Peter (*1963)}{86}
\indexentry{Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}{86}
\indexentry{QuodLibet@{\sc  Quod\discretionary {-}{}{}Libet}}{86}
\indexentry{Common Lisp@{\sc  Common Lisp}}{86}
\indexentry{Schmidt-Samoa, Tobias (*1973)}{86}
\indexentry{descente infinie}{86}
\indexentry{QuodLibet@{\sc  Quod\discretionary {-}{}{}Libet}}{86}
\indexentry{Wirth, Claus-Peter (*1963)}{86}
\indexentry{QuodLibet@{\sc  Quod\discretionary {-}{}{}Libet}}{86}
\indexentry{Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}{86}
\indexentry{recursion analysis}{86}
\indexentry{Boyer, Robert S. (*1946)}{86}
\indexentry{Moore, J Strother (*1947)}{86}
\indexentry{QuodLibet@{\sc  Quod\discretionary {-}{}{}Libet}}{86}
\indexentry{Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}{86}
\indexentry{ACL2@{\sc  ACL2}}{86}
\indexentry{QuodLibet@{\sc  Quod\discretionary {-}{}{}Libet}}{86}
\indexentry{recursion analysis}{86}
\indexentry{recursion analysis}{86}
\indexentry{induction variables}{86}
\indexentry{induction templates}{86}
\indexentry{induction!explicit}{86}
\indexentry{induction schemes}{86}
\indexentry{descente infinie}{86}
\indexentry{Wirth, Claus-Peter (*1963)}{86}
\indexentry{Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}{86}
\indexentry{Schmidt-Samoa, Tobias (*1973)}{86}
\indexentry{QuodLibet@{\sc  Quod\discretionary {-}{}{}Libet}}{86}
\indexentry{QuodLibet@{\sc  Quod\discretionary {-}{}{}Libet}}{87}
\indexentry{Schmidt-Samoa, Tobias (*1973)}{87}
\indexentry{Schmidt-Samoa, Tobias (*1973)}{87}
\indexentry{linear arithmetic}{87}
\indexentry{Schmidt-Samoa, Tobias (*1973)}{87}
\indexentry{QuodLibet@{\sc  Quod\discretionary {-}{}{}Libet}}{87}
\indexentry{QuodLibet@{\sc  Quod\discretionary {-}{}{}Libet}}{87}
\indexentry{descente infinie}{87}
\indexentry{QuodLibet@{\sc  Quod\discretionary {-}{}{}Libet}}{87}
\indexentry{QuodLibet@{\sc  Quod\discretionary {-}{}{}Libet}}{87}
\indexentry{descente infinie}{87}
\indexentry{induction!lazy}{87}
\indexentry{induction!explicit}{87}
\indexentry{induction!explicit}{87}
\indexentry{descente infinie}{87}
\indexentry{Wirth, Claus-Peter (*1963)}{87}
\indexentry{QuodLibet@{\sc  Quod\discretionary {-}{}{}Libet}}{87}
\indexentry{induction schemes}{87}
\indexentry{induction schemes}{87}
\indexentry{QuodLibet@{\sc  Quod\discretionary {-}{}{}Libet}}{87}
\indexentry{Thm@{\sc  Thm}}{87}
\indexentry{induction schemes}{87}
\indexentry{QuodLibet@{\sc  Quod\discretionary {-}{}{}Libet}}{87}
\indexentry{Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}{87}
\indexentry{QuodLibet@{\sc  Quod\discretionary {-}{}{}Libet}}{87}
\indexentry{recursion analysis}{87}
\indexentry{Thm@{\sc  Thm}}{87}
\indexentry{Thm@{\sc  Thm}}{87}
\indexentry{descente infinie}{87}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{88}
\indexentry{LISP@{\sc  LISP}}{88}
\indexentry{Thm@{\sc  Thm}}{88}
\indexentry{Nqthm@{\sc  Nqthm}}{88}
\indexentry{ACL2@{\sc  ACL2}}{88}
\indexentry{ACL2@{\sc  ACL2}}{88}
\indexentry{ACL2@{\sc  ACL2}}{89}
\indexentry{Boyer--Moore theorem provers}{89}
\indexentry{Boyer, Robert S. (*1946)}{89}
\indexentry{Moore, J Strother (*1947)}{89}
\indexentry{Acerbi, Fabio}{89}
\indexentry{Barner, Klaus}{89}
\indexentry{Boyer, Robert S. (*1946)}{89}
\indexentry{Bundy, Alan (*1947)}{89}
\indexentry{Goldstein, Catherine (*1958)}{89}
\indexentry{Gramlich, Bernhard (*1959)}{89}
\indexentry{Hunt, Warren A.}{89}
\indexentry{Hutter, Dieter (*1959)}{89}
\indexentry{Kaufmann, Matt (*1952)}{89}
\indexentry{Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}{89}
\indexentry{Schmidt-Samoa, Tobias (*1973)}{89}
\indexentry{Wirth, Claus-Peter (*1963)}{89}
\indexentry{Acerbi, Fabio}{90}
\indexentry{Acerbi, Fabio}{90}
\indexentry{Ackermann, Wilhelm (1896--1962)}{90}
\indexentry{Ackermann, Wilhelm (1896--1962)}{90}
\indexentry{Ackermann, Wilhelm (1896--1962)}{90}
\indexentry{Ackermann, Wilhelm (1896--1962)}{90}
\indexentry{Aubin, Raymond}{90}
\indexentry{Aubin, Raymond}{90}
\indexentry{Aubin, Raymond}{90}
\indexentry{Aubin, Raymond}{90}
\indexentry{Aubin, Raymond}{90}
\indexentry{Aubin, Raymond}{90}
\indexentry{Autexier, Serge (*1971)}{90}
\indexentry{Autexier, Serge (*1971)}{90}
\indexentry{Hutter, Dieter (*1959)}{90}
\indexentry{Inka@{\sc  Inka}}{90}
\indexentry{Autexier, Serge (*1971)}{90}
\indexentry{Autexier, Serge (*1971)}{90}
\indexentry{Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}{90}
\indexentry{Schmidt-Samoa, Tobias (*1973)}{90}
\indexentry{Wirth, Claus-Peter (*1963)}{90}
\indexentry{QuodLibet@{\sc  Quod\discretionary {-}{}{}Libet}}{90}
\indexentry{Goedel, Kurt@G\"odel, Kurt (1906--1978)}{90}
\indexentry{Barner, Klaus}{90}
\indexentry{Barner, Klaus}{90}
\indexentry{Fermat, Pierre (160?--1665)}{90}
\indexentry{Barner, Klaus}{90}
\indexentry{Barner, Klaus}{90}
\indexentry{Barner, Klaus}{90}
\indexentry{Barner, Klaus}{90}
\indexentry{Barner, Klaus}{90}
\indexentry{Barner, Klaus}{91}
\indexentry{Barner, Klaus}{91}
\indexentry{Barner, Klaus}{91}
\indexentry{Barner, Klaus}{91}
\indexentry{Barner, Klaus}{91}
\indexentry{Barner, Klaus}{91}
\indexentry{Barner, Klaus}{91}
\indexentry{Benzmueller, Christoph (*1968)@{Benzm\"uller, Christoph\ (*1968)}}{91}
\indexentry{Benzmueller, Christoph (*1968)@{Benzm\"uller, Christoph\ (*1968)}}{91}
\indexentry{Leo-II@{\sc  Leo-II}}{91}
\indexentry{Hunt, Warren A.}{91}
\indexentry{Moore, J Strother (*1947)}{91}
\indexentry{Kowalski, Robert A. (*1941)}{91}
\indexentry{Kowalski, Robert A. (*1941)}{91}
\indexentry{Hutter, Dieter (*1959)}{91}
\indexentry{Walther, Christoph (*1950)}{91}
\indexentry{Siekmann, J\unprotectedoe rg\ (*1941)}{91}
\indexentry{Bledsoe, W. W. (1921--1995)}{91}
\indexentry{Bledsoe, W. W. (1921--1995)}{91}
\indexentry{Bledsoe, W. W. (1921--1995)}{91}
\indexentry{Bledsoe, W. W. (1921--1995)}{91}
\indexentry{Boyer, Robert S. (*1946)}{91}
\indexentry{Bledsoe, W. W. (1921--1995)}{91}
\indexentry{Bledsoe, W. W. (1921--1995)}{91}
\indexentry{Bledsoe, W. W. (1921--1995)}{91}
\indexentry{Boyer, Robert S. (*1946)}{91}
\indexentry{Bledsoe, W. W. (1921--1995)}{91}
\indexentry{Bledsoe, W. W. (1921--1995)}{91}
\indexentry{Bledsoe, W. W. (1921--1995)}{91}
\indexentry{Bourbaki, Nicolas (pseudonym)}{91}
\indexentry{Bourbaki, Nicolas (pseudonym)}{91}
\indexentry{Bourbaki, Nicolas (pseudonym)}{91}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Bourbaki, Nicolas (pseudonym)}{92}
\indexentry{Boyer, Robert S. (*1946)}{92}
\indexentry{Moore, J Strother (*1947)}{92}
\indexentry{Boyer, Robert S. (*1946)}{92}
\indexentry{Moore, J Strother (*1947)}{92}
\indexentry{Boyer, Robert S. (*1946)}{92}
\indexentry{Moore, J Strother (*1947)}{92}
\indexentry{Boyer, Robert S. (*1946)}{92}
\indexentry{Moore, J Strother (*1947)}{92}
\indexentry{Boyer, Robert S. (*1946)}{92}
\indexentry{Moore, J Strother (*1947)}{92}
\indexentry{Meltzer, Bernard (1916?--2008)}{92}
\indexentry{Michie, Donald (1923--2007)}{92}
\indexentry{Boyer, Robert S. (*1946)}{92}
\indexentry{Moore, J Strother (*1947)}{92}
\indexentry{Boyer, Robert S. (*1946)}{92}
\indexentry{Moore, J Strother (*1947)}{92}
\indexentry{Boyer, Robert S. (*1946)}{92}
\indexentry{Moore, J Strother (*1947)}{92}
\indexentry{Boyer, Robert S. (*1946)}{92}
\indexentry{Moore, J Strother (*1947)}{92}
\indexentry{Boyer, Robert S. (*1946)}{92}
\indexentry{Moore, J Strother (*1947)}{92}
\indexentry{Boyer, Robert S. (*1946)}{92}
\indexentry{Moore, J Strother (*1947)}{92}
\indexentry{Boyer, Robert S. (*1946)}{92}
\indexentry{Boyer--Moore fast string searching algorithm}{92}
\indexentry{Moore, J Strother (*1947)}{92}
\indexentry{Boyer, Robert S. (*1946)}{92}
\indexentry{Boyer--Moore fast string searching algorithm}{92}
\indexentry{Moore, J Strother (*1947)}{92}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{LISP@{\sc  LISP}}{93}
\indexentry{Bledsoe, W. W. (1921--1995)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{linear arithmetic}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Nqthm@{\sc  Nqthm}}{93}
\indexentry{Nqthm@{\sc  Nqthm}}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Moore, J Strother (*1947)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Boyer, Robert S. (*1946)}{93}
\indexentry{Wirth, Claus-Peter (*1963)}{93}
\indexentry{Hunt, Warren A.}{93}
\indexentry{Hunt, Warren A.}{93}
\indexentry{Satallax@{\sc  Satallax}}{94}
\indexentry{Gramlich, Bernhard (*1959)}{94}
\indexentry{Hillenbrand, Thomas}{94}
\indexentry{Hillenbrand, Thomas}{94}
\indexentry{Waldmeister@{\sc  Wald\discretionary {-}{}{}Meister}}{94}
\indexentry{Bundy, Alan (*1947)}{94}
\indexentry{Bundy, Alan (*1947)}{94}
\indexentry{Bundy, Alan (*1947)}{94}
\indexentry{Bundy, Alan (*1947)}{94}
\indexentry{Oyster/CLAM@{{\sc  Oyster}/{\rm  CL\kern -.36em\raise .39ex\hbox {\sc  a}\kern -.15emM}}}{94}
\indexentry{Bundy, Alan (*1947)}{94}
\indexentry{Bundy, Alan (*1947)}{94}
\indexentry{Bundy, Alan (*1947)}{94}
\indexentry{Bundy, Alan (*1947)}{94}
\indexentry{Hutter, Dieter (*1959)}{94}
\indexentry{Bundy, Alan (*1947)}{94}
\indexentry{Bundy, Alan (*1947)}{94}
\indexentry{Bundy, Alan (*1947)}{94}
\indexentry{Bundy, Alan (*1947)}{94}
\indexentry{Bundy, Alan (*1947)}{94}
\indexentry{Bundy, Alan (*1947)}{94}
\indexentry{Bundy, Alan (*1947)}{94}
\indexentry{Bundy, Alan (*1947)}{94}
\indexentry{Robinson, J. Alan (*1930?)}{94}
\indexentry{Burstall, Rod M. (*1934)}{94}
\indexentry{Burstall, Rod M. (*1934)}{94}
\indexentry{Burstall, Rod M. (*1934)}{94}
\indexentry{Burstall, Rod M. (*1934)}{94}
\indexentry{Bourbaki, Nicolas (pseudonym)}{94}
\indexentry{Robinson, J. Alan (*1930?)}{95}
\indexentry{Nuprl@{\sc  Nuprl}}{95}
\indexentry{Michie, Donald (1923--2007)}{95}
\indexentry{Dedekind, Richard (1831--1916)}{95}
\indexentry{Dedekind, Richard (1831--1916)}{95}
\indexentry{Dedekind, Richard (1831--1916)}{95}
\indexentry{Dedekind, Richard (1831--1916)}{95}
\indexentry{Dedekind, Richard (1831--1916)}{95}
\indexentry{Dedekind, Richard (1831--1916)}{95}
\indexentry{Noether, Emmy (1882--1935)}{95}
\indexentry{Dedekind, Richard (1831--1916)}{95}
\indexentry{Dedekind, Richard (1831--1916)}{95}
\indexentry{IsaPlanner@{\sc  IsaPlanner}}{95}
\indexentry{Euclid}{95}
\indexentry{Euclid}{95}
\indexentry{Fries, Jakob Friedrich (1773--1843)}{96}
\indexentry{Fries, Jakob Friedrich (1773--1843)}{96}
\indexentry{Hippasus of Metapontum (ca.\,550\,{\sc  b.c.})}{96}
\indexentry{Gabbay, Dov (*1945)}{96}
\indexentry{Gabbay, Dov (*1945)}{96}
\indexentry{Gabbay, Dov (*1945)}{96}
\indexentry{Gabbay, Dov (*1945)}{96}
\indexentry{Robinson, J. Alan (*1930?)}{96}
\indexentry{Gentzen, Gerhard (1909--1945)}{96}
\indexentry{Goedel, Kurt@G\"odel, Kurt (1906--1978)}{96}
\indexentry{Goedel, Kurt@G\"odel, Kurt (1906--1978)}{96}
\indexentry{Goedel, Kurt@G\"odel, Kurt (1906--1978)}{96}
\indexentry{Heijenoort, Jean van (1912--1986)}{96}
\indexentry{Goedel, Kurt@G\"odel, Kurt (1906--1978)}{96}
\indexentry{Goedel, Kurt@G\"odel, Kurt (1906--1978)}{96}
\indexentry{Goedel, Kurt@G\"odel, Kurt (1906--1978)}{96}
\indexentry{Goedel, Kurt@G\"odel, Kurt (1906--1978)}{96}
\indexentry{Meltzer, Bernard (1916?--2008)}{96}
\indexentry{Goedel, Kurt@G\"odel, Kurt (1906--1978)}{96}
\indexentry{Goedel, Kurt@G\"odel, Kurt (1906--1978)}{96}
\indexentry{Feferman, Sol(omon) (*1928)}{96}
\indexentry{Dawson, John W., Jr.\ (*1944)}{96}
\indexentry{Dawson, John W., Jr.\ (*1944)}{96}
\indexentry{Goldfarb, Warren}{96}
\indexentry{Heijenoort, Jean van (1912--1986)}{96}
\indexentry{Kleene, Stephen C. (1909--1994)}{96}
\indexentry{Parsons, Charles (*1933)}{96}
\indexentry{Sieg, Wilfried}{96}
\indexentry{Kowalski, Robert A. (*1941)}{96}
\indexentry{Goldstein, Catherine (*1958)}{96}
\indexentry{Goldstein, Catherine (*1958)}{96}
\indexentry{Fermat, Pierre (160?--1665)}{96}
\indexentry{Gordon, Mike J. C. (*1948)}{96}
\indexentry{Gordon, Mike J. C. (*1948)}{96}
\indexentry{LCF@{\sc  LCF}}{96}
\indexentry{HOL@{\sc  HOL}}{96}
\indexentry{Gramlich, Bernhard (*1959)}{97}
\indexentry{Gramlich, Bernhard (*1959)}{97}
\indexentry{Unicom@{\sc  Unicom}}{97}
\indexentry{Gramlich, Bernhard (*1959)}{97}
\indexentry{Wirth, Claus-Peter (*1963)}{97}
\indexentry{Gramlich, Bernhard (*1959)}{97}
\indexentry{Wirth, Claus-Peter (*1963)}{97}
\indexentry{Gramlich, Bernhard (*1959)}{97}
\indexentry{Gramlich, Bernhard (*1959)}{97}
\indexentry{Michie, Donald (1923--2007)}{97}
\indexentry{Heijenoort, Jean van (1912--1986)}{97}
\indexentry{Heijenoort, Jean van (1912--1986)}{97}
\indexentry{Coq@{\sc  Coq}}{97}
\indexentry{Hilbert, David (1862--1943)}{97}
\indexentry{Bernays, Paul (1888--1977)}{97}
\indexentry{Hilbert, David (1862--1943)}{97}
\indexentry{Bernays, Paul (1888--1977)}{97}
\indexentry{Hilbert, David (1862--1943)}{97}
\indexentry{Bernays, Paul (1888--1977)}{97}
\indexentry{Hilbert, David (1862--1943)}{97}
\indexentry{Bernays, Paul (1888--1977)}{97}
\indexentry{Hilbert, David (1862--1943)}{97}
\indexentry{Bernays, Paul (1888--1977)}{97}
\indexentry{Hilbert, David (1862--1943)}{97}
\indexentry{Bernays, Paul (1888--1977)}{97}
\indexentry{Hilbert, David (1862--1943)}{97}
\indexentry{Bernays, Paul (1888--1977)}{97}
\indexentry{Hilbert, David (1862--1943)}{97}
\indexentry{Bernays, Paul (1888--1977)}{97}
\indexentry{Hilbert, David (1862--1943)}{97}
\indexentry{Bernays, Paul (1888--1977)}{97}
\indexentry{Hilbert, David (1862--1943)}{97}
\indexentry{Bernays, Paul (1888--1977)}{97}
\indexentry{Hilbert, David (1862--1943)}{97}
\indexentry{Bernays, Paul (1888--1977)}{97}
\indexentry{Hilbert, David (1862--1943)}{97}
\indexentry{Bernays, Paul (1888--1977)}{97}
\indexentry{Hilbert, David (1862--1943)}{97}
\indexentry{Bernays, Paul (1888--1977)}{97}
\indexentry{Hilbert, David (1862--1943)}{97}
\indexentry{Bernays, Paul (1888--1977)}{97}
\indexentry{Hilbert, David (1862--1943)}{97}
\indexentry{Bernays, Paul (1888--1977)}{97}
\indexentry{Hilbert, David (1862--1943)}{97}
\indexentry{Bernays, Paul (1888--1977)}{97}
\indexentry{Wirth, Claus-Peter (*1963)}{97}
\indexentry{Wirth, Claus-Peter (*1963)}{97}
\indexentry{Siekmann, J\unprotectedoe rg\ (*1941)}{97}
\indexentry{Gabbay, Dov (*1945)}{97}
\indexentry{Sieg, Wilfried}{97}
\indexentry{Anellis, Irving H. (1946--2013)}{97}
\indexentry{Buldt, Bernd}{97}
\indexentry{Parsons, Charles (*1933)}{97}
\indexentry{Peckhaus, Volker (*1955)}{97}
\indexentry{Tait, William W. (*1929)}{97}
\indexentry{Tapp, Christian}{97}
\indexentry{Zach, Richard}{97}
\indexentry{Hillenbrand, Thomas}{97}
\indexentry{Loechner, Bernd (*1967)@{L\"ochner, Bernd (*1967)}}{97}
\indexentry{Hillenbrand, Thomas}{97}
\indexentry{Loechner, Bernd (*1967)@{L\"ochner, Bernd (*1967)}}{97}
\indexentry{Waldmeister@{\sc  Wald\discretionary {-}{}{}Meister}}{97}
\indexentry{Haskell@{\sc  Haskell}}{97}
\indexentry{Hunt, Warren A.}{98}
\indexentry{Hunt, Warren A.}{98}
\indexentry{Hunt, Warren A.}{98}
\indexentry{Hunt, Warren A.}{98}
\indexentry{Hunt, Warren A.}{98}
\indexentry{Hunt, Warren A.}{98}
\indexentry{Hunt, Warren A.}{98}
\indexentry{Hunt, Warren A.}{98}
\indexentry{Hunt, Warren A.}{98}
\indexentry{Hunt, Warren A.}{98}
\indexentry{Hutter, Dieter (*1959)}{98}
\indexentry{Bundy, Alan (*1947)}{98}
\indexentry{Hutter, Dieter (*1959)}{98}
\indexentry{Bundy, Alan (*1947)}{98}
\indexentry{Hutter, Dieter (*1959)}{98}
\indexentry{Hutter, Dieter (*1959)}{98}
\indexentry{Inka@{\sc  Inka}}{98}
\indexentry{Hutter, Dieter (*1959)}{98}
\indexentry{Hutter, Dieter (*1959)}{98}
\indexentry{Siekmann, J\unprotectedoe rg\ (*1941)}{98}
\indexentry{Hutter, Dieter (*1959)}{98}
\indexentry{Hutter, Dieter (*1959)}{98}
\indexentry{Bundy, Alan (*1947)}{98}
\indexentry{Bundy, Alan (*1947)}{98}
\indexentry{Benzmueller, Christoph (*1968)@{Benzm\"uller, Christoph\ (*1968)}}{98}
\indexentry{Rrl@{\sc  Rrl}}{98}
\indexentry{Rrl@{\sc  Rrl}}{98}
\indexentry{Kaufmann, Matt (*1952)}{98}
\indexentry{Kaufmann, Matt (*1952)}{98}
\indexentry{Moore, J Strother (*1947)}{98}
\indexentry{ACL2@{\sc  ACL2}}{98}
\indexentry{Kaufmann, Matt (*1952)}{98}
\indexentry{Kaufmann, Matt (*1952)}{98}
\indexentry{Moore, J Strother (*1947)}{98}
\indexentry{Kowalski, Robert A. (*1941)}{99}
\indexentry{Kowalski, Robert A. (*1941)}{99}
\indexentry{Kowalski, Robert A. (*1941)}{99}
\indexentry{Kowalski, Robert A. (*1941)}{99}
\indexentry{Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}{99}
\indexentry{Wirth, Claus-Peter (*1963)}{99}
\indexentry{Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}{99}
\indexentry{Wirth, Claus-Peter (*1963)}{99}
\indexentry{Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}{99}
\indexentry{Wirth, Claus-Peter (*1963)}{99}
\indexentry{Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}{99}
\indexentry{Wirth, Claus-Peter (*1963)}{99}
\indexentry{Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}{99}
\indexentry{Wirth, Claus-Peter (*1963)}{99}
\indexentry{Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}{99}
\indexentry{Wirth, Claus-Peter (*1963)}{99}
\indexentry{Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}{99}
\indexentry{Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}{99}
\indexentry{Inka@{\sc  Inka}}{99}
\indexentry{Nqthm@{\sc  Nqthm}}{99}
\indexentry{Rrl@{\sc  Rrl}}{99}
\indexentry{Unicom@{\sc  Unicom}}{99}
\indexentry{Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}{99}
\indexentry{Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}{99}
\indexentry{Robinson, J. Alan (*1930?)}{99}
\indexentry{Loechner, Bernd (*1967)@{L\"ochner, Bernd (*1967)}}{99}
\indexentry{Loechner, Bernd (*1967)@{L\"ochner, Bernd (*1967)}}{99}
\indexentry{Fermat, Pierre (160?--1665)}{100}
\indexentry{Smith, James T.}{100}
\indexentry{Smith, James T.}{100}
\indexentry{Pieri, Mario (1860--1913)}{100}
\indexentry{Siekmann, J\unprotectedoe rg\ (*1941)}{100}
\indexentry{Meltzer, Bernard (1916?--2008)}{100}
\indexentry{Michie, Donald (1923--2007)}{100}
\indexentry{Meltzer, Bernard (1916?--2008)}{100}
\indexentry{Michie, Donald (1923--2007)}{100}
\indexentry{Meltzer, Bernard (1916?--2008)}{100}
\indexentry{Meltzer, Bernard (1916?--2008)}{100}
\indexentry{Michie, Donald (1923--2007)}{100}
\indexentry{Michie, Donald (1923--2007)}{100}
\indexentry{Moore, J Strother (*1947)}{100}
\indexentry{Moore, J Strother (*1947)}{100}
\indexentry{Kaufmann, Matt (*1952)}{100}
\indexentry{Moore, J Strother (*1947)}{100}
\indexentry{Moore, J Strother (*1947)}{100}
\indexentry{Moore, J Strother (*1947)}{100}
\indexentry{Moore, J Strother (*1947)}{100}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{100}
\indexentry{LISP@{\sc  LISP}}{100}
\indexentry{Moore, J Strother (*1947)}{100}
\indexentry{Moore, J Strother (*1947)}{100}
\indexentry{Moore, J Strother (*1947)}{100}
\indexentry{Pure LISP Theorem Prover@{\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{100}
\indexentry{LISP@{\sc  LISP}}{100}
\indexentry{Moore, J Strother (*1947)}{100}
\indexentry{Moore, J Strother (*1947)}{100}
\indexentry{Moore, J Strother (*1947)}{100}
\indexentry{Moore, J Strother (*1947)}{100}
\indexentry{Moore, J Strother (*1947)}{100}
\indexentry{Moore, J Strother (*1947)}{100}
\indexentry{Moore, J Strother (*1947)}{100}
\indexentry{Moore, J Strother (*1947)}{100}
\indexentry{Moore, J Strother (*1947)}{100}
\indexentry{Padoa, Alessandro (1868--1937)}{101}
\indexentry{Padoa, Alessandro (1868--1937)}{101}
\indexentry{ml@{\sc  ml}}{101}
\indexentry{Peano, Guiseppe (1858--1932)}{101}
\indexentry{Peano, Guiseppe (1858--1932)}{101}
\indexentry{P\'eter, R\'osza (1905--1977)}{101}
\indexentry{P\'eter, R\'osza (1905--1977)}{101}
\indexentry{Pieri, Mario (1860--1913)}{101}
\indexentry{Pieri, Mario (1860--1913)}{101}
\indexentry{Smith, James T.}{101}
\indexentry{Milner, Robin (1934--2010)}{101}
\indexentry{Presburger, Moj\unprotectedzwithdot es{}z (1904--1943?)}{101}
\indexentry{Presburger, Moj\unprotectedzwithdot es{}z (1904--1943?)}{101}
\indexentry{Protzen, Martin (*1962)}{101}
\indexentry{Protzen, Martin (*1962)}{101}
\indexentry{Bundy, Alan (*1947)}{101}
\indexentry{Protzen, Martin (*1962)}{101}
\indexentry{Protzen, Martin (*1962)}{101}
\indexentry{Protzen, Martin (*1962)}{101}
\indexentry{Protzen, Martin (*1962)}{101}
\indexentry{Gerson, Levi ben (1288--1344)}{101}
\indexentry{Robinson, J. Alan (*1930?)}{101}
\indexentry{Robinson, J. Alan (*1930?)}{101}
\indexentry{Schmidt-Samoa, Tobias (*1973)}{102}
\indexentry{Schmidt-Samoa, Tobias (*1973)}{102}
\indexentry{linear arithmetic}{102}
\indexentry{Schmidt-Samoa, Tobias (*1973)}{102}
\indexentry{Schmidt-Samoa, Tobias (*1973)}{102}
\indexentry{Schmidt-Samoa, Tobias (*1973)}{102}
\indexentry{Schmidt-Samoa, Tobias (*1973)}{102}
\indexentry{Scott, Dana S. (*1932)}{102}
\indexentry{Scott, Dana S. (*1932)}{102}
\indexentry{Shankar, Natarajan}{102}
\indexentry{Shankar, Natarajan}{102}
\indexentry{Shankar, Natarajan}{102}
\indexentry{Shankar, Natarajan}{102}
\indexentry{Shankar, Natarajan}{102}
\indexentry{Shankar, Natarajan}{102}
\indexentry{Shankar, Natarajan}{102}
\indexentry{Shankar, Natarajan}{102}
\indexentry{Shankar, Natarajan}{102}
\indexentry{Siekmann, J\unprotectedoe rg\ (*1941)}{102}
\indexentry{Siekmann, J\unprotectedoe rg\ (*1941)}{102}
\indexentry{Presburger, Moj\unprotectedzwithdot es{}z (1904--1943?)}{102}
\indexentry{Common Lisp@{\sc  Common Lisp}}{102}
\indexentry{Simonyi, Charles}{102}
\indexentry{descente infinie}{102}
\indexentry{Coq@{\sc  Coq}}{102}
\indexentry{Walther, Christoph (*1950)}{103}
\indexentry{Walther, Christoph (*1950)}{103}
\indexentry{Walther, Christoph (*1950)}{103}
\indexentry{Walther, Christoph (*1950)}{103}
\indexentry{Walther, Christoph (*1950)}{103}
\indexentry{Walther, Christoph (*1950)}{103}
\indexentry{Walther, Christoph (*1950)}{103}
\indexentry{Walther, Christoph (*1950)}{103}
\indexentry{Gabbay, Dov (*1945)}{103}
\indexentry{Walther, Christoph (*1950)}{103}
\indexentry{Walther, Christoph (*1950)}{103}
\indexentry{Wirth, Claus-Peter (*1963)}{103}
\indexentry{Wirth, Claus-Peter (*1963)}{103}
\indexentry{Wirth, Claus-Peter (*1963)}{103}
\indexentry{Gramlich, Bernhard (*1959)}{103}
\indexentry{Wirth, Claus-Peter (*1963)}{103}
\indexentry{Gramlich, Bernhard (*1959)}{103}
\indexentry{Wirth, Claus-Peter (*1963)}{103}
\indexentry{Gramlich, Bernhard (*1959)}{103}
\indexentry{Wirth, Claus-Peter (*1963)}{103}
\indexentry{Gramlich, Bernhard (*1959)}{103}
\indexentry{Bundy, Alan (*1947)}{103}
\indexentry{Wirth, Claus-Peter (*1963)}{103}
\indexentry{Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}{103}
\indexentry{Wirth, Claus-Peter (*1963)}{103}
\indexentry{Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}{103}
\indexentry{Wirth, Claus-Peter (*1963)}{103}
\indexentry{Wirth, Claus-Peter (*1963)}{103}
\indexentry{Gramlich, Bernhard (*1959)}{103}
\indexentry{Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}{103}
\indexentry{Wirth, Claus-Peter (*1963)}{103}
\indexentry{Gramlich, Bernhard (*1959)}{103}
\indexentry{Wirth, Claus-Peter (*1963)}{103}
\indexentry{Gramlich, Bernhard (*1959)}{103}
\indexentry{Wirth, Claus-Peter (*1963)}{103}
\indexentry{Wirth, Claus-Peter (*1963)}{103}
\indexentry{Benzmueller, Christoph (*1968)@{Benzm\"uller, Christoph\ (*1968)}}{103}
\indexentry{Autexier, Serge (*1971)}{103}
\indexentry{Herbrand, Jacques (1908--1938)}{103}
\indexentry{Gabbay, Dov (*1945)}{103}
\indexentry{Wirth, Claus-Peter (*1963)}{103}
\indexentry{Wirth, Claus-Peter (*1963)}{103}
\indexentry{Wirth, Claus-Peter (*1963)}{103}
\indexentry{Wirth, Claus-Peter (*1963)}{103}
\indexentry{Wirth, Claus-Peter (*1963)}{103}
\indexentry{Wirth, Claus-Peter (*1963)}{103}
\indexentry{descente infinie}{103}
\indexentry{Wirth, Claus-Peter (*1963)}{103}
\indexentry{Wirth, Claus-Peter (*1963)}{103}
\indexentry{Hutter, Dieter (*1959)}{103}
\indexentry{Wirth, Claus-Peter (*1963)}{103}
\indexentry{Wirth, Claus-Peter (*1963)}{103}
\indexentry{Wirth, Claus-Peter (*1963)}{104}
\indexentry{Wirth, Claus-Peter (*1963)}{104}
\indexentry{Wirth, Claus-Peter (*1963)}{104}
\indexentry{Wirth, Claus-Peter (*1963)}{104}
\indexentry{Wirth, Claus-Peter (*1963)}{104}
\indexentry{Wirth, Claus-Peter (*1963)}{104}
\indexentry{Wirth, Claus-Peter (*1963)}{104}
\indexentry{Wirth, Claus-Peter (*1963)}{104}
\indexentry{Wirth, Claus-Peter (*1963)}{104}
\indexentry{Wirth, Claus-Peter (*1963)}{104}
\indexentry{Wirth, Claus-Peter (*1963)}{104}
\indexentry{Heijenoort, Jean van (1912--1986)}{104}
\indexentry{Wirth, Claus-Peter (*1963)}{104}
\indexentry{Wirth, Claus-Peter (*1963)}{104}
\indexentry{Wirth, Claus-Peter (*1963)}{104}
\indexentry{Wirth, Claus-Peter (*1963)}{104}
\indexentry{Wirth, Claus-Peter (*1963)}{104}
\indexentry{Wirth, Claus-Peter (*1963)}{104}
\indexentry{Wirth, Claus-Peter (*1963)}{104}
\indexentry{Boyer, Robert S. (*1946)}{104}
\indexentry{Moore, J Strother (*1947)}{104}
\indexentry{Wirth, Claus-Peter (*1963)}{104}
\indexentry{Wirth, Claus-Peter (*1963)}{104}
\indexentry{Presburger, Moj\unprotectedzwithdot es{}z (1904--1943?)}{104}
\indexentry{Axiom of Choice|see{choice, Axiom of Choice}}{104}
\indexentry{Axiom of Structural Induction|see{induction, structural}}{104}
\indexentry{Theorem of Noetherian Induction|see{induction, Noetherian}}{104}
\indexentry{structural induction|see{induction, structural}}{104}
\indexentry{Noetherian induction|see{induction, Noetherian}}{104}
\indexentry{induction!descente infinie|see{descente infinie}}{104}
\indexentry{Presburger Arithmetic|see{linear arithmetic}}{104}