\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}; Works as of 4/06/87 20:14:00

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

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{min} \\  
\=\+{\rm{min}}\,({\it{x\/}}, {\it{y\/}})\index{min} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $<$ {\it{y\/}}$\;\;${\bf then }{\it{x\/}} \\ 
{\bf else }{\it{y\/}}$\;${\bf  endif}\-\-
\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{put} \\  
\=\+{\rm{put}}\,({\it{n\/}}, {\it{val\/}}, {\it{l\/}})\index{put} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{cons}}\,({\it{val\/}}, {\rm{cdr}}\,({\it{l\/}})) \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\it{l\/}}), {\rm{put}}\,({\it{n\/}} $-\;1$, {\it{val\/}}, {\rm{cdr}}\,({\it{l\/}}))\index{put})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  nth-of-put \\ \index{nth-of-put}
{\rm{nth}}\,({\it{i\/}}, {\rm{put}}\,({\it{i\/}}, {\it{v\/}}, {\it{l\/}})\index{put})\index{nth} $=$ {\it{v\/}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  nth-of-put-neq \\ \index{nth-of-put-neq}
(({\it{i\/}} $\not=$ {\it{j\/}}) $\wedge$ ({\it{i\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{j\/}} $\in\;${\bf{N}}${}$)) $\rightarrow$ ({\rm{nth}}\,({\it{i\/}}, {\rm{put}}\,({\it{j\/}}, {\it{v\/}}, {\it{l\/}})\index{put})\index{nth} $=$ {\rm{nth}}\,({\it{i\/}}, {\it{l\/}})\index{nth})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{access} \\  
{\rm{access}}\,({\it{matrix\/}}, {\it{i\/}}, {\it{j\/}})\index{access} $=$ ($\neg$ ($\neg$ {\rm{nth}}\,({\it{j\/}}, {\rm{nth}}\,({\it{i\/}}, {\it{matrix\/}})\index{nth})\index{nth}))
\end{tabbing}


\noindent{\sc Event}:   Disable access.

\addvspace{18pt}

\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 Definition}:\index{col}$\;\;$
{\rm{col}}\,({\it{matrix\/}})\index{col} $=$ {\rm{length}}\,({\rm{car}}\,({\it{matrix\/}}))\index{length}
\end{tabbing}


\noindent{\sc Event}:   Disable col.

\addvspace{18pt}

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

\begin{tabbing}{\sc Definition}:\index{segmentp} \\  
\=\+{\rm{segmentp}}\,({\it{i\/}}, {\it{j\/}}, {\it{left\/}}, {\it{matrix\/}})\index{segmentp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{left\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{access}}\,({\it{matrix\/}}, {\it{i\/}}, {\it{j\/}})\index{access} $\wedge$ {\rm{segmentp}}\,({\it{i\/}}, {\it{j\/}} $-\;1$, {\it{left\/}} $-\;1$, {\it{matrix\/}})\index{segmentp}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  segmentp-access \\ \index{segmentp-access}
\=\+(({\it{i\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{j\/}} $\in\;${\bf{N}}${}$) $\wedge$ {\rm{segmentp}}\,({\it{i\/}}, {\it{j\/}}, {\it{left\/}}, {\it{matrix\/}})\index{segmentp} $\wedge$ ({\it{k\/}} $<$ {\it{left\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{access}}\,({\it{matrix\/}}, {\it{i\/}}, {\it{j\/}} $-$ {\it{k\/}})\index{access}\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{rectanglep} \\  
\=\+{\rm{rectanglep}}\,({\it{i\/}}, {\it{j\/}}, {\it{left\/}}, {\it{up\/}}, {\it{matrix\/}})\index{rectanglep} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{left\/}} $\simeq {\tt{0}}$) $\vee$ ({\it{up\/}} $\simeq {\tt{0}}$)$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }\=\+{\rm{rectanglep}}\,({\it{i\/}} $-\;1$, {\it{j\/}}, {\it{left\/}}, {\it{up\/}} $-\;1$, {\it{matrix\/}})\index{rectanglep} \\ 
$\wedge$$\;\;\;\;${\rm{segmentp}}\,({\it{i\/}}, {\it{j\/}}, {\it{left\/}}, {\it{matrix\/}})\index{segmentp}\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  rectanglep-access \\ \index{rectanglep-access}
\=\+(\=\+({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{up\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{up\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{rectanglep}}\,({\it{i\/}}, {\it{j\/}}, {\it{left\/}}, {\it{up\/}}, {\it{matrix\/}})\index{rectanglep} \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $<$ {\it{left\/}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{access}}\,({\it{matrix\/}}, {\it{i\/}}, {\it{j\/}} $-$ {\it{k\/}})\index{access}\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{tsquarep} \\  
\=\+{\rm{tsquarep}}\,({\it{i\/}}, {\it{j\/}}, {\it{side\/}}, {\it{matrix\/}})\index{tsquarep} \\ 
$=$$\;\;\;\;$(\=\+{\rm{rectanglep}}\,({\it{i\/}}, {\it{j\/}}, {\it{side\/}}, {\it{side\/}}, {\it{matrix\/}})\index{rectanglep} \\ 
$\wedge$$\;\;\;\;$(($1\;+$ {\it{i\/}}) $\not<$ {\it{side\/}}) \\ 
$\wedge$$\;\;\;\;$(($1\;+$ {\it{j\/}}) $\not<$ {\it{side\/}}))\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable tsquarep.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  tsquarep-0 \\ \index{tsquarep-0}
{\rm{tsquarep}}\,({\it{i\/}}, {\it{j\/}}, {\tt{0}}, {\it{matrix\/}})\index{tsquarep}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  segmentp-goes-down \\ \index{segmentp-goes-down}
(({\it{m\/}} $\not<$ {\it{n\/}}) $\wedge$ {\rm{segmentp}}\,({\it{i\/}}, {\it{j\/}}, {\it{m\/}}, {\it{matrix\/}})\index{segmentp}) $\rightarrow$ {\rm{segmentp}}\,({\it{i\/}}, {\it{j\/}}, {\it{n\/}}, {\it{matrix\/}})\index{segmentp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  rectanglep-goes-down \\ \index{rectanglep-goes-down}
\=\+(({\it{m1\/}} $\not<$ {\it{n1\/}}) $\wedge$ ({\it{m2\/}} $\not<$ {\it{n2\/}}) $\wedge$ {\rm{rectanglep}}\,({\it{i\/}}, {\it{j\/}}, {\it{m1\/}}, {\it{m2\/}}, {\it{matrix\/}})\index{rectanglep}) \\ 
$\rightarrow$$\;\;\;\;${\rm{rectanglep}}\,({\it{i\/}}, {\it{j\/}}, {\it{n1\/}}, {\it{n2\/}}, {\it{matrix\/}})\index{rectanglep}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  tsquarep-goes-down \\ \index{tsquarep-goes-down}
(({\it{m\/}} $\not<$ {\it{n\/}}) $\wedge$ {\rm{tsquarep}}\,({\it{i\/}}, {\it{j\/}}, {\it{m\/}}, {\it{matrix\/}})\index{tsquarep}) $\rightarrow$ {\rm{tsquarep}}\,({\it{i\/}}, {\it{j\/}}, {\it{n\/}}, {\it{matrix\/}})\index{tsquarep}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{ok-c-before} \\  
\=\+{\rm{ok-c-before}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{ok-c-before} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{j\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }\=\+{\rm{tsquarep}}\,({\it{i\/}}, {\it{j\/}} $-\;1$, {\rm{nth}}\,({\it{j\/}} $-\;1$, {\it{c\/}})\index{nth}, {\it{matrix\/}})\index{tsquarep} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{tsquarep}}\,({\it{i\/}}, {\it{j\/}} $-\;1$, $1\;+$ {\rm{nth}}\,({\it{j\/}} $-\;1$, {\it{c\/}})\index{nth}, {\it{matrix\/}})\index{tsquarep}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-c-before}}\,({\it{i\/}}, {\it{j\/}} $-\;1$, {\it{c\/}}, {\it{matrix\/}})\index{ok-c-before}\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{ok-c-after} \\  
\=\+{\rm{ok-c-after}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{ok-c-after} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }($1\;+$ {\it{j\/}}) $<$ {\rm{col}}\,({\it{matrix\/}})\index{col} \\ 
{\bf then }\=\+{\rm{tsquarep}}\,({\it{i\/}} $-\;1$, $1\;+$ {\it{j\/}}, {\rm{nth}}\,($1\;+$ {\it{j\/}}, {\it{c\/}})\index{nth}, {\it{matrix\/}})\index{tsquarep} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{tsquarep}}\,({\it{i\/}} $-\;1$, $1\;+$ {\it{j\/}}, $1\;+$ {\rm{nth}}\,($1\;+$ {\it{j\/}}, {\it{c\/}})\index{nth}, {\it{matrix\/}})\index{tsquarep}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-c-after}}\,({\it{i\/}}, $1\;+$ {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{ok-c-after}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{zero-tail} \\  
\=\+{\rm{zero-tail}}\,({\it{c\/}}, {\it{j\/}}, {\it{col\/}})\index{zero-tail} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{j\/}} $<$ {\it{col\/}}$\;\;${\bf then }({\rm{nth}}\,({\it{j\/}}, {\it{c\/}})\index{nth} $=$ {\tt{0}}) $\wedge$ {\rm{zero-tail}}\,({\it{c\/}}, $1\;+$ {\it{j\/}}, {\it{col\/}})\index{zero-tail} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{ok-c} \\  
\=\+{\rm{ok-c}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{ok-c} \\ 
$=$$\;\;\;\;$(\=\+{\rm{ok-c-before}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{ok-c-before} \\ 
$\wedge$$\;\;\;\;${\rm{ok-c-after}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{ok-c-after} \\ 
$\wedge$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{zero-tail}}\,({\it{c\/}}, {\it{j\/}}, {\rm{col}}\,({\it{matrix\/}})\index{col})\index{zero-tail} \\ 
{\bf else }\=\+{\rm{tsquarep}}\,({\it{i\/}} $-\;1$, {\it{j\/}}, {\rm{nth}}\,({\it{j\/}}, {\it{c\/}})\index{nth}, {\it{matrix\/}})\index{tsquarep} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{tsquarep}}\,({\it{i\/}} $-\;1$, {\it{j\/}}, $1\;+$ {\rm{nth}}\,({\it{j\/}}, {\it{c\/}})\index{nth}, {\it{matrix\/}})\index{tsquarep})\-$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  put-preserves-ok-before \\ \index{put-preserves-ok-before}
\=\+(({\it{i\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{j\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{k\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{j\/}} $\not<$ {\it{k\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{ok-c-before}}\,({\it{i\/}}, {\it{k\/}}, {\rm{put}}\,({\it{j\/}}, {\it{side\/}}, {\it{c\/}})\index{put}, {\it{matrix\/}})\index{ok-c-before} $=$ {\rm{ok-c-before}}\,({\it{i\/}}, {\it{k\/}}, {\it{c\/}}, {\it{matrix\/}})\index{ok-c-before})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  put-preserves-length \\ \index{put-preserves-length}
({\it{n\/}} $<$ {\rm{length}}\,({\it{l\/}})\index{length}) $\rightarrow$ ({\rm{length}}\,({\rm{put}}\,({\it{n\/}}, {\it{val\/}}, {\it{l\/}})\index{put})\index{length} $=$ {\rm{length}}\,({\it{l\/}})\index{length})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  put-preserves-ok-after \\ \index{put-preserves-ok-after}
\=\+(({\it{i\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{j\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{k\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{j\/}} $<$ {\it{k\/}}) $\wedge$ ({\it{j\/}} $<$ {\rm{col}}\,({\it{matrix\/}})\index{col})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{ok-c-after}}\,({\it{i\/}}, {\it{k\/}}, {\rm{put}}\,({\it{j\/}}, {\it{side\/}}, {\it{c\/}})\index{put}, {\it{matrix\/}})\index{ok-c-after} $=$ {\rm{ok-c-after}}\,({\it{i\/}}, {\it{k\/}}, {\it{c\/}}, {\it{matrix\/}})\index{ok-c-after})\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{next} \\  
\=\+{\rm{next}}\,({\it{i\/}}, {\it{j\/}}, {\it{col\/}})\index{next} \\ 
$=$$\;\;\;\;$\=\+{\bf if }($1\;+$ {\it{j\/}}) $<$ {\it{col\/}}$\;\;${\bf then }{\rm{cons}}\,({\it{i\/}}, $1\;+$ {\it{j\/}}) \\ 
{\bf else }{\rm{cons}}\,($1\;+$ {\it{i\/}}, {\tt{0}})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};;; We are headed next toward proving that the accumulating
;;; vector C has the OK-C property preserved by PUTting in
;;; a new entry which is appropriate, i.e. which is the size
;;; of the largest square submatrix with the current coordinate
;;; at the lower right corner.  First we prove PUT-PRESERVES-OK,
;;; which shows that this is the case when SIDE is that
;;; appropriate size.  Then we define the function TSQ-LOCAL
;;; which actually computes this SIDE, and show that it really
;;; does so.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  zero-tail-preserved \\ \index{zero-tail-preserved}
({\it{j\/}} $<$ {\it{k\/}}) $\rightarrow$ ({\rm{zero-tail}}\,({\rm{put}}\,({\it{j\/}}, {\it{side\/}}, {\it{c\/}})\index{put}, {\it{k\/}}, {\it{col\/}})\index{zero-tail} $=$ {\rm{zero-tail}}\,({\it{c\/}}, {\it{k\/}}, {\it{col\/}})\index{zero-tail})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  put-preserves-ok-1 \\ \index{put-preserves-ok-1}
\=\+(\=\+({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{ok-c}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{ok-c} \\ 
$\wedge$$\;\;\;\;${\rm{tsquarep}}\,({\it{i\/}}, {\it{j\/}}, {\it{side\/}}, {\it{matrix\/}})\index{tsquarep} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{tsquarep}}\,({\it{i\/}}, {\it{j\/}}, $1\;+$ {\it{side\/}}, {\it{matrix\/}})\index{tsquarep}) \\ 
$\wedge$$\;\;\;\;$(($1\;+$ {\it{j\/}}) $<$ {\rm{col}}\,({\it{matrix\/}})\index{col}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{ok-c}}\,(\=\+{\rm{car}}\,({\rm{next}}\,({\it{i\/}}, {\it{j\/}}, {\rm{col}}\,({\it{matrix\/}})\index{col})\index{next}), \\ 
{\rm{cdr}}\,({\rm{next}}\,({\it{i\/}}, {\it{j\/}}, {\rm{col}}\,({\it{matrix\/}})\index{col})\index{next}), \\ 
{\rm{put}}\,({\it{j\/}}, {\it{side\/}}, {\it{c\/}})\index{put}, \\ 
{\it{matrix\/}})\-\index{ok-c}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ok-c-before-property \\ \index{ok-c-before-property}
\=\+({\rm{ok-c-before}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{ok-c-before} $\wedge$ ({\it{k\/}} $<$ {\it{j\/}}) $\wedge$ ({\it{k\/}} $\in\;${\bf{N}}${}$)) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{tsquarep}}\,({\it{i\/}}, {\it{k\/}}, {\rm{nth}}\,({\it{k\/}}, {\it{c\/}})\index{nth}, {\it{matrix\/}})\index{tsquarep} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{tsquarep}}\,({\it{i\/}}, {\it{k\/}}, $1\;+$ {\rm{nth}}\,({\it{k\/}}, {\it{c\/}})\index{nth}, {\it{matrix\/}})\index{tsquarep}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  put-preserves-ok-2 \\ \index{put-preserves-ok-2}
\=\+(\=\+({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{ok-c-before}}\,({\it{i\/}} $-\;1$, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{ok-c-before} \\ 
$\wedge$$\;\;\;\;${\rm{tsquarep}}\,({\it{i\/}} $-\;1$, {\it{j\/}}, {\it{side\/}}, {\it{matrix\/}})\index{tsquarep} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{tsquarep}}\,({\it{i\/}} $-\;1$, {\it{j\/}}, $1\;+$ {\it{side\/}}, {\it{matrix\/}})\index{tsquarep}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $=$ ({\rm{col}}\,({\it{matrix\/}})\index{col} $-\;1$)) \\ 
$\wedge$$\;\;\;\;$({\rm{col}}\,({\it{matrix\/}})\index{col} $\not=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{ok-c-after}}\,({\it{i\/}}, {\it{k\/}}, {\rm{put}}\,({\it{j\/}}, {\it{side\/}}, {\it{c\/}})\index{put}, {\it{matrix\/}})\index{ok-c-after}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  put-preserves-ok \\ \index{put-preserves-ok}
\=\+(\=\+({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{ok-c}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{ok-c} \\ 
$\wedge$$\;\;\;\;${\rm{tsquarep}}\,({\it{i\/}}, {\it{j\/}}, {\it{side\/}}, {\it{matrix\/}})\index{tsquarep} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{tsquarep}}\,({\it{i\/}}, {\it{j\/}}, $1\;+$ {\it{side\/}}, {\it{matrix\/}})\index{tsquarep}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ {\rm{col}}\,({\it{matrix\/}})\index{col}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{ok-c}}\,(\=\+{\rm{car}}\,({\rm{next}}\,({\it{i\/}}, {\it{j\/}}, {\rm{col}}\,({\it{matrix\/}})\index{col})\index{next}), \\ 
{\rm{cdr}}\,({\rm{next}}\,({\it{i\/}}, {\it{j\/}}, {\rm{col}}\,({\it{matrix\/}})\index{col})\index{next}), \\ 
{\rm{put}}\,({\it{j\/}}, {\it{side\/}}, {\it{c\/}})\index{put}, \\ 
{\it{matrix\/}})\-\index{ok-c}\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{tsq-local} \\  
\=\+{\rm{tsq-local}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{tsq-local} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{access}}\,({\it{matrix\/}}, {\it{i\/}}, {\it{j\/}})\index{access} \\ 
{\bf then }\=\+{\bf if }{\it{j\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\rm{access}}\,(\=\+{\it{matrix\/}}, \\ 
{\it{i\/}} $-$ {\rm{min}}\,({\rm{nth}}\,({\it{j\/}} $-\;1$, {\it{c\/}})\index{nth}, {\rm{nth}}\,({\it{j\/}}, {\it{c\/}})\index{nth})\index{min}, \\ 
{\it{j\/}} $-$ {\rm{min}}\,({\rm{nth}}\,({\it{j\/}} $-\;1$, {\it{c\/}})\index{nth}, {\rm{nth}}\,({\it{j\/}}, {\it{c\/}})\index{nth})\index{min})\-\index{access} \\ 
{\bf then }$1\;+$ {\rm{min}}\,({\rm{nth}}\,({\it{j\/}} $-\;1$, {\it{c\/}})\index{nth}, {\rm{nth}}\,({\it{j\/}}, {\it{c\/}})\index{nth})\index{min} \\ 
{\bf else }{\rm{min}}\,({\rm{nth}}\,({\it{j\/}} $-\;1$, {\it{c\/}})\index{nth}, {\rm{nth}}\,({\it{j\/}}, {\it{c\/}})\index{nth})\index{min}$\;${\bf  endif}\- \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{update-c} \\  
{\rm{update-c}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{update-c} $=$ {\rm{put}}\,({\it{j\/}}, {\rm{tsq-local}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{tsq-local}, {\it{c\/}})\index{put}
\end{tabbing}

\begin{verbatim}; In order to prove the correctness of TSQ-LOCAL, we need to show
; that joining together appropriately nearby square submatrices
; results in a submatrix of appropriate size.  The lemmas
; TSQUAREP-JOIN-WITHOUT-CORNER-1 and -2 show that one gets a
; TSQAREP of the common size (cf. the statement of problem),
; while TSQUAREP-JOIN-WITH-CORNER gives a square of side one greater
; when the opposite corner has value TRUE.  Recall that the point
; now is to relieve the following two hypotheses of
; PUT-PRESERVES-OK, (TSQUAREP I J SIDE MATRIX) and
; (NOT (TSQUAREP I J (ADD1 SIDE) MATRIX)), where here SIDE is
; computed by UPDATE-C to be (TSQ-LOCAL I J C MATRIX).

\end{verbatim}\begin{tabbing}{\sc Theorem}:  tsquarep-join-without-corner-1 \\ \index{tsquarep-join-without-corner-1}
\=\+({\rm{tsquarep}}\,({\tt{0}}, {\it{j\/}} $-\;1$, {\it{side\/}}, {\it{matrix\/}})\index{tsquarep} $\wedge$ {\rm{access}}\,({\it{matrix\/}}, {\tt{0}}, {\it{j\/}})\index{access}) \\ 
$\rightarrow$$\;\;\;\;${\rm{tsquarep}}\,({\tt{0}}, {\it{j\/}}, {\it{side\/}}, {\it{matrix\/}})\index{tsquarep}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  tsquarep-join-without-corner-2 \\ \index{tsquarep-join-without-corner-2}
\=\+(\=\+({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{tsquarep}}\,({\it{i\/}} $-\;1$, {\it{j\/}}, {\it{side\/}}, {\it{matrix\/}})\index{tsquarep} \\ 
$\wedge$$\;\;\;\;${\rm{tsquarep}}\,({\it{i\/}}, {\it{j\/}} $-\;1$, {\it{side\/}}, {\it{matrix\/}})\index{tsquarep} \\ 
$\wedge$$\;\;\;\;${\rm{access}}\,({\it{matrix\/}}, {\it{i\/}}, {\it{j\/}})\index{access})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{tsquarep}}\,({\it{i\/}}, {\it{j\/}}, {\it{side\/}}, {\it{matrix\/}})\index{tsquarep}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  segmentp-one-longer-base \\ \index{segmentp-one-longer-base}
{\rm{segmentp}}\,({\it{i\/}}, {\it{j\/}}, {\tt{1}}, {\it{matrix\/}})\index{segmentp} $=$ {\rm{access}}\,({\it{matrix\/}}, {\it{i\/}}, {\it{j\/}})\index{access}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  segmentp-goes-down-special-case \\ \index{segmentp-goes-down-special-case}
\=\+({\rm{segmentp}}\,({\it{i\/}}, {\it{j\/}} $-\;1$, {\it{left\/}}, {\it{matrix\/}})\index{segmentp} $\wedge$ {\rm{access}}\,({\it{matrix\/}}, {\it{i\/}}, {\it{j\/}})\index{access}) \\ 
$\rightarrow$$\;\;\;\;${\rm{segmentp}}\,({\it{i\/}}, {\it{j\/}}, {\it{left\/}}, {\it{matrix\/}})\index{segmentp}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  segmentp-one-longer \\ \index{segmentp-one-longer}
\=\+(\=\+({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{segmentp}}\,({\it{i\/}}, {\it{j\/}}, {\it{left\/}}, {\it{matrix\/}})\index{segmentp} \\ 
$\wedge$$\;\;\;\;${\rm{access}}\,({\it{matrix\/}}, {\it{i\/}}, {\it{j\/}} $-$ {\it{left\/}})\index{access})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{segmentp}}\,({\it{i\/}}, {\it{j\/}}, $1\;+$ {\it{left\/}}, {\it{matrix\/}})\index{segmentp}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  rectanglep-join-with-corner \\ \index{rectanglep-join-with-corner}
\=\+(\=\+{\rm{rectanglep}}\,({\it{i\/}} $-\;1$, {\it{j\/}}, {\it{left\/}}, {\it{up\/}}, {\it{matrix\/}})\index{rectanglep} \\ 
$\wedge$$\;\;\;\;${\rm{rectanglep}}\,({\it{i\/}}, {\it{j\/}} $-\;1$, {\it{left\/}}, {\it{up\/}}, {\it{matrix\/}})\index{rectanglep} \\ 
$\wedge$$\;\;\;\;${\rm{access}}\,({\it{matrix\/}}, {\it{i\/}} $-$ {\it{up\/}}, {\it{j\/}} $-$ {\it{left\/}})\index{access} \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\not<$ {\it{left\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not<$ {\it{up\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{left\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{left\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{up\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{up\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{access}}\,({\it{matrix\/}}, {\it{i\/}}, {\it{j\/}})\index{access})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{rectanglep}}\,({\it{i\/}}, {\it{j\/}}, $1\;+$ {\it{left\/}}, $1\;+$ {\it{up\/}}, {\it{matrix\/}})\index{rectanglep}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  tsquarep-join-with-corner \\ \index{tsquarep-join-with-corner}
\=\+(\=\+{\rm{tsquarep}}\,({\it{i\/}} $-\;1$, {\it{j\/}}, {\it{side\/}}, {\it{matrix\/}})\index{tsquarep} \\ 
$\wedge$$\;\;\;\;${\rm{tsquarep}}\,({\it{i\/}}, {\it{j\/}} $-\;1$, {\it{side\/}}, {\it{matrix\/}})\index{tsquarep} \\ 
$\wedge$$\;\;\;\;${\rm{access}}\,({\it{matrix\/}}, {\it{i\/}} $-$ {\it{side\/}}, {\it{j\/}} $-$ {\it{side\/}})\index{access} \\ 
$\wedge$$\;\;\;\;${\rm{access}}\,({\it{matrix\/}}, {\it{i\/}}, {\it{j\/}})\index{access} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\not=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{tsquarep}}\,({\it{i\/}}, {\it{j\/}}, $1\;+$ {\it{side\/}}, {\it{matrix\/}})\index{tsquarep}\-
\end{tabbing}

\begin{verbatim}; So now finally we show that UPDATE-C yields the appropriate SIDE
; for the hypotheses of PUT-PRESERVES-OK by applying the joining
; lemmas above.  First, a useful lemma.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  ok-c-0 \\ \index{ok-c-0}
\=\+({\rm{ok-c}}\,({\tt{0}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{ok-c} $\wedge$ ({\it{j\/}} $<$ {\rm{col}}\,({\it{matrix\/}})\index{col})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{tsq-local}}\,({\tt{0}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{tsq-local} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{access}}\,({\it{matrix\/}}, {\tt{0}}, {\it{j\/}})\index{access}$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  tsquarep-preserved-by-tsq-local-for-i-zero \\ \index{tsquarep-preserved-by-tsq-local!-for-i-zero}
\=\+(({\it{j\/}} $\in\;${\bf{N}}${}$) $\wedge$ {\rm{ok-c}}\,({\tt{0}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{ok-c} $\wedge$ ({\it{j\/}} $<$ {\rm{col}}\,({\it{matrix\/}})\index{col})) \\ 
$\rightarrow$$\;\;\;\;${\rm{tsquarep}}\,({\tt{0}}, {\it{j\/}}, {\rm{tsq-local}}\,({\tt{0}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{tsq-local}, {\it{matrix\/}})\index{tsquarep}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  tsq-local-tsquarep-bound-0 \\ \index{tsq-local-tsquarep-bound-0}
\=\+(({\it{j\/}} $\in\;${\bf{N}}${}$) $\wedge$ {\rm{ok-c}}\,({\tt{0}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{ok-c} $\wedge$ ({\it{j\/}} $<$ {\rm{col}}\,({\it{matrix\/}})\index{col})) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{tsquarep}}\,({\tt{0}}, {\it{j\/}}, $1\;+$ {\rm{tsq-local}}\,({\tt{0}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{tsq-local}, {\it{matrix\/}})\index{tsquarep})\-
\end{tabbing}

\begin{verbatim}; For the case where I is non-zero in showing that TSQ-LOCAL has the
; desired property, the following lemma is useful.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  ok-c-main-property \\ \index{ok-c-main-property}
\=\+(({\it{j\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{j\/}} $\not=$ {\tt{0}}) $\wedge$ ({\it{i\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{i\/}} $\not=$ {\tt{0}}) $\wedge$ {\rm{ok-c}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{ok-c}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{tsquarep}}\,({\it{i\/}} $-\;1$, {\it{j\/}}, {\rm{min}}\,({\rm{nth}}\,({\it{j\/}} $-\;1$, {\it{c\/}})\index{nth}, {\rm{nth}}\,({\it{j\/}}, {\it{c\/}})\index{nth})\index{min}, {\it{matrix\/}})\index{tsquarep} \\ 
$\wedge$$\;\;\;\;${\rm{tsquarep}}\,({\it{i\/}}, {\it{j\/}} $-\;1$, {\rm{min}}\,({\rm{nth}}\,({\it{j\/}} $-\;1$, {\it{c\/}})\index{nth}, {\rm{nth}}\,({\it{j\/}}, {\it{c\/}})\index{nth})\index{min}, {\it{matrix\/}})\index{tsquarep})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  tsquarep-preserved-by-tsq-local-for-i-non-zero \\ \index{tsquarep-preserved-by-tsq-local!-for-i-non-zero}
\=\+(\=\+({\it{j\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-c}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{ok-c} \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ {\rm{col}}\,({\it{matrix\/}})\index{col}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{tsquarep}}\,({\it{i\/}}, {\it{j\/}}, {\rm{tsq-local}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{tsq-local}, {\it{matrix\/}})\index{tsquarep}\-
\end{tabbing}

\begin{verbatim}; It remains then to show that (add1 (tsq-local ...)) is too large a side
; in the non-zero case.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  access-i-non-numberp \\ \index{access-i-non-numberp}
({\it{i\/}} $\not\in\;${\bf{N}}${}$) $\rightarrow$ ({\rm{access}}\,({\it{matrix\/}}, {\it{i\/}}, {\it{j\/}})\index{access} $=$ {\rm{access}}\,({\it{matrix\/}}, {\tt{0}}, {\it{j\/}})\index{access})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  access-j-non-numberp \\ \index{access-j-non-numberp}
({\it{j\/}} $\not\in\;${\bf{N}}${}$) $\rightarrow$ ({\rm{access}}\,({\it{matrix\/}}, {\it{i\/}}, {\it{j\/}})\index{access} $=$ {\rm{access}}\,({\it{matrix\/}}, {\it{i\/}}, {\tt{0}})\index{access})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  segmentp-gives-every-access \\ \index{segmentp-gives-every-access}
\=\+({\rm{segmentp}}\,({\it{i\/}}, {\it{j\/}}, {\it{left\/}}, {\it{matrix\/}})\index{segmentp} $\wedge$ ({\it{left1\/}} $<$ {\it{left\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{access}}\,({\it{matrix\/}}, {\it{i\/}}, {\it{j\/}} $-$ {\it{left1\/}})\index{access}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  rectanglep-gives-every-access \\ \index{rectanglep-gives-every-access}
\=\+({\rm{rectanglep}}\,({\it{i\/}}, {\it{j\/}}, {\it{left\/}}, {\it{up\/}}, {\it{matrix\/}})\index{rectanglep} $\wedge$ ({\it{up1\/}} $<$ {\it{up\/}}) $\wedge$ ({\it{left1\/}} $<$ {\it{left\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{access}}\,({\it{matrix\/}}, {\it{i\/}} $-$ {\it{up1\/}}, {\it{j\/}} $-$ {\it{left1\/}})\index{access}\-
\end{tabbing}

\begin{verbatim}; and a clear corollary:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  tsquarep-gives-every-access \\ \index{tsquarep-gives-every-access}
\=\+({\rm{tsquarep}}\,({\it{i\/}}, {\it{j\/}}, {\it{side\/}}, {\it{matrix\/}})\index{tsquarep} $\wedge$ ({\it{side1\/}} $<$ {\it{side\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{access}}\,({\it{matrix\/}}, {\it{i\/}} $-$ {\it{side1\/}}, {\it{j\/}} $-$ {\it{side1\/}})\index{access}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ok-c-main-bound-property \\ \index{ok-c-main-bound-property}
\=\+(\=\+({\it{j\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-c}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{ok-c} \\ 
$\wedge$$\;\;\;\;${\rm{tsquarep}}\,({\it{i\/}} $-\;1$, {\it{j\/}}, $1\;+$ {\rm{min}}\,({\rm{nth}}\,({\it{j\/}} $-\;1$, {\it{c\/}})\index{nth}, {\rm{nth}}\,({\it{j\/}}, {\it{c\/}})\index{nth})\index{min}, {\it{matrix\/}})\index{tsquarep})\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{tsquarep}}\,({\it{i\/}}, {\it{j\/}} $-\;1$, $1\;+$ {\rm{min}}\,({\rm{nth}}\,({\it{j\/}} $-\;1$, {\it{c\/}})\index{nth}, {\rm{nth}}\,({\it{j\/}}, {\it{c\/}})\index{nth})\index{min}, {\it{matrix\/}})\index{tsquarep})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  rectanglep-goes-down-in-i-and-up \\ \index{rectanglep-goes-down-in-i-and-up}
\=\+(({\it{i\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{j\/}} $\in\;${\bf{N}}${}$) $\wedge$ {\rm{rectanglep}}\,({\it{i\/}}, {\it{j\/}}, {\it{left\/}}, $1\;+$ {\it{up\/}}, {\it{matrix\/}})\index{rectanglep}) \\ 
$\rightarrow$$\;\;\;\;${\rm{rectanglep}}\,({\it{i\/}} $-\;1$, {\it{j\/}}, {\it{left\/}}, {\it{up\/}}, {\it{matrix\/}})\index{rectanglep}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  rectanglep-goes-down-in-j-and-left \\ \index{rectanglep-goes-down-in-j-and-le!ft}
\=\+(({\it{i\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{j\/}} $\in\;${\bf{N}}${}$) $\wedge$ {\rm{rectanglep}}\,({\it{i\/}}, {\it{j\/}}, $1\;+$ {\it{left\/}}, {\it{up\/}}, {\it{matrix\/}})\index{rectanglep}) \\ 
$\rightarrow$$\;\;\;\;${\rm{rectanglep}}\,({\it{i\/}}, {\it{j\/}} $-\;1$, {\it{left\/}}, {\it{up\/}}, {\it{matrix\/}})\index{rectanglep}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  tsquarep-goes-down-in-coordinates-and-side \\ \index{tsquarep-goes-down-in-coordinate!s-and-side}
\=\+(\=\+({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{side\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{tsquarep}}\,({\it{i\/}}, {\it{j\/}}, $1\;+$ {\it{side\/}}, {\it{matrix\/}})\index{tsquarep})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{tsquarep}}\,({\it{i\/}}, {\it{j\/}} $-\;1$, {\it{side\/}}, {\it{matrix\/}})\index{tsquarep} $\wedge$ {\rm{tsquarep}}\,({\it{i\/}} $-\;1$, {\it{j\/}}, {\it{side\/}}, {\it{matrix\/}})\index{tsquarep})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  tsq-local-tsquarep-bound-non-0 \\ \index{tsq-local-tsquarep-bound-non-0}
\=\+(\=\+({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{ok-c}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{ok-c} \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ {\rm{col}}\,({\it{matrix\/}})\index{col}))\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{tsquarep}}\,({\it{i\/}}, {\it{j\/}}, $1\;+$ {\rm{tsq-local}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{tsq-local}, {\it{matrix\/}})\index{tsquarep})\-
\end{tabbing}

\begin{verbatim}; Here then is what we've been aiming at:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  update-c-preserves-ok-c \\ \index{update-c-preserves-ok-c}
\=\+(({\it{i\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{j\/}} $\in\;${\bf{N}}${}$) $\wedge$ {\rm{ok-c}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{ok-c} $\wedge$ ({\it{j\/}} $<$ {\rm{col}}\,({\it{matrix\/}})\index{col})) \\ 
$\rightarrow$$\;\;\;\;${\rm{ok-c}}\,(\=\+{\rm{car}}\,({\rm{next}}\,({\it{i\/}}, {\it{j\/}}, {\rm{col}}\,({\it{matrix\/}})\index{col})\index{next}), \\ 
{\rm{cdr}}\,({\rm{next}}\,({\it{i\/}}, {\it{j\/}}, {\rm{col}}\,({\it{matrix\/}})\index{col})\index{next}), \\ 
{\rm{update-c}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{update-c}, \\ 
{\it{matrix\/}})\-\index{ok-c}\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{update-acc} \\  
\=\+{\rm{update-acc}}\,({\it{i\/}}, {\it{j\/}}, {\it{new\/}}, {\it{acc\/}})\index{update-acc} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{car}}\,({\it{acc\/}}) $<$ {\it{new\/}}$\;\;${\bf then }{\rm{list}}\,({\it{new\/}}, {\it{i\/}}, {\it{j\/}}) \\ 
{\bf else }{\it{acc\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{lex2} \\  
\=\+{\rm{lex2}}\,({\it{l1\/}}, {\it{l2\/}})\index{lex2} \\ 
$=$$\;\;\;\;$(\=\+({\rm{car}}\,({\it{l1\/}}) $<$ {\rm{car}}\,({\it{l2\/}})) \\ 
$\vee$$\;\;\;\;$(({\rm{car}}\,({\it{l1\/}}) $=$ {\rm{car}}\,({\it{l2\/}})) $\wedge$ ({\rm{cadr}}\,({\it{l1\/}}) $<$ {\rm{cadr}}\,({\it{l2\/}}))))\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{tsq-rec} \\  
\=\+{\rm{tsq-rec}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}}, {\it{acc\/}})\index{tsq-rec} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{lex2}}\,({\rm{list}}\,({\it{i\/}}, {\it{j\/}}), {\rm{list}}\,({\rm{length}}\,({\it{matrix\/}})\index{length}, {\tt{0}}))\index{lex2} \\ 
{\bf then }{\rm{tsq-rec}}\,(\=\+{\rm{car}}\,({\rm{next}}\,({\it{i\/}}, {\it{j\/}}, {\rm{col}}\,({\it{matrix\/}})\index{col})\index{next}), \\ 
{\rm{cdr}}\,({\rm{next}}\,({\it{i\/}}, {\it{j\/}}, {\rm{col}}\,({\it{matrix\/}})\index{col})\index{next}), \\ 
{\rm{update-c}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{update-c}, \\ 
{\it{matrix\/}}, \\ 
{\rm{update-acc}}\,({\it{i\/}}, {\it{j\/}}, {\rm{tsq-local}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{tsq-local}, {\it{acc\/}})\index{update-acc})\-\index{tsq-rec} \\ 
{\bf else }{\it{acc\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{c-init}$\;\;$
{\rm{c-init}}\,({\it{matrix\/}})\index{c-init} $=$ {\rm{zeroes}}\,({\rm{col}}\,({\it{matrix\/}})\index{col} $-\;1$)\index{zeroes}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{previous} \\  
\=\+{\rm{previous}}\,({\it{i\/}}, {\it{j\/}}, {\it{col\/}})\index{previous} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{j\/}} $\simeq {\tt{0}}$ \\ 
{\bf then }\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{cons}}\,({\tt{0}}, {\tt{0}}) \\ 
{\bf else }{\rm{cons}}\,({\it{i\/}} $-\;1$, {\it{col\/}} $-\;1$)$\;${\bf  endif}\- \\ 
{\bf else }{\rm{cons}}\,({\it{i\/}}, {\it{j\/}} $-\;1$)$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  previous-next \\ \index{previous-next}
\=\+(({\it{i\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{j\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{j\/}} $<$ {\it{col\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{previous}}\,({\rm{car}}\,({\rm{next}}\,({\it{i\/}}, {\it{j\/}}, {\it{col\/}})\index{next}), {\rm{cdr}}\,({\rm{next}}\,({\it{i\/}}, {\it{j\/}}, {\it{col\/}})\index{next}), {\it{col\/}})\index{previous} $=$ {\rm{cons}}\,({\it{i\/}}, {\it{j\/}}))\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{bound} \\  
\=\+{\rm{bound}}\,({\it{i\/}}, {\it{j\/}}, {\it{matrix\/}}, {\it{size\/}})\index{bound} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{i\/}} $\simeq {\tt{0}}$) $\wedge$ ({\it{j\/}} $\simeq {\tt{0}}$)$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }\=\+($\neg$ {\rm{tsquarep}}\,(\=\+{\rm{car}}\,({\rm{previous}}\,({\it{i\/}}, {\it{j\/}}, {\rm{col}}\,({\it{matrix\/}})\index{col})\index{previous}), \\ 
{\rm{cdr}}\,({\rm{previous}}\,({\it{i\/}}, {\it{j\/}}, {\rm{col}}\,({\it{matrix\/}})\index{col})\index{previous}), \\ 
$1\;+$ {\it{size\/}}, \\ 
{\it{matrix\/}})\-\index{tsquarep}) \\ 
$\wedge$$\;\;\;\;${\rm{bound}}\,(\=\+{\rm{car}}\,({\rm{previous}}\,({\it{i\/}}, {\it{j\/}}, {\rm{col}}\,({\it{matrix\/}})\index{col})\index{previous}), \\ 
{\rm{cdr}}\,({\rm{previous}}\,({\it{i\/}}, {\it{j\/}}, {\rm{col}}\,({\it{matrix\/}})\index{col})\index{previous}), \\ 
{\it{matrix\/}}, \\ 
{\it{size\/}})\-\index{bound}\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{in-matrix} \\  
\=\+{\rm{in-matrix}}\,({\it{i\/}}, {\it{j\/}}, {\it{matrix\/}})\index{in-matrix} \\ 
$=$$\;\;\;\;$(\=\+({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\rm{length}}\,({\it{matrix\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ {\rm{col}}\,({\it{matrix\/}})\index{col}))\-\-
\end{tabbing}

\begin{verbatim}; The main lemma remaining on the way to
; INVARIANT-IS-PRESERVED-BY-CALL-OF-TSQ-REC is the following:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  bound-goes-up \\ \index{bound-goes-up}
({\rm{bound}}\,({\it{i\/}}, {\it{j\/}}, {\it{matrix\/}}, {\it{b\/}})\index{bound} $\wedge$ ({\it{b1\/}} $\not<$ {\it{b\/}})) $\rightarrow$ {\rm{bound}}\,({\it{i\/}}, {\it{j\/}}, {\it{matrix\/}}, {\it{b1\/}})\index{bound}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-update-acc \\ \index{lessp-update-acc}
\=\+(({\rm{car}}\,({\rm{update-acc}}\,({\it{i\/}}, {\it{j\/}}, {\it{anything\/}}, {\it{acc\/}})\index{update-acc}) $<$ {\it{anything\/}}) $=$ {\bf{f}}) \\ 
$\wedge$$\;\;\;\;$(({\rm{car}}\,({\rm{update-acc}}\,({\it{i\/}}, {\it{j\/}}, {\it{anything\/}}, {\it{acc\/}})\index{update-acc}) $<$ {\rm{car}}\,({\it{acc\/}})) $=$ {\bf{f}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bound-preserved-by-update-acc \\ \index{bound-preserved-by-update-acc}
\=\+(\=\+({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{ok-c}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{ok-c} \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ {\rm{col}}\,({\it{matrix\/}})\index{col}) \\ 
$\wedge$$\;\;\;\;${\rm{bound}}\,({\it{i\/}}, {\it{j\/}}, {\it{matrix\/}}, {\rm{car}}\,({\it{acc\/}}))\index{bound})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{bound}}\,(\=\+{\rm{car}}\,({\rm{next}}\,({\it{i\/}}, {\it{j\/}}, {\rm{col}}\,({\it{matrix\/}})\index{col})\index{next}), \\ 
{\rm{cdr}}\,({\rm{next}}\,({\it{i\/}}, {\it{j\/}}, {\rm{col}}\,({\it{matrix\/}})\index{col})\index{next}), \\ 
{\it{matrix\/}}, \\ 
{\rm{car}}\,({\rm{update-acc}}\,({\it{i\/}}, {\it{j\/}}, {\rm{tsq-local}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{tsq-local}, {\it{acc\/}})\index{update-acc}))\-\index{bound}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  car-of-next-numberp \\ \index{car-of-next-numberp}
({\it{i\/}} $\in\;${\bf{N}}${}$) $\rightarrow$ ({\rm{car}}\,({\rm{next}}\,({\it{i\/}}, {\it{j\/}}, {\it{col\/}})\index{next}) $\in\;${\bf{N}}${}$)
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  cdr-of-next-numberp \\ \index{cdr-of-next-numberp}
{\rm{cdr}}\,({\rm{next}}\,({\it{i\/}}, {\it{j\/}}, {\it{col\/}})\index{next}) $\in\;${\bf{N}}${}$
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  cdr-of-next-lessp \\ \index{cdr-of-next-lessp}
({\it{x\/}} $<$ {\it{col\/}}) $\rightarrow$ (({\rm{cdr}}\,({\rm{next}}\,({\it{i\/}}, {\it{j\/}}, {\it{col\/}})\index{next}) $<$ {\it{col\/}}) $=$ {\bf{t}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lex2-next \\ \index{lex2-next}
{\rm{lex2}}\,({\rm{list}}\,({\it{i\/}}, {\it{j\/}}), {\rm{list}}\,({\rm{car}}\,({\rm{next}}\,({\it{i\/}}, {\it{j\/}}, {\it{col\/}})\index{next}), {\rm{cdr}}\,({\rm{next}}\,({\it{i\/}}, {\it{j\/}}, {\it{col\/}})\index{next})))\index{lex2}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lex2-transitivity \\ \index{lex2-transitivity}
({\rm{lex2}}\,({\it{x\/}}, {\it{y\/}})\index{lex2} $\wedge$ {\rm{lex2}}\,({\it{y\/}}, {\it{z\/}})\index{lex2}) $\rightarrow$ {\rm{lex2}}\,({\it{x\/}}, {\it{z\/}})\index{lex2}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{all-f} \\  
\=\+{\rm{all-f}}\,({\it{i\/}}, {\it{j\/}}, {\it{matrix\/}})\index{all-f} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{i\/}} $\simeq {\tt{0}}$) $\wedge$ ({\it{j\/}} $\simeq {\tt{0}}$)$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }\=\+($\neg$ {\rm{access}}\,(\=\+{\it{matrix\/}}, \\ 
{\rm{car}}\,({\rm{previous}}\,({\it{i\/}}, {\it{j\/}}, {\rm{col}}\,({\it{matrix\/}})\index{col})\index{previous}), \\ 
{\rm{cdr}}\,({\rm{previous}}\,({\it{i\/}}, {\it{j\/}}, {\rm{col}}\,({\it{matrix\/}})\index{col})\index{previous}))\-\index{access}) \\ 
$\wedge$$\;\;\;\;${\rm{all-f}}\,(\=\+{\rm{car}}\,({\rm{previous}}\,({\it{i\/}}, {\it{j\/}}, {\rm{col}}\,({\it{matrix\/}})\index{col})\index{previous}), \\ 
{\rm{cdr}}\,({\rm{previous}}\,({\it{i\/}}, {\it{j\/}}, {\rm{col}}\,({\it{matrix\/}})\index{col})\index{previous}), \\ 
{\it{matrix\/}})\-\index{all-f}\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{invariant} \\  
\=\+{\rm{invariant}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}}, {\it{acc\/}})\index{invariant} \\ 
$=$$\;\;\;\;$(\=\+({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{in-matrix}}\,({\rm{cadr}}\,({\it{acc\/}}), {\rm{caddr}}\,({\it{acc\/}}), {\it{matrix\/}})\index{in-matrix} \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ {\rm{col}}\,({\it{matrix\/}})\index{col}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-c}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{ok-c} \\ 
$\wedge$$\;\;\;\;$(\=\+({\rm{all-f}}\,({\it{i\/}}, {\it{j\/}}, {\it{matrix\/}})\index{all-f} $\wedge$ ({\it{acc\/}} $=$ {\rm{list}}\,({\tt{0}}, {\tt{0}}, {\tt{0}}))) \\ 
$\vee$$\;\;\;\;${\rm{tsquarep}}\,({\rm{cadr}}\,({\it{acc\/}}), {\rm{caddr}}\,({\it{acc\/}}), {\rm{car}}\,({\it{acc\/}}), {\it{matrix\/}})\index{tsquarep})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{lex2}}\,({\rm{cdr}}\,({\it{acc\/}}), {\rm{list}}\,({\it{i\/}}, {\it{j\/}}))\index{lex2} \\ 
$\vee$$\;\;\;\;$(({\it{i\/}} $=$ {\tt{0}}) $\wedge$ ({\it{j\/}} $=$ {\tt{0}}) $\wedge$ ({\it{acc\/}} $=$ {\rm{list}}\,({\tt{0}}, {\tt{0}}, {\tt{0}}))))\- \\ 
$\wedge$$\;\;\;\;${\rm{bound}}\,({\it{i\/}}, {\it{j\/}}, {\it{matrix\/}}, {\rm{car}}\,({\it{acc\/}}))\index{bound})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  invariant-is-preserved-by-call-of-tsq-rec \\ \index{invariant-is-preserved-by-call-!of-tsq-rec}
\=\+({\rm{lex2}}\,({\rm{list}}\,({\it{i\/}}, {\it{j\/}}), {\rm{cons}}\,({\rm{length}}\,({\it{matrix\/}})\index{length}, {\tt{'}}{\tt{(}}{\tt{0}}{\tt{)}}))\index{lex2} $\wedge$ {\rm{invariant}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}}, {\it{acc\/}})\index{invariant}) \\ 
$\rightarrow$$\;\;\;\;${\rm{invariant}}\,(\=\+{\rm{car}}\,({\rm{next}}\,({\it{i\/}}, {\it{j\/}}, {\rm{col}}\,({\it{matrix\/}})\index{col})\index{next}), \\ 
{\rm{cdr}}\,({\rm{next}}\,({\it{i\/}}, {\it{j\/}}, {\rm{col}}\,({\it{matrix\/}})\index{col})\index{next}), \\ 
{\rm{update-c}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{update-c}, \\ 
{\it{matrix\/}}, \\ 
{\rm{update-acc}}\,({\it{i\/}}, {\it{j\/}}, {\rm{tsq-local}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}})\index{tsq-local}, {\it{acc\/}})\index{update-acc})\-\index{invariant}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  tsq-rec-correctness-from-invariant-base \\ \index{tsq-rec-correctness-from-invari!ant-base}
\=\+{\rm{invariant}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}}, {\it{acc\/}})\index{invariant} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{tsquarep}}\,({\rm{cadr}}\,({\it{acc\/}}), {\rm{caddr}}\,({\it{acc\/}}), {\rm{car}}\,({\it{acc\/}}), {\it{matrix\/}})\index{tsquarep} \\ 
$\wedge$$\;\;\;\;${\rm{in-matrix}}\,({\rm{cadr}}\,({\it{acc\/}}), {\rm{caddr}}\,({\it{acc\/}}), {\it{matrix\/}})\index{in-matrix} \\ 
$\wedge$$\;\;\;\;${\rm{bound}}\,({\it{i\/}}, {\it{j\/}}, {\it{matrix\/}}, {\rm{car}}\,({\it{acc\/}}))\index{bound})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bound-lex2 \\ \index{bound-lex2}
\=\+(\=\+{\rm{bound}}\,({\it{i\/}}, {\it{j\/}}, {\it{matrix\/}}, {\it{b\/}})\index{bound} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{i1\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{j1\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{j1\/}} $<$ {\rm{col}}\,({\it{matrix\/}})\index{col}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{lex2}}\,({\rm{list}}\,({\it{i\/}}, {\it{j\/}}), {\rm{list}}\,({\it{i1\/}}, {\it{j1\/}}))\index{lex2}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{bound}}\,({\it{i1\/}}, {\it{j1\/}}, {\it{matrix\/}}, {\it{b\/}})\index{bound}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  tsq-rec-correctness-from-invariant \\ \index{tsq-rec-correctness-from-invari!ant}
\=\+{\rm{invariant}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}}, {\it{acc\/}})\index{invariant} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{tsquarep}}\,(\=\+{\rm{cadr}}\,({\rm{tsq-rec}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}}, {\it{acc\/}})\index{tsq-rec}), \\ 
{\rm{caddr}}\,({\rm{tsq-rec}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}}, {\it{acc\/}})\index{tsq-rec}), \\ 
{\rm{car}}\,({\rm{tsq-rec}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}}, {\it{acc\/}})\index{tsq-rec}), \\ 
{\it{matrix\/}})\-\index{tsquarep} \\ 
$\wedge$$\;\;\;\;${\rm{in-matrix}}\,(\=\+{\rm{cadr}}\,({\rm{tsq-rec}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}}, {\it{acc\/}})\index{tsq-rec}), \\ 
{\rm{caddr}}\,({\rm{tsq-rec}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}}, {\it{acc\/}})\index{tsq-rec}), \\ 
{\it{matrix\/}})\-\index{in-matrix} \\ 
$\wedge$$\;\;\;\;${\rm{bound}}\,({\rm{length}}\,({\it{matrix\/}})\index{length}, {\tt{0}}, {\it{matrix\/}}, {\rm{car}}\,({\rm{tsq-rec}}\,({\it{i\/}}, {\it{j\/}}, {\it{c\/}}, {\it{matrix\/}}, {\it{acc\/}})\index{tsq-rec}))\index{bound})\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{tsq-i-coord} \\  
\=\+{\rm{tsq-i-coord}}\,({\it{matrix\/}})\index{tsq-i-coord} \\ 
$=$$\;\;\;\;${\rm{cadr}}\,({\rm{tsq-rec}}\,({\tt{0}}, {\tt{0}}, {\rm{c-init}}\,({\it{matrix\/}})\index{c-init}, {\it{matrix\/}}, {\rm{list}}\,({\tt{0}}, {\tt{0}}, {\tt{0}}))\index{tsq-rec})\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{tsq-j-coord} \\  
\=\+{\rm{tsq-j-coord}}\,({\it{matrix\/}})\index{tsq-j-coord} \\ 
$=$$\;\;\;\;${\rm{caddr}}\,({\rm{tsq-rec}}\,({\tt{0}}, {\tt{0}}, {\rm{c-init}}\,({\it{matrix\/}})\index{c-init}, {\it{matrix\/}}, {\rm{list}}\,({\tt{0}}, {\tt{0}}, {\tt{0}}))\index{tsq-rec})\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{tsq} \\  
{\rm{tsq}}\,({\it{matrix\/}})\index{tsq} $=$ {\rm{car}}\,({\rm{tsq-rec}}\,({\tt{0}}, {\tt{0}}, {\rm{c-init}}\,({\it{matrix\/}})\index{c-init}, {\it{matrix\/}}, {\rm{list}}\,({\tt{0}}, {\tt{0}}, {\tt{0}}))\index{tsq-rec})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  zero-tail-zeroes-lemma \\ \index{zero-tail-zeroes-lemma}
{\rm{nth}}\,({\it{i\/}}, {\rm{zeroes}}\,({\it{n\/}})\index{zeroes})\index{nth} $=$ {\tt{0}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  zero-tail-zeroes \\ \index{zero-tail-zeroes}
{\rm{zero-tail}}\,({\rm{zeroes}}\,({\it{n\/}})\index{zeroes}, {\it{i\/}}, {\it{j\/}})\index{zero-tail}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  correctness-of-tsq \\ \index{correctness-of-tsq}
\=\+(({\rm{length}}\,({\it{matrix\/}})\index{length} $\not=$ {\tt{0}}) $\wedge$ ({\rm{col}}\,({\it{matrix\/}})\index{col} $\not=$ {\tt{0}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{tsquarep}}\,({\rm{tsq-i-coord}}\,({\it{matrix\/}})\index{tsq-i-coord}, {\rm{tsq-j-coord}}\,({\it{matrix\/}})\index{tsq-j-coord}, {\rm{tsq}}\,({\it{matrix\/}})\index{tsq}, {\it{matrix\/}})\index{tsquarep} \\ 
$\wedge$$\;\;\;\;${\rm{in-matrix}}\,({\rm{tsq-i-coord}}\,({\it{matrix\/}})\index{tsq-i-coord}, {\rm{tsq-j-coord}}\,({\it{matrix\/}})\index{tsq-j-coord}, {\it{matrix\/}})\index{in-matrix} \\ 
$\wedge$$\;\;\;\;${\rm{bound}}\,({\rm{length}}\,({\it{matrix\/}})\index{length}, {\tt{0}}, {\it{matrix\/}}, {\rm{tsq}}\,({\it{matrix\/}})\index{tsq})\index{bound})\-\-
\end{tabbing}

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