\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{bubble1} \\  
\=\+{\rm{bubble1}}\,({\it{l\/}})\index{bubble1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }$\neg$ {\rm{listp}}\,({\it{l\/}})$\;\;${\bf then }{\it{l\/}} \\ 
{\bf elseif }$\neg$ {\rm{listp}}\,({\rm{cdr}}\,({\it{l\/}}))$\;\;${\bf then }{\it{l\/}} \\ 
{\bf elseif }{\rm{car}}\,({\it{l\/}}) $<$ {\rm{car}}\,({\rm{bubble1}}\,({\rm{cdr}}\,({\it{l\/}}))\index{bubble1}) \\ 
{\bf then }{\rm{cons}}\,({\rm{car}}\,({\it{l\/}}), {\rm{bubble1}}\,({\rm{cdr}}\,({\it{l\/}}))\index{bubble1}) \\ 
{\bf else }{\rm{cons}}\,(\=\+{\rm{car}}\,({\rm{bubble1}}\,({\rm{cdr}}\,({\it{l\/}}))\index{bubble1}), \\ 
{\rm{cons}}\,({\rm{car}}\,({\it{l\/}}), {\rm{cdr}}\,({\rm{bubble1}}\,({\rm{cdr}}\,({\it{l\/}}))\index{bubble1})))\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{length} \\  
\=\+{\rm{length}}\,({\it{lst\/}})\index{length} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{lst\/}})$\;\;${\bf then }$1\;+$ {\rm{length}}\,({\rm{cdr}}\,({\it{lst\/}}))\index{length} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bubble1-preserves-length \\ \index{bubble1-preserves-length}
{\rm{length}}\,({\rm{bubble1}}\,({\it{l\/}})\index{bubble1})\index{length} $=$ {\rm{length}}\,({\it{l\/}})\index{length}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  stupid-lemma-1 \\ \index{stupid-lemma-1}
{\rm{listp}}\,({\it{l\/}}) $\rightarrow$ ({\rm{length}}\,({\rm{cdr}}\,({\rm{bubble1}}\,({\it{l\/}})\index{bubble1}))\index{length} $<$ {\rm{length}}\,({\it{l\/}})\index{length})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{bubblesort} \\  
\=\+{\rm{bubblesort}}\,({\it{l\/}})\index{bubblesort} \\ 
$=$$\;\;\;\;$\=\+{\bf if }$\neg$ {\rm{listp}}\,({\it{l\/}})$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\rm{bubble1}}\,({\it{l\/}})\index{bubble1}), {\rm{bubblesort}}\,({\rm{cdr}}\,({\rm{bubble1}}\,({\it{l\/}})\index{bubble1}))\index{bubblesort})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{sortedp} \\  
\=\+{\rm{sortedp}}\,({\it{l\/}})\index{sortedp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }$\neg$ {\rm{listp}}\,({\it{l\/}})$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }$\neg$ {\rm{listp}}\,({\rm{cdr}}\,({\it{l\/}}))$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }({\rm{car}}\,({\it{l\/}}) $\leq$ {\rm{cadr}}\,({\it{l\/}})) $\wedge$ {\rm{sortedp}}\,({\rm{cdr}}\,({\it{l\/}}))\index{sortedp}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-cdr-bubble1-not-lessp \\ \index{member-cdr-bubble1-not-lessp}
({\it{x\/}} $\in$ {\rm{cdr}}\,({\rm{bubble1}}\,({\it{l\/}})\index{bubble1})) $\rightarrow$ (({\it{x\/}} $<$ {\rm{car}}\,({\rm{bubble1}}\,({\it{l\/}})\index{bubble1})) $=$ {\bf{f}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bubblesort-is-sorted \\ \index{bubblesort-is-sorted}
{\rm{sortedp}}\,({\rm{bubblesort}}\,({\it{l\/}})\index{bubblesort})\index{sortedp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bubblesort-is-sortedp \\ \index{bubblesort-is-sortedp}
{\rm{sortedp}}\,({\rm{bubblesort}}\,({\it{l\/}})\index{bubblesort})\index{sortedp}
\end{tabbing}  \begin{verbatim}; the last of these seems to be new
                                ; somehow, 2/20/88

\end{verbatim}
\noindent{\sc Event}:   Introduce the function symbol {\it amb\index{amb}\/} of 2 arguments.

\addvspace{18pt}

\begin{tabbing}{\sc Axiom}:  amb-axiom \\ \index{amb-axiom}
({\rm{amb}}\,({\it{x\/}}, {\it{y\/}})\index{amb} $=$ {\it{x\/}}) $\vee$ ({\rm{amb}}\,({\it{x\/}}, {\it{y\/}})\index{amb} $=$ {\it{y\/}})
\end{tabbing}

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


\noindent{\sc Event}:   Introduce the function symbol {\it constant\index{constant}\/} of 0 arguments.

\addvspace{18pt}

\begin{tabbing}{\sc Axiom}:  constant-axiom \\ \index{constant-axiom}
\=\+(({\sc{constant}}\index{constant} $\in\;${\bf{N}}${}$) $\wedge$ ({\rm{car}}\,({\rm{state}}\,({\sc{constant}}\index{constant})\index{state}) $=$ {\tt{1}})) \\ 
$\vee$$\;\;\;\;$($\neg$ (({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\rm{car}}\,({\rm{state}}\,({\it{x\/}})\index{state}) $=$ {\tt{1}})))\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{zz} \\  
\=\+{\rm{zz}}\,({\it{x\/}})\index{zz} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{zz}}\,({\it{x\/}} $-\;1$)\index{zz}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  car-of-state-is-numberp \\ \index{car-of-state-is-numberp}
{\rm{car}}\,({\rm{state}}\,({\it{x\/}})\index{state}) $\in\;${\bf{N}}${}$
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  cdr-of-state-is-numberp \\ \index{cdr-of-state-is-numberp}
{\rm{cdr}}\,({\rm{state}}\,({\it{x\/}})\index{state}) $\in\;${\bf{N}}${}$
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{thm-ind} \\  
\=\+{\rm{thm-ind}}\,({\it{x\/}}, {\it{y\/}})\index{thm-ind} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{y\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{thm-ind}}\,($1\;+$ {\it{x\/}}, {\it{y\/}} $-\;1$)\index{thm-ind}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  main-base \\ \index{main-base}
{\bf{t}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  main-thm \\ \index{main-thm}
\=\+(({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\rm{car}}\,({\rm{state}}\,({\it{x\/}})\index{state}) $=$ {\tt{1}}) $\wedge$ ({\rm{cdr}}\,({\rm{state}}\,({\it{x\/}})\index{state}) $=$ {\it{y\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{state}}\,({\it{x\/}} $+$ {\it{y\/}})\index{state} $=$ {\tt{'}}{\tt{(}}{\tt{1}}{\tt{ .\ }}{\tt{0}}{\tt{)}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  pnueli-1 \\ \index{pnueli-1}
\=\+(({\sc{constant}}\index{constant} $\in\;${\bf{N}}${}$) $\wedge$ ({\rm{car}}\,({\rm{state}}\,({\sc{constant}}\index{constant})\index{state}) $=$ {\tt{1}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{cdr}}\,({\rm{state}}\,({\sc{constant}}\index{constant} $+$ {\rm{cdr}}\,({\rm{state}}\,({\sc{constant}}\index{constant})\index{state}))\index{state}) $=$ {\tt{0}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  car-of-state-is-zero-or-1 \\ \index{car-of-state-is-zero-or-1}
({\rm{car}}\,({\rm{state}}\,({\it{x\/}})\index{state}) $\not=$ {\tt{1}}) $\rightarrow$ ({\rm{car}}\,({\rm{state}}\,({\it{x\/}})\index{state}) $=$ {\tt{0}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  pnueli-2 \\ \index{pnueli-2}
($\neg$ (({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\rm{car}}\,({\rm{state}}\,({\it{x\/}})\index{state}) $=$ {\tt{1}}))) $\rightarrow$ ({\rm{car}}\,({\rm{state}}\,({\it{x\/}})\index{state}) $\simeq {\tt{0}}$)
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  pnueli-thm \\ \index{pnueli-thm}
\=\+({\rm{cdr}}\,({\rm{state}}\,({\sc{constant}}\index{constant} $+$ {\rm{cdr}}\,({\rm{state}}\,({\sc{constant}}\index{constant})\index{state}))\index{state}) $=$ {\tt{0}}) \\ 
$\vee$$\;\;\;\;$({\rm{car}}\,({\rm{state}}\,({\it{x\/}})\index{state}) $\simeq {\tt{0}}$)\-
\end{tabbing}

\begin{verbatim}; Begin commutativity of times

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{double-ind} \\  
\=\+{\rm{double-ind}}\,({\it{x\/}}, {\it{y\/}})\index{double-ind} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{x\/}} $\simeq {\tt{0}}$) $\vee$ ({\it{y\/}} $\simeq {\tt{0}}$)$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }\=\+{\rm{double-ind}}\,({\it{x\/}}, {\it{y\/}} $-\;1$)\index{double-ind} \\ 
$\wedge$$\;\;\;\;${\rm{double-ind}}\,({\it{x\/}} $-\;1$, {\it{y\/}})\index{double-ind} \\ 
$\wedge$$\;\;\;\;${\rm{double-ind}}\,({\it{x\/}} $-\;1$, {\it{y\/}} $-\;1$)\index{double-ind}\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; the following has USE-GOAL and hence is omitted, 2/88
#|
(PROVE-LEMMA TIMES-COMM
	     (REWRITE)
	     (EQUAL (TIMES X Y) (TIMES Y X))
	     ((INSTRUCTIONS (INDUCT (DOUBLE-IND X Y))
			    S SPLIT SUBV S
			    (PUSH TIMES-0)
			    PROVE SUBV S USE-GOAL
			    (HIDE-HYPS 1 2 3)
			    (PUSH TIMES-NOT-NUMBERP)
			    PROVE USE-GOAL S DIVE PUSH DIVE
			    (DIVE 1)
			    X
			    (DIVE 2)
			    (= * (TIMES Y (SUB1 X)) T)
			    X UP NX X
			    (DIVE 2)
			    (= * (TIMES X (SUB1 Y)) T)
			    X UP UP
			    (DIVE 1 2 2)
			    (= * (TIMES (SUB1 X) (SUB1 Y)) T)
			    TOP
			    (GENERALIZE (((TIMES (SUB1 X) (SUB1 Y)) ?)))
			    PROVE)))
|#

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{flatten} \\  
\=\+{\rm{flatten}}\,({\it{x\/}})\index{flatten} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\rm{list}}\,({\it{x\/}}) \\ 
{\bf else }{\rm{append}}\,({\rm{flatten}}\,({\rm{car}}\,({\it{x\/}}))\index{flatten}, {\rm{flatten}}\,({\rm{cdr}}\,({\it{x\/}}))\index{flatten})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{mcflatten} \\  
\=\+{\rm{mcflatten}}\,({\it{x\/}}, {\it{y\/}})\index{mcflatten} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\rm{cons}}\,({\it{x\/}}, {\it{y\/}}) \\ 
{\bf else }{\rm{mcflatten}}\,({\rm{car}}\,({\it{x\/}}), {\rm{mcflatten}}\,({\rm{cdr}}\,({\it{x\/}}), {\it{y\/}})\index{mcflatten})\index{mcflatten}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{fmfind} \\  
\=\+{\rm{fmfind}}\,({\it{x\/}}, {\it{y\/}})\index{fmfind} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{fmfind}}\,({\rm{car}}\,({\it{x\/}}), {\rm{mcflatten}}\,({\rm{cdr}}\,({\it{x\/}}), {\it{y\/}})\index{mcflatten})\index{fmfind} $\wedge$ {\rm{fmfind}}\,({\rm{cdr}}\,({\it{x\/}}), {\it{y\/}})\index{fmfind}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bookmark \\ \index{bookmark}
{\bf{t}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  assoc-of-append \\ \index{assoc-of-append}
{\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}:  flatten-mcflatten \\ \index{flatten-mcflatten}
{\rm{mcflatten}}\,({\it{x\/}}, {\it{y\/}})\index{mcflatten} $=$ {\rm{append}}\,({\rm{flatten}}\,({\it{x\/}})\index{flatten}, {\it{y\/}})
\end{tabbing}

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

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

\begin{tabbing}{\sc Definition}:\index{rev} \\  
\=\+{\rm{rev}}\,({\it{l\/}})\index{rev} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{l\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{append}}\,({\rm{rev}}\,({\rm{cdr}}\,({\it{l\/}}))\index{rev}, {\rm{list}}\,({\rm{car}}\,({\it{l\/}})))$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{plistp} \\  
\=\+{\rm{plistp}}\,({\it{l\/}})\index{plistp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{l\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\it{l\/}} $=$ {\bf{nil}} \\ 
{\bf else }{\rm{plistp}}\,({\rm{cdr}}\,({\it{l\/}}))\index{plistp}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  rev-rev \\ \index{rev-rev}
{\rm{plistp}}\,({\it{l\/}})\index{plistp} $\rightarrow$ ({\rm{rev}}\,({\rm{rev}}\,({\it{l\/}})\index{rev})\index{rev} $=$ {\it{l\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  rev-plistp \\ \index{rev-plistp}
{\rm{plistp}}\,({\rm{rev}}\,({\it{l\/}})\index{rev})\index{plistp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  rev-append-1 \\ \index{rev-append-1}
{\rm{rev}}\,({\it{y\/}})\index{rev} $=$ {\rm{append}}\,({\rm{rev}}\,({\it{y\/}})\index{rev}, {\bf{nil}})
\end{tabbing}

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

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