\newcommand\inductionrule{\index{induction rule}\mbox{induction} rule}
\newcommand\inductionrules{\inductionrule s}
\renewcommand\lessymbol{\ident{lessp}}
\renewcommand\sizesymbol{\ident{count}}
\newcommand\HopeParkSquare{\index{Hope Park}Hope Park Square}
\newcommand\englishEBPURELISPMACHINE{ICL--4130}
\newcommand\eineenglishEBPURELISPMACHINE{an \englishEBPURELISPMACHINE}
\newcommand\englishdiesespapier{this article}
\newcommand\englishDiesespapier{This article}
\newcommand\englishDiesesPapier{This Article}
\newcommand\englishdiesesPapier{this Article}

\newcommand\figurewaterfall[1]{\begin{figure}[#1]%
%\yestop
\index{destructor elimination}%
\index{simplification}%
\index{generalization}%
\index{destructor elimination}%
\index{cross-fertilization}%
\index{elimination of irrelevance}%
\noindent\LINEnomath{\includegraphics
[scale=.36,bb=0 0 1078 708]{waterfall.eps.gz}%
}\caption
{The \boyermooreWaterfall\label{figure waterfall}}
\LINEnomath{\footnotesize Note that a formula falls back to 
the center pool after each successful
application \hfill\mbox{}%
\\[-1ex]%
\mbox{}\hfill
of one of the stages in the circle.}
\yestop%\yestop
\end{figure}}

\newcommand\figuremerging[1]{\begin{figure}[#1]%\notop
\LINEmaths{\begin{array}{l|l l l@{\hspace*{-1.7em}}r}
 &\mbox{pos.\ set~~}
 &\mbox{ind.\ var.s}
 &\mbox{step-case description}
 &%2 * 
  \mbox{hitting\,ratio}
\\\hline\headroom
  1
 &\{1\}
 &\{x\}
 &\displayset{\!\!\!\displaytrip
  {\!\!\domres\id{\{x,z\}}}
  {\{\mu_1\}}
  {\{x\tightnotequal\zeropp\}\!\!}\!\!\!}
 &1
\\2
 &\{2\}
 &\{x\}
 &\displayset{\!\!\!\displaytrip{\!\!\domres\id{\{x,y\}}}{\{\mu_2\}}
  {\{x\tightnotequal\zeropp\}\!\!}\!\!\!}
 &1%2
\\3
 &\{2\}
 &\{y\}
 &\displayset{\!\!\!\displaytrip{\!\!\domres\id{\{x,y\}}}{\{\mu_2\}}
  {\{y\tightnotequal\zeropp\}\!\!}\!\!\!}
 &1%2
\\4
 &\{3\}
 &\{y\}
 &\displayset{\!\!\!\displaytrip{\!\!\domres\id{\{y,z\}}}{\{\mu_3\}}
  {\{y\tightnotequal\zeropp\}\!\!}\!\!\!}
 &1%2
\\5
 &\{3\}
 &\{z\}
 &\displayset{\!\!\!\displaytrip{\!\!\domres\id{\{y,z\}}}{\{\mu_3\}}
  {\{z\tightnotequal\zeropp\}\!\!}\!\!\!}
 &1%2
\\6
 &\{2\}
 &\{x,y\}
 &\displayset{\!\!\!\displaytrip{\!\!\domres\id{\{x,y\}}}{\{\mu_2\}}
  {\{x\tightnotequal\zeropp\comma y\tightnotequal\zeropp\}\!\!}\!\!\!}
 &2
\\7
 &\{3\}
 &\{y,z\}
 &\displayset{\!\!\!\displaytrip{\!\!\domres\id{\{y,z\}}}{\{\mu_3\}}
  {\{y\tightnotequal\zeropp\comma z\tightnotequal\zeropp\}\!\!}\!\!\!}
 &2%4
\\8
 &\{2,3\}
 &\{x,y,z\}
 &\displayset{\!\!\!\displaytrip{\!\!\domres\id{\{x,y,z\}}}{\{\mu_4\}}
  {\{x\tightnotequal\zeropp\comma 
     y\tightnotequal\zeropp\comma 
     z\tightnotequal\zeropp\}\!\!}\!\!\!}
 &4%8
\\9
 &\{1,2,3\}
 &\{x,y,z\}
 &\displayset{\!\!\!\displaytrip{\!\!\domres\id{\{x,y,z\}}}{\{\mu_4\}}
  {\{x\tightnotequal\zeropp\comma 
     y\tightnotequal\zeropp\comma 
     z\tightnotequal\zeropp\}\!\!}\!\!\!}
 &5%9
\\\end{array}}{}
\\\headroom\LINEnomath
{\math{\mu_1=\{x\tight\mapsto\ppp x\comma z\tight\mapsto\ppp z\}}, 
\hskip 2em
\math{\mu_2=\{x\tight\mapsto\ppp x\comma y\tight\mapsto\ppp y\}},
\nlnomath
\math{\mu_3=\{y\tight\mapsto\ppp y\comma z\tight\mapsto\ppp z\}}, \hskip 2em
and \hskip 2em
\maths{\mu_4=\{x\tight\mapsto\ppp x\comma y\tight\mapsto\ppp y
\comma z\tight\mapsto\ppp z\}}.}
\\\LINEnomath{pos.\ 
% set 
= 
position%set
; \ \ \ \
ind.\ var.s = set of induction variables;
\ \ \ \  
hit.\ = hitting% 
% \nlnomath
% \math{2 * \mbox{hit.\ ratio}} = hitting ratio multiplied by \nlbmaths 2
.}%
\notop\halftop\caption{\protect\footroom
The induction schemes of \examref{example merging 2}\label
{figure induction schemes}}\notop\notop\end{figure}}

\newcommand\footnoteonMetamathematicsUnitandMembersofUnivEB
{\majorheadroom
 In the early 1970s,
 the \uniEB\ hosted most remarkable scientists,
 of which the following are relevant in our context
 (sources: \cite{meltzer-1975}, \cite{kowalski-1988}, \etc):
 \\\mbox{}\\\noindent\LINEnomath{\begin{tabular}{l|l l l}
  &\uniEBshort\ 
  &\PhD
  &life time 
 \\
  &(time, \Dept)
  &(year, advisor)
  &(birth--death)
 \\\hline
   \michiename
  &(1965--1984, MI)
  &(1953, unknown)
  &\michielifetime
 \\
   \meltzername
  &(1965--1978%Dec 31 %some say 1977
    , CL)
  &(1953, {\namefont %Reinhold 
    F\ue rth})
  &\meltzerlifetime
 \\\popplestonename
  &(1965--1984, MI)
  &(no \PhD)
  &\popplestonelifetime
 \\\burstallname\ 
  &(1965--2000, MI \& \Dept\,AI)
  &(1966, {\namefont Dudley})
  &\burstalllifetime\ 
 \\\kowalskiname  
  &(1967%Oct
    --1974%Dec
    , CL)
  &(1970, \meltzer)
  &\kowalskilifetime
 \\\hayesname
  &(1967--1973, CL)
  &(1973, \meltzer)
  &\hayeslifetime
 \\\plotkinname\ 
  &(1968--today, CL \& LFCS)
  &(1972, \burstall)
  &\plotkinlifetime\
 \\\moorename
  &(1970--1973, CL)
  &(1973, \burstall)
  &\moorelifetime
 \\\gordonname\ 
  &(1970--1978, MI)
  &(1973, \burstall)
  &\gordonlifetime
 \\\boyername
  &(1971--%
  % 1974%
  1973%
% Hi CP.  Bob read the article -- at least he spent as
% much time on it as he felt he could -- and only made
% one suggestion: he believes that he and his family left
% Edinburgh for California in 1973 (probably November or
% December).  (I know I left in December, 1973: I
% celebrated New Years 1974 in Palo Alto.)
  , CL)
  &(1971, \bledsoe)
  &\boyerlifetime
 \\\bundyname
  &(1971--today, CL)
  &(1971, {\goodsteinindex\goodstein})
  &\bundylifetime
 \\\milnername
  &(1973--1979, LFCS)
  &(no \PhD)
  &\milnerlifetime\ 
 \\\end{tabular}}%
\\[+3ex]\noindent
\getittotheright{\begin{tabular}{@{}l@{~~}l@{~~}l@{}}
  CL
 &= 
 &Metamathematics Unit (founded and headed by \meltzername) 
\\
&&(new name from late 1971 to \Oct\,1974: \Dept\ of Computational Logic)
\\
&&(new name from \Oct\,1974: \Dept\ of \AI)
\\MI
 &=
 &Experimental Programming Unit (founded and headed by \michiename)
\\
&&(new name from 1966 to \Oct\,1974: 
   \Dept\ for Machine Intelligence and Perception)
\\
&&(new name from \Oct\,1974: 
   Machine Intelligence Unit)
\\LFCS
 &=
 &Laboratory for Foundations of Computer Science\footroom
\\\end{tabular}}}
\newcommand\footnotetextworkwithacomputerinearlyseventies
{\footnotetext{%
\majorheadroom
Today's
readers might have difficulty imagining the computing infrastructure
in Scotland in the early 1970s.
\par\boyer\ and \moore\ developed their software
on \eineenglishEBPURELISPMACHINE, \hskip.1em
with \nlbmath{64\kByte} (\nlbmath{128\kByte} in 1972) 
core memory (RAM)\@. \hskip.2em
Paper tape was used for archival storage. \hskip.1em
The machine was physically located
in the \ForrestHillEB\ building of the University of \EB, \hskip.1em
about 1\km\ from \HopeParkSquare. \hskip.15em
A rudimentary time-sharing system allowed several
users at once to run lightweight applications from teletype machines at 
\HopeParkSquare. \par
During the day
\boyer\ and \moore\
worked at \HopeParkSquare, 
with frequent trips by foot
\nopagebreak
or bicycle through \mbox{The Meadows}
to \ForrestHillEB\ to make archival paper tapes
\nopagebreak
or to pick up line-printer output. \hskip.3em
\nopagebreak\pagebreak
During the night
\nopagebreak
---~when they could often have
\nopagebreak
the \englishEBPURELISPMACHINE\ to themselves~--- 
\nopagebreak
they often worked at \boyer's home where another
\nopagebreak
teletype was available.\par
The only high-level programming language supported was {\sc POP--2}, \hskip.2em
a simple stack-based list-processing language with an 
{\sc Algol}-like syntax, \cfnlb\ \cite{pop2}.\par
Programs were prepared with a primitive text editor modeled on a paper-tape
editor: 
A \nolinebreak disk file could 
be
copied through a one byte buffer to an output file. \hskip.2em
By halting the copying and typing characters into or deleting characters from
the buffer one could edit a file 
---~a process that usually took several passes.
\hskip.3em
Memory limitations of the \mbox\englishEBPURELISPMACHINE\ 
prohibited storing large files in memory
for \nolinebreak editing. \par
In \nolinebreak their very early 
collaboration, \hskip.1em
\boyer\ and \moore\ solved this
problem by inventing what has come to be called the 
``piece table\closequotecommasmallextraspace
whereby
an edited document is represented by a linked list of ``pieces'' referring to
the original file which remains on disk. \hskip.3em
Their ``77-editor'' \cite{boyer-moore-davies-1973} 
\hskip.05em (written in
1971 and named for the disk track on which it resided) \hskip.1em
provided an interface like \MIT's Teco, \hskip.1em
but with {\sc POP--2} as the command language.
It was thus with their own editor that \boyer\ and \moore\
wrote the code for the {\PURELISPTP}.
\par
 The 77-editor was widely used by researchers at \HopeParkSquare\ 
 until the \mbox\englishEBPURELISPMACHINE\ was decommissioned. 
 When \moore\
 went to Xerox PARC 
 %CP (logicians and historians will not know where Xerox PARC is,
 %    and then do not get the "Alto" reference below):
 in Palo Alto (CA)
 (\Dec\,1973), \hskip.2em 
 the \boyermoore\ representation \cite{moore-1981} was adopted by
 \simonyiname\ \simonyilifetime\ for the Bravo editor on the Alto 
 and subsequently found its way into
 Microsoft Word, \cfnlb\ \cite{simonyi-interview}.\majorfootroom%
}}

\newcommand\bigexampleformulaone
{\exists\tight<\stopq\inparenthesesoplist{\!
   \forall\pair x y\stopq\inparentheses{\!\!\inpit{\plusppnoparentheses x y
\tightequal\plusppnoparentheses y x}
\nottight\antiimplies
\forall\pair{x''}{y''}\,\tight<\,\pair x y\stopq\inpit
{\plusppnoparentheses{x''}{y''}
\tightequal\plusppnoparentheses{y''}{x''}}\!\!}\!\!\!
\oplistund
\!\Wellfpp<}}%
\renewcommand\mindexsymbol[1]{w_{#1}}
\renewcommand\Avignon{\mbox{A\hskip-.09em vignon}}

\mathcommand\termsofdepthnovars[1]{{\mathcal T}_{#1}}

\newcommand{\responsible}[1]{\protect\marginpar{\textbf{Res.:} #1}}


\newenvironment{draft}{\begin{quote}\hrulefill\par\sl\textbf{Draft:}}{\hrulefill\par\end{quote}}

\newcommand\frenchfont{}%{\sf}
\newcommand\germanfont{}%{\fraknomath}
\newcommand\germanfontfootnote{}%{\scriptscriptfrak}
\renewcommand\namefont{}

\newcommand\ednote[1]{{\red\Frak #1\marginpar{\huge\math\forall}}}

\renewcommand\etc{etc.}
\renewcommand\etalabbrev{{\it et al.}}

\renewcommand\secondincompletenesstheorem{second \incompletenesstheorem}
\renewcommand\secondIncompletenessTheorem{Second \IncompletenessTheorem}

\renewcommand\udiff{if}

\def\citep{\cite}
\def\citet#1{\citeauthor{#1} \shortcite{#1}}

\newenvironment{ack}{\section*{Acknowledgments}}{}
\newcommand\qed
{\relax\ifmmode\hskip2em \Box\else\unskip\nobreak\hskip1em $\Box$\fi}

\newcommand\secondreaders[1]
{\insert\footins{%
    \def\@thefnmark{$\ast$}
    \reset@font\footnotesize
    \interlinepenalty\interfootnotelinepenalty
    \splittopskip\footnotesep
    \splitmaxdepth \dp\strutbox \floatingpenalty \@MM
    \hsize\columnwidth \@parboxrestore
    \protected@edef\@currentlabel{%
       \csname p@footnote\endcsname
       \@thefnmark
    }%
    \color@begingroup
      \@makefntext{%
        \rule\z@\footnotesep\ignorespaces{Second Readers: #1}
\@finalstrut\strutbox}%
    \color@endgroup}}
