\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=.375,bb=0 0 540 344]{waterfall.ps.gz}%
[scale=.1875,bb=0 0 1078 708]{waterfall.eps.gz}%
% [scale=.15,bb=0 0 1078 708]{waterfall.eps.gz}%
}\notop\notop\halftop\halftop%\footnotesize
\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.}
\notop\notop\halftop\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{hit.\,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
{The Metamathematics Unit of the University of \EB\ was renamed
 into ``\Dept\ of Computational Logic'' in late 1971,
 and was absorbed into the new ``\Dept\ of \AI'' in \Oct\,1974.
 It was founded and headed by \meltzername.
 In the early 1970s,
 the \uniEB\ hosted most remarkable scientists,
 of which the following are relevant in our context:
 \\[+.3ex]\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, {\namefont Goodstein})
  &\bundylifetime
 \\\milnername
  &(1973--1979, LFCS)
  &(no \PhD)
  &\milnerlifetime\ 
 \\\end{tabular}}%
\nopagebreak\\[+.3ex]%
\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
\\\end{tabular}}
\nopagebreak\\[+.3ex]\noindent(Sources: 
\cite{meltzer-1975}, 
\cite{kowalski-1988}, 
\etc)%\notop
%\halftop
}

\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*{Acknowlegdgements}}{}
\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}}
