\documentstyle[makeidx]{article}
\makeindex
%\setlength{\oddsidemargin}{.5in}
%\setlength{\evensidemargin}{.5in}
%\setlength{\textwidth}{5.8in}
\begin{document}
%\setlength{\parindent}{0pt}
%\newcounter{bean}
%\begin{list}{\arabic{bean}.}{\usecounter{bean}\setlength{\leftmargin}{0pt}\setlength{\rightmargin}{0pt}\setlength{\listparindent}{20pt}\setlength{\parsep}{5pt}}
%\item[]

\begin{verbatim}#|
 Copyright (C) 1994 by Natarajan Shankar.  All Rights Reserved.

 This script is hereby placed in the public domain, and therefore unlimited
 editing and redistribution is permitted.

 NO WARRANTY

 Natarajan Shankar PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT IS
 PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED,
 INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND
 FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND
 PERFORMANCE OF THE SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU
 ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.

 IN NO EVENT WILL Natarajan Shankar BE LIABLE TO YOU FOR ANY DAMAGES, ANY LOST
 PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES
 ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT NOT
 LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED
 BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF SUCH
 DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.

|#

\end{verbatim}
\noindent{\sc Event}:   Start with the initial {\bf thm} theory.

\addvspace{18pt}
\begin{verbatim};An Annotated Script of A MECHANICAL PROOF OF THE CHURCH-ROSSER THEOREM.
;                          by
;                    N. Shankar
;
;What follows is a list of events (definitions and lemmas) in the mechanical
;proof of the Church-Rosser theorem that was carried out with the Boyer-Moore
;theorem-prover.  The formal expressions below are subtle and complex and
;the annotations provide only a small amount of help.  The proof consists of
;the following parts -
;1. Formalization of Lambda-calculus in the standard notation.
;2. Formalization of Lambda-calculus in the de Bruijn notation.
;3. Proof of the Diamond property of walks in the de Bruijn notation.
;4. Proof of the Diamond property of sequences of beta-steps.
;5. Proof that a sequence of beta-steps is the transitive closure of
;   a walk.
;6. Proof that the standard notation translates into the de Bruijn notation.
;7. Proof that the Church-Rosser proof for the de Bruijn notation can be
;   translated back into the standard notation.
;8. Proof of the Diamond property of walks directly in the standard notation.
;standard formalization:  The prefix "N" stands for "normal".  The two shells
;NLAMBDA and NCOMB represent lambda-abstraction and application, respectively.
;Variables are represented by numbers and constants by literal atoms.
\end{verbatim}
\noindent{\sc Event}:   Add the shell {\it{nlambda\/}}\index{nlambda}, with recognizer function symbol {\it{nlambdap\/}} and 2 accessors: {\it{nbind\/}}, with type restriction (one-of numberp) and default value zero; {\it{nbody\/}}, with type restriction (none-of) and default value zero.

\addvspace{18pt}

\noindent{\sc Event}:   Add the shell {\it{ncomb\/}}\index{ncomb}, with recognizer function symbol {\it{ncombp\/}} and 2 accessors: {\it{nleft\/}}, with type restriction (none-of) and default value zero; {\it{nright\/}}, with type restriction (none-of) and default value zero.

\addvspace{18pt}
\begin{verbatim};(NSUBST X Y N) is the result of substituting term Y for variable N in term X.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{nsubst} \\  
\=\+{\rm{nsubst}}\,({\it{x\/}}, {\it{y\/}}, {\it{n\/}})\index{nsubst} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{nlambdap}}\,({\it{x\/}})\index{nlambdap} \\ 
{\bf then }\=\+{\bf if }{\rm{nbind}}\,({\it{x\/}})\index{nbind} $=$ {\it{n\/}}$\;\;${\bf then }{\it{x\/}} \\ 
{\bf else }{\rm{nlambda}}\,({\rm{nbind}}\,({\it{x\/}})\index{nbind}, {\rm{nsubst}}\,({\rm{nbody}}\,({\it{x\/}})\index{nbody}, {\it{y\/}}, {\it{n\/}})\index{nsubst})\index{nlambda}$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{ncombp}}\,({\it{x\/}})\index{ncombp} \\ 
{\bf then }{\rm{ncomb}}\,({\rm{nsubst}}\,({\rm{nleft}}\,({\it{x\/}})\index{nleft}, {\it{y\/}}, {\it{n\/}})\index{nsubst}, {\rm{nsubst}}\,({\rm{nright}}\,({\it{x\/}})\index{nright}, {\it{y\/}}, {\it{n\/}})\index{nsubst})\index{ncomb} \\ 
{\bf elseif }{\it{x\/}} $\in\;${\bf{N}}${}$ \\ 
{\bf then }\=\+{\bf if }{\it{x\/}} $=$ {\it{n\/}}$\;\;${\bf then }{\it{y\/}} \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\- \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim};Variable X does not occur free in term Y.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{not-free-in} \\  
\=\+{\rm{not-free-in}}\,({\it{x\/}}, {\it{y\/}})\index{not-free-in} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{nlambdap}}\,({\it{y\/}})\index{nlambdap} \\ 
{\bf then }\=\+{\bf if }{\it{x\/}} $=$ {\rm{nbind}}\,({\it{y\/}})\index{nbind}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{not-free-in}}\,({\it{x\/}}, {\rm{nbody}}\,({\it{y\/}})\index{nbody})\index{not-free-in}$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{ncombp}}\,({\it{y\/}})\index{ncombp} \\ 
{\bf then }{\rm{not-free-in}}\,({\it{x\/}}, {\rm{nleft}}\,({\it{y\/}})\index{nleft})\index{not-free-in} $\wedge$ {\rm{not-free-in}}\,({\it{x\/}}, {\rm{nright}}\,({\it{y\/}})\index{nright})\index{not-free-in} \\ 
{\bf else }{\it{x\/}} $\not=$ {\it{y\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim};The free variables in Y are disjoint from the bound variables in X.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{free-for} \\  
\=\+{\rm{free-for}}\,({\it{x\/}}, {\it{y\/}})\index{free-for} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{nlambdap}}\,({\it{x\/}})\index{nlambdap}$\;\;${\bf then }\=\+{\rm{not-free-in}}\,({\rm{nbind}}\,({\it{x\/}})\index{nbind}, {\it{y\/}})\index{not-free-in} \\ 
$\wedge$$\;\;\;\;${\rm{free-for}}\,({\rm{nbody}}\,({\it{x\/}})\index{nbody}, {\it{y\/}})\index{free-for}\- \\ 
{\bf elseif }{\rm{ncombp}}\,({\it{x\/}})\index{ncombp}$\;\;${\bf then }\=\+{\rm{free-for}}\,({\rm{nleft}}\,({\it{x\/}})\index{nleft}, {\it{y\/}})\index{free-for} \\ 
$\wedge$$\;\;\;\;${\rm{free-for}}\,({\rm{nright}}\,({\it{x\/}})\index{nright}, {\it{y\/}})\index{free-for}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim};Index of the first occurrence of N in the list LIST.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{index} \\  
\=\+{\rm{index}}\,({\it{n\/}}, {\it{list\/}})\index{index} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{list\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{car}}\,({\it{list\/}}) $=$ {\it{n\/}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }$1\;+$ {\rm{index}}\,({\it{n\/}}, {\rm{cdr}}\,({\it{list\/}}))\index{index}$\;${\bf  endif}\- \\ 
{\bf else }$1\;+$ {\it{n\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim};A and B are identical modulo bound-variables which are accumulated in
;X and Y, respectively.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{alpha-equal} \\  
\=\+{\rm{alpha-equal}}\,({\it{a\/}}, {\it{b\/}}, {\it{x\/}}, {\it{y\/}})\index{alpha-equal} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{nlambdap}}\,({\it{a\/}})\index{nlambdap} $\wedge$ {\rm{nlambdap}}\,({\it{b\/}})\index{nlambdap} \\ 
{\bf then }{\rm{alpha-equal}}\,({\rm{nbody}}\,({\it{a\/}})\index{nbody}, {\rm{nbody}}\,({\it{b\/}})\index{nbody}, {\rm{cons}}\,({\rm{nbind}}\,({\it{a\/}})\index{nbind}, {\it{x\/}}), {\rm{cons}}\,({\rm{nbind}}\,({\it{b\/}})\index{nbind}, {\it{y\/}}))\index{alpha-equal} \\ 
{\bf elseif }{\rm{ncombp}}\,({\it{a\/}})\index{ncombp} $\wedge$ {\rm{ncombp}}\,({\it{b\/}})\index{ncombp} \\ 
{\bf then }\=\+{\rm{alpha-equal}}\,({\rm{nleft}}\,({\it{a\/}})\index{nleft}, {\rm{nleft}}\,({\it{b\/}})\index{nleft}, {\it{x\/}}, {\it{y\/}})\index{alpha-equal} \\ 
$\wedge$$\;\;\;\;${\rm{alpha-equal}}\,({\rm{nright}}\,({\it{a\/}})\index{nright}, {\rm{nright}}\,({\it{b\/}})\index{nright}, {\it{x\/}}, {\it{y\/}})\index{alpha-equal}\- \\ 
{\bf elseif }({\it{a\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{b\/}} $\in\;${\bf{N}}${}$)$\;\;${\bf then }{\rm{index}}\,({\it{a\/}}, {\it{x\/}})\index{index} $=$ {\rm{index}}\,({\it{b\/}}, {\it{y\/}})\index{index} \\ 
{\bf else }{\it{a\/}} $=$ {\it{b\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim};X is a well-formed term in the standard notation.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{ntermp} \\  
\=\+{\rm{ntermp}}\,({\it{x\/}})\index{ntermp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{nlambdap}}\,({\it{x\/}})\index{nlambdap}$\;\;${\bf then }{\rm{ntermp}}\,({\rm{nbody}}\,({\it{x\/}})\index{nbody})\index{ntermp} \\ 
{\bf elseif }{\rm{ncombp}}\,({\it{x\/}})\index{ncombp}$\;\;${\bf then }{\rm{ntermp}}\,({\rm{nleft}}\,({\it{x\/}})\index{nleft})\index{ntermp} $\wedge$ {\rm{ntermp}}\,({\rm{nright}}\,({\it{x\/}})\index{nright})\index{ntermp} \\ 
{\bf else }({\it{x\/}} $\in\;${\bf{N}}${}$) $\vee$ {\rm{litatom}}\,({\it{x\/}})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim};A goes to B by the beta-reduction of some non-overlapping redexes.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{nbeta-step} \\  
\=\+{\rm{nbeta-step}}\,({\it{a\/}}, {\it{b\/}})\index{nbeta-step} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{a\/}} $=$ {\it{b\/}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{nlambdap}}\,({\it{a\/}})\index{nlambdap} \\ 
{\bf then }\=\+{\rm{nlambdap}}\,({\it{b\/}})\index{nlambdap} \\ 
$\wedge$$\;\;\;\;$({\rm{nbind}}\,({\it{a\/}})\index{nbind} $=$ {\rm{nbind}}\,({\it{b\/}})\index{nbind}) \\ 
$\wedge$$\;\;\;\;${\rm{nbeta-step}}\,({\rm{nbody}}\,({\it{a\/}})\index{nbody}, {\rm{nbody}}\,({\it{b\/}})\index{nbody})\index{nbeta-step}\- \\ 
{\bf elseif }{\rm{ncombp}}\,({\it{a\/}})\index{ncombp} \\ 
{\bf then }\=\+(\=\+{\rm{nlambdap}}\,({\rm{nleft}}\,({\it{a\/}})\index{nleft})\index{nlambdap} \\ 
$\wedge$$\;\;\;\;${\rm{free-for}}\,({\rm{nbody}}\,({\rm{nleft}}\,({\it{a\/}})\index{nleft})\index{nbody}, {\rm{nright}}\,({\it{a\/}})\index{nright})\index{free-for} \\ 
$\wedge$$\;\;\;\;$({\it{b\/}} $=$ {\rm{nsubst}}\,({\rm{nbody}}\,({\rm{nleft}}\,({\it{a\/}})\index{nleft})\index{nbody}, {\rm{nright}}\,({\it{a\/}})\index{nright}, {\rm{nbind}}\,({\rm{nleft}}\,({\it{a\/}})\index{nleft})\index{nbind})\index{nsubst}))\- \\ 
$\vee$$\;\;\;\;$(\=\+{\rm{ncombp}}\,({\it{b\/}})\index{ncombp} \\ 
$\wedge$$\;\;\;\;${\rm{nbeta-step}}\,({\rm{nleft}}\,({\it{a\/}})\index{nleft}, {\rm{nleft}}\,({\it{b\/}})\index{nleft})\index{nbeta-step} \\ 
$\wedge$$\;\;\;\;${\rm{nbeta-step}}\,({\rm{nright}}\,({\it{a\/}})\index{nright}, {\rm{nright}}\,({\it{b\/}})\index{nright})\index{nbeta-step})\-\- \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim};A goes to B by an alpha-or-beta-step.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{nstep} \\  
{\rm{nstep}}\,({\it{a\/}}, {\it{b\/}})\index{nstep} $=$ ({\rm{alpha-equal}}\,({\it{a\/}}, {\it{b\/}}, {\bf{nil}}, {\bf{nil}})\index{alpha-equal} $\vee$ {\rm{nbeta-step}}\,({\it{a\/}}, {\it{b\/}})\index{nbeta-step})
\end{tabbing}
\begin{verbatim};A goes to B via a series of steps through terms in LIST.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{nreduction} \\  
\=\+{\rm{nreduction}}\,({\it{a\/}}, {\it{b\/}}, {\it{list\/}})\index{nreduction} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{list\/}}) \\ 
{\bf then }{\rm{nstep}}\,({\rm{car}}\,({\it{list\/}}), {\it{b\/}})\index{nstep} $\wedge$ {\rm{nreduction}}\,({\it{a\/}}, {\rm{car}}\,({\it{list\/}}), {\rm{cdr}}\,({\it{list\/}}))\index{nreduction} \\ 
{\bf else }{\rm{nstep}}\,({\it{a\/}}, {\it{b\/}})\index{nstep}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim};de Bruijn formalization: 
\end{verbatim}
\noindent{\sc Event}:   Add the shell {\it{lambda\/}}\index{lambda}, with recognizer function symbol {\it{lambdap\/}} and 1 accessor: {\it{body\/}}, with type restriction (none-of) and default value zero.

\addvspace{18pt}

\noindent{\sc Event}:   Add the shell {\it{comb\/}}\index{comb}, with recognizer function symbol {\it{combp\/}} and 2 accessors: {\it{left\/}}, with type restriction (none-of) and default value zero; {\it{right\/}}, with type restriction (none-of) and default value zero.

\addvspace{18pt}
\begin{verbatim};BUMP increments all variables of stack-level greater than N by one.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{bump} \\  
\=\+{\rm{bump}}\,({\it{x\/}}, {\it{n\/}})\index{bump} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{lambdap}}\,({\it{x\/}})\index{lambdap}$\;\;${\bf then }{\rm{lambda}}\,({\rm{bump}}\,({\rm{body}}\,({\it{x\/}}), $1\;+$ {\it{n\/}})\index{bump})\index{lambda} \\ 
{\bf elseif }{\rm{combp}}\,({\it{x\/}})\index{combp}$\;\;${\bf then }{\rm{comb}}\,({\rm{bump}}\,({\rm{left}}\,({\it{x\/}})\index{left}, {\it{n\/}})\index{bump}, {\rm{bump}}\,({\rm{right}}\,({\it{x\/}})\index{right}, {\it{n\/}})\index{bump})\index{comb} \\ 
{\bf elseif }{\it{n\/}} $<$ {\it{x\/}}$\;\;${\bf then }$1\;+$ {\it{x\/}} \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim};(SUBST X Y N) is the result of substituting Y for N in X.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{subst} \\  
\=\+{\rm{subst}}\,({\it{x\/}}, {\it{y\/}}, {\it{n\/}})\index{subst} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{lambdap}}\,({\it{x\/}})\index{lambdap}$\;\;${\bf then }{\rm{lambda}}\,({\rm{subst}}\,({\rm{body}}\,({\it{x\/}}), {\rm{bump}}\,({\it{y\/}}, {\tt{0}})\index{bump}, $1\;+$ {\it{n\/}})\index{subst})\index{lambda} \\ 
{\bf elseif }{\rm{combp}}\,({\it{x\/}})\index{combp}$\;\;${\bf then }{\rm{comb}}\,({\rm{subst}}\,({\rm{left}}\,({\it{x\/}})\index{left}, {\it{y\/}}, {\it{n\/}})\index{subst}, {\rm{subst}}\,({\rm{right}}\,({\it{x\/}})\index{right}, {\it{y\/}}, {\it{n\/}})\index{subst})\index{comb} \\ 
{\bf elseif }{\it{x\/}} $\not\simeq {\tt{0}}$ \\ 
{\bf then }\=\+{\bf if }{\it{x\/}} $=$ {\it{n\/}}$\;\;${\bf then }{\it{y\/}} \\ 
{\bf elseif }{\it{n\/}} $<$ {\it{x\/}}$\;\;${\bf then }{\it{x\/}} $-\;1$ \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\- \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim};BUMP commutes with itself.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  bump-bump \\ \index{bump-bump}
({\it{n\/}} $\leq$ {\it{m\/}}) $\rightarrow$ ({\rm{bump}}\,({\rm{bump}}\,({\it{y\/}}, {\it{n\/}})\index{bump}, $1\;+$ {\it{m\/}})\index{bump} $=$ {\rm{bump}}\,({\rm{bump}}\,({\it{y\/}}, {\it{m\/}})\index{bump}, {\it{n\/}})\index{bump})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{bump-subst-induct} \\  
\=\+{\rm{bump-subst-induct}}\,({\it{x\/}}, {\it{y\/}}, {\it{n\/}}, {\it{m\/}})\index{bump-subst-induct} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{lambdap}}\,({\it{x\/}})\index{lambdap}$\;\;${\bf then }{\rm{bump-subst-induct}}\,({\rm{body}}\,({\it{x\/}}), {\rm{bump}}\,({\it{y\/}}, {\tt{0}})\index{bump}, $1\;+$ {\it{n\/}}, $1\;+$ {\it{m\/}})\index{bump-subst-induct} \\ 
{\bf elseif }{\rm{combp}}\,({\it{x\/}})\index{combp} \\ 
{\bf then }\=\+{\rm{bump-subst-induct}}\,({\rm{left}}\,({\it{x\/}})\index{left}, {\it{y\/}}, {\it{n\/}}, {\it{m\/}})\index{bump-subst-induct} \\ 
$\wedge$$\;\;\;\;${\rm{bump-subst-induct}}\,({\rm{right}}\,({\it{x\/}})\index{right}, {\it{y\/}}, {\it{n\/}}, {\it{m\/}})\index{bump-subst-induct}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim};BUMP distributes over SUBST.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  bump-subst \\ \index{bump-subst}
({\it{m\/}} $<$ {\it{n\/}}) $\rightarrow$ ({\rm{bump}}\,({\rm{subst}}\,({\it{x\/}}, {\it{y\/}}, {\it{n\/}})\index{subst}, {\it{m\/}})\index{bump} $=$ {\rm{subst}}\,({\rm{bump}}\,({\it{x\/}}, {\it{m\/}})\index{bump}, {\rm{bump}}\,({\it{y\/}}, {\it{m\/}})\index{bump}, $1\;+$ {\it{n\/}})\index{subst})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{subst-induct} \\  
\=\+{\rm{subst-induct}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}}, {\it{m\/}}, {\it{n\/}})\index{subst-induct} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{lambdap}}\,({\it{x\/}})\index{lambdap} \\ 
{\bf then }{\rm{subst-induct}}\,({\rm{body}}\,({\it{x\/}}), {\rm{bump}}\,({\it{y\/}}, {\tt{0}})\index{bump}, {\rm{bump}}\,({\it{z\/}}, {\tt{0}})\index{bump}, $1\;+$ {\it{m\/}}, $1\;+$ {\it{n\/}})\index{subst-induct} \\ 
{\bf elseif }{\rm{combp}}\,({\it{x\/}})\index{combp} \\ 
{\bf then }\=\+{\rm{subst-induct}}\,({\rm{left}}\,({\it{x\/}})\index{left}, {\it{y\/}}, {\it{z\/}}, {\it{m\/}}, {\it{n\/}})\index{subst-induct} \\ 
$\wedge$$\;\;\;\;${\rm{subst-induct}}\,({\rm{right}}\,({\it{x\/}})\index{right}, {\it{y\/}}, {\it{z\/}}, {\it{m\/}}, {\it{n\/}})\index{subst-induct}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  lambdap-bump \\ \index{lambdap-bump}
{\rm{lambdap}}\,({\it{x\/}})\index{lambdap} $\rightarrow$ {\rm{lambdap}}\,({\rm{bump}}\,({\it{x\/}}, {\it{n\/}})\index{bump})\index{lambdap}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  lambdap-subst \\ \index{lambdap-subst}
{\rm{lambdap}}\,({\it{x\/}})\index{lambdap} $\rightarrow$ {\rm{lambdap}}\,({\rm{subst}}\,({\it{x\/}}, {\it{y\/}}, {\it{n\/}})\index{subst})\index{lambdap}
\end{tabbing}
\begin{verbatim};BUMP distributes over SUBST in another way.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  another-bump-subst \\ \index{another-bump-subst}
\=\+({\it{n\/}} $\leq$ ($1\;+$ {\it{m\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{subst}}\,({\rm{bump}}\,({\it{x\/}}, $1\;+$ {\it{m\/}})\index{bump}, {\rm{bump}}\,({\it{y\/}}, {\it{m\/}})\index{bump}, {\it{n\/}})\index{subst} $=$ {\rm{bump}}\,({\rm{subst}}\,({\it{x\/}}, {\it{y\/}}, {\it{n\/}})\index{subst}, {\it{m\/}})\index{bump})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  bump-lambdap \\ \index{bump-lambdap}
{\rm{lambdap}}\,({\it{x\/}})\index{lambdap} $\rightarrow$ ({\rm{body}}\,({\rm{bump}}\,({\it{x\/}}, {\it{n\/}})\index{bump}) $=$ {\rm{bump}}\,({\rm{body}}\,({\it{x\/}}), $1\;+$ {\it{n\/}})\index{bump})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  subst-lambda \\ \index{subst-lambda}
{\rm{lambdap}}\,({\it{x\/}})\index{lambdap} $\rightarrow$ ({\rm{body}}\,({\rm{subst}}\,({\it{x\/}}, {\it{y\/}}, {\it{n\/}})\index{subst}) $=$ {\rm{subst}}\,({\rm{body}}\,({\it{x\/}}), {\rm{bump}}\,({\it{y\/}}, {\tt{0}})\index{bump}, $1\;+$ {\it{n\/}})\index{subst})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{left-instrs}$\;\;$
{\rm{left-instrs}}\,({\it{x\/}})\index{left-instrs} $=$ {\rm{car}}\,({\it{x\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{right-instrs}$\;\;$
{\rm{right-instrs}}\,({\it{x\/}})\index{right-instrs} $=$ {\rm{cadr}}\,({\it{x\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{command}$\;\;$
{\rm{command}}\,({\it{x\/}})\index{command} $=$ {\rm{caddr}}\,({\it{x\/}})
\end{tabbing}
\begin{verbatim};Result of applying walk-instruction W to M in an inside-out manner.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{walk} \\  
\=\+{\rm{walk}}\,({\it{w\/}}, {\it{m\/}})\index{walk} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{lambdap}}\,({\it{m\/}})\index{lambdap}$\;\;${\bf then }{\rm{lambda}}\,({\rm{walk}}\,({\it{w\/}}, {\rm{body}}\,({\it{m\/}}))\index{walk})\index{lambda} \\ 
{\bf elseif }{\rm{combp}}\,({\it{m\/}})\index{combp} \\ 
{\bf then }\=\+{\bf if }({\rm{command}}\,({\it{w\/}})\index{command} $=$ {\tt{'}}{\tt{reduce}}) $\wedge$ {\rm{lambdap}}\,({\rm{left}}\,({\it{m\/}})\index{left})\index{lambdap} \\ 
{\bf then }{\rm{subst}}\,(\=\+{\rm{body}}\,({\rm{walk}}\,({\rm{left-instrs}}\,({\it{w\/}})\index{left-instrs}, {\rm{left}}\,({\it{m\/}})\index{left})\index{walk}), \\ 
{\rm{walk}}\,({\rm{right-instrs}}\,({\it{w\/}})\index{right-instrs}, {\rm{right}}\,({\it{m\/}})\index{right})\index{walk}, \\ 
{\tt{1}})\-\index{subst} \\ 
{\bf else }{\rm{comb}}\,(\=\+{\rm{walk}}\,({\rm{left-instrs}}\,({\it{w\/}})\index{left-instrs}, {\rm{left}}\,({\it{m\/}})\index{left})\index{walk}, \\ 
{\rm{walk}}\,({\rm{right-instrs}}\,({\it{w\/}})\index{right-instrs}, {\rm{right}}\,({\it{m\/}})\index{right})\index{walk})\-\index{comb}$\;${\bf  endif}\- \\ 
{\bf else }{\it{m\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{bump-walk-ind} \\  
\=\+{\rm{bump-walk-ind}}\,({\it{u\/}}, {\it{m\/}}, {\it{n\/}})\index{bump-walk-ind} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{lambdap}}\,({\it{m\/}})\index{lambdap}$\;\;${\bf then }{\rm{bump-walk-ind}}\,({\it{u\/}}, {\rm{body}}\,({\it{m\/}}), $1\;+$ {\it{n\/}})\index{bump-walk-ind} \\ 
{\bf elseif }{\rm{combp}}\,({\it{m\/}})\index{combp} \\ 
{\bf then }\=\+{\bf if }({\rm{command}}\,({\it{u\/}})\index{command} $=$ {\tt{'}}{\tt{reduce}}) $\wedge$ {\rm{lambdap}}\,({\rm{left}}\,({\it{m\/}})\index{left})\index{lambdap} \\ 
{\bf then }\=\+{\rm{bump-walk-ind}}\,({\rm{left-instrs}}\,({\it{u\/}})\index{left-instrs}, {\rm{left}}\,({\it{m\/}})\index{left}, {\it{n\/}})\index{bump-walk-ind} \\ 
$\wedge$$\;\;\;\;${\rm{bump-walk-ind}}\,({\rm{right-instrs}}\,({\it{u\/}})\index{right-instrs}, {\rm{right}}\,({\it{m\/}})\index{right}, {\it{n\/}})\index{bump-walk-ind}\- \\ 
{\bf else }\=\+{\rm{bump-walk-ind}}\,({\rm{left-instrs}}\,({\it{u\/}})\index{left-instrs}, {\rm{left}}\,({\it{m\/}})\index{left}, {\it{n\/}})\index{bump-walk-ind} \\ 
$\wedge$$\;\;\;\;${\rm{bump-walk-ind}}\,({\rm{right-instrs}}\,({\it{u\/}})\index{right-instrs}, {\rm{right}}\,({\it{m\/}})\index{right}, {\it{n\/}})\index{bump-walk-ind}\-$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  lambda-walk \\ \index{lambda-walk}
{\rm{lambdap}}\,({\it{m\/}})\index{lambdap} $\rightarrow$ {\rm{lambdap}}\,({\rm{walk}}\,({\it{w\/}}, {\it{m\/}})\index{walk})\index{lambdap}
\end{tabbing}
\begin{verbatim};BUMP and WALK commute with each other.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  bump-walk \\ \index{bump-walk}
{\rm{walk}}\,({\it{u\/}}, {\rm{bump}}\,({\it{m\/}}, {\it{n\/}})\index{bump})\index{walk} $=$ {\rm{bump}}\,({\rm{walk}}\,({\it{u\/}}, {\it{m\/}})\index{walk}, {\it{n\/}})\index{bump}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  nlistp-walk \\ \index{nlistp-walk}
({\it{w\/}} $\simeq\;${{\bf{nil}}}${}$) $\rightarrow$ ({\rm{walk}}\,({\it{w\/}}, {\it{m\/}})\index{walk} $=$ {\it{m\/}})
\end{tabbing}
\begin{verbatim};The `skolem' function generating the substitutive walk.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{sub-walk} \\  
\=\+{\rm{sub-walk}}\,({\it{w\/}}, {\it{m\/}}, {\it{u\/}}, {\it{n\/}})\index{sub-walk} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{lambdap}}\,({\it{m\/}})\index{lambdap}$\;\;${\bf then }{\rm{sub-walk}}\,({\it{w\/}}, {\rm{body}}\,({\it{m\/}}), {\it{u\/}}, $1\;+$ {\it{n\/}})\index{sub-walk} \\ 
{\bf elseif }{\rm{combp}}\,({\it{m\/}})\index{combp} \\ 
{\bf then }\=\+{\bf if }({\rm{command}}\,({\it{w\/}})\index{command} $=$ {\tt{'}}{\tt{reduce}}) $\wedge$ {\rm{lambdap}}\,({\rm{left}}\,({\it{m\/}})\index{left})\index{lambdap} \\ 
{\bf then }{\rm{list}}\,(\=\+{\rm{sub-walk}}\,({\rm{left-instrs}}\,({\it{w\/}})\index{left-instrs}, {\rm{left}}\,({\it{m\/}})\index{left}, {\it{u\/}}, {\it{n\/}})\index{sub-walk}, \\ 
{\rm{sub-walk}}\,({\rm{right-instrs}}\,({\it{w\/}})\index{right-instrs}, {\rm{right}}\,({\it{m\/}})\index{right}, {\it{u\/}}, {\it{n\/}})\index{sub-walk}, \\ 
{\tt{'}}{\tt{reduce}})\- \\ 
{\bf else }{\rm{list}}\,(\=\+{\rm{sub-walk}}\,({\rm{left-instrs}}\,({\it{w\/}})\index{left-instrs}, {\rm{left}}\,({\it{m\/}})\index{left}, {\it{u\/}}, {\it{n\/}})\index{sub-walk}, \\ 
{\rm{sub-walk}}\,({\rm{right-instrs}}\,({\it{w\/}})\index{right-instrs}, {\rm{right}}\,({\it{m\/}})\index{right}, {\it{u\/}}, {\it{n\/}})\index{sub-walk})\-$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{m\/}} $\not\simeq {\tt{0}}$ \\ 
{\bf then }\=\+{\bf if }{\it{m\/}} $=$ {\it{n\/}}$\;\;${\bf then }{\it{u\/}} \\ 
{\bf else }{\it{w\/}}$\;${\bf  endif}\- \\ 
{\bf else }{\it{w\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{walk-subst-ind} \\  
\=\+{\rm{walk-subst-ind}}\,({\it{w\/}}, {\it{m\/}}, {\it{u\/}}, {\it{x\/}}, {\it{n\/}})\index{walk-subst-ind} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{lambdap}}\,({\it{m\/}})\index{lambdap}$\;\;${\bf then }{\rm{walk-subst-ind}}\,({\it{w\/}}, {\rm{body}}\,({\it{m\/}}), {\it{u\/}}, {\rm{bump}}\,({\it{x\/}}, {\tt{0}})\index{bump}, $1\;+$ {\it{n\/}})\index{walk-subst-ind} \\ 
{\bf elseif }{\rm{combp}}\,({\it{m\/}})\index{combp} \\ 
{\bf then }\=\+{\bf if }({\rm{command}}\,({\it{w\/}})\index{command} $=$ {\tt{'}}{\tt{reduce}}) $\wedge$ {\rm{lambdap}}\,({\rm{left}}\,({\it{m\/}})\index{left})\index{lambdap} \\ 
{\bf then }\=\+{\rm{walk-subst-ind}}\,({\rm{left-instrs}}\,({\it{w\/}})\index{left-instrs}, {\rm{left}}\,({\it{m\/}})\index{left}, {\it{u\/}}, {\it{x\/}}, {\it{n\/}})\index{walk-subst-ind} \\ 
$\wedge$$\;\;\;\;${\rm{walk-subst-ind}}\,({\rm{right-instrs}}\,({\it{w\/}})\index{right-instrs}, {\rm{right}}\,({\it{m\/}})\index{right}, {\it{u\/}}, {\it{x\/}}, {\it{n\/}})\index{walk-subst-ind}\- \\ 
{\bf else }\=\+{\rm{walk-subst-ind}}\,({\rm{left-instrs}}\,({\it{w\/}})\index{left-instrs}, {\rm{left}}\,({\it{m\/}})\index{left}, {\it{u\/}}, {\it{x\/}}, {\it{n\/}})\index{walk-subst-ind} \\ 
$\wedge$$\;\;\;\;${\rm{walk-subst-ind}}\,({\rm{right-instrs}}\,({\it{w\/}})\index{right-instrs}, {\rm{right}}\,({\it{m\/}})\index{right}, {\it{u\/}}, {\it{x\/}}, {\it{n\/}})\index{walk-subst-ind}\-$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim};(BUMP X N) cannot contain N+1 free.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  subst-not-free-in \\ \index{subst-not-free-in}
{\rm{subst}}\,({\rm{bump}}\,({\it{x\/}}, {\it{n\/}})\index{bump}, {\it{y\/}}, $1\;+$ {\it{n\/}})\index{subst} $=$ {\it{x\/}}
\end{tabbing}
\begin{verbatim};SUBST distributes over itself.  A tricky one!
\end{verbatim}\begin{tabbing}{\sc Theorem}:  subst-subst \\ \index{subst-subst}
\=\+(({\it{m\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{m\/}} $<$ {\it{n\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{subst}}\,({\rm{subst}}\,({\it{x\/}}, {\rm{bump}}\,({\it{z\/}}, {\it{m\/}})\index{bump}, $1\;+$ {\it{n\/}})\index{subst}, {\rm{subst}}\,({\it{y\/}}, {\it{z\/}}, {\it{n\/}})\index{subst}, $1\;+$ {\it{m\/}})\index{subst} \\ 
$=$$\;\;\;\;${\rm{subst}}\,({\rm{subst}}\,({\it{x\/}}, {\it{y\/}}, $1\;+$ {\it{m\/}})\index{subst}, {\it{z\/}}, {\it{n\/}})\index{subst})\-\-
\end{tabbing}
\begin{verbatim};The substitutivity of walks lemma.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  walk-subst \\ \index{walk-subst}
\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{walk}}\,({\rm{sub-walk}}\,({\it{w\/}}, {\it{m\/}}, {\it{u\/}}, {\it{n\/}})\index{sub-walk}, {\rm{subst}}\,({\it{m\/}}, {\it{x\/}}, {\it{n\/}})\index{subst})\index{walk} \\ 
$=$$\;\;\;\;${\rm{subst}}\,({\rm{walk}}\,({\it{w\/}}, {\it{m\/}})\index{walk}, {\rm{walk}}\,({\it{u\/}}, {\it{x\/}})\index{walk}, {\it{n\/}})\index{subst})\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  walk-lambda \\ \index{walk-lambda}
{\rm{lambdap}}\,({\it{x\/}})\index{lambdap} $\rightarrow$ ({\rm{body}}\,({\rm{walk}}\,({\it{u\/}}, {\it{x\/}})\index{walk}) $=$ {\rm{walk}}\,({\it{u\/}}, {\rm{body}}\,({\it{x\/}}))\index{walk})
\end{tabbing}
\begin{verbatim};`Skolem' function generating convergent walk.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{make-walk} \\  
\=\+{\rm{make-walk}}\,({\it{m\/}}, {\it{u\/}}, {\it{v\/}})\index{make-walk} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{lambdap}}\,({\it{m\/}})\index{lambdap}$\;\;${\bf then }{\rm{make-walk}}\,({\rm{body}}\,({\it{m\/}}), {\it{u\/}}, {\it{v\/}})\index{make-walk} \\ 
{\bf elseif }{\rm{combp}}\,({\it{m\/}})\index{combp} \\ 
{\bf then }\=\+{\bf if }({\rm{command}}\,({\it{u\/}})\index{command} $=$ {\tt{'}}{\tt{reduce}}) $\wedge$ {\rm{lambdap}}\,({\rm{left}}\,({\it{m\/}})\index{left})\index{lambdap} \\ 
{\bf then }{\rm{sub-walk}}\,(\=\+{\rm{make-walk}}\,({\rm{left}}\,({\it{m\/}})\index{left}, {\rm{left-instrs}}\,({\it{u\/}})\index{left-instrs}, {\rm{left-instrs}}\,({\it{v\/}})\index{left-instrs})\index{make-walk}, \\ 
{\rm{body}}\,({\rm{walk}}\,({\rm{left-instrs}}\,({\it{u\/}})\index{left-instrs}, {\rm{left}}\,({\it{m\/}})\index{left})\index{walk}), \\ 
{\rm{make-walk}}\,({\rm{right}}\,({\it{m\/}})\index{right}, {\rm{right-instrs}}\,({\it{u\/}})\index{right-instrs}, {\rm{right-instrs}}\,({\it{v\/}})\index{right-instrs})\index{make-walk}, \\ 
{\tt{1}})\-\index{sub-walk} \\ 
{\bf elseif }({\rm{command}}\,({\it{v\/}})\index{command} $=$ {\tt{'}}{\tt{reduce}}) $\wedge$ {\rm{lambdap}}\,({\rm{left}}\,({\it{m\/}})\index{left})\index{lambdap} \\ 
{\bf then }{\rm{list}}\,(\=\+{\rm{make-walk}}\,({\rm{left}}\,({\it{m\/}})\index{left}, {\rm{left-instrs}}\,({\it{u\/}})\index{left-instrs}, {\rm{left-instrs}}\,({\it{v\/}})\index{left-instrs})\index{make-walk}, \\ 
{\rm{make-walk}}\,({\rm{right}}\,({\it{m\/}})\index{right}, {\rm{right-instrs}}\,({\it{u\/}})\index{right-instrs}, {\rm{right-instrs}}\,({\it{v\/}})\index{right-instrs})\index{make-walk}, \\ 
{\tt{'}}{\tt{reduce}})\- \\ 
{\bf else }{\rm{list}}\,(\=\+{\rm{make-walk}}\,({\rm{left}}\,({\it{m\/}})\index{left}, {\rm{left-instrs}}\,({\it{u\/}})\index{left-instrs}, {\rm{left-instrs}}\,({\it{v\/}})\index{left-instrs})\index{make-walk}, \\ 
{\rm{make-walk}}\,(\=\+{\rm{right}}\,({\it{m\/}})\index{right}, \\ 
{\rm{right-instrs}}\,({\it{u\/}})\index{right-instrs}, \\ 
{\rm{right-instrs}}\,({\it{v\/}})\index{right-instrs})\-\index{make-walk})\-$\;${\bf  endif}\- \\ 
{\bf else }{\it{u\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim};The Diamond property of walks.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main \\ \index{main}
{\rm{walk}}\,({\rm{make-walk}}\,({\it{m\/}}, {\it{u\/}}, {\it{v\/}})\index{make-walk}, {\rm{walk}}\,({\it{u\/}}, {\it{m\/}})\index{walk})\index{walk} $=$ {\rm{walk}}\,({\rm{make-walk}}\,({\it{m\/}}, {\it{v\/}}, {\it{u\/}})\index{make-walk}, {\rm{walk}}\,({\it{v\/}}, {\it{m\/}})\index{walk})\index{walk}
\end{tabbing}
\begin{verbatim};Result of applying a series of walks.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{reduce} \\  
\=\+{\rm{reduce}}\,({\it{w\/}}, {\it{m\/}})\index{reduce} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{w\/}})$\;\;${\bf then }{\rm{reduce}}\,({\rm{cdr}}\,({\it{w\/}}), {\rm{walk}}\,({\rm{car}}\,({\it{w\/}}), {\it{m\/}})\index{walk})\index{reduce} \\ 
{\bf else }{\it{m\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim};`Skolem' function constructing convergent walk given a walk W and a
;series of walks V.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{make-walk-reduce} \\  
\=\+{\rm{make-walk-reduce}}\,({\it{m\/}}, {\it{w\/}}, {\it{v\/}})\index{make-walk-reduce} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{v\/}}) \\ 
{\bf then }{\rm{make-walk-reduce}}\,({\rm{walk}}\,({\rm{car}}\,({\it{v\/}}), {\it{m\/}})\index{walk}, {\rm{make-walk}}\,({\it{m\/}}, {\rm{car}}\,({\it{v\/}}), {\it{w\/}})\index{make-walk}, {\rm{cdr}}\,({\it{v\/}}))\index{make-walk-reduce} \\ 
{\bf else }{\it{w\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim};`Skolem' function constructing convergent series of walks for same case as above.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{make-reduce-walk} \\  
\=\+{\rm{make-reduce-walk}}\,({\it{m\/}}, {\it{w\/}}, {\it{v\/}})\index{make-reduce-walk} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{v\/}}) \\ 
{\bf then }{\rm{cons}}\,(\=\+{\rm{make-walk}}\,({\it{m\/}}, {\it{w\/}}, {\rm{car}}\,({\it{v\/}}))\index{make-walk}, \\ 
{\rm{make-reduce-walk}}\,(\=\+{\rm{walk}}\,({\rm{car}}\,({\it{v\/}}), {\it{m\/}})\index{walk}, \\ 
{\rm{make-walk}}\,({\it{m\/}}, {\rm{car}}\,({\it{v\/}}), {\it{w\/}})\index{make-walk}, \\ 
{\rm{cdr}}\,({\it{v\/}}))\-\index{make-reduce-walk})\- \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim};The Rectangle property.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  walk-reduce \\ \index{walk-reduce}
\=\+{\rm{reduce}}\,({\rm{make-reduce-walk}}\,({\it{m\/}}, {\it{w\/}}, {\it{v\/}})\index{make-reduce-walk}, {\rm{walk}}\,({\it{w\/}}, {\it{m\/}})\index{walk})\index{reduce} \\ 
$=$$\;\;\;\;${\rm{walk}}\,({\rm{make-walk-reduce}}\,({\it{m\/}}, {\it{w\/}}, {\it{v\/}})\index{make-walk-reduce}, {\rm{reduce}}\,({\it{v\/}}, {\it{m\/}})\index{reduce})\index{walk}\-
\end{tabbing}
\begin{verbatim};`Skolem' function constructing convergent series of walks for Diamond property.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{make-reduce} \\  
\=\+{\rm{make-reduce}}\,({\it{m\/}}, {\it{u\/}}, {\it{v\/}})\index{make-reduce} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{u\/}}) \\ 
{\bf then }{\rm{cons}}\,(\=\+{\rm{make-walk-reduce}}\,({\it{m\/}}, {\rm{car}}\,({\it{u\/}}), {\it{v\/}})\index{make-walk-reduce}, \\ 
{\rm{make-reduce}}\,(\=\+{\rm{walk}}\,({\rm{car}}\,({\it{u\/}}), {\it{m\/}})\index{walk}, \\ 
{\rm{cdr}}\,({\it{u\/}}), \\ 
{\rm{make-reduce-walk}}\,({\it{m\/}}, {\rm{car}}\,({\it{u\/}}), {\it{v\/}})\index{make-reduce-walk})\-\index{make-reduce})\- \\ 
{\bf else }{\it{u\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  list-make-reduce \\ \index{list-make-reduce}
\=\+{\rm{listp}}\,({\it{v\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{reduce}}\,({\rm{make-reduce}}\,({\it{m\/}}, {\it{u\/}}, {\it{v\/}})\index{make-reduce}, {\rm{reduce}}\,({\it{v\/}}, {\it{m\/}})\index{reduce})\index{reduce} \\ 
$=$$\;\;\;\;${\rm{reduce}}\,(\=\+{\rm{make-reduce}}\,(\=\+{\rm{walk}}\,({\rm{car}}\,({\it{v\/}}), {\it{m\/}})\index{walk}, \\ 
{\rm{make-reduce-walk}}\,({\it{m\/}}, {\rm{car}}\,({\it{v\/}}), {\it{u\/}})\index{make-reduce-walk}, \\ 
{\rm{cdr}}\,({\it{v\/}}))\-\index{make-reduce}, \\ 
{\rm{reduce}}\,({\it{v\/}}, {\it{m\/}})\index{reduce})\-\index{reduce})\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  list-make-reduce1 \\ \index{list-make-reduce1}
\=\+{\rm{reduce}}\,({\rm{make-reduce}}\,({\it{m\/}}, {\it{u\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{make-reduce}, {\rm{reduce}}\,({\it{y\/}}, {\rm{walk}}\,({\it{x\/}}, {\it{m\/}})\index{walk})\index{reduce})\index{reduce} \\ 
$=$$\;\;\;\;${\rm{reduce}}\,(\=\+{\rm{make-reduce}}\,({\rm{walk}}\,({\it{x\/}}, {\it{m\/}})\index{walk}, {\rm{make-reduce-walk}}\,({\it{m\/}}, {\it{x\/}}, {\it{u\/}})\index{make-reduce-walk}, {\it{y\/}})\index{make-reduce}, \\ 
{\rm{reduce}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}), {\it{m\/}})\index{reduce})\-\index{reduce}\-
\end{tabbing}
\begin{verbatim};The Diamond property of a series of walks.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  church-rosser \\ \index{church-rosser}
\=\+{\rm{reduce}}\,({\rm{make-reduce}}\,({\it{m\/}}, {\it{u\/}}, {\it{v\/}})\index{make-reduce}, {\rm{reduce}}\,({\it{v\/}}, {\it{m\/}})\index{reduce})\index{reduce} \\ 
$=$$\;\;\;\;${\rm{reduce}}\,({\rm{make-reduce}}\,({\it{m\/}}, {\it{v\/}}, {\it{u\/}})\index{make-reduce}, {\rm{reduce}}\,({\it{u\/}}, {\it{m\/}})\index{reduce})\index{reduce}\-
\end{tabbing}
\begin{verbatim};Translation from standard to de Bruijn.  X a standard term, and
;BOUNDS bound variables accumulated so far.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{translate} \\  
\=\+{\rm{translate}}\,({\it{x\/}}, {\it{bounds\/}})\index{translate} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{nlambdap}}\,({\it{x\/}})\index{nlambdap}$\;\;${\bf then }{\rm{lambda}}\,({\rm{translate}}\,({\rm{nbody}}\,({\it{x\/}})\index{nbody}, {\rm{cons}}\,({\rm{nbind}}\,({\it{x\/}})\index{nbind}, {\it{bounds\/}}))\index{translate})\index{lambda} \\ 
{\bf elseif }{\rm{ncombp}}\,({\it{x\/}})\index{ncombp} \\ 
{\bf then }{\rm{comb}}\,({\rm{translate}}\,({\rm{nleft}}\,({\it{x\/}})\index{nleft}, {\it{bounds\/}})\index{translate}, {\rm{translate}}\,({\rm{nright}}\,({\it{x\/}})\index{nright}, {\it{bounds\/}})\index{translate})\index{comb} \\ 
{\bf elseif }{\it{x\/}} $\in\;${\bf{N}}${}$$\;\;${\bf then }{\rm{index}}\,({\it{x\/}}, {\it{bounds\/}})\index{index} \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim};Two alpha-equivalent terms have the same translation.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  alpha-translate \\ \index{alpha-translate}
{\rm{alpha-equal}}\,({\it{a\/}}, {\it{b\/}}, {\it{x\/}}, {\it{y\/}})\index{alpha-equal} $\rightarrow$ ({\rm{translate}}\,({\it{a\/}}, {\it{x\/}})\index{translate} $=$ {\rm{translate}}\,({\it{b\/}}, {\it{y\/}})\index{translate})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{insert} \\  
\=\+{\rm{insert}}\,({\it{x\/}}, {\it{bounds\/}}, {\it{n\/}})\index{insert} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{cons}}\,({\it{x\/}}, {\it{bounds\/}}) \\ 
{\bf elseif }{\rm{listp}}\,({\it{bounds\/}}) \\ 
{\bf then }{\rm{cons}}\,({\rm{car}}\,({\it{bounds\/}}), {\rm{insert}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{bounds\/}}), {\it{n\/}} $-\;1$)\index{insert}) \\ 
{\bf else }{\rm{cons}}\,({\it{x\/}}, {\bf{nil}})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{nsubst-ind} \\  
\=\+{\rm{nsubst-ind}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}}, {\it{bounds\/}}, {\it{n\/}})\index{nsubst-ind} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{nlambdap}}\,({\it{x\/}})\index{nlambdap} \\ 
{\bf then }\=\+{\bf if }{\rm{nbind}}\,({\it{x\/}})\index{nbind} $=$ {\it{z\/}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{nsubst-ind}}\,({\rm{nbody}}\,({\it{x\/}})\index{nbody}, {\it{y\/}}, {\it{z\/}}, {\rm{cons}}\,({\rm{nbind}}\,({\it{x\/}})\index{nbind}, {\it{bounds\/}}), $1\;+$ {\it{n\/}})\index{nsubst-ind}$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{ncombp}}\,({\it{x\/}})\index{ncombp} \\ 
{\bf then }\=\+{\rm{nsubst-ind}}\,({\rm{nleft}}\,({\it{x\/}})\index{nleft}, {\it{y\/}}, {\it{z\/}}, {\it{bounds\/}}, {\it{n\/}})\index{nsubst-ind} \\ 
$\wedge$$\;\;\;\;${\rm{nsubst-ind}}\,({\rm{nright}}\,({\it{x\/}})\index{nright}, {\it{y\/}}, {\it{z\/}}, {\it{bounds\/}}, {\it{n\/}})\index{nsubst-ind}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{trans-insert-ind} \\  
\=\+{\rm{trans-insert-ind}}\,({\it{x\/}}, {\it{z\/}}, {\it{bounds\/}}, {\it{n\/}})\index{trans-insert-ind} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{nlambdap}}\,({\it{x\/}})\index{nlambdap} \\ 
{\bf then }{\rm{trans-insert-ind}}\,({\rm{nbody}}\,({\it{x\/}})\index{nbody}, {\it{z\/}}, {\rm{cons}}\,({\rm{nbind}}\,({\it{x\/}})\index{nbind}, {\it{bounds\/}}), $1\;+$ {\it{n\/}})\index{trans-insert-ind} \\ 
{\bf elseif }{\rm{ncombp}}\,({\it{x\/}})\index{ncombp} \\ 
{\bf then }\=\+{\rm{trans-insert-ind}}\,({\rm{nleft}}\,({\it{x\/}})\index{nleft}, {\it{z\/}}, {\it{bounds\/}}, {\it{n\/}})\index{trans-insert-ind} \\ 
$\wedge$$\;\;\;\;${\rm{trans-insert-ind}}\,({\rm{nright}}\,({\it{x\/}})\index{nright}, {\it{z\/}}, {\it{bounds\/}}, {\it{n\/}})\index{trans-insert-ind}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{precede} \\  
\=\+{\rm{precede}}\,({\it{x\/}}, {\it{bounds\/}}, {\it{n\/}})\index{precede} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{f}} \\ 
{\bf elseif }{\rm{listp}}\,({\it{bounds\/}}) \\ 
{\bf then }({\rm{car}}\,({\it{bounds\/}}) $=$ {\it{x\/}}) $\vee$ {\rm{precede}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{bounds\/}}), {\it{n\/}} $-\;1$)\index{precede} \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  nprecede-index \\ \index{nprecede-index}
\=\+(($\neg$ {\rm{precede}}\,({\it{z\/}}, {\it{bounds\/}}, {\it{n\/}})\index{precede}) $\wedge$ ({\it{n\/}} $\leq$ {\rm{length}}\,({\it{bounds\/}})\index{length})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{index}}\,({\it{z\/}}, {\rm{insert}}\,({\it{z\/}}, {\it{bounds\/}}, {\it{n\/}})\index{insert})\index{index} $=$ ($1\;+$ {\it{n\/}}))\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  precede-index1 \\ \index{precede-index1}
\=\+(({\it{n\/}} $<$ {\rm{index}}\,({\it{x\/}}, {\it{bounds\/}})\index{index}) $\wedge$ ({\it{n\/}} $\leq$ {\rm{length}}\,({\it{bounds\/}})\index{length})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{index}}\,({\it{x\/}}, {\rm{insert}}\,({\it{z\/}}, {\it{bounds\/}}, {\it{n\/}})\index{insert})\index{index} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $=$ {\it{z\/}}$\;\;${\bf then }$1\;+$ {\it{n\/}} \\ 
{\bf else }$1\;+$ {\rm{index}}\,({\it{x\/}}, {\it{bounds\/}})\index{index}$\;${\bf  endif}\-)\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  precede-index \\ \index{precede-index}
{\rm{precede}}\,({\it{z\/}}, {\it{bounds\/}}, {\it{n\/}})\index{precede} $\rightarrow$ ({\rm{index}}\,({\it{z\/}}, {\rm{insert}}\,({\it{z\/}}, {\it{bounds\/}}, {\it{n\/}})\index{insert})\index{index} $<$ ($1\;+$ {\it{n\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  precede-index2 \\ \index{precede-index2}
\=\+(({\rm{index}}\,({\it{x\/}}, {\it{bounds\/}})\index{index} $\leq$ {\it{n\/}}) $\wedge$ ({\it{n\/}} $\leq$ {\rm{length}}\,({\it{bounds\/}})\index{length})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{index}}\,({\it{x\/}}, {\rm{insert}}\,({\it{z\/}}, {\it{bounds\/}}, {\it{n\/}})\index{insert})\index{index} $=$ {\rm{index}}\,({\it{x\/}}, {\it{bounds\/}})\index{index})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  translate-insert \\ \index{translate-insert}
\=\+({\rm{precede}}\,({\it{z\/}}, {\it{bounds\/}}, {\it{n\/}})\index{precede} $\wedge$ ({\it{n\/}} $\leq$ {\rm{length}}\,({\it{bounds\/}})\index{length}) $\wedge$ {\rm{ntermp}}\,({\it{x\/}})\index{ntermp}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{translate}}\,({\it{x\/}}, {\rm{insert}}\,({\it{z\/}}, {\it{bounds\/}}, {\it{n\/}})\index{insert})\index{translate} $=$ {\rm{bump}}\,({\rm{translate}}\,({\it{x\/}}, {\it{bounds\/}})\index{translate}, {\it{n\/}})\index{bump})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  subst-nsubst \\ \index{subst-nsubst}
\=\+({\rm{precede}}\,({\it{z\/}}, {\it{bounds\/}}, {\it{n\/}})\index{precede} $\wedge$ {\rm{ntermp}}\,({\it{x\/}})\index{ntermp} $\wedge$ ({\it{n\/}} $\leq$ {\rm{length}}\,({\it{bounds\/}})\index{length})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{subst}}\,({\rm{translate}}\,({\it{x\/}}, {\rm{insert}}\,({\it{z\/}}, {\it{bounds\/}}, {\it{n\/}})\index{insert})\index{translate}, {\it{y\/}}, $1\;+$ {\it{n\/}})\index{subst} \\ 
$=$$\;\;\;\;${\rm{translate}}\,({\it{x\/}}, {\it{bounds\/}})\index{translate})\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{not-free-ind} \\  
\=\+{\rm{not-free-ind}}\,({\it{y\/}}, {\it{z\/}}, {\it{bounds\/}}, {\it{n\/}})\index{not-free-ind} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{nlambdap}}\,({\it{y\/}})\index{nlambdap} \\ 
{\bf then }{\rm{not-free-ind}}\,({\rm{nbody}}\,({\it{y\/}})\index{nbody}, {\it{z\/}}, {\rm{cons}}\,({\rm{nbind}}\,({\it{y\/}})\index{nbind}, {\it{bounds\/}}), $1\;+$ {\it{n\/}})\index{not-free-ind} \\ 
{\bf elseif }{\rm{ncombp}}\,({\it{y\/}})\index{ncombp} \\ 
{\bf then }\=\+{\rm{not-free-ind}}\,({\rm{nleft}}\,({\it{y\/}})\index{nleft}, {\it{z\/}}, {\it{bounds\/}}, {\it{n\/}})\index{not-free-ind} \\ 
$\wedge$$\;\;\;\;${\rm{not-free-ind}}\,({\rm{nright}}\,({\it{y\/}})\index{nright}, {\it{z\/}}, {\it{bounds\/}}, {\it{n\/}})\index{not-free-ind}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  translate-insert1 \\ \index{translate-insert1}
\=\+({\rm{precede}}\,({\it{z\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{bounds\/}}), $1\;+$ {\it{n\/}})\index{precede} $\wedge$ {\rm{ntermp}}\,({\it{y\/}})\index{ntermp} $\wedge$ ({\it{n\/}} $\leq$ {\rm{length}}\,({\it{bounds\/}})\index{length})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{translate}}\,({\it{y\/}}, {\rm{cons}}\,({\it{x\/}}, {\rm{insert}}\,({\it{z\/}}, {\it{bounds\/}}, {\it{n\/}})\index{insert}))\index{translate} \\ 
$=$$\;\;\;\;${\rm{bump}}\,({\rm{translate}}\,({\it{y\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{bounds\/}}))\index{translate}, $1\;+$ {\it{n\/}})\index{bump})\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  not-free-in-translate \\ \index{not-free-in-translate}
\=\+({\rm{not-free-in}}\,({\it{z\/}}, {\it{y\/}})\index{not-free-in} $\wedge$ ({\it{n\/}} $\leq$ {\rm{length}}\,({\it{bounds\/}})\index{length}) $\wedge$ {\rm{ntermp}}\,({\it{y\/}})\index{ntermp}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{translate}}\,({\it{y\/}}, {\rm{insert}}\,({\it{z\/}}, {\it{bounds\/}}, {\it{n\/}})\index{insert})\index{translate} $=$ {\rm{bump}}\,({\rm{translate}}\,({\it{y\/}}, {\it{bounds\/}})\index{translate}, {\it{n\/}})\index{bump})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  not-free-in-corr \\ \index{not-free-in-corr}
\=\+({\rm{ntermp}}\,({\it{y\/}})\index{ntermp} $\wedge$ {\rm{not-free-in}}\,({\it{z\/}}, {\it{y\/}})\index{not-free-in}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{translate}}\,({\it{y\/}}, {\rm{cons}}\,({\it{z\/}}, {\it{bounds\/}}))\index{translate} $=$ {\rm{bump}}\,({\rm{translate}}\,({\it{y\/}}, {\it{bounds\/}})\index{translate}, {\tt{0}})\index{bump})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  subst-nsubst2 \\ \index{subst-nsubst2}
\=\+({\rm{precede}}\,({\it{z\/}}, {\rm{cons}}\,({\it{w\/}}, {\it{bounds\/}}), $1\;+$ {\it{n\/}})\index{precede} $\wedge$ {\rm{ntermp}}\,({\it{x\/}})\index{ntermp} $\wedge$ ({\it{n\/}} $\leq$ {\rm{length}}\,({\it{bounds\/}})\index{length})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{subst}}\,({\rm{translate}}\,({\it{x\/}}, {\rm{cons}}\,({\it{w\/}}, {\rm{insert}}\,({\it{z\/}}, {\it{bounds\/}}, {\it{n\/}})\index{insert}))\index{translate}, {\it{y\/}}, $1\;+$ ($1\;+$ {\it{n\/}}))\index{subst} \\ 
$=$$\;\;\;\;${\rm{translate}}\,({\it{x\/}}, {\rm{cons}}\,({\it{w\/}}, {\it{bounds\/}}))\index{translate})\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  subst-nsubst2-corr \\ \index{subst-nsubst2-corr}
\=\+{\rm{ntermp}}\,({\it{x\/}})\index{ntermp} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{subst}}\,({\rm{translate}}\,({\it{x\/}}, {\rm{cons}}\,({\it{z\/}}, {\rm{cons}}\,({\it{z\/}}, {\it{bounds\/}})))\index{translate}, {\it{y\/}}, $1\;+$ ($1\;+$ {\tt{0}}))\index{subst} \\ 
$=$$\;\;\;\;${\rm{translate}}\,({\it{x\/}}, {\rm{cons}}\,({\it{z\/}}, {\it{bounds\/}}))\index{translate})\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  index-insert \\ \index{index-insert}
\=\+(({\it{x\/}} $\not=$ {\it{z\/}}) $\wedge$ ({\it{n\/}} $\leq$ {\rm{length}}\,({\it{bounds\/}})\index{length})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{index}}\,({\it{x\/}}, {\rm{insert}}\,({\it{z\/}}, {\it{bounds\/}}, {\it{n\/}})\index{insert})\index{index} $\not=$ ($1\;+$ {\it{n\/}}))\-
\end{tabbing}
\begin{verbatim};Translation distributes over substitution.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  translate-preserves-subst \\ \index{translate-preserves-subst}
\=\+(\=\+{\rm{free-for}}\,({\it{x\/}}, {\it{y\/}})\index{free-for} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{precede}}\,({\it{z\/}}, {\it{bounds\/}}, {\it{n\/}})\index{precede}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\leq$ {\rm{length}}\,({\it{bounds\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;${\rm{ntermp}}\,({\it{x\/}})\index{ntermp} \\ 
$\wedge$$\;\;\;\;${\rm{ntermp}}\,({\it{y\/}})\index{ntermp})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{translate}}\,({\rm{nsubst}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{nsubst}, {\it{bounds\/}})\index{translate} \\ 
$=$$\;\;\;\;${\rm{subst}}\,(\=\+{\rm{translate}}\,({\it{x\/}}, {\rm{insert}}\,({\it{z\/}}, {\it{bounds\/}}, {\it{n\/}})\index{insert})\index{translate}, \\ 
{\rm{translate}}\,({\it{y\/}}, {\it{bounds\/}})\index{translate}, \\ 
$1\;+$ {\it{n\/}})\-\index{subst})\-\-
\end{tabbing}
\begin{verbatim};Translation distributes over beta-reduction.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  translate-preserves-reduction \\ \index{translate-preserves-reduction}
\=\+({\rm{nlambdap}}\,({\it{x\/}})\index{nlambdap} $\wedge$ {\rm{free-for}}\,({\rm{nbody}}\,({\it{x\/}})\index{nbody}, {\it{y\/}})\index{free-for} $\wedge$ {\rm{ntermp}}\,({\it{x\/}})\index{ntermp} $\wedge$ {\rm{ntermp}}\,({\it{y\/}})\index{ntermp}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{translate}}\,({\rm{nsubst}}\,({\rm{nbody}}\,({\it{x\/}})\index{nbody}, {\it{y\/}}, {\rm{nbind}}\,({\it{x\/}})\index{nbind})\index{nsubst}, {\it{bounds\/}})\index{translate} \\ 
$=$$\;\;\;\;${\rm{subst}}\,({\rm{body}}\,({\rm{translate}}\,({\it{x\/}}, {\it{bounds\/}})\index{translate}), {\rm{translate}}\,({\it{y\/}}, {\it{bounds\/}})\index{translate}, {\tt{1}})\index{subst})\-\-
\end{tabbing}
\begin{verbatim};Reduction is the transitive closure of a walk.
;X goes to Y in a beta-step, in the de Bruijn notation.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{beta-step} \\  
\=\+{\rm{beta-step}}\,({\it{x\/}}, {\it{y\/}})\index{beta-step} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $=$ {\it{y\/}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{lambdap}}\,({\it{x\/}})\index{lambdap}$\;\;${\bf then }{\rm{lambdap}}\,({\it{y\/}})\index{lambdap} $\wedge$ {\rm{beta-step}}\,({\rm{body}}\,({\it{x\/}}), {\rm{body}}\,({\it{y\/}}))\index{beta-step} \\ 
{\bf elseif }{\rm{combp}}\,({\it{x\/}})\index{combp} \\ 
{\bf then }\=\+({\rm{lambdap}}\,({\rm{left}}\,({\it{x\/}})\index{left})\index{lambdap} $\wedge$ ({\it{y\/}} $=$ {\rm{subst}}\,({\rm{body}}\,({\rm{left}}\,({\it{x\/}})\index{left}), {\rm{right}}\,({\it{x\/}})\index{right}, {\tt{1}})\index{subst})) \\ 
$\vee$$\;\;\;\;$(\=\+{\rm{combp}}\,({\it{y\/}})\index{combp} \\ 
$\wedge$$\;\;\;\;${\rm{beta-step}}\,({\rm{left}}\,({\it{x\/}})\index{left}, {\rm{left}}\,({\it{y\/}})\index{left})\index{beta-step} \\ 
$\wedge$$\;\;\;\;${\rm{beta-step}}\,({\rm{right}}\,({\it{x\/}})\index{right}, {\rm{right}}\,({\it{y\/}})\index{right})\index{beta-step})\-\- \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim};A goes to B via LIST in a series of beta-steps.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{reduction} \\  
\=\+{\rm{reduction}}\,({\it{a\/}}, {\it{b\/}}, {\it{list\/}})\index{reduction} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{list\/}}) \\ 
{\bf then }{\rm{beta-step}}\,({\rm{car}}\,({\it{list\/}}), {\it{b\/}})\index{beta-step} $\wedge$ {\rm{reduction}}\,({\it{a\/}}, {\rm{car}}\,({\it{list\/}}), {\rm{cdr}}\,({\it{list\/}}))\index{reduction} \\ 
{\bf else }{\rm{beta-step}}\,({\it{a\/}}, {\it{b\/}})\index{beta-step}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{make-walk-step} \\  
\=\+{\rm{make-walk-step}}\,({\it{x\/}}, {\it{y\/}})\index{make-walk-step} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $=$ {\it{y\/}}$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }{\rm{lambdap}}\,({\it{x\/}})\index{lambdap}$\;\;${\bf then }{\rm{make-walk-step}}\,({\rm{body}}\,({\it{x\/}}), {\rm{body}}\,({\it{y\/}}))\index{make-walk-step} \\ 
{\bf elseif }{\rm{combp}}\,({\it{x\/}})\index{combp} \\ 
{\bf then }\=\+{\bf if }\=\+{\rm{lambdap}}\,({\rm{left}}\,({\it{x\/}})\index{left})\index{lambdap} \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $=$ {\rm{subst}}\,({\rm{body}}\,({\rm{left}}\,({\it{x\/}})\index{left}), {\rm{right}}\,({\it{x\/}})\index{right}, {\tt{1}})\index{subst})\- \\ 
{\bf then }{\tt{'}}{\tt{(}}{\tt{nil}}{\tt{ }}{\tt{nil}}{\tt{ }}{\tt{reduce}}{\tt{)}} \\ 
{\bf else }{\rm{list}}\,(\=\+{\rm{make-walk-step}}\,({\rm{left}}\,({\it{x\/}})\index{left}, {\rm{left}}\,({\it{y\/}})\index{left})\index{make-walk-step}, \\ 
{\rm{make-walk-step}}\,({\rm{right}}\,({\it{x\/}})\index{right}, {\rm{right}}\,({\it{y\/}})\index{right})\index{make-walk-step})\-$\;${\bf  endif}\- \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  make-walk-step-walks \\ \index{make-walk-step-walks}
{\rm{beta-step}}\,({\it{a\/}}, {\it{b\/}})\index{beta-step} $\rightarrow$ ({\rm{walk}}\,({\rm{make-walk-step}}\,({\it{a\/}}, {\it{b\/}})\index{make-walk-step}, {\it{a\/}})\index{walk} $=$ {\it{b\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{append} \\  
\=\+{\rm{append}}\,({\it{x\/}}, {\it{y\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}})$\;\;${\bf then }{\rm{cons}}\,({\rm{car}}\,({\it{x\/}}), {\rm{append}}\,({\rm{cdr}}\,({\it{x\/}}), {\it{y\/}})) \\ 
{\bf else }{\it{y\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{make-reduce-reduction} \\  
\=\+{\rm{make-reduce-reduction}}\,({\it{a\/}}, {\it{b\/}}, {\it{list\/}})\index{make-reduce-reduction} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{list\/}}) \\ 
{\bf then }{\rm{append}}\,(\=\+{\rm{make-reduce-reduction}}\,({\it{a\/}}, {\rm{car}}\,({\it{list\/}}), {\rm{cdr}}\,({\it{list\/}}))\index{make-reduce-reduction}, \\ 
{\rm{list}}\,({\rm{make-walk-step}}\,({\rm{car}}\,({\it{list\/}}), {\it{b\/}})\index{make-walk-step}, {\bf{nil}}))\- \\ 
{\bf else }{\rm{list}}\,({\rm{make-walk-step}}\,({\it{a\/}}, {\it{b\/}})\index{make-walk-step})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  reduce-append \\ \index{reduce-append}
{\rm{reduce}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}), {\it{a\/}})\index{reduce} $=$ {\rm{reduce}}\,({\it{y\/}}, {\rm{reduce}}\,({\it{x\/}}, {\it{a\/}})\index{reduce})\index{reduce}
\end{tabbing}
\begin{verbatim};A reduction is a series of walks.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  make-reduce-reduction-reduction \\ \index{make-reduce-reduction-reduction}
{\rm{reduction}}\,({\it{a\/}}, {\it{b\/}}, {\it{list\/}})\index{reduction} $\rightarrow$ ({\rm{reduce}}\,({\rm{make-reduce-reduction}}\,({\it{a\/}}, {\it{b\/}}, {\it{list\/}})\index{make-reduce-reduction}, {\it{a\/}})\index{reduce} $=$ {\it{b\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{list-lambda} \\  
\=\+{\rm{list-lambda}}\,({\it{list\/}})\index{list-lambda} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{list\/}})$\;\;${\bf then }{\rm{cons}}\,({\rm{lambda}}\,({\rm{car}}\,({\it{list\/}}))\index{lambda}, {\rm{list-lambda}}\,({\rm{cdr}}\,({\it{list\/}}))\index{list-lambda}) \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  lambda-reduction \\ \index{lambda-reduction}
{\rm{reduction}}\,({\it{a\/}}, {\it{a1\/}}, {\it{list\/}})\index{reduction} $\rightarrow$ {\rm{reduction}}\,({\rm{lambda}}\,({\it{a\/}})\index{lambda}, {\rm{lambda}}\,({\it{a1\/}})\index{lambda}, {\rm{list-lambda}}\,({\it{list\/}})\index{list-lambda})\index{reduction}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{map-comb-left} \\  
\=\+{\rm{map-comb-left}}\,({\it{a\/}}, {\it{list\/}})\index{map-comb-left} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{list\/}}) \\ 
{\bf then }{\rm{cons}}\,({\rm{comb}}\,({\it{a\/}}, {\rm{car}}\,({\it{list\/}}))\index{comb}, {\rm{map-comb-left}}\,({\it{a\/}}, {\rm{cdr}}\,({\it{list\/}}))\index{map-comb-left}) \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{map-comb-right} \\  
\=\+{\rm{map-comb-right}}\,({\it{a\/}}, {\it{list\/}})\index{map-comb-right} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{list\/}}) \\ 
{\bf then }{\rm{cons}}\,({\rm{comb}}\,({\rm{car}}\,({\it{list\/}}), {\it{a\/}})\index{comb}, {\rm{map-comb-right}}\,({\it{a\/}}, {\rm{cdr}}\,({\it{list\/}}))\index{map-comb-right}) \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{list-comb} \\  
\=\+{\rm{list-comb}}\,({\it{a\/}}, {\it{b\/}}, {\it{list1\/}}, {\it{list2\/}})\index{list-comb} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{list1\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{listp}}\,({\it{list2\/}}) \\ 
{\bf then }{\rm{cons}}\,(\=\+{\rm{comb}}\,({\rm{car}}\,({\it{list1\/}}), {\rm{car}}\,({\it{list2\/}}))\index{comb}, \\ 
{\rm{list-comb}}\,({\it{a\/}}, {\it{b\/}}, {\rm{cdr}}\,({\it{list1\/}}), {\rm{cdr}}\,({\it{list2\/}}))\index{list-comb})\- \\ 
{\bf else }{\rm{map-comb-right}}\,({\it{b\/}}, {\it{list1\/}})\index{map-comb-right}$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{listp}}\,({\it{list2\/}})$\;\;${\bf then }{\rm{map-comb-left}}\,({\it{a\/}}, {\it{list2\/}})\index{map-comb-left} \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  map-comb-right-reduction2 \\ \index{map-comb-right-reduction2}
\=\+{\rm{reduction}}\,({\it{a\/}}, {\it{a1\/}}, {\it{list1\/}})\index{reduction} \\ 
$\rightarrow$$\;\;\;\;${\rm{reduction}}\,({\rm{comb}}\,({\it{a\/}}, {\it{b1\/}})\index{comb}, {\rm{comb}}\,({\it{a1\/}}, {\it{b1\/}})\index{comb}, {\rm{map-comb-right}}\,({\it{b1\/}}, {\it{list1\/}})\index{map-comb-right})\index{reduction}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  map-comb-right-reduction \\ \index{map-comb-right-reduction}
\=\+({\rm{beta-step}}\,({\it{b\/}}, {\it{b1\/}})\index{beta-step} $\wedge$ {\rm{reduction}}\,({\it{a\/}}, {\it{a1\/}}, {\it{list1\/}})\index{reduction}) \\ 
$\rightarrow$$\;\;\;\;${\rm{reduction}}\,({\rm{comb}}\,({\it{a\/}}, {\it{b\/}})\index{comb}, {\rm{comb}}\,({\it{a1\/}}, {\it{b1\/}})\index{comb}, {\rm{map-comb-right}}\,({\it{b\/}}, {\it{list1\/}})\index{map-comb-right})\index{reduction}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  map-comb-left-reduction2 \\ \index{map-comb-left-reduction2}
\=\+{\rm{reduction}}\,({\it{b\/}}, {\it{b1\/}}, {\it{list2\/}})\index{reduction} \\ 
$\rightarrow$$\;\;\;\;${\rm{reduction}}\,({\rm{comb}}\,({\it{a1\/}}, {\it{b\/}})\index{comb}, {\rm{comb}}\,({\it{a1\/}}, {\it{b1\/}})\index{comb}, {\rm{map-comb-left}}\,({\it{a1\/}}, {\it{list2\/}})\index{map-comb-left})\index{reduction}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  map-comb-left-reduction \\ \index{map-comb-left-reduction}
\=\+({\rm{reduction}}\,({\it{b\/}}, {\it{b1\/}}, {\it{list2\/}})\index{reduction} $\wedge$ {\rm{beta-step}}\,({\it{a\/}}, {\it{a1\/}})\index{beta-step}) \\ 
$\rightarrow$$\;\;\;\;${\rm{reduction}}\,({\rm{comb}}\,({\it{a\/}}, {\it{b\/}})\index{comb}, {\rm{comb}}\,({\it{a1\/}}, {\it{b1\/}})\index{comb}, {\rm{map-comb-left}}\,({\it{a\/}}, {\it{list2\/}})\index{map-comb-left})\index{reduction}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  list-comb-reduction \\ \index{list-comb-reduction}
\=\+({\rm{reduction}}\,({\it{a\/}}, {\it{a1\/}}, {\it{list1\/}})\index{reduction} $\wedge$ {\rm{reduction}}\,({\it{b\/}}, {\it{b1\/}}, {\it{list2\/}})\index{reduction}) \\ 
$\rightarrow$$\;\;\;\;${\rm{reduction}}\,({\rm{comb}}\,({\it{a\/}}, {\it{b\/}})\index{comb}, {\rm{comb}}\,({\it{a1\/}}, {\it{b1\/}})\index{comb}, {\rm{list-comb}}\,({\it{a\/}}, {\it{b\/}}, {\it{list1\/}}, {\it{list2\/}})\index{list-comb})\index{reduction}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  beta-subst \\ \index{beta-subst}
{\rm{beta-step}}\,({\rm{comb}}\,({\rm{lambda}}\,({\it{a\/}})\index{lambda}, {\it{b\/}})\index{comb}, {\rm{subst}}\,({\it{a\/}}, {\it{b\/}}, {\tt{1}})\index{subst})\index{beta-step}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{make-reduction-walk} \\  
\=\+{\rm{make-reduction-walk}}\,({\it{w\/}}, {\it{a\/}})\index{make-reduction-walk} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{walk}}\,({\it{w\/}}, {\it{a\/}})\index{walk} $=$ {\it{a\/}}$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }{\rm{lambdap}}\,({\it{a\/}})\index{lambdap}$\;\;${\bf then }{\rm{list-lambda}}\,({\rm{make-reduction-walk}}\,({\it{w\/}}, {\rm{body}}\,({\it{a\/}}))\index{make-reduction-walk})\index{list-lambda} \\ 
{\bf elseif }{\rm{combp}}\,({\it{a\/}})\index{combp} \\ 
{\bf then }\=\+{\bf if }{\rm{lambdap}}\,({\rm{left}}\,({\it{a\/}})\index{left})\index{lambdap} $\wedge$ ({\rm{command}}\,({\it{w\/}})\index{command} $=$ {\tt{'}}{\tt{reduce}}) \\ 
{\bf then }{\rm{cons}}\,(\=\+{\rm{subst}}\,(\=\+{\rm{body}}\,({\rm{walk}}\,({\rm{left-instrs}}\,({\it{w\/}})\index{left-instrs}, {\rm{left}}\,({\it{a\/}})\index{left})\index{walk}), \\ 
{\rm{walk}}\,({\rm{right-instrs}}\,({\it{w\/}})\index{right-instrs}, {\rm{right}}\,({\it{a\/}})\index{right})\index{walk}, \\ 
{\tt{1}})\-\index{subst}, \\ 
{\rm{cons}}\,(\=\+{\rm{comb}}\,(\=\+{\rm{walk}}\,({\rm{left-instrs}}\,({\it{w\/}})\index{left-instrs}, {\rm{left}}\,({\it{a\/}})\index{left})\index{walk}, \\ 
{\rm{walk}}\,({\rm{right-instrs}}\,({\it{w\/}})\index{right-instrs}, {\rm{right}}\,({\it{a\/}})\index{right})\index{walk})\-\index{comb}, \\ 
{\rm{list-comb}}\,(\=\+{\rm{left}}\,({\it{a\/}})\index{left}, \\ 
{\rm{right}}\,({\it{a\/}})\index{right}, \\ 
{\rm{make-reduction-walk}}\,(\=\+{\rm{left-instrs}}\,({\it{w\/}})\index{left-instrs}, \\ 
{\rm{left}}\,({\it{a\/}})\index{left})\-\index{make-reduction-walk}, \\ 
{\rm{make-reduction-walk}}\,(\=\+{\rm{right-instrs}}\,({\it{w\/}})\index{right-instrs}, \\ 
{\rm{right}}\,({\it{a\/}})\index{right})\-\index{make-reduction-walk})\-\index{list-comb})\-)\- \\ 
{\bf else }{\rm{list-comb}}\,(\=\+{\rm{left}}\,({\it{a\/}})\index{left}, \\ 
{\rm{right}}\,({\it{a\/}})\index{right}, \\ 
{\rm{make-reduction-walk}}\,({\rm{left-instrs}}\,({\it{w\/}})\index{left-instrs}, {\rm{left}}\,({\it{a\/}})\index{left})\index{make-reduction-walk}, \\ 
{\rm{make-reduction-walk}}\,(\=\+{\rm{right-instrs}}\,({\it{w\/}})\index{right-instrs}, \\ 
{\rm{right}}\,({\it{a\/}})\index{right})\-\index{make-reduction-walk})\-\index{list-comb}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim};A walk is a series of beta-steps.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  make-reduction-walk-steps \\ \index{make-reduction-walk-steps}
{\rm{reduction}}\,({\it{a\/}}, {\rm{walk}}\,({\it{w\/}}, {\it{a\/}})\index{walk}, {\rm{make-reduction-walk}}\,({\it{w\/}}, {\it{a\/}})\index{make-reduction-walk})\index{reduction}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  reduction-append \\ \index{reduction-append}
\=\+({\rm{reduction}}\,({\it{a\/}}, {\it{b\/}}, {\it{x\/}})\index{reduction} $\wedge$ {\rm{reduction}}\,({\it{b\/}}, {\it{c\/}}, {\it{y\/}})\index{reduction}) \\ 
$\rightarrow$$\;\;\;\;${\rm{reduction}}\,({\it{a\/}}, {\it{c\/}}, {\rm{append}}\,({\it{y\/}}, {\rm{cons}}\,({\it{b\/}}, {\it{x\/}})))\index{reduction}\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{make-reduce-steps} \\  
\=\+{\rm{make-reduce-steps}}\,({\it{w\/}}, {\it{a\/}})\index{make-reduce-steps} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{w\/}}) \\ 
{\bf then }{\rm{append}}\,(\=\+{\rm{make-reduce-steps}}\,({\rm{cdr}}\,({\it{w\/}}), {\rm{walk}}\,({\rm{car}}\,({\it{w\/}}), {\it{a\/}})\index{walk})\index{make-reduce-steps}, \\ 
{\rm{cons}}\,({\rm{walk}}\,({\rm{car}}\,({\it{w\/}}), {\it{a\/}})\index{walk}, {\rm{make-reduction-walk}}\,({\rm{car}}\,({\it{w\/}}), {\it{a\/}})\index{make-reduction-walk}))\- \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  make-reduce-steps-steps \\ \index{make-reduce-steps-steps}
{\rm{reduction}}\,({\it{a\/}}, {\rm{reduce}}\,({\it{w\/}}, {\it{a\/}})\index{reduce}, {\rm{make-reduce-steps}}\,({\it{w\/}}, {\it{a\/}})\index{make-reduce-steps})\index{reduction}
\end{tabbing}
\begin{verbatim};`Skolem' function MAKE-W constructs the W to which Y and Z converge.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{make-w} \\  
\=\+{\rm{make-w}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}}, {\it{list1\/}}, {\it{list2\/}})\index{make-w} \\ 
$=$$\;\;\;\;${\rm{reduce}}\,(\=\+{\rm{make-reduce}}\,(\=\+{\it{x\/}}, \\ 
{\rm{make-reduce-reduction}}\,({\it{x\/}}, {\it{y\/}}, {\it{list1\/}})\index{make-reduce-reduction}, \\ 
{\rm{make-reduce-reduction}}\,({\it{x\/}}, {\it{z\/}}, {\it{list2\/}})\index{make-reduce-reduction})\-\index{make-reduce}, \\ 
{\rm{reduce}}\,({\rm{make-reduce-reduction}}\,({\it{x\/}}, {\it{z\/}}, {\it{list2\/}})\index{make-reduce-reduction}, {\it{x\/}})\index{reduce})\-\index{reduce}\-
\end{tabbing}
\begin{verbatim};MAKE-REDUCTION constructs the corresponding series of beta-steps.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{make-reduction} \\  
\=\+{\rm{make-reduction}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}}, {\it{list1\/}}, {\it{list2\/}})\index{make-reduction} \\ 
$=$$\;\;\;\;${\rm{make-reduce-steps}}\,(\=\+{\rm{make-reduce}}\,(\=\+{\it{x\/}}, \\ 
{\rm{make-reduce-reduction}}\,({\it{x\/}}, {\it{z\/}}, {\it{list2\/}})\index{make-reduce-reduction}, \\ 
{\rm{make-reduce-reduction}}\,({\it{x\/}}, {\it{y\/}}, {\it{list1\/}})\index{make-reduce-reduction})\-\index{make-reduce}, \\ 
{\it{y\/}})\-\index{make-reduce-steps}\-
\end{tabbing}
\begin{verbatim};The next two events together give the Church-Rosser theorem for the de Bruijn
;representation.  The first one shows the existence of convergent reductions,
;and the second one shows that they converge.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  the-real-church-rosser \\ \index{the-real-church-rosser}
\=\+({\rm{reduction}}\,({\it{x\/}}, {\it{y\/}}, {\it{list1\/}})\index{reduction} $\wedge$ {\rm{reduction}}\,({\it{x\/}}, {\it{z\/}}, {\it{list2\/}})\index{reduction}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{reduction}}\,(\=\+{\it{y\/}}, \\ 
{\rm{make-w}}\,({\it{x\/}}, {\it{z\/}}, {\it{y\/}}, {\it{list2\/}}, {\it{list1\/}})\index{make-w}, \\ 
{\rm{make-reduction}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}}, {\it{list1\/}}, {\it{list2\/}})\index{make-reduction})\-\index{reduction} \\ 
$\wedge$$\;\;\;\;${\rm{reduction}}\,(\=\+{\it{z\/}}, \\ 
{\rm{make-w}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}}, {\it{list1\/}}, {\it{list2\/}})\index{make-w}, \\ 
{\rm{make-reduction}}\,({\it{x\/}}, {\it{z\/}}, {\it{y\/}}, {\it{list2\/}}, {\it{list1\/}})\index{make-reduction})\-\index{reduction})\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  both-make-w-are-same \\ \index{both-make-w-are-same}
\=\+({\rm{reduction}}\,({\it{x\/}}, {\it{y\/}}, {\it{list1\/}})\index{reduction} $\wedge$ {\rm{reduction}}\,({\it{x\/}}, {\it{z\/}}, {\it{list2\/}})\index{reduction}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{make-w}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}}, {\it{list1\/}}, {\it{list2\/}})\index{make-w} $=$ {\rm{make-w}}\,({\it{x\/}}, {\it{z\/}}, {\it{y\/}}, {\it{list2\/}}, {\it{list1\/}})\index{make-w})\-
\end{tabbing}
\begin{verbatim};Translating the proof back into the standard notation.
;A standard beta-step translates to a de Bruijn beta-step.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  nbeta-step-translates \\ \index{nbeta-step-translates}
\=\+({\rm{ntermp}}\,({\it{a\/}})\index{ntermp} $\wedge$ {\rm{nbeta-step}}\,({\it{a\/}}, {\it{b\/}})\index{nbeta-step}) \\ 
$\rightarrow$$\;\;\;\;${\rm{beta-step}}\,({\rm{translate}}\,({\it{a\/}}, {\it{x\/}})\index{translate}, {\rm{translate}}\,({\it{b\/}}, {\it{x\/}})\index{translate})\index{beta-step}\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{trans-list} \\  
\=\+{\rm{trans-list}}\,({\it{x\/}})\index{trans-list} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}})$\;\;${\bf then }{\rm{cons}}\,({\rm{translate}}\,({\rm{car}}\,({\it{x\/}}), {\bf{nil}})\index{translate}, {\rm{trans-list}}\,({\rm{cdr}}\,({\it{x\/}}))\index{trans-list}) \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  ntermp-subst \\ \index{ntermp-subst}
({\rm{ntermp}}\,({\it{x\/}})\index{ntermp} $\wedge$ {\rm{ntermp}}\,({\it{y\/}})\index{ntermp}) $\rightarrow$ {\rm{ntermp}}\,({\rm{nsubst}}\,({\it{x\/}}, {\it{y\/}}, {\it{n\/}})\index{nsubst})\index{ntermp}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  ntermp-bstep \\ \index{ntermp-bstep}
({\rm{nbeta-step}}\,({\it{a\/}}, {\it{b\/}})\index{nbeta-step} $\wedge$ {\rm{ntermp}}\,({\it{a\/}})\index{ntermp}) $\rightarrow$ {\rm{ntermp}}\,({\it{b\/}})\index{ntermp}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  ntermp-astep \\ \index{ntermp-astep}
({\rm{alpha-equal}}\,({\it{a\/}}, {\it{b\/}}, {\it{x\/}}, {\it{y\/}})\index{alpha-equal} $\wedge$ {\rm{ntermp}}\,({\it{a\/}})\index{ntermp}) $\rightarrow$ {\rm{ntermp}}\,({\it{b\/}})\index{ntermp}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  ntermp-list \\ \index{ntermp-list}
({\rm{nreduction}}\,({\it{a\/}}, {\it{b\/}}, {\it{list\/}})\index{nreduction} $\wedge$ {\rm{ntermp}}\,({\it{a\/}})\index{ntermp}) $\rightarrow$ {\rm{ntermp}}\,({\it{b\/}})\index{ntermp}
\end{tabbing}
\begin{verbatim};Standard reduction goes to de Bruijn reduction.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  reduction-translates \\ \index{reduction-translates}
\=\+({\rm{ntermp}}\,({\it{a\/}})\index{ntermp} $\wedge$ {\rm{nreduction}}\,({\it{a\/}}, {\it{b\/}}, {\it{list\/}})\index{nreduction}) \\ 
$\rightarrow$$\;\;\;\;${\rm{reduction}}\,({\rm{translate}}\,({\it{a\/}}, {\bf{nil}})\index{translate}, {\rm{translate}}\,({\it{b\/}}, {\bf{nil}})\index{translate}, {\rm{trans-list}}\,({\it{list\/}})\index{trans-list})\index{reduction}\-
\end{tabbing}
\begin{verbatim};Finds the largest free-variable in the de Bruijn term X.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{find-m} \\  
\=\+{\rm{find-m}}\,({\it{x\/}}, {\it{n\/}})\index{find-m} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{lambdap}}\,({\it{x\/}})\index{lambdap}$\;\;${\bf then }{\rm{find-m}}\,({\rm{body}}\,({\it{x\/}}), $1\;+$ {\it{n\/}})\index{find-m} \\ 
{\bf elseif }{\rm{combp}}\,({\it{x\/}})\index{combp} \\ 
{\bf then }\=\+{\bf if }{\rm{find-m}}\,({\rm{left}}\,({\it{x\/}})\index{left}, {\it{n\/}})\index{find-m} $<$ {\rm{find-m}}\,({\rm{right}}\,({\it{x\/}})\index{right}, {\it{n\/}})\index{find-m} \\ 
{\bf then }{\rm{find-m}}\,({\rm{right}}\,({\it{x\/}})\index{right}, {\it{n\/}})\index{find-m} \\ 
{\bf else }{\rm{find-m}}\,({\rm{left}}\,({\it{x\/}})\index{left}, {\it{n\/}})\index{find-m}$\;${\bf  endif}\- \\ 
{\bf else }{\it{x\/}} $-$ {\it{n\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim};Translates the de Bruijn term X into a standard term given stack level N,
;and that M is the largest free variable in X.  Very tricky!
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{untrans} \\  
\=\+{\rm{untrans}}\,({\it{x\/}}, {\it{m\/}}, {\it{n\/}})\index{untrans} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{lambdap}}\,({\it{x\/}})\index{lambdap}$\;\;${\bf then }{\rm{nlambda}}\,({\it{m\/}} $+$ ($1\;+$ {\it{n\/}}), {\rm{untrans}}\,({\rm{body}}\,({\it{x\/}}), {\it{m\/}}, $1\;+$ {\it{n\/}})\index{untrans})\index{nlambda} \\ 
{\bf elseif }{\rm{combp}}\,({\it{x\/}})\index{combp} \\ 
{\bf then }{\rm{ncomb}}\,({\rm{untrans}}\,({\rm{left}}\,({\it{x\/}})\index{left}, {\it{m\/}}, {\it{n\/}})\index{untrans}, {\rm{untrans}}\,({\rm{right}}\,({\it{x\/}})\index{right}, {\it{m\/}}, {\it{n\/}})\index{untrans})\index{ncomb} \\ 
{\bf elseif }{\it{n\/}} $<$ {\it{x\/}}$\;\;${\bf then }{\it{x\/}} $-$ ($1\;+$ {\it{n\/}}) \\ 
{\bf elseif }{\it{x\/}} $\not\simeq {\tt{0}}$$\;\;${\bf then }$1\;+$ ({\it{m\/}} $+$ ({\it{n\/}} $-$ {\it{x\/}})) \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim};X is a well-formed de Bruijn term.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{termp} \\  
\=\+{\rm{termp}}\,({\it{x\/}})\index{termp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{lambdap}}\,({\it{x\/}})\index{lambdap}$\;\;${\bf then }{\rm{termp}}\,({\rm{body}}\,({\it{x\/}}))\index{termp} \\ 
{\bf elseif }{\rm{combp}}\,({\it{x\/}})\index{combp}$\;\;${\bf then }{\rm{termp}}\,({\rm{left}}\,({\it{x\/}})\index{left})\index{termp} $\wedge$ {\rm{termp}}\,({\rm{right}}\,({\it{x\/}})\index{right})\index{termp} \\ 
{\bf else }({\it{x\/}} $\not\simeq {\tt{0}}$) $\vee$ {\rm{litatom}}\,({\it{x\/}})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  not-free-in-untrans \\ \index{not-free-in-untrans}
\=\+({\rm{termp}}\,({\it{x\/}})\index{termp} $\wedge$ ({\rm{find-m}}\,({\it{x\/}}, {\it{n\/}})\index{find-m} $\leq$ {\it{m\/}}) $\wedge$ (({\it{m\/}} $+$ {\it{n\/}}) $<$ {\it{y\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{not-free-in}}\,({\it{y\/}}, {\rm{untrans}}\,({\it{x\/}}, {\it{m\/}}, {\it{n\/}})\index{untrans})\index{not-free-in}\-
\end{tabbing}
\begin{verbatim};An untranslated term is free for another untranslated term.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  free-for-untrans \\ \index{free-for-untrans}
\=\+({\rm{termp}}\,({\it{x\/}})\index{termp} $\wedge$ {\rm{termp}}\,({\it{y\/}})\index{termp} $\wedge$ ({\it{n2\/}} $\leq$ {\it{n1\/}}) $\wedge$ ({\rm{find-m}}\,({\it{y\/}}, {\it{n2\/}})\index{find-m} $\leq$ {\it{m\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{free-for}}\,({\rm{untrans}}\,({\it{x\/}}, {\it{m\/}}, {\it{n1\/}})\index{untrans}, {\rm{untrans}}\,({\it{y\/}}, {\it{m\/}}, {\it{n2\/}})\index{untrans})\index{free-for}\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{trans-untrans-ind} \\  
\=\+{\rm{trans-untrans-ind}}\,({\it{x\/}}, {\it{bounds\/}}, {\it{m\/}}, {\it{n\/}})\index{trans-untrans-ind} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{nlambdap}}\,({\it{x\/}})\index{nlambdap} \\ 
{\bf then }{\rm{trans-untrans-ind}}\,({\rm{nbody}}\,({\it{x\/}})\index{nbody}, {\rm{cons}}\,({\rm{nbind}}\,({\it{x\/}})\index{nbind}, {\it{bounds\/}}), {\it{m\/}}, $1\;+$ {\it{n\/}})\index{trans-untrans-ind} \\ 
{\bf elseif }{\rm{ncombp}}\,({\it{x\/}})\index{ncombp} \\ 
{\bf then }\=\+{\rm{trans-untrans-ind}}\,({\rm{nleft}}\,({\it{x\/}})\index{nleft}, {\it{bounds\/}}, {\it{m\/}}, {\it{n\/}})\index{trans-untrans-ind} \\ 
$\wedge$$\;\;\;\;${\rm{trans-untrans-ind}}\,({\rm{nright}}\,({\it{x\/}})\index{nright}, {\it{bounds\/}}, {\it{m\/}}, {\it{n\/}})\index{trans-untrans-ind}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim};Generates a list of bound variables of length N.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{bindings} \\  
\=\+{\rm{bindings}}\,({\it{m\/}}, {\it{n\/}})\index{bindings} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,({\it{m\/}} $+$ {\it{n\/}}, {\rm{bindings}}\,({\it{m\/}}, {\it{n\/}} $-\;1$)\index{bindings})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim};A TRANSLATE followed by an UNTRANS leaves X unchanged (modulo bound variables).
\end{verbatim}\begin{tabbing}{\sc Theorem}:  trans-untrans \\ \index{trans-untrans}
\=\+(\=\+({\rm{length}}\,({\it{bounds\/}})\index{length} $=$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{ntermp}}\,({\it{x\/}})\index{ntermp} \\ 
$\wedge$$\;\;\;\;$({\rm{find-m}}\,({\rm{translate}}\,({\it{x\/}}, {\it{bounds\/}})\index{translate}, {\it{n\/}})\index{find-m} $\leq$ {\it{m\/}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{alpha-equal}}\,({\it{x\/}}, {\rm{untrans}}\,({\rm{translate}}\,({\it{x\/}}, {\it{bounds\/}})\index{translate}, {\it{m\/}}, {\it{n\/}})\index{untrans}, {\it{bounds\/}}, {\rm{bindings}}\,({\it{m\/}}, {\it{n\/}})\index{bindings})\index{alpha-equal}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  termp-ntermp \\ \index{termp-ntermp}
{\rm{ntermp}}\,({\it{x\/}})\index{ntermp} $\rightarrow$ {\rm{termp}}\,({\rm{translate}}\,({\it{x\/}}, {\it{bounds\/}})\index{translate})\index{termp}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  ntermp-termp \\ \index{ntermp-termp}
{\rm{termp}}\,({\it{x\/}})\index{termp} $\rightarrow$ {\rm{ntermp}}\,({\rm{untrans}}\,({\it{x\/}}, {\it{m\/}}, {\it{n\/}})\index{untrans})\index{ntermp}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  index-freevar \\ \index{index-freevar}
\=\+(({\it{n\/}} $<$ {\it{x\/}}) $\wedge$ (({\it{x\/}} $-$ {\it{n\/}}) $\leq$ {\it{m\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{index}}\,(({\it{x\/}} $-\;1$) $-$ {\it{n\/}}, {\rm{bindings}}\,({\it{m\/}}, {\it{n\/}})\index{bindings})\index{index} $=$ {\it{x\/}})\-
\end{tabbing}
\begin{verbatim};An UNTRANS followed by a TRANSLATE doesn't change a thing.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  untrans-trans \\ \index{untrans-trans}
\=\+({\rm{termp}}\,({\it{x\/}})\index{termp} $\wedge$ ({\rm{find-m}}\,({\it{x\/}}, {\it{n\/}})\index{find-m} $\leq$ {\it{m\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{translate}}\,({\rm{untrans}}\,({\it{x\/}}, {\it{m\/}}, {\it{n\/}})\index{untrans}, {\rm{bindings}}\,({\it{m\/}}, {\it{n\/}})\index{bindings})\index{translate} $=$ {\it{x\/}})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  untrans-subst \\ \index{untrans-subst}
\=\+(\=\+{\rm{termp}}\,({\it{x\/}})\index{termp} \\ 
$\wedge$$\;\;\;\;${\rm{termp}}\,({\it{y\/}})\index{termp} \\ 
$\wedge$$\;\;\;\;${\rm{lambdap}}\,({\it{x\/}})\index{lambdap} \\ 
$\wedge$$\;\;\;\;$({\rm{find-m}}\,({\it{y\/}}, {\it{n\/}})\index{find-m} $\leq$ {\it{m\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{find-m}}\,({\it{x\/}}, {\it{n\/}})\index{find-m} $\leq$ {\it{m\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{translate}}\,(\=\+{\rm{nsubst}}\,(\=\+{\rm{nbody}}\,({\rm{untrans}}\,({\it{x\/}}, {\it{m\/}}, {\it{n\/}})\index{untrans})\index{nbody}, \\ 
{\rm{untrans}}\,({\it{y\/}}, {\it{m\/}}, {\it{n\/}})\index{untrans}, \\ 
{\rm{nbind}}\,({\rm{untrans}}\,({\it{x\/}}, {\it{m\/}}, {\it{n\/}})\index{untrans})\index{nbind})\-\index{nsubst}, \\ 
{\rm{bindings}}\,({\it{m\/}}, {\it{n\/}})\index{bindings})\-\index{translate} \\ 
$=$$\;\;\;\;${\rm{subst}}\,({\rm{body}}\,({\it{x\/}}), {\it{y\/}}, {\tt{1}})\index{subst})\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  litatom-translate \\ \index{litatom-translate}
{\rm{litatom}}\,({\rm{translate}}\,({\it{a\/}}, {\it{bounds\/}})\index{translate}) $\rightarrow$ ({\rm{translate}}\,({\it{a\/}}, {\it{bounds\/}})\index{translate} $=$ {\it{a\/}})
\end{tabbing}
\begin{verbatim};If A and B have the same translation, then they are alpha-equal.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  translate-alpha \\ \index{translate-alpha}
\=\+({\rm{ntermp}}\,({\it{a\/}})\index{ntermp} $\wedge$ {\rm{ntermp}}\,({\it{b\/}})\index{ntermp} $\wedge$ ({\rm{translate}}\,({\it{a\/}}, {\it{bounds\/}})\index{translate} $=$ {\rm{translate}}\,({\it{b\/}}, {\it{bounds2\/}})\index{translate})) \\ 
$\rightarrow$$\;\;\;\;${\rm{alpha-equal}}\,({\it{a\/}}, {\it{b\/}}, {\it{bounds\/}}, {\it{bounds2\/}})\index{alpha-equal}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  termp-bump \\ \index{termp-bump}
{\rm{termp}}\,({\it{x\/}})\index{termp} $\rightarrow$ {\rm{termp}}\,({\rm{bump}}\,({\it{x\/}}, {\it{n\/}})\index{bump})\index{termp}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  termp-subst \\ \index{termp-subst}
({\rm{termp}}\,({\it{x\/}})\index{termp} $\wedge$ {\rm{termp}}\,({\it{y\/}})\index{termp} $\wedge$ ({\it{n\/}} $\not\simeq {\tt{0}}$)) $\rightarrow$ {\rm{termp}}\,({\rm{subst}}\,({\it{x\/}}, {\it{y\/}}, {\it{n\/}})\index{subst})\index{termp}
\end{tabbing}
\begin{verbatim};Returns an instruction corresponding to a beta-step.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{make-bstep} \\  
\=\+{\rm{make-bstep}}\,({\it{a\/}}, {\it{b\/}})\index{make-bstep} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{a\/}} $=$ {\it{b\/}}$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }{\rm{lambdap}}\,({\it{a\/}})\index{lambdap} $\wedge$ {\rm{lambdap}}\,({\it{b\/}})\index{lambdap}$\;\;${\bf then }{\rm{make-bstep}}\,({\rm{body}}\,({\it{a\/}}), {\rm{body}}\,({\it{b\/}}))\index{make-bstep} \\ 
{\bf elseif }{\rm{combp}}\,({\it{a\/}})\index{combp} \\ 
{\bf then }\=\+{\bf if }\=\+{\rm{lambdap}}\,({\rm{left}}\,({\it{a\/}})\index{left})\index{lambdap} \\ 
$\wedge$$\;\;\;\;$({\it{b\/}} $=$ {\rm{subst}}\,({\rm{body}}\,({\rm{left}}\,({\it{a\/}})\index{left}), {\rm{right}}\,({\it{a\/}})\index{right}, {\tt{1}})\index{subst})\- \\ 
{\bf then }{\rm{list}}\,({\bf{nil}}, {\bf{nil}}, {\tt{'}}{\tt{reduce}}) \\ 
{\bf else }{\rm{list}}\,(\=\+{\rm{make-bstep}}\,({\rm{left}}\,({\it{a\/}})\index{left}, {\rm{left}}\,({\it{b\/}})\index{left})\index{make-bstep}, \\ 
{\rm{make-bstep}}\,({\rm{right}}\,({\it{a\/}})\index{right}, {\rm{right}}\,({\it{b\/}})\index{right})\index{make-bstep})\-$\;${\bf  endif}\- \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim};Applies the instruction to a term.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{bstep} \\  
\=\+{\rm{bstep}}\,({\it{w\/}}, {\it{x\/}})\index{bstep} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{lambdap}}\,({\it{x\/}})\index{lambdap}$\;\;${\bf then }{\rm{lambda}}\,({\rm{bstep}}\,({\it{w\/}}, {\rm{body}}\,({\it{x\/}}))\index{bstep})\index{lambda} \\ 
{\bf elseif }{\rm{combp}}\,({\it{x\/}})\index{combp} \\ 
{\bf then }\=\+{\bf if }{\rm{lambdap}}\,({\rm{left}}\,({\it{x\/}})\index{left})\index{lambdap} $\wedge$ ({\rm{command}}\,({\it{w\/}})\index{command} $=$ {\tt{'}}{\tt{reduce}}) \\ 
{\bf then }{\rm{subst}}\,({\rm{body}}\,({\rm{left}}\,({\it{x\/}})\index{left}), {\rm{right}}\,({\it{x\/}})\index{right}, {\tt{1}})\index{subst} \\ 
{\bf else }{\rm{comb}}\,(\=\+{\rm{bstep}}\,({\rm{left-instrs}}\,({\it{w\/}})\index{left-instrs}, {\rm{left}}\,({\it{x\/}})\index{left})\index{bstep}, \\ 
{\rm{bstep}}\,({\rm{right-instrs}}\,({\it{w\/}})\index{right-instrs}, {\rm{right}}\,({\it{x\/}})\index{right})\index{bstep})\-\index{comb}$\;${\bf  endif}\- \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim};The instruction works.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  make-bstep-beta-step \\ \index{make-bstep-beta-step}
{\rm{beta-step}}\,({\it{a\/}}, {\it{b\/}})\index{beta-step} $\rightarrow$ ({\rm{bstep}}\,({\rm{make-bstep}}\,({\it{a\/}}, {\it{b\/}})\index{make-bstep}, {\it{a\/}})\index{bstep} $=$ {\it{b\/}})
\end{tabbing}
\begin{verbatim};A standard beta-step.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{nbstep} \\  
\=\+{\rm{nbstep}}\,({\it{w\/}}, {\it{x\/}})\index{nbstep} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{nlambdap}}\,({\it{x\/}})\index{nlambdap}$\;\;${\bf then }{\rm{nlambda}}\,({\rm{nbind}}\,({\it{x\/}})\index{nbind}, {\rm{nbstep}}\,({\it{w\/}}, {\rm{nbody}}\,({\it{x\/}})\index{nbody})\index{nbstep})\index{nlambda} \\ 
{\bf elseif }{\rm{ncombp}}\,({\it{x\/}})\index{ncombp} \\ 
{\bf then }\=\+{\bf if }{\rm{nlambdap}}\,({\rm{nleft}}\,({\it{x\/}})\index{nleft})\index{nlambdap} $\wedge$ ({\rm{command}}\,({\it{w\/}})\index{command} $=$ {\tt{'}}{\tt{reduce}}) \\ 
{\bf then }{\rm{nsubst}}\,({\rm{nbody}}\,({\rm{nleft}}\,({\it{x\/}})\index{nleft})\index{nbody}, {\rm{nright}}\,({\it{x\/}})\index{nright}, {\rm{nbind}}\,({\rm{nleft}}\,({\it{x\/}})\index{nleft})\index{nbind})\index{nsubst} \\ 
{\bf else }{\rm{ncomb}}\,(\=\+{\rm{nbstep}}\,({\rm{left-instrs}}\,({\it{w\/}})\index{left-instrs}, {\rm{nleft}}\,({\it{x\/}})\index{nleft})\index{nbstep}, \\ 
{\rm{nbstep}}\,({\rm{right-instrs}}\,({\it{w\/}})\index{right-instrs}, {\rm{nright}}\,({\it{x\/}})\index{nright})\index{nbstep})\-\index{ncomb}$\;${\bf  endif}\- \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  lambdap-untrans \\ \index{lambdap-untrans}
{\rm{termp}}\,({\it{x\/}})\index{termp} $\rightarrow$ ({\rm{nlambdap}}\,({\rm{untrans}}\,({\it{x\/}}, {\it{m\/}}, {\it{n\/}})\index{untrans})\index{nlambdap} $=$ {\rm{lambdap}}\,({\it{x\/}})\index{lambdap})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{find-m-subst-ind} \\  
\=\+{\rm{find-m-subst-ind}}\,({\it{x\/}}, {\it{y\/}}, {\it{m\/}}, {\it{n\/}}, {\it{ind\/}})\index{find-m-subst-ind} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{lambdap}}\,({\it{x\/}})\index{lambdap} \\ 
{\bf then }{\rm{find-m-subst-ind}}\,({\rm{body}}\,({\it{x\/}}), {\rm{bump}}\,({\it{y\/}}, {\tt{0}})\index{bump}, {\it{m\/}}, $1\;+$ {\it{n\/}}, $1\;+$ {\it{ind\/}})\index{find-m-subst-ind} \\ 
{\bf elseif }{\rm{combp}}\,({\it{x\/}})\index{combp} \\ 
{\bf then }\=\+{\rm{find-m-subst-ind}}\,({\rm{left}}\,({\it{x\/}})\index{left}, {\it{y\/}}, {\it{m\/}}, {\it{n\/}}, {\it{ind\/}})\index{find-m-subst-ind} \\ 
$\wedge$$\;\;\;\;${\rm{find-m-subst-ind}}\,({\rm{right}}\,({\it{x\/}})\index{right}, {\it{y\/}}, {\it{m\/}}, {\it{n\/}}, {\it{ind\/}})\index{find-m-subst-ind}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  find-m-bump \\ \index{find-m-bump}
{\rm{find-m}}\,({\it{y\/}}, {\it{n\/}})\index{find-m} $\not<$ {\rm{find-m}}\,({\rm{bump}}\,({\it{y\/}}, {\it{count\/}})\index{bump}, $1\;+$ {\it{n\/}})\index{find-m}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  diff-zero \\ \index{diff-zero}
({\it{m\/}} $\leq$ {\it{n\/}}) $\rightarrow$ (({\it{m\/}} $-$ {\it{n\/}}) $=$ {\tt{0}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{untrans-bstep-ind} \\  
\=\+{\rm{untrans-bstep-ind}}\,({\it{a\/}}, {\it{b\/}}, {\it{m\/}}, {\it{n\/}})\index{untrans-bstep-ind} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{a\/}} $=$ {\it{b\/}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{lambdap}}\,({\it{a\/}})\index{lambdap} $\wedge$ {\rm{lambdap}}\,({\it{b\/}})\index{lambdap} \\ 
{\bf then }{\rm{untrans-bstep-ind}}\,({\rm{body}}\,({\it{a\/}}), {\rm{body}}\,({\it{b\/}}), {\it{m\/}}, $1\;+$ {\it{n\/}})\index{untrans-bstep-ind} \\ 
{\bf elseif }{\rm{combp}}\,({\it{a\/}})\index{combp} \\ 
{\bf then }\=\+{\bf if }\=\+{\rm{lambdap}}\,({\rm{left}}\,({\it{a\/}})\index{left})\index{lambdap} \\ 
$\wedge$$\;\;\;\;$({\it{b\/}} $=$ {\rm{subst}}\,({\rm{body}}\,({\rm{left}}\,({\it{a\/}})\index{left}), {\rm{right}}\,({\it{a\/}})\index{right}, {\tt{1}})\index{subst})\-$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }\=\+{\rm{untrans-bstep-ind}}\,({\rm{left}}\,({\it{a\/}})\index{left}, {\rm{left}}\,({\it{b\/}})\index{left}, {\it{m\/}}, {\it{n\/}})\index{untrans-bstep-ind} \\ 
$\wedge$$\;\;\;\;${\rm{untrans-bstep-ind}}\,({\rm{right}}\,({\it{a\/}})\index{right}, {\rm{right}}\,({\it{b\/}})\index{right}, {\it{m\/}}, {\it{n\/}})\index{untrans-bstep-ind}\-$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  nbstep-nil \\ \index{nbstep-nil}
({\it{w\/}} $\simeq\;${{\bf{nil}}}${}$) $\rightarrow$ ({\rm{nbstep}}\,({\it{w\/}}, {\it{a\/}})\index{nbstep} $=$ {\it{a\/}})
\end{tabbing}
\begin{verbatim};A beta-step translates back.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  untrans-beta-step \\ \index{untrans-beta-step}
\=\+({\rm{beta-step}}\,({\it{a\/}}, {\it{b\/}})\index{beta-step} $\wedge$ {\rm{termp}}\,({\it{a\/}})\index{termp} $\wedge$ ({\rm{find-m}}\,({\it{a\/}}, {\it{n\/}})\index{find-m} $\leq$ {\it{m\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{nbeta-step}}\,({\rm{untrans}}\,({\it{a\/}}, {\it{m\/}}, {\it{n\/}})\index{untrans}, {\rm{nbstep}}\,({\rm{make-bstep}}\,({\it{a\/}}, {\it{b\/}})\index{make-bstep}, {\rm{untrans}}\,({\it{a\/}}, {\it{m\/}}, {\it{n\/}})\index{untrans})\index{nbstep})\index{nbeta-step}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  find-m-bump2 \\ \index{find-m-bump2}
({\it{count\/}} $\leq$ {\it{n\/}}) $\rightarrow$ ({\rm{find-m}}\,({\rm{bump}}\,({\it{y\/}}, {\it{count\/}})\index{bump}, $1\;+$ {\it{n\/}})\index{find-m} $=$ {\rm{find-m}}\,({\it{y\/}}, {\it{n\/}})\index{find-m})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  termp-beta-step \\ \index{termp-beta-step}
({\rm{beta-step}}\,({\it{a\/}}, {\it{b\/}})\index{beta-step} $\wedge$ {\rm{termp}}\,({\it{a\/}})\index{termp}) $\rightarrow$ {\rm{termp}}\,({\it{b\/}})\index{termp}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  termp-reduction \\ \index{termp-reduction}
({\rm{reduction}}\,({\it{a\/}}, {\it{b\/}}, {\it{list\/}})\index{reduction} $\wedge$ {\rm{termp}}\,({\it{a\/}})\index{termp}) $\rightarrow$ {\rm{termp}}\,({\it{b\/}})\index{termp}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  find-m-subst \\ \index{find-m-subst}
\=\+(({\rm{find-m}}\,({\it{x\/}}, $1\;+$ {\it{n\/}})\index{find-m} $\leq$ {\it{m\/}}) $\wedge$ ({\rm{find-m}}\,({\it{y\/}}, {\it{n\/}})\index{find-m} $\leq$ {\it{m\/}}) $\wedge$ ({\it{ind\/}} $\leq$ {\it{n\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\it{m\/}} $\not<$ {\rm{find-m}}\,({\rm{subst}}\,({\it{x\/}}, {\it{y\/}}, $1\;+$ {\it{ind\/}})\index{subst}, {\it{n\/}})\index{find-m})\-
\end{tabbing}
\begin{verbatim};What a beta-step translates back into is alpha-equal to what would've
;been gotten by doing the step directly in the standard form.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  untrans-subst-nsubst \\ \index{untrans-subst-nsubst}
\=\+(\=\+{\rm{termp}}\,({\it{x\/}})\index{termp} \\ 
$\wedge$$\;\;\;\;${\rm{termp}}\,({\it{y\/}})\index{termp} \\ 
$\wedge$$\;\;\;\;${\rm{lambdap}}\,({\it{x\/}})\index{lambdap} \\ 
$\wedge$$\;\;\;\;$({\rm{find-m}}\,({\it{y\/}}, {\it{n\/}})\index{find-m} $\leq$ {\it{m\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{find-m}}\,({\it{x\/}}, {\it{n\/}})\index{find-m} $\leq$ {\it{m\/}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{alpha-equal}}\,(\=\+{\rm{nsubst}}\,(\=\+{\rm{nbody}}\,({\rm{untrans}}\,({\it{x\/}}, {\it{m\/}}, {\it{n\/}})\index{untrans})\index{nbody}, \\ 
{\rm{untrans}}\,({\it{y\/}}, {\it{m\/}}, {\it{n\/}})\index{untrans}, \\ 
{\rm{nbind}}\,({\rm{untrans}}\,({\it{x\/}}, {\it{m\/}}, {\it{n\/}})\index{untrans})\index{nbind})\-\index{nsubst}, \\ 
{\rm{untrans}}\,({\rm{subst}}\,({\rm{body}}\,({\it{x\/}}), {\it{y\/}}, {\tt{1}})\index{subst}, {\it{m\/}}, {\it{n\/}})\index{untrans}, \\ 
{\rm{bindings}}\,({\it{m\/}}, {\it{n\/}})\index{bindings}, \\ 
{\rm{bindings}}\,({\it{m\/}}, {\it{n\/}})\index{bindings})\-\index{alpha-equal}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  untrans-nbstep \\ \index{untrans-nbstep}
\=\+({\rm{termp}}\,({\it{x\/}})\index{termp} $\wedge$ ({\rm{find-m}}\,({\it{x\/}}, {\it{n\/}})\index{find-m} $\leq$ {\it{m\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{alpha-equal}}\,(\=\+{\rm{nbstep}}\,({\it{w\/}}, {\rm{untrans}}\,({\it{x\/}}, {\it{m\/}}, {\it{n\/}})\index{untrans})\index{nbstep}, \\ 
{\rm{untrans}}\,({\rm{bstep}}\,({\it{w\/}}, {\it{x\/}})\index{bstep}, {\it{m\/}}, {\it{n\/}})\index{untrans}, \\ 
{\rm{bindings}}\,({\it{m\/}}, {\it{n\/}})\index{bindings}, \\ 
{\rm{bindings}}\,({\it{m\/}}, {\it{n\/}})\index{bindings})\-\index{alpha-equal}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  another-find-m-subst \\ \index{another-find-m-subst}
\=\+(({\rm{find-m}}\,({\it{y\/}}, {\it{n\/}})\index{find-m} $\leq$ {\it{m\/}}) $\wedge$ ({\rm{find-m}}\,({\it{x\/}}, $1\;+$ {\it{n\/}})\index{find-m} $\leq$ {\it{m\/}}) $\wedge$ ({\it{ind\/}} $\leq$ {\it{n\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\it{m\/}} $\not<$ {\rm{find-m}}\,({\rm{subst}}\,({\it{x\/}}, {\it{y\/}}, $1\;+$ {\it{ind\/}})\index{subst}, {\it{n\/}})\index{find-m})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  untrans-nbstep-zero \\ \index{untrans-nbstep-zero}
\=\+({\rm{beta-step}}\,({\it{x\/}}, {\it{y\/}})\index{beta-step} $\wedge$ {\rm{termp}}\,({\it{x\/}})\index{termp} $\wedge$ ({\rm{find-m}}\,({\it{x\/}}, {\tt{0}})\index{find-m} $\leq$ {\it{m\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{alpha-equal}}\,(\=\+{\rm{nbstep}}\,({\rm{make-bstep}}\,({\it{x\/}}, {\it{y\/}})\index{make-bstep}, {\rm{untrans}}\,({\it{x\/}}, {\it{m\/}}, {\tt{0}})\index{untrans})\index{nbstep}, \\ 
{\rm{untrans}}\,({\it{y\/}}, {\it{m\/}}, {\tt{0}})\index{untrans}, \\ 
{\bf{nil}}, \\ 
{\bf{nil}})\-\index{alpha-equal}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  beta-step-find-m \\ \index{beta-step-find-m}
({\rm{beta-step}}\,({\it{a\/}}, {\it{b\/}})\index{beta-step} $\wedge$ ({\rm{find-m}}\,({\it{a\/}}, {\it{n\/}})\index{find-m} $\leq$ {\it{m\/}})) $\rightarrow$ ({\it{m\/}} $\not<$ {\rm{find-m}}\,({\it{b\/}}, {\it{n\/}})\index{find-m})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  another-beta-step-find-m \\ \index{another-beta-step-find-m}
{\rm{beta-step}}\,({\it{a\/}}, {\it{b\/}})\index{beta-step} $\rightarrow$ ({\rm{find-m}}\,({\it{a\/}}, {\it{n\/}})\index{find-m} $\not<$ {\rm{find-m}}\,({\it{b\/}}, {\it{n\/}})\index{find-m})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  reduction-find-m \\ \index{reduction-find-m}
{\rm{reduction}}\,({\it{a\/}}, {\it{b\/}}, {\it{list\/}})\index{reduction} $\rightarrow$ ({\rm{find-m}}\,({\it{a\/}}, {\it{n\/}})\index{find-m} $\not<$ {\rm{find-m}}\,({\it{b\/}}, {\it{n\/}})\index{find-m})
\end{tabbing}

\noindent{\sc Event}:   Enable make-w; name this event `g0350'.\index{g0350}

\addvspace{18pt}

\noindent{\sc Event}:   Enable make-reduction; name this event `g0351'.\index{g0351}

\addvspace{18pt}
\begin{verbatim};Standard term corresponding to MAKE-W.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{make-n-w} \\  
\=\+{\rm{make-n-w}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}}, {\it{list1\/}}, {\it{list2\/}})\index{make-n-w} \\ 
$=$$\;\;\;\;${\rm{untrans}}\,(\=\+{\rm{make-w}}\,(\=\+{\rm{translate}}\,({\it{x\/}}, {\bf{nil}})\index{translate}, \\ 
{\rm{translate}}\,({\it{y\/}}, {\bf{nil}})\index{translate}, \\ 
{\rm{translate}}\,({\it{z\/}}, {\bf{nil}})\index{translate}, \\ 
{\rm{trans-list}}\,({\it{list1\/}})\index{trans-list}, \\ 
{\rm{trans-list}}\,({\it{list2\/}})\index{trans-list})\-\index{make-w}, \\ 
{\rm{find-m}}\,({\rm{translate}}\,({\it{x\/}}, {\bf{nil}})\index{translate}, {\tt{0}})\index{find-m}, \\ 
{\tt{0}})\-\index{untrans}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  alpha-equal-commutes \\ \index{alpha-equal-commutes}
{\rm{alpha-equal}}\,({\it{a\/}}, {\it{b\/}}, {\it{x\/}}, {\it{y\/}})\index{alpha-equal} $=$ {\rm{alpha-equal}}\,({\it{b\/}}, {\it{a\/}}, {\it{y\/}}, {\it{x\/}})\index{alpha-equal}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{end-cons} \\  
\=\+{\rm{end-cons}}\,({\it{x\/}}, {\it{y\/}})\index{end-cons} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{y\/}})$\;\;${\bf then }{\rm{cons}}\,({\rm{car}}\,({\it{y\/}}), {\rm{end-cons}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{y\/}}))\index{end-cons}) \\ 
{\bf else }{\rm{cons}}\,({\it{x\/}}, {\bf{nil}})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  end-cons-nreduction \\ \index{end-cons-nreduction}
\=\+({\rm{nreduction}}\,({\it{a\/}}, {\it{b\/}}, {\it{list\/}})\index{nreduction} $\wedge$ {\rm{nstep}}\,({\it{a1\/}}, {\it{a\/}})\index{nstep}) \\ 
$\rightarrow$$\;\;\;\;${\rm{nreduction}}\,({\it{a1\/}}, {\it{b\/}}, {\rm{end-cons}}\,({\it{a\/}}, {\it{list\/}})\index{end-cons})\index{nreduction}\-
\end{tabbing}
\begin{verbatim};Translates reductions back.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{make-nreduction} \\  
\=\+{\rm{make-nreduction}}\,({\it{a\/}}, {\it{b\/}}, {\it{w\/}}, {\it{m\/}})\index{make-nreduction} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{w\/}}) \\ 
{\bf then }{\rm{cons}}\,(\=\+{\rm{nbstep}}\,({\rm{make-bstep}}\,({\rm{car}}\,({\it{w\/}}), {\it{b\/}})\index{make-bstep}, {\rm{untrans}}\,({\rm{car}}\,({\it{w\/}}), {\it{m\/}}, {\tt{0}})\index{untrans})\index{nbstep}, \\ 
{\rm{cons}}\,(\=\+{\rm{untrans}}\,({\rm{car}}\,({\it{w\/}}), {\it{m\/}}, {\tt{0}})\index{untrans}, \\ 
{\rm{make-nreduction}}\,({\it{a\/}}, {\rm{car}}\,({\it{w\/}}), {\rm{cdr}}\,({\it{w\/}}), {\it{m\/}})\index{make-nreduction})\-)\- \\ 
{\bf else }{\rm{cons}}\,(\=\+{\rm{untrans}}\,({\it{b\/}}, {\it{m\/}}, {\tt{0}})\index{untrans}, \\ 
{\rm{cons}}\,({\rm{nbstep}}\,({\rm{make-bstep}}\,({\it{a\/}}, {\it{b\/}})\index{make-bstep}, {\rm{untrans}}\,({\it{a\/}}, {\it{m\/}}, {\tt{0}})\index{untrans})\index{nbstep}, {\bf{nil}}))\-$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim};Reductions translate.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  reduction-make-nreduction \\ \index{reduction-make-nreduction}
\=\+({\rm{reduction}}\,({\it{a\/}}, {\it{b\/}}, {\it{list\/}})\index{reduction} $\wedge$ {\rm{termp}}\,({\it{a\/}})\index{termp} $\wedge$ ({\rm{find-m}}\,({\it{a\/}}, {\tt{0}})\index{find-m} $\leq$ {\it{m\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{nreduction}}\,({\rm{untrans}}\,({\it{a\/}}, {\it{m\/}}, {\tt{0}})\index{untrans}, {\rm{untrans}}\,({\it{b\/}}, {\it{m\/}}, {\tt{0}})\index{untrans}, {\rm{make-nreduction}}\,({\it{a\/}}, {\it{b\/}}, {\it{list\/}}, {\it{m\/}})\index{make-nreduction})\index{nreduction}\-
\end{tabbing}
\begin{verbatim};Standard convergent reduction corresponding to MAKE-REDUCTION.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{nmake-reduction} \\  
\=\+{\rm{nmake-reduction}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}}, {\it{list1\/}}, {\it{list2\/}})\index{nmake-reduction} \\ 
$=$$\;\;\;\;${\rm{end-cons}}\,(\=\+{\rm{untrans}}\,({\rm{translate}}\,({\it{y\/}}, {\bf{nil}})\index{translate}, {\rm{find-m}}\,({\rm{translate}}\,({\it{x\/}}, {\bf{nil}})\index{translate}, {\tt{0}})\index{find-m}, {\tt{0}})\index{untrans}, \\ 
{\rm{make-nreduction}}\,(\=\+{\rm{translate}}\,({\it{y\/}}, {\bf{nil}})\index{translate}, \\ 
{\rm{make-w}}\,(\=\+{\rm{translate}}\,({\it{x\/}}, {\bf{nil}})\index{translate}, \\ 
{\rm{translate}}\,({\it{z\/}}, {\bf{nil}})\index{translate}, \\ 
{\rm{translate}}\,({\it{y\/}}, {\bf{nil}})\index{translate}, \\ 
{\rm{trans-list}}\,({\it{list2\/}})\index{trans-list}, \\ 
{\rm{trans-list}}\,({\it{list1\/}})\index{trans-list})\-\index{make-w}, \\ 
{\rm{make-reduction}}\,(\=\+{\rm{translate}}\,({\it{x\/}}, {\bf{nil}})\index{translate}, \\ 
{\rm{translate}}\,({\it{y\/}}, {\bf{nil}})\index{translate}, \\ 
{\rm{translate}}\,({\it{z\/}}, {\bf{nil}})\index{translate}, \\ 
{\rm{trans-list}}\,({\it{list1\/}})\index{trans-list}, \\ 
{\rm{trans-list}}\,({\it{list2\/}})\index{trans-list})\-\index{make-reduction}, \\ 
{\rm{find-m}}\,({\rm{translate}}\,({\it{x\/}}, {\bf{nil}})\index{translate}, {\tt{0}})\index{find-m})\-\index{make-nreduction})\-\index{end-cons}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  trans-untrans-nil \\ \index{trans-untrans-nil}
\=\+({\rm{ntermp}}\,({\it{x\/}})\index{ntermp} $\wedge$ ({\rm{find-m}}\,({\rm{translate}}\,({\it{x\/}}, {\bf{nil}})\index{translate}, {\tt{0}})\index{find-m} $\leq$ {\it{m\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{alpha-equal}}\,({\it{x\/}}, {\rm{untrans}}\,({\rm{translate}}\,({\it{x\/}}, {\bf{nil}})\index{translate}, {\it{m\/}}, {\tt{0}})\index{untrans}, {\bf{nil}}, {\bf{nil}})\index{alpha-equal}\-
\end{tabbing}
\begin{verbatim};Church-Rosser theorem for standard representation.  FINALLY-CHURCH-ROSSER
;gives the complete form.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  standard-church-rosser \\ \index{standard-church-rosser}
\=\+({\rm{nreduction}}\,({\it{x\/}}, {\it{y\/}}, {\it{list1\/}})\index{nreduction} $\wedge$ {\rm{nreduction}}\,({\it{x\/}}, {\it{z\/}}, {\it{list2\/}})\index{nreduction} $\wedge$ {\rm{ntermp}}\,({\it{x\/}})\index{ntermp}) \\ 
$\rightarrow$$\;\;\;\;${\rm{nreduction}}\,(\=\+{\it{y\/}}, \\ 
{\rm{make-n-w}}\,({\it{x\/}}, {\it{z\/}}, {\it{y\/}}, {\it{list2\/}}, {\it{list1\/}})\index{make-n-w}, \\ 
{\rm{nmake-reduction}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}}, {\it{list1\/}}, {\it{list2\/}})\index{nmake-reduction})\-\index{nreduction}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  both-make-n-w-are-same \\ \index{both-make-n-w-are-same}
\=\+({\rm{ntermp}}\,({\it{x\/}})\index{ntermp} $\wedge$ {\rm{nreduction}}\,({\it{x\/}}, {\it{y\/}}, {\it{list1\/}})\index{nreduction} $\wedge$ {\rm{nreduction}}\,({\it{x\/}}, {\it{z\/}}, {\it{list2\/}})\index{nreduction}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{make-n-w}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}}, {\it{list1\/}}, {\it{list2\/}})\index{make-n-w} $=$ {\rm{make-n-w}}\,({\it{x\/}}, {\it{z\/}}, {\it{y\/}}, {\it{list2\/}}, {\it{list1\/}})\index{make-n-w})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  finally-church-rosser \\ \index{finally-church-rosser}
\=\+({\rm{ntermp}}\,({\it{x\/}})\index{ntermp} $\wedge$ {\rm{nreduction}}\,({\it{x\/}}, {\it{y\/}}, {\it{list1\/}})\index{nreduction} $\wedge$ {\rm{nreduction}}\,({\it{x\/}}, {\it{z\/}}, {\it{list2\/}})\index{nreduction}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{nreduction}}\,(\=\+{\it{y\/}}, \\ 
{\rm{make-n-w}}\,({\it{x\/}}, {\it{z\/}}, {\it{y\/}}, {\it{list2\/}}, {\it{list1\/}})\index{make-n-w}, \\ 
{\rm{nmake-reduction}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}}, {\it{list1\/}}, {\it{list2\/}})\index{nmake-reduction})\-\index{nreduction} \\ 
$\wedge$$\;\;\;\;${\rm{nreduction}}\,(\=\+{\it{z\/}}, \\ 
{\rm{make-n-w}}\,({\it{x\/}}, {\it{z\/}}, {\it{y\/}}, {\it{list2\/}}, {\it{list1\/}})\index{make-n-w}, \\ 
{\rm{nmake-reduction}}\,({\it{x\/}}, {\it{z\/}}, {\it{y\/}}, {\it{list2\/}}, {\it{list1\/}})\index{nmake-reduction})\-\index{nreduction})\-\-
\end{tabbing}
\begin{verbatim};Now, the Diamond property of walks done directly in the standard notation.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  free-for-nsubst \\ \index{free-for-nsubst}
({\rm{free-for}}\,({\it{exp\/}}, {\it{x\/}})\index{free-for} $\wedge$ {\rm{free-for}}\,({\it{y\/}}, {\it{x\/}})\index{free-for}) $\rightarrow$ {\rm{free-for}}\,({\rm{nsubst}}\,({\it{exp\/}}, {\it{y\/}}, {\it{z\/}})\index{nsubst}, {\it{x\/}})\index{free-for}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  not-free-in-nsubst \\ \index{not-free-in-nsubst}
\=\+({\rm{not-free-in}}\,({\it{x\/}}, {\it{exp\/}})\index{not-free-in} $\wedge$ {\rm{not-free-in}}\,({\it{x\/}}, {\it{y\/}})\index{not-free-in}) \\ 
$\rightarrow$$\;\;\;\;${\rm{not-free-in}}\,({\it{x\/}}, {\rm{nsubst}}\,({\it{exp\/}}, {\it{y\/}}, {\it{z\/}})\index{nsubst})\index{not-free-in}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  not-free-in-nsubst1 \\ \index{not-free-in-nsubst1}
({\rm{not-free-in}}\,({\it{x\/}}, {\it{y\/}})\index{not-free-in} $\wedge$ ({\it{x\/}} $\in\;${\bf{N}}${}$)) $\rightarrow$ {\rm{not-free-in}}\,({\it{x\/}}, {\rm{nsubst}}\,({\it{exp\/}}, {\it{y\/}}, {\it{x\/}})\index{nsubst})\index{not-free-in}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{nwalk} \\  
\=\+{\rm{nwalk}}\,({\it{w\/}}, {\it{x\/}})\index{nwalk} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{nlambdap}}\,({\it{x\/}})\index{nlambdap}$\;\;${\bf then }{\rm{nlambda}}\,({\rm{nbind}}\,({\it{x\/}})\index{nbind}, {\rm{nwalk}}\,({\it{w\/}}, {\rm{nbody}}\,({\it{x\/}})\index{nbody})\index{nwalk})\index{nlambda} \\ 
{\bf elseif }{\rm{ncombp}}\,({\it{x\/}})\index{ncombp} \\ 
{\bf then }\=\+{\bf if }{\rm{nlambdap}}\,({\rm{nleft}}\,({\it{x\/}})\index{nleft})\index{nlambdap} $\wedge$ ({\rm{command}}\,({\it{w\/}})\index{command} $=$ {\tt{'}}{\tt{reduce}}) \\ 
{\bf then }{\rm{nsubst}}\,(\=\+{\rm{nbody}}\,({\rm{nwalk}}\,({\rm{left-instrs}}\,({\it{w\/}})\index{left-instrs}, {\rm{nleft}}\,({\it{x\/}})\index{nleft})\index{nwalk})\index{nbody}, \\ 
{\rm{nwalk}}\,({\rm{right-instrs}}\,({\it{w\/}})\index{right-instrs}, {\rm{nright}}\,({\it{x\/}})\index{nright})\index{nwalk}, \\ 
{\rm{nbind}}\,({\rm{nwalk}}\,({\rm{left-instrs}}\,({\it{w\/}})\index{left-instrs}, {\rm{nleft}}\,({\it{x\/}})\index{nleft})\index{nwalk})\index{nbind})\-\index{nsubst} \\ 
{\bf else }{\rm{ncomb}}\,(\=\+{\rm{nwalk}}\,({\rm{left-instrs}}\,({\it{w\/}})\index{left-instrs}, {\rm{nleft}}\,({\it{x\/}})\index{nleft})\index{nwalk}, \\ 
{\rm{nwalk}}\,({\rm{right-instrs}}\,({\it{w\/}})\index{right-instrs}, {\rm{nright}}\,({\it{x\/}})\index{nright})\index{nwalk})\-\index{ncomb}$\;${\bf  endif}\- \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  not-free-in-walk \\ \index{not-free-in-walk}
{\rm{not-free-in}}\,({\it{x\/}}, {\it{exp\/}})\index{not-free-in} $\rightarrow$ {\rm{not-free-in}}\,({\it{x\/}}, {\rm{nwalk}}\,({\it{w\/}}, {\it{exp\/}})\index{nwalk})\index{not-free-in}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  transitivity-of-alpha-equal \\ \index{transitivity-of-alpha-equal}
({\rm{alpha-equal}}\,({\it{a\/}}, {\it{b\/}}, {\it{x\/}}, {\it{y\/}})\index{alpha-equal} $\wedge$ {\rm{alpha-equal}}\,({\it{b\/}}, {\it{c\/}}, {\it{y\/}}, {\it{z\/}})\index{alpha-equal}) $\rightarrow$ {\rm{alpha-equal}}\,({\it{a\/}}, {\it{c\/}}, {\it{x\/}}, {\it{z\/}})\index{alpha-equal}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  free-for-in-walk \\ \index{free-for-in-walk}
{\rm{free-for}}\,({\it{exp\/}}, {\it{x\/}})\index{free-for} $\rightarrow$ {\rm{free-for}}\,({\rm{nwalk}}\,({\it{w\/}}, {\it{exp\/}})\index{nwalk}, {\it{x\/}})\index{free-for}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{free-for-walk} \\  
\=\+{\rm{free-for-walk}}\,({\it{w\/}}, {\it{x\/}})\index{free-for-walk} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{nlambdap}}\,({\it{x\/}})\index{nlambdap}$\;\;${\bf then }{\rm{free-for-walk}}\,({\it{w\/}}, {\rm{nbody}}\,({\it{x\/}})\index{nbody})\index{free-for-walk} \\ 
{\bf elseif }{\rm{ncombp}}\,({\it{x\/}})\index{ncombp} \\ 
{\bf then }\=\+{\bf if }{\rm{nlambdap}}\,({\rm{nleft}}\,({\it{x\/}})\index{nleft})\index{nlambdap} $\wedge$ ({\rm{command}}\,({\it{w\/}})\index{command} $=$ {\tt{'}}{\tt{reduce}}) \\ 
{\bf then }\=\+{\rm{free-for}}\,({\rm{nbody}}\,({\rm{nleft}}\,({\it{x\/}})\index{nleft})\index{nbody}, {\rm{nright}}\,({\it{x\/}})\index{nright})\index{free-for} \\ 
$\wedge$$\;\;\;\;${\rm{free-for-walk}}\,({\rm{left-instrs}}\,({\it{w\/}})\index{left-instrs}, {\rm{nleft}}\,({\it{x\/}})\index{nleft})\index{free-for-walk} \\ 
$\wedge$$\;\;\;\;${\rm{free-for-walk}}\,({\rm{right-instrs}}\,({\it{w\/}})\index{right-instrs}, {\rm{nright}}\,({\it{x\/}})\index{nright})\index{free-for-walk}\- \\ 
{\bf else }\=\+{\rm{free-for-walk}}\,({\rm{left-instrs}}\,({\it{w\/}})\index{left-instrs}, {\rm{nleft}}\,({\it{x\/}})\index{nleft})\index{free-for-walk} \\ 
$\wedge$$\;\;\;\;${\rm{free-for-walk}}\,({\rm{right-instrs}}\,({\it{w\/}})\index{right-instrs}, {\rm{nright}}\,({\it{x\/}})\index{nright})\index{free-for-walk}\-$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  nlistp-free-for-walk \\ \index{nlistp-free-for-walk}
({\it{w\/}} $\simeq\;${{\bf{nil}}}${}$) $\rightarrow$ {\rm{free-for-walk}}\,({\it{w\/}}, {\it{x\/}})\index{free-for-walk}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{free-for-trans-ind} \\  
\=\+{\rm{free-for-trans-ind}}\,({\it{w\/}}, {\it{x\/}}, {\it{bounds\/}})\index{free-for-trans-ind} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{nlambdap}}\,({\it{x\/}})\index{nlambdap} \\ 
{\bf then }{\rm{free-for-trans-ind}}\,({\it{w\/}}, {\rm{nbody}}\,({\it{x\/}})\index{nbody}, {\rm{cons}}\,({\rm{nbind}}\,({\it{x\/}})\index{nbind}, {\it{bounds\/}}))\index{free-for-trans-ind} \\ 
{\bf elseif }{\rm{ncombp}}\,({\it{x\/}})\index{ncombp} \\ 
{\bf then }\=\+{\rm{free-for-trans-ind}}\,({\rm{left-instrs}}\,({\it{w\/}})\index{left-instrs}, {\rm{nleft}}\,({\it{x\/}})\index{nleft}, {\it{bounds\/}})\index{free-for-trans-ind} \\ 
$\wedge$$\;\;\;\;${\rm{free-for-trans-ind}}\,({\rm{right-instrs}}\,({\it{w\/}})\index{right-instrs}, {\rm{nright}}\,({\it{x\/}})\index{nright}, {\it{bounds\/}})\index{free-for-trans-ind}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  nbody-untrans \\ \index{nbody-untrans}
\=\+({\rm{ntermp}}\,({\it{x\/}})\index{ntermp} $\wedge$ {\rm{lambdap}}\,({\rm{translate}}\,({\it{x\/}}, {\it{bounds\/}})\index{translate})\index{lambdap}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{nbody}}\,({\rm{untrans}}\,({\rm{translate}}\,({\it{x\/}}, {\it{bounds\/}})\index{translate}, {\it{m\/}}, {\it{n\/}})\index{untrans})\index{nbody} \\ 
$=$$\;\;\;\;${\rm{untrans}}\,({\rm{translate}}\,({\rm{nbody}}\,({\it{x\/}})\index{nbody}, {\rm{cons}}\,({\rm{nbind}}\,({\it{x\/}})\index{nbind}, {\it{bounds\/}}))\index{translate}, {\it{m\/}}, $1\;+$ {\it{n\/}})\index{untrans})\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  free-for-walk-untrans-trans \\ \index{free-for-walk-untrans-trans}
\=\+({\rm{ntermp}}\,({\it{x\/}})\index{ntermp} $\wedge$ ({\rm{find-m}}\,({\rm{translate}}\,({\it{x\/}}, {\it{bounds\/}})\index{translate}, {\rm{length}}\,({\it{bounds\/}})\index{length})\index{find-m} $\leq$ {\it{m\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{free-for-walk}}\,({\it{w\/}}, {\rm{untrans}}\,({\rm{translate}}\,({\it{x\/}}, {\it{bounds\/}})\index{translate}, {\it{m\/}}, {\rm{length}}\,({\it{bounds\/}})\index{length})\index{untrans})\index{free-for-walk}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  free-for-in-walk1 \\ \index{free-for-in-walk1}
{\rm{free-for}}\,({\it{x\/}}, {\it{y\/}})\index{free-for} $\rightarrow$ {\rm{free-for}}\,({\rm{nwalk}}\,({\it{w1\/}}, {\it{x\/}})\index{nwalk}, {\rm{nwalk}}\,({\it{w2\/}}, {\it{y\/}})\index{nwalk})\index{free-for}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  alpha-equal-nsubst \\ \index{alpha-equal-nsubst}
\=\+(\=\+{\rm{ntermp}}\,({\it{x\/}})\index{ntermp} \\ 
$\wedge$$\;\;\;\;${\rm{ntermp}}\,({\it{y\/}})\index{ntermp} \\ 
$\wedge$$\;\;\;\;${\rm{ntermp}}\,({\it{x1\/}})\index{ntermp} \\ 
$\wedge$$\;\;\;\;${\rm{ntermp}}\,({\it{y1\/}})\index{ntermp} \\ 
$\wedge$$\;\;\;\;${\rm{nlambdap}}\,({\it{x\/}})\index{nlambdap} \\ 
$\wedge$$\;\;\;\;${\rm{nlambdap}}\,({\it{x1\/}})\index{nlambdap} \\ 
$\wedge$$\;\;\;\;${\rm{free-for}}\,({\rm{nbody}}\,({\it{x\/}})\index{nbody}, {\it{y\/}})\index{free-for} \\ 
$\wedge$$\;\;\;\;${\rm{free-for}}\,({\rm{nbody}}\,({\it{x1\/}})\index{nbody}, {\it{y1\/}})\index{free-for} \\ 
$\wedge$$\;\;\;\;${\rm{alpha-equal}}\,({\it{x\/}}, {\it{x1\/}}, {\it{bnd\/}}, {\it{bnd1\/}})\index{alpha-equal} \\ 
$\wedge$$\;\;\;\;${\rm{alpha-equal}}\,({\it{y\/}}, {\it{y1\/}}, {\it{bnd\/}}, {\it{bnd1\/}})\index{alpha-equal})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{alpha-equal}}\,(\=\+{\rm{nsubst}}\,({\rm{nbody}}\,({\it{x\/}})\index{nbody}, {\it{y\/}}, {\rm{nbind}}\,({\it{x\/}})\index{nbind})\index{nsubst}, \\ 
{\rm{nsubst}}\,({\rm{nbody}}\,({\it{x1\/}})\index{nbody}, {\it{y1\/}}, {\rm{nbind}}\,({\it{x1\/}})\index{nbind})\index{nsubst}, \\ 
{\it{bnd\/}}, \\ 
{\it{bnd1\/}})\-\index{alpha-equal}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  nwalk-ntermp \\ \index{nwalk-ntermp}
{\rm{ntermp}}\,({\it{a\/}})\index{ntermp} $\rightarrow$ {\rm{ntermp}}\,({\rm{nwalk}}\,({\it{w\/}}, {\it{a\/}})\index{nwalk})\index{ntermp}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  nlambdap-nwalk \\ \index{nlambdap-nwalk}
{\rm{nlambdap}}\,({\it{a\/}})\index{nlambdap} $\rightarrow$ {\rm{nlambdap}}\,({\rm{nwalk}}\,({\it{w\/}}, {\it{a\/}})\index{nwalk})\index{nlambdap}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  free-for-nwalk2 \\ \index{free-for-nwalk2}
\=\+({\rm{nlambdap}}\,({\it{x\/}})\index{nlambdap} $\wedge$ {\rm{free-for}}\,({\rm{nbody}}\,({\it{x\/}})\index{nbody}, {\it{y\/}})\index{free-for}) \\ 
$\rightarrow$$\;\;\;\;${\rm{free-for}}\,({\rm{nbody}}\,({\rm{nwalk}}\,({\it{w1\/}}, {\it{x\/}})\index{nwalk})\index{nbody}, {\rm{nwalk}}\,({\it{w2\/}}, {\it{y\/}})\index{nwalk})\index{free-for}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  nwalk-alpha \\ \index{nwalk-alpha}
\=\+(\=\+{\rm{ntermp}}\,({\it{a\/}})\index{ntermp} \\ 
$\wedge$$\;\;\;\;${\rm{ntermp}}\,({\it{b\/}})\index{ntermp} \\ 
$\wedge$$\;\;\;\;${\rm{alpha-equal}}\,({\it{a\/}}, {\it{b\/}}, {\it{x\/}}, {\it{y\/}})\index{alpha-equal} \\ 
$\wedge$$\;\;\;\;${\rm{free-for-walk}}\,({\it{w\/}}, {\it{a\/}})\index{free-for-walk} \\ 
$\wedge$$\;\;\;\;${\rm{free-for-walk}}\,({\it{w\/}}, {\it{b\/}})\index{free-for-walk})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{alpha-equal}}\,({\rm{nwalk}}\,({\it{w\/}}, {\it{a\/}})\index{nwalk}, {\rm{nwalk}}\,({\it{w\/}}, {\it{b\/}})\index{nwalk}, {\it{x\/}}, {\it{y\/}})\index{alpha-equal}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  nsubst-not-free-in \\ \index{nsubst-not-free-in}
{\rm{not-free-in}}\,({\it{x\/}}, {\it{a\/}})\index{not-free-in} $\rightarrow$ ({\rm{nsubst}}\,({\it{a\/}}, {\it{b\/}}, {\it{x\/}})\index{nsubst} $=$ {\it{a\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  nsubst-nsubst \\ \index{nsubst-nsubst}
\=\+({\rm{free-for}}\,({\it{a\/}}, {\it{b\/}})\index{free-for} $\wedge$ {\rm{not-free-in}}\,({\it{x\/}}, {\it{c\/}})\index{not-free-in} $\wedge$ ({\it{x\/}} $\not=$ {\it{y\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{nsubst}}\,({\rm{nsubst}}\,({\it{a\/}}, {\it{b\/}}, {\it{x\/}})\index{nsubst}, {\it{c\/}}, {\it{y\/}})\index{nsubst} $=$ {\rm{nsubst}}\,({\rm{nsubst}}\,({\it{a\/}}, {\it{c\/}}, {\it{y\/}})\index{nsubst}, {\rm{nsubst}}\,({\it{b\/}}, {\it{c\/}}, {\it{y\/}})\index{nsubst}, {\it{x\/}})\index{nsubst})\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{sub-nwalk} \\  
\=\+{\rm{sub-nwalk}}\,({\it{w\/}}, {\it{m\/}}, {\it{u\/}}, {\it{n\/}})\index{sub-nwalk} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{nlambdap}}\,({\it{m\/}})\index{nlambdap} \\ 
{\bf then }\=\+{\bf if }{\rm{nbind}}\,({\it{m\/}})\index{nbind} $=$ {\it{n\/}}$\;\;${\bf then }{\it{w\/}} \\ 
{\bf else }{\rm{sub-nwalk}}\,({\it{w\/}}, {\rm{nbody}}\,({\it{m\/}})\index{nbody}, {\it{u\/}}, {\it{n\/}})\index{sub-nwalk}$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{ncombp}}\,({\it{m\/}})\index{ncombp} \\ 
{\bf then }\=\+{\bf if }({\rm{command}}\,({\it{w\/}})\index{command} $=$ {\tt{'}}{\tt{reduce}}) $\wedge$ {\rm{nlambdap}}\,({\rm{nleft}}\,({\it{m\/}})\index{nleft})\index{nlambdap} \\ 
{\bf then }{\rm{list}}\,(\=\+{\rm{sub-nwalk}}\,({\rm{left-instrs}}\,({\it{w\/}})\index{left-instrs}, {\rm{nleft}}\,({\it{m\/}})\index{nleft}, {\it{u\/}}, {\it{n\/}})\index{sub-nwalk}, \\ 
{\rm{sub-nwalk}}\,({\rm{right-instrs}}\,({\it{w\/}})\index{right-instrs}, {\rm{nright}}\,({\it{m\/}})\index{nright}, {\it{u\/}}, {\it{n\/}})\index{sub-nwalk}, \\ 
{\tt{'}}{\tt{reduce}})\- \\ 
{\bf else }{\rm{list}}\,(\=\+{\rm{sub-nwalk}}\,({\rm{left-instrs}}\,({\it{w\/}})\index{left-instrs}, {\rm{nleft}}\,({\it{m\/}})\index{nleft}, {\it{u\/}}, {\it{n\/}})\index{sub-nwalk}, \\ 
{\rm{sub-nwalk}}\,({\rm{right-instrs}}\,({\it{w\/}})\index{right-instrs}, {\rm{nright}}\,({\it{m\/}})\index{nright}, {\it{u\/}}, {\it{n\/}})\index{sub-nwalk})\-$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{m\/}} $\in\;${\bf{N}}${}$ \\ 
{\bf then }\=\+{\bf if }{\it{m\/}} $=$ {\it{n\/}}$\;\;${\bf then }{\it{u\/}} \\ 
{\bf else }{\it{w\/}}$\;${\bf  endif}\- \\ 
{\bf else }{\it{w\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  nlambdap-nsubst \\ \index{nlambdap-nsubst}
{\rm{nlambdap}}\,({\it{x\/}})\index{nlambdap} $\rightarrow$ {\rm{nlambdap}}\,({\rm{nsubst}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{nsubst})\index{nlambdap}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  nsubst-twice \\ \index{nsubst-twice}
{\rm{free-for}}\,({\it{a\/}}, {\it{b\/}})\index{free-for} $\rightarrow$ ({\rm{nsubst}}\,({\rm{nsubst}}\,({\it{a\/}}, {\it{b\/}}, {\it{x\/}})\index{nsubst}, {\it{c\/}}, {\it{x\/}})\index{nsubst} $=$ {\rm{nsubst}}\,({\it{a\/}}, {\rm{nsubst}}\,({\it{b\/}}, {\it{c\/}}, {\it{x\/}})\index{nsubst}, {\it{x\/}})\index{nsubst})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  nwalk-nsubst \\ \index{nwalk-nsubst}
\=\+({\rm{free-for}}\,({\it{m\/}}, {\it{x\/}})\index{free-for} $\wedge$ {\rm{free-for-walk}}\,({\it{w\/}}, {\it{m\/}})\index{free-for-walk}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{nwalk}}\,({\rm{sub-nwalk}}\,({\it{w\/}}, {\it{m\/}}, {\it{u\/}}, {\it{n\/}})\index{sub-nwalk}, {\rm{nsubst}}\,({\it{m\/}}, {\it{x\/}}, {\it{n\/}})\index{nsubst})\index{nwalk} \\ 
$=$$\;\;\;\;${\rm{nsubst}}\,({\rm{nwalk}}\,({\it{w\/}}, {\it{m\/}})\index{nwalk}, {\rm{nwalk}}\,({\it{u\/}}, {\it{x\/}})\index{nwalk}, {\it{n\/}})\index{nsubst})\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{free-forx} \\  
\=\+{\rm{free-forx}}\,({\it{a\/}}, {\it{b\/}}, {\it{x\/}})\index{free-forx} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{not-free-in}}\,({\it{x\/}}, {\it{a\/}})\index{not-free-in}$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{nlambdap}}\,({\it{a\/}})\index{nlambdap} \\ 
{\bf then }\=\+{\bf if }{\rm{nbind}}\,({\it{a\/}})\index{nbind} $=$ {\it{x\/}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{not-free-in}}\,({\rm{nbind}}\,({\it{a\/}})\index{nbind}, {\it{b\/}})\index{not-free-in} $\wedge$ {\rm{free-forx}}\,({\rm{nbody}}\,({\it{a\/}})\index{nbody}, {\it{b\/}}, {\it{x\/}})\index{free-forx}$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{ncombp}}\,({\it{a\/}})\index{ncombp} \\ 
{\bf then }{\rm{free-forx}}\,({\rm{nleft}}\,({\it{a\/}})\index{nleft}, {\it{b\/}}, {\it{x\/}})\index{free-forx} $\wedge$ {\rm{free-forx}}\,({\rm{nright}}\,({\it{a\/}})\index{nright}, {\it{b\/}}, {\it{x\/}})\index{free-forx} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  nsubst-nsubstx \\ \index{nsubst-nsubstx}
\=\+({\rm{free-forx}}\,({\it{a\/}}, {\it{b\/}}, {\it{x\/}})\index{free-forx} $\wedge$ {\rm{not-free-in}}\,({\it{x\/}}, {\it{c\/}})\index{not-free-in} $\wedge$ ({\it{x\/}} $\not=$ {\it{y\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{nsubst}}\,({\rm{nsubst}}\,({\it{a\/}}, {\it{b\/}}, {\it{x\/}})\index{nsubst}, {\it{c\/}}, {\it{y\/}})\index{nsubst} $=$ {\rm{nsubst}}\,({\rm{nsubst}}\,({\it{a\/}}, {\it{c\/}}, {\it{y\/}})\index{nsubst}, {\rm{nsubst}}\,({\it{b\/}}, {\it{c\/}}, {\it{y\/}})\index{nsubst}, {\it{x\/}})\index{nsubst})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  nsubst-twicex \\ \index{nsubst-twicex}
\=\+{\rm{free-forx}}\,({\it{a\/}}, {\it{b\/}}, {\it{x\/}})\index{free-forx} \\ 
$\rightarrow$$\;\;\;\;$({\rm{nsubst}}\,({\rm{nsubst}}\,({\it{a\/}}, {\it{b\/}}, {\it{x\/}})\index{nsubst}, {\it{c\/}}, {\it{x\/}})\index{nsubst} $=$ {\rm{nsubst}}\,({\it{a\/}}, {\rm{nsubst}}\,({\it{b\/}}, {\it{c\/}}, {\it{x\/}})\index{nsubst}, {\it{x\/}})\index{nsubst})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  free-for-free-forx \\ \index{free-for-free-forx}
{\rm{free-for}}\,({\it{a\/}}, {\it{b\/}})\index{free-for} $\rightarrow$ {\rm{free-forx}}\,({\it{a\/}}, {\it{b\/}}, {\it{x\/}})\index{free-forx}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{free-forx-walk} \\  
\=\+{\rm{free-forx-walk}}\,({\it{w\/}}, {\it{x\/}})\index{free-forx-walk} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{nlambdap}}\,({\it{x\/}})\index{nlambdap}$\;\;${\bf then }{\rm{free-forx-walk}}\,({\it{w\/}}, {\rm{nbody}}\,({\it{x\/}})\index{nbody})\index{free-forx-walk} \\ 
{\bf elseif }{\rm{ncombp}}\,({\it{x\/}})\index{ncombp} \\ 
{\bf then }\=\+{\bf if }{\rm{nlambdap}}\,({\rm{nleft}}\,({\it{x\/}})\index{nleft})\index{nlambdap} $\wedge$ ({\rm{command}}\,({\it{w\/}})\index{command} $=$ {\tt{'}}{\tt{reduce}}) \\ 
{\bf then }\=\+{\rm{free-forx}}\,(\=\+{\rm{nbody}}\,({\rm{nwalk}}\,({\rm{left-instrs}}\,({\it{w\/}})\index{left-instrs}, {\rm{nleft}}\,({\it{x\/}})\index{nleft})\index{nwalk})\index{nbody}, \\ 
{\rm{nwalk}}\,({\rm{right-instrs}}\,({\it{w\/}})\index{right-instrs}, {\rm{nright}}\,({\it{x\/}})\index{nright})\index{nwalk}, \\ 
{\rm{nbind}}\,({\rm{nwalk}}\,({\rm{left-instrs}}\,({\it{w\/}})\index{left-instrs}, {\rm{nleft}}\,({\it{x\/}})\index{nleft})\index{nwalk})\index{nbind})\-\index{free-forx} \\ 
$\wedge$$\;\;\;\;${\rm{free-forx-walk}}\,({\rm{left-instrs}}\,({\it{w\/}})\index{left-instrs}, {\rm{nleft}}\,({\it{x\/}})\index{nleft})\index{free-forx-walk} \\ 
$\wedge$$\;\;\;\;${\rm{free-forx-walk}}\,({\rm{right-instrs}}\,({\it{w\/}})\index{right-instrs}, {\rm{nright}}\,({\it{x\/}})\index{nright})\index{free-forx-walk}\- \\ 
{\bf else }\=\+{\rm{free-forx-walk}}\,({\rm{left-instrs}}\,({\it{w\/}})\index{left-instrs}, {\rm{nleft}}\,({\it{x\/}})\index{nleft})\index{free-forx-walk} \\ 
$\wedge$$\;\;\;\;${\rm{free-forx-walk}}\,({\rm{right-instrs}}\,({\it{w\/}})\index{right-instrs}, {\rm{nright}}\,({\it{x\/}})\index{nright})\index{free-forx-walk}\-$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  free-for-free-forx-walk \\ \index{free-for-free-forx-walk}
{\rm{free-for-walk}}\,({\it{w\/}}, {\it{x\/}})\index{free-for-walk} $\rightarrow$ {\rm{free-forx-walk}}\,({\it{w\/}}, {\it{x\/}})\index{free-forx-walk}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  free-forx-nsubst \\ \index{free-forx-nsubst}
\=\+({\rm{free-forx}}\,({\it{x\/}}, {\it{m\/}}, {\it{n\/}})\index{free-forx} $\wedge$ {\rm{free-forx}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{free-forx} $\wedge$ {\rm{not-free-in}}\,({\it{z\/}}, {\it{m\/}})\index{not-free-in}) \\ 
$\rightarrow$$\;\;\;\;${\rm{free-forx}}\,({\rm{nsubst}}\,({\it{x\/}}, {\it{m\/}}, {\it{n\/}})\index{nsubst}, {\it{y\/}}, {\it{z\/}})\index{free-forx}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  free-forx-nsubst2 \\ \index{free-forx-nsubst2}
({\rm{free-for}}\,({\it{x\/}}, {\it{m\/}})\index{free-for} $\wedge$ {\rm{free-forx}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{free-forx}) $\rightarrow$ {\rm{free-forx}}\,({\it{x\/}}, {\rm{nsubst}}\,({\it{y\/}}, {\it{m\/}}, {\it{n\/}})\index{nsubst}, {\it{z\/}})\index{free-forx}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  nwalk-nlambda1 \\ \index{nwalk-nlambda1}
{\rm{nlambdap}}\,({\it{x\/}})\index{nlambdap} $\rightarrow$ ({\rm{nbody}}\,({\rm{nwalk}}\,({\it{u\/}}, {\it{x\/}})\index{nwalk})\index{nbody} $=$ {\rm{nwalk}}\,({\it{u\/}}, {\rm{nbody}}\,({\it{x\/}})\index{nbody})\index{nwalk})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  nwalk-nlambda2 \\ \index{nwalk-nlambda2}
{\rm{nlambdap}}\,({\it{x\/}})\index{nlambdap} $\rightarrow$ ({\rm{nbind}}\,({\rm{nwalk}}\,({\it{u\/}}, {\it{x\/}})\index{nwalk})\index{nbind} $=$ {\rm{nbind}}\,({\it{x\/}})\index{nbind})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  nwalk-nsubstx \\ \index{nwalk-nsubstx}
\=\+({\rm{free-for}}\,({\it{m\/}}, {\it{x\/}})\index{free-for} $\wedge$ {\rm{free-forx-walk}}\,({\it{w\/}}, {\it{m\/}})\index{free-forx-walk}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{nwalk}}\,({\rm{sub-nwalk}}\,({\it{w\/}}, {\it{m\/}}, {\it{u\/}}, {\it{n\/}})\index{sub-nwalk}, {\rm{nsubst}}\,({\it{m\/}}, {\it{x\/}}, {\it{n\/}})\index{nsubst})\index{nwalk} \\ 
$=$$\;\;\;\;${\rm{nsubst}}\,({\rm{nwalk}}\,({\it{w\/}}, {\it{m\/}})\index{nwalk}, {\rm{nwalk}}\,({\it{u\/}}, {\it{x\/}})\index{nwalk}, {\it{n\/}})\index{nsubst})\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{make-nwalk} \\  
\=\+{\rm{make-nwalk}}\,({\it{m\/}}, {\it{u\/}}, {\it{v\/}})\index{make-nwalk} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{nlambdap}}\,({\it{m\/}})\index{nlambdap}$\;\;${\bf then }{\rm{make-nwalk}}\,({\rm{nbody}}\,({\it{m\/}})\index{nbody}, {\it{u\/}}, {\it{v\/}})\index{make-nwalk} \\ 
{\bf elseif }{\rm{ncombp}}\,({\it{m\/}})\index{ncombp} \\ 
{\bf then }\=\+{\bf if }({\rm{command}}\,({\it{u\/}})\index{command} $=$ {\tt{'}}{\tt{reduce}}) $\wedge$ {\rm{nlambdap}}\,({\rm{nleft}}\,({\it{m\/}})\index{nleft})\index{nlambdap} \\ 
{\bf then }{\rm{sub-nwalk}}\,(\=\+{\rm{make-nwalk}}\,({\rm{nleft}}\,({\it{m\/}})\index{nleft}, {\rm{left-instrs}}\,({\it{u\/}})\index{left-instrs}, {\rm{left-instrs}}\,({\it{v\/}})\index{left-instrs})\index{make-nwalk}, \\ 
{\rm{nbody}}\,({\rm{nwalk}}\,({\rm{left-instrs}}\,({\it{u\/}})\index{left-instrs}, {\rm{nleft}}\,({\it{m\/}})\index{nleft})\index{nwalk})\index{nbody}, \\ 
{\rm{make-nwalk}}\,(\=\+{\rm{nright}}\,({\it{m\/}})\index{nright}, \\ 
{\rm{right-instrs}}\,({\it{u\/}})\index{right-instrs}, \\ 
{\rm{right-instrs}}\,({\it{v\/}})\index{right-instrs})\-\index{make-nwalk}, \\ 
{\rm{nbind}}\,({\rm{nwalk}}\,({\rm{left-instrs}}\,({\it{u\/}})\index{left-instrs}, {\rm{nleft}}\,({\it{m\/}})\index{nleft})\index{nwalk})\index{nbind})\-\index{sub-nwalk} \\ 
{\bf elseif }({\rm{command}}\,({\it{v\/}})\index{command} $=$ {\tt{'}}{\tt{reduce}}) $\wedge$ {\rm{nlambdap}}\,({\rm{nleft}}\,({\it{m\/}})\index{nleft})\index{nlambdap} \\ 
{\bf then }{\rm{list}}\,(\=\+{\rm{make-nwalk}}\,({\rm{nleft}}\,({\it{m\/}})\index{nleft}, {\rm{left-instrs}}\,({\it{u\/}})\index{left-instrs}, {\rm{left-instrs}}\,({\it{v\/}})\index{left-instrs})\index{make-nwalk}, \\ 
{\rm{make-nwalk}}\,({\rm{nright}}\,({\it{m\/}})\index{nright}, {\rm{right-instrs}}\,({\it{u\/}})\index{right-instrs}, {\rm{right-instrs}}\,({\it{v\/}})\index{right-instrs})\index{make-nwalk}, \\ 
{\tt{'}}{\tt{reduce}})\- \\ 
{\bf else }{\rm{list}}\,(\=\+{\rm{make-nwalk}}\,(\=\+{\rm{nleft}}\,({\it{m\/}})\index{nleft}, \\ 
{\rm{left-instrs}}\,({\it{u\/}})\index{left-instrs}, \\ 
{\rm{left-instrs}}\,({\it{v\/}})\index{left-instrs})\-\index{make-nwalk}, \\ 
{\rm{make-nwalk}}\,(\=\+{\rm{nright}}\,({\it{m\/}})\index{nright}, \\ 
{\rm{right-instrs}}\,({\it{u\/}})\index{right-instrs}, \\ 
{\rm{right-instrs}}\,({\it{v\/}})\index{right-instrs})\-\index{make-nwalk})\-$\;${\bf  endif}\- \\ 
{\bf else }{\it{u\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  free-for-sub-nwalk \\ \index{free-for-sub-nwalk}
\=\+({\rm{free-for}}\,({\it{m\/}}, {\it{x\/}})\index{free-for} $\wedge$ {\rm{free-forx-walk}}\,({\it{w\/}}, {\it{m\/}})\index{free-forx-walk} $\wedge$ {\rm{free-forx-walk}}\,({\it{u\/}}, {\it{x\/}})\index{free-forx-walk}) \\ 
$\rightarrow$$\;\;\;\;${\rm{free-forx-walk}}\,({\rm{sub-nwalk}}\,({\it{w\/}}, {\it{m\/}}, {\it{u\/}}, {\it{n\/}})\index{sub-nwalk}, {\rm{nsubst}}\,({\it{m\/}}, {\it{x\/}}, {\it{n\/}})\index{nsubst})\index{free-forx-walk}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  free-forx-make-nwalk \\ \index{free-forx-make-nwalk}
\=\+({\rm{free-for-walk}}\,({\it{u\/}}, {\it{m\/}})\index{free-for-walk} $\wedge$ {\rm{free-for-walk}}\,({\it{v\/}}, {\it{m\/}})\index{free-for-walk}) \\ 
$\rightarrow$$\;\;\;\;${\rm{free-forx-walk}}\,({\rm{make-nwalk}}\,({\it{m\/}}, {\it{u\/}}, {\it{v\/}})\index{make-nwalk}, {\rm{nwalk}}\,({\it{u\/}}, {\it{m\/}})\index{nwalk})\index{free-forx-walk}\-
\end{tabbing}
\begin{verbatim};The Diamond property of beta-walks.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  diamond-of-beta \\ \index{diamond-of-beta}
\=\+({\rm{free-for-walk}}\,({\it{u\/}}, {\it{m\/}})\index{free-for-walk} $\wedge$ {\rm{free-for-walk}}\,({\it{v\/}}, {\it{m\/}})\index{free-for-walk}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{nwalk}}\,({\rm{make-nwalk}}\,({\it{m\/}}, {\it{u\/}}, {\it{v\/}})\index{make-nwalk}, {\rm{nwalk}}\,({\it{u\/}}, {\it{m\/}})\index{nwalk})\index{nwalk} \\ 
$=$$\;\;\;\;${\rm{nwalk}}\,({\rm{make-nwalk}}\,({\it{m\/}}, {\it{v\/}}, {\it{u\/}})\index{make-nwalk}, {\rm{nwalk}}\,({\it{v\/}}, {\it{m\/}})\index{nwalk})\index{nwalk})\-\-
\end{tabbing}



%\end{list}
\printindex
\end{document}
