\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[]


\noindent{\sc Event}:   Start with the initial {\bf nqthm} theory.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{h} \\  
\=\+{\rm{h}}\,({\it{n\/}}, {\it{from\/}}, {\it{to\/}}, {\it{temp\/}})\index{h} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{append}}\,(\=\+{\rm{h}}\,({\it{n\/}} $-\;1$, {\it{from\/}}, {\it{temp\/}}, {\it{to\/}})\index{h}, \\ 
{\rm{cons}}\,({\rm{cons}}\,({\it{from\/}}, {\it{to\/}}), {\rm{h}}\,({\it{n\/}} $-\;1$, {\it{temp\/}}, {\it{to\/}}, {\it{from\/}})\index{h}))\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{hanoi}$\;\;$
{\rm{hanoi}}\,({\it{n\/}})\index{hanoi} $=$ {\rm{h}}\,({\it{n\/}}, {\tt{0}}, {\tt{1}}, {\tt{2}})\index{h}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{nth} \\  
\=\+{\rm{nth}}\,({\it{i\/}}, {\it{l\/}})\index{nth} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{car}}\,({\it{l\/}}) \\ 
{\bf else }{\rm{nth}}\,({\it{i\/}} $-\;1$, {\rm{cdr}}\,({\it{l\/}}))\index{nth}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{set-nth} \\  
\=\+{\rm{set-nth}}\,({\it{i\/}}, {\it{l\/}}, {\it{v\/}})\index{set-nth} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{cons}}\,({\it{v\/}}, {\rm{cdr}}\,({\it{l\/}})) \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\it{l\/}}), {\rm{set-nth}}\,({\it{i\/}} $-\;1$, {\rm{cdr}}\,({\it{l\/}}), {\it{v\/}})\index{set-nth})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{legal} \\  
\=\+{\rm{legal}}\,({\it{move\/}}, {\it{st\/}})\index{legal} \\ 
$=$$\;\;\;\;$(\=\+{\rm{listp}}\,({\it{move\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{move\/}}) $\in$ {\tt{'}}{\tt{(}}{\tt{0}}{\tt{ }}{\tt{1}}{\tt{ }}{\tt{2}}{\tt{)}}) \\ 
$\wedge$$\;\;\;\;$({\rm{cdr}}\,({\it{move\/}}) $\in$ {\tt{'}}{\tt{(}}{\tt{0}}{\tt{ }}{\tt{1}}{\tt{ }}{\tt{2}}{\tt{)}}) \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\rm{nth}}\,({\rm{car}}\,({\it{move\/}}), {\it{st\/}})\index{nth}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\rm{nth}}\,({\rm{cdr}}\,({\it{move\/}}), {\it{st\/}})\index{nth} $\simeq\;${{\bf{nil}}}${}$) \\ 
$\vee$$\;\;\;\;$({\rm{car}}\,({\rm{nth}}\,({\rm{car}}\,({\it{move\/}}), {\it{st\/}})\index{nth}) $<$ {\rm{car}}\,({\rm{nth}}\,({\rm{cdr}}\,({\it{move\/}}), {\it{st\/}})\index{nth})))\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{step} \\  
\=\+{\rm{step}}\,({\it{move\/}}, {\it{st\/}})\index{step} \\ 
$=$$\;\;\;\;${\rm{set-nth}}\,(\=\+{\rm{car}}\,({\it{move\/}}), \\ 
{\rm{set-nth}}\,(\=\+{\rm{cdr}}\,({\it{move\/}}), \\ 
{\it{st\/}}, \\ 
{\rm{cons}}\,({\rm{car}}\,({\rm{nth}}\,({\rm{car}}\,({\it{move\/}}), {\it{st\/}})\index{nth}), {\rm{nth}}\,({\rm{cdr}}\,({\it{move\/}}), {\it{st\/}})\index{nth}))\-\index{set-nth}, \\ 
{\rm{cdr}}\,({\rm{nth}}\,({\rm{car}}\,({\it{move\/}}), {\it{st\/}})\index{nth}))\-\index{set-nth}\-
\end{tabbing}


\noindent{\sc Event}:   Disable legal.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{play} \\  
\=\+{\rm{play}}\,({\it{moves\/}}, {\it{st\/}})\index{play} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{moves\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{legal}}\,({\rm{car}}\,({\it{moves\/}}), {\it{st\/}})\index{legal} \\ 
{\bf then }{\rm{play}}\,({\rm{cdr}}\,({\it{moves\/}}), {\rm{step}}\,({\rm{car}}\,({\it{moves\/}}), {\it{st\/}})\index{step})\index{play} \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\- \\ 
{\bf else }{\it{st\/}}$\;${\bf  endif}\-\-
\end{tabbing}


\noindent{\sc Event}:   Enable legal.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{tower} \\  
\=\+{\rm{tower}}\,({\it{n\/}})\index{tower} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{append}}\,({\rm{tower}}\,({\it{n\/}} $-\;1$)\index{tower}, {\rm{list}}\,({\it{n\/}}))$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{permp} \\  
\=\+{\rm{permp}}\,({\it{i\/}}, {\it{j\/}}, {\it{k\/}})\index{permp} \\ 
$=$$\;\;\;\;$(\=\+({\it{i\/}} $\in$ {\tt{'}}{\tt{(}}{\tt{0}}{\tt{ }}{\tt{1}}{\tt{ }}{\tt{2}}{\tt{)}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\in$ {\tt{'}}{\tt{(}}{\tt{0}}{\tt{ }}{\tt{1}}{\tt{ }}{\tt{2}}{\tt{)}}) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $\in$ {\tt{'}}{\tt{(}}{\tt{0}}{\tt{ }}{\tt{1}}{\tt{ }}{\tt{2}}{\tt{)}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not=$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not=$ {\it{k\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\not=$ {\it{k\/}}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{statep} \\  
{\rm{statep}}\,({\it{s\/}})\index{statep} $=$ ({\rm{listp}}\,({\it{s\/}}) $\wedge$ {\rm{listp}}\,({\rm{cdr}}\,({\it{s\/}})) $\wedge$ {\rm{listp}}\,({\rm{cddr}}\,({\it{s\/}})))
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{slessp} \\  
\=\+{\rm{slessp}}\,({\it{n\/}}, {\it{s\/}})\index{slessp} \\ 
$=$$\;\;\;\;$(\=\+\=\+{\bf if }{\rm{nth}}\,({\tt{0}}, {\it{s\/}})\index{nth} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\it{n\/}} $<$ {\rm{car}}\,({\rm{nth}}\,({\tt{0}}, {\it{s\/}})\index{nth})$\;${\bf  endif}\- \\ 
$\wedge$$\;\;\;\;$\=\+{\bf if }{\rm{nth}}\,({\tt{1}}, {\it{s\/}})\index{nth} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\it{n\/}} $<$ {\rm{car}}\,({\rm{nth}}\,({\tt{1}}, {\it{s\/}})\index{nth})$\;${\bf  endif}\- \\ 
$\wedge$$\;\;\;\;$\=\+{\bf if }{\rm{nth}}\,({\tt{2}}, {\it{s\/}})\index{nth} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\it{n\/}} $<$ {\rm{car}}\,({\rm{nth}}\,({\tt{2}}, {\it{s\/}})\index{nth})$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{verbatim}; We wish to prove:

;(equal (play (hanoi n) (list (tower n) nil nil))
;       (list nil (tower n) nil))

; i.e.

;(equal (play (h n 0 1 2) (list (tower n) nil nil))
;       (list nil (tower n) nil))

; But to do so we go for a more general fact:

; (implies
;   (and (statep s)
;        (slessp n s)
;        (permp i j k))
;   (and (play (h n i j k)
;              (set-nth i s
;                       (append (tower n) (nth i s))))
;        (equal (play (h n i j k)
;                     (set-nth i s
;                              (append (tower n) (nth i s))))
;               (set-nth j s
;                        (append (tower n) (nth j s))))))

; The proof should go roughly by induction along the definition of
; h, but with s instantiated appropriately.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{main-ind} \\  
\=\+{\rm{main-ind}}\,({\it{i\/}}, {\it{j\/}}, {\it{k\/}}, {\it{n\/}}, {\it{s\/}})\index{main-ind} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }\=\+{\rm{main-ind}}\,({\it{i\/}}, {\it{k\/}}, {\it{j\/}}, {\it{n\/}} $-\;1$, {\rm{set-nth}}\,({\it{i\/}}, {\it{s\/}}, {\rm{cons}}\,({\it{n\/}}, {\rm{nth}}\,({\it{i\/}}, {\it{s\/}})\index{nth}))\index{set-nth})\index{main-ind} \\ 
$\wedge$$\;\;\;\;${\rm{main-ind}}\,({\it{k\/}}, {\it{j\/}}, {\it{i\/}}, {\it{n\/}} $-\;1$, {\rm{set-nth}}\,({\it{j\/}}, {\it{s\/}}, {\rm{cons}}\,({\it{n\/}}, {\rm{nth}}\,({\it{j\/}}, {\it{s\/}})\index{nth}))\index{set-nth})\index{main-ind}\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; The following is used to conclude the proof of the base case.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  set-nth-nth \\ \index{set-nth-nth}
(({\it{i\/}} $\in$ {\tt{'}}{\tt{(}}{\tt{0}}{\tt{ }}{\tt{1}}{\tt{ }}{\tt{2}}{\tt{)}}) $\wedge$ {\rm{statep}}\,({\it{s\/}})\index{statep}) $\rightarrow$ ({\rm{set-nth}}\,({\it{i\/}}, {\it{s\/}}, {\rm{nth}}\,({\it{i\/}}, {\it{s\/}})\index{nth})\index{set-nth} $=$ {\it{s\/}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{hyps} \\  
{\rm{hyps}}\,({\it{i\/}}, {\it{j\/}}, {\it{k\/}}, {\it{n\/}}, {\it{s\/}})\index{hyps} $=$ ({\rm{statep}}\,({\it{s\/}})\index{statep} $\wedge$ {\rm{slessp}}\,({\it{n\/}}, {\it{s\/}})\index{slessp} $\wedge$ {\rm{permp}}\,({\it{i\/}}, {\it{j\/}}, {\it{k\/}})\index{permp})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{conc} \\  
\=\+{\rm{conc}}\,({\it{i\/}}, {\it{j\/}}, {\it{k\/}}, {\it{n\/}}, {\it{s\/}})\index{conc} \\ 
$=$$\;\;\;\;$(\=\+{\rm{play}}\,({\rm{h}}\,({\it{n\/}}, {\it{i\/}}, {\it{j\/}}, {\it{k\/}})\index{h}, {\rm{set-nth}}\,({\it{i\/}}, {\it{s\/}}, {\rm{append}}\,({\rm{tower}}\,({\it{n\/}})\index{tower}, {\rm{nth}}\,({\it{i\/}}, {\it{s\/}})\index{nth}))\index{set-nth})\index{play} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{play}}\,({\rm{h}}\,({\it{n\/}}, {\it{i\/}}, {\it{j\/}}, {\it{k\/}})\index{h}, {\rm{set-nth}}\,({\it{i\/}}, {\it{s\/}}, {\rm{append}}\,({\rm{tower}}\,({\it{n\/}})\index{tower}, {\rm{nth}}\,({\it{i\/}}, {\it{s\/}})\index{nth}))\index{set-nth})\index{play} \\ 
$=$$\;\;\;\;${\rm{set-nth}}\,({\it{j\/}}, {\it{s\/}}, {\rm{append}}\,({\rm{tower}}\,({\it{n\/}})\index{tower}, {\rm{nth}}\,({\it{j\/}}, {\it{s\/}})\index{nth}))\index{set-nth})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{main-thm} \\  
{\rm{main-thm}}\,({\it{i\/}}, {\it{j\/}}, {\it{k\/}}, {\it{n\/}}, {\it{s\/}})\index{main-thm} $=$ ({\rm{hyps}}\,({\it{i\/}}, {\it{j\/}}, {\it{k\/}}, {\it{n\/}}, {\it{s\/}})\index{hyps} $\rightarrow$ {\rm{conc}}\,({\it{i\/}}, {\it{j\/}}, {\it{k\/}}, {\it{n\/}}, {\it{s\/}})\index{conc})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  base-case \\ \index{base-case}
({\it{n\/}} $\simeq {\tt{0}}$) $\rightarrow$ {\rm{main-thm}}\,({\it{i\/}}, {\it{j\/}}, {\it{k\/}}, {\it{n\/}}, {\it{s\/}})\index{main-thm}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  nth-of-nlistp \\ \index{nth-of-nlistp}
($\neg$ {\rm{listp}}\,({\it{x\/}})) $\rightarrow$ ({\rm{nth}}\,({\it{n\/}}, {\it{x\/}})\index{nth} $=$ {\tt{0}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  play-append \\ \index{play-append}
{\rm{play}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}), {\it{s\/}})\index{play} $=$ {\rm{play}}\,({\it{y\/}}, {\rm{play}}\,({\it{x\/}}, {\it{s\/}})\index{play})\index{play}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  statep-set-nth \\ \index{statep-set-nth}
{\rm{statep}}\,({\it{s\/}})\index{statep} $\rightarrow$ {\rm{statep}}\,({\rm{set-nth}}\,({\it{i\/}}, {\it{s\/}}, {\rm{cons}}\,({\it{n\/}}, {\rm{nth}}\,({\it{i\/}}, {\it{s\/}})\index{nth}))\index{set-nth})\index{statep}
\end{tabbing}


\begin{verbatim}; Got to here, and then aborted out as follows:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  nth-of-set-nth \\ \index{nth-of-set-nth}
\=\+({\rm{statep}}\,({\it{s\/}})\index{statep} $\wedge$ ({\it{i\/}} $\in$ {\tt{'}}{\tt{(}}{\tt{0}}{\tt{ }}{\tt{1}}{\tt{ }}{\tt{2}}{\tt{)}}) $\wedge$ ({\it{j\/}} $\in$ {\tt{'}}{\tt{(}}{\tt{0}}{\tt{ }}{\tt{1}}{\tt{ }}{\tt{2}}{\tt{)}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{nth}}\,({\it{i\/}}, {\rm{set-nth}}\,({\it{j\/}}, {\it{s\/}}, {\it{v\/}})\index{set-nth})\index{nth} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $=$ {\it{j\/}}$\;\;${\bf then }{\it{v\/}} \\ 
{\bf else }{\rm{nth}}\,({\it{i\/}}, {\it{s\/}})\index{nth}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{statep-tower-ind} \\  
\=\+{\rm{statep-tower-ind}}\,({\it{i\/}}, {\it{n\/}}, {\it{s\/}})\index{statep-tower-ind} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{statep-tower-ind}}\,({\it{i\/}}, {\it{n\/}} $-\;1$, {\rm{set-nth}}\,({\it{i\/}}, {\it{s\/}}, {\rm{cons}}\,({\it{n\/}}, {\rm{nth}}\,({\it{i\/}}, {\it{s\/}})\index{nth}))\index{set-nth})\index{statep-tower-ind}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  append-assoc \\ \index{append-assoc}
{\rm{append}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}), {\it{z\/}}) $=$ {\rm{append}}\,({\it{x\/}}, {\rm{append}}\,({\it{y\/}}, {\it{z\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  set-nth-twice \\ \index{set-nth-twice}
{\rm{set-nth}}\,({\it{i\/}}, {\rm{set-nth}}\,({\it{i\/}}, {\it{s\/}}, {\it{v1\/}})\index{set-nth}, {\it{v2\/}})\index{set-nth} $=$ {\rm{set-nth}}\,({\it{i\/}}, {\it{s\/}}, {\it{v2\/}})\index{set-nth}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  slessp-preserved \\ \index{slessp-preserved}
\=\+(({\it{n\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{n\/}} $\not=$ {\tt{0}}) $\wedge$ {\rm{statep}}\,({\it{s\/}})\index{statep} $\wedge$ ({\it{i\/}} $\in$ {\tt{'}}{\tt{(}}{\tt{0}}{\tt{ }}{\tt{1}}{\tt{ }}{\tt{2}}{\tt{)}}) $\wedge$ {\rm{slessp}}\,({\it{n\/}}, {\it{s\/}})\index{slessp}) \\ 
$\rightarrow$$\;\;\;\;${\rm{slessp}}\,({\it{n\/}} $-\;1$, {\rm{set-nth}}\,({\it{i\/}}, {\it{s\/}}, {\rm{cons}}\,({\it{n\/}}, {\rm{nth}}\,({\it{i\/}}, {\it{s\/}})\index{nth}))\index{set-nth})\index{slessp}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  statep-tower \\ \index{statep-tower}
\=\+(({\it{n\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{n\/}} $\not=$ {\tt{0}}) $\wedge$ {\rm{statep}}\,({\it{s\/}})\index{statep} $\wedge$ {\rm{slessp}}\,({\it{n\/}}, {\it{s\/}})\index{slessp} $\wedge$ ({\it{i\/}} $\in$ {\tt{'}}{\tt{(}}{\tt{0}}{\tt{ }}{\tt{1}}{\tt{ }}{\tt{2}}{\tt{)}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{statep}}\,({\rm{set-nth}}\,({\it{i\/}}, {\it{s\/}}, {\rm{append}}\,({\rm{tower}}\,({\it{n\/}})\index{tower}, {\rm{nth}}\,({\it{i\/}}, {\it{s\/}})\index{nth}))\index{set-nth})\index{statep}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  play-is-non-f-bookmark \\ \index{play-is-non-f-bookmark}
{\bf{t}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  permp-preserved-1 \\ \index{permp-preserved-1}
{\rm{permp}}\,({\it{i\/}}, {\it{j\/}}, {\it{k\/}})\index{permp} $\rightarrow$ {\rm{permp}}\,({\it{i\/}}, {\it{k\/}}, {\it{j\/}})\index{permp}
\end{tabbing}


\noindent{\sc Event}:   Disable permp-preserved-1.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  used-first-ind-hyp \\ \index{used-first-ind-hyp}
{\bf{t}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  set-nth-different-twice \\ \index{set-nth-different-twice}
\=\+(({\it{i\/}} $\in$ {\tt{'}}{\tt{(}}{\tt{0}}{\tt{ }}{\tt{1}}{\tt{ }}{\tt{2}}{\tt{)}}) $\wedge$ ({\it{j\/}} $\in$ {\tt{'}}{\tt{(}}{\tt{0}}{\tt{ }}{\tt{1}}{\tt{ }}{\tt{2}}{\tt{)}}) $\wedge$ ({\it{i\/}} $\not=$ {\it{j\/}}) $\wedge$ {\rm{statep}}\,({\it{s\/}})\index{statep}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{set-nth}}\,({\it{i\/}}, {\rm{set-nth}}\,({\it{j\/}}, {\it{s\/}}, {\it{v\/}})\index{set-nth}, {\it{w\/}})\index{set-nth} $=$ {\rm{set-nth}}\,({\it{j\/}}, {\rm{set-nth}}\,({\it{i\/}}, {\it{s\/}}, {\it{w\/}})\index{set-nth}, {\it{v\/}})\index{set-nth})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  slessp-sub1 \\ \index{slessp-sub1}
{\rm{slessp}}\,({\it{n\/}}, {\it{s\/}})\index{slessp} $\rightarrow$ {\rm{slessp}}\,({\it{n\/}} $-\;1$, {\it{s\/}})\index{slessp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  permp-preserved-2 \\ \index{permp-preserved-2}
{\rm{permp}}\,({\it{i\/}}, {\it{j\/}}, {\it{k\/}})\index{permp} $\rightarrow$ {\rm{permp}}\,({\it{k\/}}, {\it{j\/}}, {\it{i\/}})\index{permp}
\end{tabbing}


\noindent{\sc Event}:   Disable permp-preserved-2.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  statep-preserved-by-set-nth \\ \index{statep-preserved-by-set-nth}
({\rm{statep}}\,({\it{s\/}})\index{statep} $\wedge$ ({\it{i\/}} $\in$ {\tt{'}}{\tt{(}}{\tt{0}}{\tt{ }}{\tt{1}}{\tt{ }}{\tt{2}}{\tt{)}})) $\rightarrow$ {\rm{statep}}\,({\rm{set-nth}}\,({\it{i\/}}, {\it{s\/}}, {\it{v\/}})\index{set-nth})\index{statep}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-but-legal \\ \index{all-but-legal}
{\bf{t}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ind-step \\ \index{ind-step}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;${\rm{main-thm}}\,({\it{i\/}}, {\it{k\/}}, {\it{j\/}}, {\it{n\/}} $-\;1$, {\rm{set-nth}}\,({\it{i\/}}, {\it{s\/}}, {\rm{cons}}\,({\it{n\/}}, {\rm{nth}}\,({\it{i\/}}, {\it{s\/}})\index{nth}))\index{set-nth})\index{main-thm} \\ 
$\wedge$$\;\;\;\;${\rm{main-thm}}\,({\it{k\/}}, {\it{j\/}}, {\it{i\/}}, {\it{n\/}} $-\;1$, {\rm{set-nth}}\,({\it{j\/}}, {\it{s\/}}, {\rm{cons}}\,({\it{n\/}}, {\rm{nth}}\,({\it{j\/}}, {\it{s\/}})\index{nth}))\index{set-nth})\index{main-thm})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{main-thm}}\,({\it{i\/}}, {\it{j\/}}, {\it{k\/}}, {\it{n\/}}, {\it{s\/}})\index{main-thm}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  main-theorem-abbreviated \\ \index{main-theorem-abbreviated}
{\rm{main-thm}}\,({\it{i\/}}, {\it{j\/}}, {\it{k\/}}, {\it{n\/}}, {\it{s\/}})\index{main-thm}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  main-theorem \\ \index{main-theorem}
\=\+({\rm{statep}}\,({\it{s\/}})\index{statep} $\wedge$ {\rm{slessp}}\,({\it{n\/}}, {\it{s\/}})\index{slessp} $\wedge$ {\rm{permp}}\,({\it{i\/}}, {\it{j\/}}, {\it{k\/}})\index{permp}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{play}}\,({\rm{h}}\,({\it{n\/}}, {\it{i\/}}, {\it{j\/}}, {\it{k\/}})\index{h}, {\rm{set-nth}}\,({\it{i\/}}, {\it{s\/}}, {\rm{append}}\,({\rm{tower}}\,({\it{n\/}})\index{tower}, {\rm{nth}}\,({\it{i\/}}, {\it{s\/}})\index{nth}))\index{set-nth})\index{play} \\ 
$=$$\;\;\;\;${\rm{set-nth}}\,({\it{j\/}}, {\it{s\/}}, {\rm{append}}\,({\rm{tower}}\,({\it{n\/}})\index{tower}, {\rm{nth}}\,({\it{j\/}}, {\it{s\/}})\index{nth}))\index{set-nth})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  correctness-of-hanoi \\ \index{correctness-of-hanoi}
\=\+{\rm{play}}\,({\rm{hanoi}}\,({\it{n\/}})\index{hanoi}, {\rm{cons}}\,({\rm{tower}}\,({\it{n\/}})\index{tower}, {\tt{'}}{\tt{(}}{\tt{nil}}{\tt{ }}{\tt{nil}}{\tt{)}}))\index{play} \\ 
$=$$\;\;\;\;${\rm{cons}}\,({\bf{nil}}, {\rm{cons}}\,({\rm{tower}}\,({\it{n\/}})\index{tower}, {\tt{'}}{\tt{(}}{\tt{nil}}{\tt{)}}))\-
\end{tabbing}

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