\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 Yuan Yu.  All Rights Reserved.

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

 NO WARRANTY

 Yuan Yu 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 Yuan Yu 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 library {\tt{"mc20-2"}} using the compiled version.

\addvspace{18pt}
\begin{verbatim};           Proof of the Correctness of a Quicksort Program
;
#|
The following C function QSORT sorts a[left], ..., a[right] into increasing 
order.  The program is a slightly modified version of K&R. 

/* qsort: sort a[left]...a[right] into increasing order.  We use the middle */
/* element of each subarray for partitioning.   */
void qsort (int a[], int left, int right)
{
  int i, last, temp;

  if (left >= right)
    return;
  last = (left + right) / 2;
  temp = a[left];
  a[left] = a[last];
  a[last] = temp;
  last = left;
  for (i = left + 1; i<= right; i++)
    if (a[i] < a[left]){
      temp = a[++last];
      a[last] = a[i];
      a[i] = temp;
    };
  temp = a[left];
  a[left] = a[last];
  a[last] = temp;
  qsort(a, left, last-1);
  qsort(a, last+1, right);
}

Here is the MC68020 assembly code of the above QSORT program.  The code is
generated by "gcc -O".

0x22b8 <qsort>:         linkw fp,#0
0x22bc <qsort+4>:       moveml d2-d4/a2-a3,sp@-
0x22c0 <qsort+8>:       moveal fp@(8),a3
0x22c4 <qsort+12>:      movel fp@(12),d3
0x22c8 <qsort+16>:      movel fp@(16),d4
0x22cc <qsort+20>:      cmpl d3,d4
0x22ce <qsort+22>:      ble 0x2338 <qsort+128>
0x22d0 <qsort+24>:      movel d3,d2
0x22d2 <qsort+26>:      addl d4,d2
0x22d4 <qsort+28>:      bpl 0x22d8 <qsort+32>
0x22d6 <qsort+30>:      addql #1,d2
0x22d8 <qsort+32>:      asrl #1,d2
0x22da <qsort+34>:      movel 0(a3)[d3.l*4],d1
0x22de <qsort+38>:      movel 0(a3)[d2.l*4],0(a3)[d3.l*4]
0x22e4 <qsort+44>:      movel d1,0(a3)[d2.l*4]
0x22e8 <qsort+48>:      movel d3,d2
0x22ea <qsort+50>:      movel d2,d0
0x22ec <qsort+52>:      bra 0x2308 <qsort+80>
0x22ee <qsort+54>:      moveal 0(a3)[d0.l*4],a0
0x22f2 <qsort+58>:      cmpal 0(a3)[d3.l*4],a0
0x22f6 <qsort+62>:      bge 0x2308 <qsort+80>
0x22f8 <qsort+64>:      addql #1,d2
0x22fa <qsort+66>:      movel 0(a3)[d2.l*4],d1
0x22fe <qsort+70>:      movel 0(a3)[d0.l*4],0(a3)[d2.l*4]
0x2304 <qsort+76>:      movel d1,0(a3)[d0.l*4]
0x2308 <qsort+80>:      addql #1,d0
0x230a <qsort+82>:      cmpl d0,d4
0x230c <qsort+84>:      bge 0x22ee <qsort+54>
0x230e <qsort+86>:      movel 0(a3)[d3.l*4],d1
0x2312 <qsort+90>:      movel 0(a3)[d2.l*4],0(a3)[d3.l*4]
0x2318 <qsort+96>:      movel d1,0(a3)[d2.l*4]
0x231c <qsort+100>:     moveal d2,a0
0x231e <qsort+102>:     pea a0@(-1)
0x2322 <qsort+106>:     movel d3,sp@-
0x2324 <qsort+108>:     movel a3,sp@-
0x2326 <qsort+110>:     lea 0x22b8 <qsort>,a2
0x232a <qsort+114>:     jsr a2@
0x232c <qsort+116>:     movel d4,sp@-
0x232e <qsort+118>:     moveal d2,a0
0x2330 <qsort+120>:     pea a0@(1)
0x2334 <qsort+124>:     movel a3,sp@-
0x2336 <qsort+126>:     jsr a2@
0x2338 <qsort+128>:     moveml fp@(-20),d2-d4/a2-a3
0x233e <qsort+134>:     unlk fp
0x2340 <qsort+136>:     rts

The machine code of the above program is:

<qsort>:      0x4e56  0x0000  0x48e7  0x3830  0x266e  0x0008  0x262e  0x000c
<qsort+16>:   0x282e  0x0010  0xb883  0x6f68  0x2403  0xd484  0x6a02  0x5282
<qsort+32>:   0xe282  0x2233  0x3c00  0x27b3  0x2c00  0x3c00  0x2781  0x2c00
<qsort+48>:   0x2403  0x2002  0x601a  0x2073  0x0c00  0xb1f3  0x3c00  0x6c10
<qsort+64>:   0x5282  0x2233  0x2c00  0x27b3  0x0c00  0x2c00  0x2781  0x0c00
<qsort+80>:   0x5280  0xb880  0x6ce0  0x2233  0x3c00  0x27b3  0x2c00  0x3c00
<qsort+96>:   0x2781  0x2c00  0x2042  0x4868  0xffff  0x2f03  0x2f0b  0x45fa
<qsort+112>:  0xff90  0x4e92  0x2f04  0x2042  0x4868  0x0001  0x2f0b  0x4e92
<qsort+128>:  0x4cee  0x0c1c  0xffec  0x4e5e  0x4e75

In the Logic, it looks like:

'(78      86      0       0       72      231     56      48
  38      110     0       8       38      46      0       12
  40      46      0       16      184     131     111     104
  36      3       212     132     106     2       82      130
  226     130     34      51      60      0       39      179
  44      0       60      0       39      129     44      0
  36      3       32      2       96      26      32      115
  12      0       177     243     60      0       108     16
  82      130     34      51      44      0       39      179
  12      0       44      0       39      129     12      0
  82      128     184     128     108     224     34      51
  60      0       39      179     44      0       60      0
  39      129     44      0       32      66      72      104
  255     255     47      3       47      11      69      250
  255     144     78      146     47      4       32      66
  72      104     0       1       47      11      78      146
  76      238     12      28      255     236     78      94
  78      117)
|#

; in the Logic, the above program is defined by (qsort-code).
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{qsort-code} \\  
\=\+{\sc{qsort-code}}\index{qsort-code} \\ 
$=$$\;\;\;\;${\tt{'}}{\tt{(}}\=\+{\tt{78}}{\tt{ }}{\tt{86}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{72}}{\tt{ }}{\tt{231}}{\tt{ }}{\tt{56}}{\tt{ }}{\tt{48}}{\tt{ }}{\tt{38}}{\tt{ }}{\tt{110}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{8}}{\tt{ }}{\tt{38}}{\tt{ }}{\tt{46}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{12}}{\tt{ }}{\tt{40}}{\tt{ }}{\tt{46}}{\tt{ }}{\tt{0}} \\ 
{\tt{16}}{\tt{ }}{\tt{184}}{\tt{ }}{\tt{131}}{\tt{ }}{\tt{111}}{\tt{ }}{\tt{104}}{\tt{ }}{\tt{36}}{\tt{ }}{\tt{3}}{\tt{ }}{\tt{212}}{\tt{ }}{\tt{132}}{\tt{ }}{\tt{106}}{\tt{ }}{\tt{2}}{\tt{ }}{\tt{82}}{\tt{ }}{\tt{130}}{\tt{ }}{\tt{226}}{\tt{ }}{\tt{130}} \\ 
{\tt{34}}{\tt{ }}{\tt{51}}{\tt{ }}{\tt{60}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{39}}{\tt{ }}{\tt{179}}{\tt{ }}{\tt{44}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{60}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{39}}{\tt{ }}{\tt{129}}{\tt{ }}{\tt{44}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{36}}{\tt{ }}{\tt{3}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{2}}{\tt{ }}{\tt{96}} \\ 
{\tt{26}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{115}}{\tt{ }}{\tt{12}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{177}}{\tt{ }}{\tt{243}}{\tt{ }}{\tt{60}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{108}}{\tt{ }}{\tt{16}}{\tt{ }}{\tt{82}}{\tt{ }}{\tt{130}}{\tt{ }}{\tt{34}}{\tt{ }}{\tt{51}}{\tt{ }}{\tt{44}}{\tt{ }}{\tt{0}} \\ 
{\tt{39}}{\tt{ }}{\tt{179}}{\tt{ }}{\tt{12}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{44}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{39}}{\tt{ }}{\tt{129}}{\tt{ }}{\tt{12}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{82}}{\tt{ }}{\tt{128}}{\tt{ }}{\tt{184}}{\tt{ }}{\tt{128}}{\tt{ }}{\tt{108}}{\tt{ }}{\tt{224}} \\ 
{\tt{34}}{\tt{ }}{\tt{51}}{\tt{ }}{\tt{60}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{39}}{\tt{ }}{\tt{179}}{\tt{ }}{\tt{44}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{60}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{39}}{\tt{ }}{\tt{129}}{\tt{ }}{\tt{44}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{66}}{\tt{ }}{\tt{72}}{\tt{ }}{\tt{104}} \\ 
{\tt{255}}{\tt{ }}{\tt{255}}{\tt{ }}{\tt{47}}{\tt{ }}{\tt{3}}{\tt{ }}{\tt{47}}{\tt{ }}{\tt{11}}{\tt{ }}{\tt{69}}{\tt{ }}{\tt{250}}{\tt{ }}{\tt{255}}{\tt{ }}{\tt{144}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{146}}{\tt{ }}{\tt{47}}{\tt{ }}{\tt{4}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{66}} \\ 
{\tt{72}}{\tt{ }}{\tt{104}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{1}}{\tt{ }}{\tt{47}}{\tt{ }}{\tt{11}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{146}}{\tt{ }}{\tt{76}}{\tt{ }}{\tt{238}}{\tt{ }}{\tt{12}}{\tt{ }}{\tt{28}}{\tt{ }}{\tt{255}}{\tt{ }}{\tt{236}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{94}} \\ 
{\tt{78}}{\tt{ }}{\tt{117}}{\tt{)}}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ilessp-lessp \\ \index{ilessp-lessp}
({\it{x\/}} $\in\;${\bf{N}}${}$) $\rightarrow$ ({\rm{ilessp}}\,({\it{x\/}}, {\it{y\/}})\index{ilessp} $=$ ({\it{x\/}} $<$ {\it{y\/}}))
\end{tabbing}


\noindent{\sc Event}:   Disable ilessp.

\addvspace{18pt}

\noindent{\sc Event}:   Enable iplus.

\addvspace{18pt}

\noindent{\sc Event}:   Enable idifference.

\addvspace{18pt}

\noindent{\sc Event}:   Enable iquotient.

\addvspace{18pt}

\begin{verbatim}; qsort is a function in Nqthm that characterizes the functional semantics of 
; the program (qsort-code).
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{qpart-aux} \\  
\=\+{\rm{qpart-aux}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qpart-aux} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{r\/}} $<$ {\it{i\/}}$\;\;${\bf then }{\rm{swap}}\,({\it{l\/}}, {\it{last\/}}, {\it{lst\/}})\index{swap} \\ 
{\bf elseif }{\rm{ilessp}}\,({\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth}, {\rm{get-nth}}\,({\it{l\/}}, {\it{lst\/}})\index{get-nth})\index{ilessp} \\ 
{\bf then }{\rm{qpart-aux}}\,({\it{l\/}}, {\it{r\/}}, {\rm{swap}}\,($1\;+$ {\it{last\/}}, {\it{i\/}}, {\it{lst\/}})\index{swap}, $1\;+$ {\it{last\/}}, $1\;+$ {\it{i\/}})\index{qpart-aux} \\ 
{\bf else }{\rm{qpart-aux}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{last\/}}, $1\;+$ {\it{i\/}})\index{qpart-aux}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{qpart} \\  
{\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qpart} $=$ {\rm{qpart-aux}}\,({\it{l\/}}, {\it{r\/}}, {\rm{swap}}\,({\it{l\/}}, ({\it{l\/}} $+$ {\it{r\/}}) $\div$ {\tt{2}}, {\it{lst\/}})\index{swap}, {\it{l\/}}, $1\;+$ {\it{l\/}})\index{qpart-aux}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{qlast-aux} \\  
\=\+{\rm{qlast-aux}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qlast-aux} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{r\/}} $<$ {\it{i\/}}$\;\;${\bf then }{\rm{fix}}\,({\it{last\/}}) \\ 
{\bf elseif }{\rm{ilessp}}\,({\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth}, {\rm{get-nth}}\,({\it{l\/}}, {\it{lst\/}})\index{get-nth})\index{ilessp} \\ 
{\bf then }{\rm{qlast-aux}}\,({\it{l\/}}, {\it{r\/}}, {\rm{swap}}\,($1\;+$ {\it{last\/}}, {\it{i\/}}, {\it{lst\/}})\index{swap}, $1\;+$ {\it{last\/}}, $1\;+$ {\it{i\/}})\index{qlast-aux} \\ 
{\bf else }{\rm{qlast-aux}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{last\/}}, $1\;+$ {\it{i\/}})\index{qlast-aux}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{qlast} \\  
{\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast} $=$ {\rm{qlast-aux}}\,({\it{l\/}}, {\it{r\/}}, {\rm{swap}}\,({\it{l\/}}, ({\it{l\/}} $+$ {\it{r\/}}) $\div$ {\tt{2}}, {\it{lst\/}})\index{swap}, {\it{l\/}}, $1\;+$ {\it{l\/}})\index{qlast-aux}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qlast-aux-lb \\ \index{qlast-aux-lb}
({\it{left\/}} $\leq$ {\it{last\/}}) $\rightarrow$ ({\rm{qlast-aux}}\,({\it{left\/}}, {\it{right\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qlast-aux} $\not<$ {\it{left\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qlast-lb \\ \index{qlast-lb}
{\rm{qlast}}\,({\it{left\/}}, {\it{right\/}}, {\it{lst\/}})\index{qlast} $\not<$ {\it{left\/}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qlast-aux-ub \\ \index{qlast-aux-ub}
\=\+(({\it{last\/}} $<$ {\it{i\/}}) $\wedge$ ({\it{i\/}} $\leq$ {\it{right\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\it{right\/}} $\not<$ {\rm{qlast-aux}}\,({\it{left\/}}, {\it{right\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qlast-aux})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qlast-ub \\ \index{qlast-ub}
({\it{left\/}} $<$ {\it{right\/}}) $\rightarrow$ ({\it{right\/}} $\not<$ {\rm{qlast}}\,({\it{left\/}}, {\it{right\/}}, {\it{lst\/}})\index{qlast})
\end{tabbing}


\noindent{\sc Event}:   Disable qlast.

\addvspace{18pt}

\noindent{\sc Event}:   Disable qpart.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{qsort} \\  
\=\+{\rm{qsort}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qsort} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{l\/}} $<$ {\it{r\/}} \\ 
{\bf then }{\rm{qsort}}\,(\=\+$1\;+$ {\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast}, \\ 
{\it{r\/}}, \\ 
{\rm{qsort}}\,({\it{l\/}}, {\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast} $-\;1$, {\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qpart})\index{qsort})\-\index{qsort} \\ 
{\bf else }{\it{lst\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; the computation time of the program.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{qpart-aux-t} \\  
\=\+{\rm{qpart-aux-t}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qpart-aux-t} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{r\/}} $<$ {\it{i\/}}$\;\;${\bf then }{\tt{11}} \\ 
{\bf elseif }{\rm{ilessp}}\,({\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth}, {\rm{get-nth}}\,({\it{l\/}}, {\it{lst\/}})\index{get-nth})\index{ilessp} \\ 
{\bf then }{\rm{splus}}\,(\=\+{\tt{10}}, \\ 
{\rm{qpart-aux-t}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\rm{swap}}\,($1\;+$ {\it{last\/}}, {\it{i\/}}, {\it{lst\/}})\index{swap}, $1\;+$ {\it{last\/}}, $1\;+$ {\it{i\/}})\index{qpart-aux-t})\-\index{splus} \\ 
{\bf else }{\rm{splus}}\,({\tt{6}}, {\rm{qpart-aux-t}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{last\/}}, $1\;+$ {\it{i\/}})\index{qpart-aux-t})\index{splus}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{qpart-t} \\  
\=\+{\rm{qpart-t}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qpart-t} \\ 
$=$$\;\;\;\;$\=\+{\bf let }\=\+{\it{lst1\/}}{\bf $\;$ be$\;\;$}{\rm{swap}}\,({\it{l\/}}, ({\it{l\/}} $+$ {\it{r\/}}) $\div$ {\tt{2}}, {\it{lst\/}})\index{swap}\- \\ 
{\bf in} \\ 
{\rm{splus}}\,({\tt{18}}, {\rm{qpart-aux-t}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst1\/}}, {\it{l\/}}, $1\;+$ {\it{l\/}})\index{qpart-aux-t})\index{splus}$\;${\bf  endlet}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{qsort-10}$\;\;$
{\rm{qsort-10}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-10} $=$ {\tt{10}}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{qsort-5}$\;\;$
{\rm{qsort-5}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-5} $=$ {\tt{5}}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{qsort-3}$\;\;$
{\rm{qsort-3}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-3} $=$ {\tt{3}}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{qsort-t} \\  
\=\+{\rm{qsort-t}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-t} \\ 
$=$$\;\;\;\;$\=\+{\bf let }\=\+{\it{last\/}}{\bf $\;$ be$\;\;$}{\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast}, \\ 
{\it{qlst\/}}{\bf $\;$ be$\;\;$}{\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qpart}\- \\ 
{\bf in} \\ 
\=\+{\bf if }{\it{l\/}} $<$ {\it{r\/}} \\ 
{\bf then }{\rm{splus}}\,(\=\+{\rm{qpart-t}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qpart-t}, \\ 
{\rm{splus}}\,(\=\+{\rm{qsort-t}}\,({\it{a\/}}, {\it{l\/}}, {\it{last\/}} $-\;1$, {\it{n\/}}, {\it{qlst\/}})\index{qsort-t}, \\ 
{\rm{splus}}\,(\=\+{\rm{qsort-5}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-5}, \\ 
{\rm{splus}}\,(\=\+{\rm{qsort-t}}\,(\=\+{\it{a\/}}, \\ 
$1\;+$ {\it{last\/}}, \\ 
{\it{r\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{qsort}}\,({\it{l\/}}, {\it{last\/}} $-\;1$, {\it{qlst\/}})\index{qsort})\-\index{qsort-t}, \\ 
{\rm{qsort-3}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-3})\-\index{splus})\-\index{splus})\-\index{splus})\-\index{splus} \\ 
{\bf else }{\rm{qsort-10}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-10}$\;${\bf  endif}\-$\;${\bf  endlet}\-\-
\end{tabbing}

\begin{verbatim}; an induction hint.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{qsort-induct} \\  
\=\+{\rm{qsort-induct}}\,({\it{s\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-induct} \\ 
$=$$\;\;\;\;$\=\+{\bf let }\=\+{\it{last\/}}{\bf $\;$ be$\;\;$}{\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast}, \\ 
{\it{qlst\/}}{\bf $\;$ be$\;\;$}{\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qpart}\- \\ 
{\bf in} \\ 
\=\+{\bf if }{\it{l\/}} $<$ {\it{r\/}} \\ 
{\bf then }\=\+{\rm{qsort-induct}}\,(\=\+{\rm{stepn}}\,({\it{s\/}}, {\rm{qpart-t}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qpart-t})\index{stepn}, \\ 
{\it{a\/}}, \\ 
{\it{l\/}}, \\ 
{\rm{idifference}}\,({\it{last\/}}, {\tt{1}})\index{idifference}, \\ 
{\it{n\/}}, \\ 
{\it{qlst\/}})\-\index{qsort-induct} \\ 
$\wedge$$\;\;\;\;${\rm{qsort-induct}}\,(\=\+{\rm{stepn}}\,(\=\+{\it{s\/}}, \\ 
{\rm{splus}}\,(\=\+{\rm{qpart-t}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qpart-t}, \\ 
{\rm{splus}}\,(\=\+{\rm{qsort-t}}\,(\=\+{\it{a\/}}, \\ 
{\it{l\/}}, \\ 
{\it{last\/}} $-\;1$, \\ 
{\it{n\/}}, \\ 
{\it{qlst\/}})\-\index{qsort-t}, \\ 
{\rm{qsort-5}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-5})\-\index{splus})\-\index{splus})\-\index{stepn}, \\ 
{\it{a\/}}, \\ 
$1\;+$ {\it{last\/}}, \\ 
{\it{r\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{qsort}}\,({\it{l\/}}, {\it{last\/}} $-\;1$, {\it{qlst\/}})\index{qsort})\-\index{qsort-induct}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-$\;${\bf  endlet}\-\-
\end{tabbing}

\begin{verbatim}; the preconditions of the initial state.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{qstack} \\  
\=\+{\rm{qstack}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qstack} \\ 
$=$$\;\;\;\;$\=\+{\bf let }\=\+{\it{last\/}}{\bf $\;$ be$\;\;$}{\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast}, \\ 
{\it{lst1\/}}{\bf $\;$ be$\;\;$}{\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qpart}\- \\ 
{\bf in} \\ 
\=\+{\bf if }{\it{l\/}} $<$ {\it{r\/}} \\ 
{\bf then }{\rm{max}}\,(\=\+{\tt{40}} $+$ {\rm{qstack}}\,({\it{l\/}}, {\it{last\/}} $-\;1$, {\it{lst1\/}})\index{qstack}, \\ 
{\tt{52}} $+$ {\rm{qstack}}\,($1\;+$ {\it{last\/}}, {\it{r\/}}, {\rm{qsort}}\,({\it{l\/}}, {\it{last\/}} $-\;1$, {\it{lst1\/}})\index{qsort})\index{qstack})\- \\ 
{\bf else }{\tt{68}}$\;${\bf  endif}\-$\;${\bf  endlet}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qstack-la0 \\ \index{qstack-la0}
{\rm{qstack}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qstack} $\not<$ {\tt{68}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qstack-la1 \\ \index{qstack-la1}
\=\+{\bf let }\=\+{\it{last\/}}{\bf $\;$ be$\;\;$}{\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast}, \\ 
{\it{lst1\/}}{\bf $\;$ be$\;\;$}{\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qpart}\- \\ 
{\bf in} \\ 
\=\+({\it{l\/}} $<$ {\it{r\/}}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{qstack}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qstack} $\not<$ ({\tt{40}} $+$ {\rm{qstack}}\,({\it{l\/}}, {\it{last\/}} $-\;1$, {\it{lst1\/}})\index{qstack}))\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qstack-la2 \\ \index{qstack-la2}
\=\+{\bf let }\=\+{\it{last\/}}{\bf $\;$ be$\;\;$}{\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast}, \\ 
{\it{lst1\/}}{\bf $\;$ be$\;\;$}{\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qpart}\- \\ 
{\bf in} \\ 
\=\+({\it{l\/}} $<$ {\it{r\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{qstack}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qstack} \\ 
$\not<$$\;\;\;\;$({\tt{52}} $+$ {\rm{qstack}}\,($1\;+$ {\it{last\/}}, {\it{r\/}}, {\rm{qsort}}\,({\it{l\/}}, {\it{last\/}} $-\;1$, {\it{lst1\/}})\index{qsort})\index{qstack}))\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim}; an upper bound of stack space.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  qstack-ubound-la-1 \\ \index{qstack-ubound-la-1}
\=\+({\it{l\/}} $<$ {\it{r\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\tt{52}} $*$ ({\it{r\/}} $-$ {\it{l\/}})) \\ 
$\not<$$\;\;\;\;$({\tt{52}} $+$ ({\tt{52}} $*$ (({\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast} $-\;1$) $-$ {\it{l\/}}))))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qstack-ubound-la-2 \\ \index{qstack-ubound-la-2}
\=\+({\it{l\/}} $<$ {\it{r\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\tt{52}} $*$ ({\it{r\/}} $-$ {\it{l\/}})) \\ 
$\not<$$\;\;\;\;$({\tt{52}} $+$ ({\tt{52}} $*$ ({\it{r\/}} $-$ ($1\;+$ {\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast})))))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qstack-ubound \\ \index{qstack-ubound}
{\rm{qstack}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qstack} $\leq$ ({\tt{68}} $+$ ({\tt{52}} $*$ ({\it{r\/}} $-$ {\it{l\/}})))
\end{tabbing}


\noindent{\sc Event}:   Disable qstack.

\addvspace{18pt}

\begin{verbatim}; the initial state.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{qsort-statep} \\  
\=\+{\rm{qsort-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-statep} \\ 
$=$$\;\;\;\;$\=\+{\bf let }\=\+{\it{sp\/}}{\bf $\;$ be$\;\;$}{\rm{sub}}\,({\tt{32}}, {\rm{qstack}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qstack} $-$ {\tt{16}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}\- \\ 
{\bf in} \\ 
\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{evenp}}\,({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{evenp} \\ 
$\wedge$$\;\;\;\;${\rm{rom-addrp}}\,({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{138}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{qsort-code}}\index{qsort-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\it{a\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}} $*$ {\it{n\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mem-ilst}}\,({\tt{4}}, {\it{a\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n\/}}, {\it{lst\/}})\index{mem-ilst} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\it{sp\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\rm{qstack}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qstack})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{a\/}}, {\tt{4}} $*$ {\it{n\/}}, {\it{sp\/}}, {\rm{qstack}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qstack})\index{disjoint} \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $=$ {\rm{read-mem}}\,({\rm{add}}\,({\tt{32}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\tt{4}})\index{add}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{read-mem}) \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $=$ {\rm{iread-mem}}\,({\rm{add}}\,({\tt{32}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\tt{8}})\index{add}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{iread-mem}) \\ 
$\wedge$$\;\;\;\;$({\it{r\/}} $=$ {\rm{iread-mem}}\,({\rm{add}}\,({\tt{32}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\tt{12}})\index{add}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{iread-mem}) \\ 
$\wedge$$\;\;\;\;$({\rm{qstack}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qstack} $<$ {\rm{exp}}\,({\tt{2}}, {\tt{32}})\index{exp}) \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{r\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\tt{4}} $*$ {\it{n\/}}, {\tt{32}})\index{uint-rangep}\-$\;${\bf  endlet}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{qsort-sp} \\  
\=\+{\rm{qsort-sp}}\,({\it{s\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-sp} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{evenp}}\,({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{evenp} \\ 
$\wedge$$\;\;\;\;${\rm{rom-addrp}}\,({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{138}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{qsort-code}}\index{qsort-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\it{a\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}} $*$ {\it{n\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mem-ilst}}\,({\tt{4}}, {\it{a\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n\/}}, {\it{lst\/}})\index{mem-ilst} \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $=$ {\rm{read-mem}}\,({\rm{add}}\,({\tt{32}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\tt{4}})\index{add}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{read-mem}) \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $=$ {\rm{iread-mem}}\,({\rm{add}}\,({\tt{32}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\tt{8}})\index{add}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{iread-mem}) \\ 
$\wedge$$\;\;\;\;$({\it{r\/}} $=$ {\rm{iread-mem}}\,({\rm{add}}\,({\tt{32}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\tt{12}})\index{add}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{iread-mem}) \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{r\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{int-rangep}}\,({\it{n\/}}, {\tt{32}})\index{int-rangep} \\ 
$\wedge$$\;\;\;\;${\rm{int-rangep}}\,({\tt{2}} $*$ {\it{r\/}}, {\tt{32}})\index{int-rangep} \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\tt{4}} $*$ {\it{n\/}}, {\tt{32}})\index{uint-rangep} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{52}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{68}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{a\/}}, {\tt{4}} $*$ {\it{n\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{52}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{68}})\index{disjoint})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-statep-sp \\ \index{qsort-statep-sp}
{\rm{qsort-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-statep} $\rightarrow$ {\rm{qsort-sp}}\,({\it{s\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-sp}
\end{tabbing}

\begin{verbatim}; the conditions of the intermediate state s0.  s0 is the state of the 
; machine right before the for statement in the corresponding C program.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{qsort-s0p} \\  
\=\+{\rm{qsort-s0p}}\,({\it{s\/}}, {\it{s0\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qsort-s0p} \\ 
$=$$\;\;\;\;$(\=\+({\rm{linked-rts-addr}}\,({\it{s0\/}})\index{linked-rts-addr} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\it{s0\/}})\index{linked-a6} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s0\/}})\index{mc-rfile})\index{read-rn}, {\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub})\index{equal*} \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\it{s0\/}})\index{mc-rfile})\index{read-rn}, {\rm{sub}}\,({\tt{32}}, {\tt{24}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub})\index{equal*} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{movem-saved}}\,({\it{s0\/}}, {\tt{4}}, {\tt{20}}, {\tt{5}})\index{movem-saved} \\ 
$=$$\;\;\;\;${\rm{readm-rn}}\,({\tt{32}}, {\tt{'}}{\tt{(}}{\tt{2}}{\tt{ }}{\tt{3}}{\tt{ }}{\tt{4}}{\tt{ }}{\tt{10}}{\tt{ }}{\tt{11}}{\tt{)}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{readm-rn})\- \\ 
$\wedge$$\;\;\;\;$({\rm{mc-status}}\,({\it{s0\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{evenp}}\,({\rm{mc-pc}}\,({\it{s0\/}})\index{mc-pc})\index{evenp} \\ 
$\wedge$$\;\;\;\;${\rm{rom-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{82}}, {\rm{mc-pc}}\,({\it{s0\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s0\/}})\index{mc-mem}, {\tt{138}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{82}}, {\rm{mc-pc}}\,({\it{s0\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s0\/}})\index{mc-mem}, {\sc{qsort-code}}\index{qsort-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{52}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\rm{mc-mem}}\,({\it{s0\/}})\index{mc-mem}, {\tt{68}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\it{a\/}}, {\rm{mc-mem}}\,({\it{s0\/}})\index{mc-mem}, {\tt{4}} $*$ {\it{n\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mem-ilst}}\,({\tt{4}}, {\it{a\/}}, {\rm{mc-mem}}\,({\it{s0\/}})\index{mc-mem}, {\it{n\/}}, {\it{lst\/}})\index{mem-ilst} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{a\/}}, {\tt{4}} $*$ {\it{n\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{52}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{68}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{3}}, {\it{s0\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $=$ {\rm{nat-to-int}}\,({\rm{read-rn}}\,({\tt{32}}, {\tt{3}}, {\rm{mc-rfile}}\,({\it{s0\/}})\index{mc-rfile})\index{read-rn}, {\tt{32}})\index{nat-to-int}) \\ 
$\wedge$$\;\;\;\;$({\it{r\/}} $=$ {\rm{nat-to-int}}\,({\rm{read-rn}}\,({\tt{32}}, {\tt{4}}, {\rm{mc-rfile}}\,({\it{s0\/}})\index{mc-rfile})\index{read-rn}, {\tt{32}})\index{nat-to-int}) \\ 
$\wedge$$\;\;\;\;$({\it{last\/}} $=$ {\rm{nat-to-int}}\,({\rm{read-rn}}\,({\tt{32}}, {\tt{2}}, {\rm{mc-rfile}}\,({\it{s0\/}})\index{mc-rfile})\index{read-rn}, {\tt{32}})\index{nat-to-int}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $=$ {\rm{nat-to-int}}\,({\rm{read-rn}}\,({\tt{32}}, {\tt{0}}, {\rm{mc-rfile}}\,({\it{s0\/}})\index{mc-rfile})\index{read-rn}, {\tt{32}})\index{nat-to-int}) \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{r\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{last\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $<$ {\it{r\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{last\/}} $<$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\leq$ ($1\;+$ {\it{r\/}})) \\ 
$\wedge$$\;\;\;\;$({\it{r\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{int-rangep}}\,({\it{n\/}}, {\tt{32}})\index{int-rangep} \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\tt{4}} $*$ {\it{n\/}}, {\tt{32}})\index{uint-rangep})\-\-
\end{tabbing}

\begin{verbatim}; the conditions of the intermediate state s1.  s1 is the machine 
; state after the execution of the first JSR instruction, but before
; the recursive execution of QSORT.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{qsort-s1p} \\  
\=\+{\rm{qsort-s1p}}\,({\it{s\/}}, {\it{s1\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{last\/}})\index{qsort-s1p} \\ 
$=$$\;\;\;\;$(\=\+({\rm{linked-rts-addr}}\,({\it{s1\/}})\index{linked-rts-addr} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\it{s1\/}})\index{linked-a6} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s1\/}})\index{mc-rfile})\index{read-rn}, {\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub})\index{equal*} \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\it{s1\/}})\index{mc-rfile})\index{read-rn}, {\rm{sub}}\,({\tt{32}}, {\tt{40}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub})\index{equal*} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{movem-saved}}\,({\it{s1\/}}, {\tt{4}}, {\tt{20}}, {\tt{5}})\index{movem-saved} \\ 
$=$$\;\;\;\;${\rm{readm-rn}}\,({\tt{32}}, {\tt{'}}{\tt{(}}{\tt{2}}{\tt{ }}{\tt{3}}{\tt{ }}{\tt{4}}{\tt{ }}{\tt{10}}{\tt{ }}{\tt{11}}{\tt{)}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{readm-rn})\- \\ 
$\wedge$$\;\;\;\;$({\rm{mc-status}}\,({\it{s1\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{s1\/}})\index{mc-pc} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{2}}, {\it{s1\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;${\rm{evenp}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{2}}, {\it{s1\/}})\index{read-an})\index{evenp} \\ 
$\wedge$$\;\;\;\;${\rm{evenp}}\,({\rm{rts-addr}}\,({\it{s1\/}})\index{rts-addr})\index{evenp} \\ 
$\wedge$$\;\;\;\;${\rm{rom-addrp}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{2}}, {\it{s1\/}})\index{read-an}, {\rm{mc-mem}}\,({\it{s1\/}})\index{mc-mem}, {\tt{138}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{2}}, {\it{s1\/}})\index{read-an}, {\rm{mc-mem}}\,({\it{s1\/}})\index{mc-mem}, {\sc{qsort-code}}\index{qsort-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{rom-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{116}}, {\rm{rts-addr}}\,({\it{s1\/}})\index{rts-addr})\index{sub}, {\rm{mc-mem}}\,({\it{s1\/}})\index{mc-mem}, {\tt{138}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{116}}, {\rm{rts-addr}}\,({\it{s1\/}})\index{rts-addr})\index{sub}, {\rm{mc-mem}}\,({\it{s1\/}})\index{mc-mem}, {\sc{qsort-code}}\index{qsort-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{52}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\rm{mc-mem}}\,({\it{s1\/}})\index{mc-mem}, {\tt{68}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\it{a\/}}, {\rm{mc-mem}}\,({\it{s1\/}})\index{mc-mem}, {\tt{4}} $*$ {\it{n\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mem-ilst}}\,({\tt{4}}, {\it{a\/}}, {\rm{mc-mem}}\,({\it{s1\/}})\index{mc-mem}, {\it{n\/}}, {\it{lst\/}})\index{mem-ilst} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{a\/}}, {\tt{4}} $*$ {\it{n\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{52}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{68}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{3}}, {\it{s1\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $=$ {\rm{nat-to-int}}\,({\rm{read-rn}}\,({\tt{32}}, {\tt{3}}, {\rm{mc-rfile}}\,({\it{s1\/}})\index{mc-rfile})\index{read-rn}, {\tt{32}})\index{nat-to-int}) \\ 
$\wedge$$\;\;\;\;$({\it{r\/}} $=$ {\rm{nat-to-int}}\,({\rm{read-rn}}\,({\tt{32}}, {\tt{4}}, {\rm{mc-rfile}}\,({\it{s1\/}})\index{mc-rfile})\index{read-rn}, {\tt{32}})\index{nat-to-int}) \\ 
$\wedge$$\;\;\;\;$({\it{last\/}} $=$ {\rm{nat-to-int}}\,({\rm{read-rn}}\,({\tt{32}}, {\tt{2}}, {\rm{mc-rfile}}\,({\it{s1\/}})\index{mc-rfile})\index{read-rn}, {\tt{32}})\index{nat-to-int}) \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $=$ {\rm{read-mem}}\,({\rm{add}}\,({\tt{32}}, {\rm{read-sp}}\,({\it{s1\/}})\index{read-sp}, {\tt{4}})\index{add}, {\rm{mc-mem}}\,({\it{s1\/}})\index{mc-mem}, {\tt{4}})\index{read-mem}) \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $=$ {\rm{iread-mem}}\,({\rm{add}}\,({\tt{32}}, {\rm{read-sp}}\,({\it{s1\/}})\index{read-sp}, {\tt{8}})\index{add}, {\rm{mc-mem}}\,({\it{s1\/}})\index{mc-mem}, {\tt{4}})\index{iread-mem}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{iread-mem}}\,({\rm{add}}\,({\tt{32}}, {\rm{read-sp}}\,({\it{s1\/}})\index{read-sp}, {\tt{12}})\index{add}, {\rm{mc-mem}}\,({\it{s1\/}})\index{mc-mem}, {\tt{4}})\index{iread-mem} \\ 
$=$$\;\;\;\;${\rm{idifference}}\,({\it{last\/}}, {\tt{1}})\index{idifference})\- \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{r\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{last\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $<$ {\it{r\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{last\/}} $\leq$ {\it{r\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{r\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{int-rangep}}\,({\it{n\/}}, {\tt{32}})\index{int-rangep} \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\tt{4}} $*$ {\it{n\/}}, {\tt{32}})\index{uint-rangep})\-\-
\end{tabbing}

\begin{verbatim}; the conditions of the intermediate state s2.  s2 is the machine 
; state right after the first recursive call to QSORT.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{qsort-s2p} \\  
\=\+{\rm{qsort-s2p}}\,({\it{s\/}}, {\it{s2\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{last\/}})\index{qsort-s2p} \\ 
$=$$\;\;\;\;$(\=\+({\rm{linked-rts-addr}}\,({\it{s2\/}})\index{linked-rts-addr} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\it{s2\/}})\index{linked-a6} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s2\/}})\index{mc-rfile})\index{read-rn}, {\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub})\index{equal*} \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\it{s2\/}})\index{mc-rfile})\index{read-rn}, {\rm{sub}}\,({\tt{32}}, {\tt{36}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub})\index{equal*} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{movem-saved}}\,({\it{s2\/}}, {\tt{4}}, {\tt{20}}, {\tt{5}})\index{movem-saved} \\ 
$=$$\;\;\;\;${\rm{readm-rn}}\,({\tt{32}}, {\tt{'}}{\tt{(}}{\tt{2}}{\tt{ }}{\tt{3}}{\tt{ }}{\tt{4}}{\tt{ }}{\tt{10}}{\tt{ }}{\tt{11}}{\tt{)}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{readm-rn})\- \\ 
$\wedge$$\;\;\;\;$({\rm{mc-status}}\,({\it{s2\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{evenp}}\,({\rm{mc-pc}}\,({\it{s2\/}})\index{mc-pc})\index{evenp} \\ 
$\wedge$$\;\;\;\;${\rm{evenp}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{2}}, {\it{s2\/}})\index{read-an})\index{evenp} \\ 
$\wedge$$\;\;\;\;${\rm{rom-addrp}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{2}}, {\it{s2\/}})\index{read-an}, {\rm{mc-mem}}\,({\it{s2\/}})\index{mc-mem}, {\tt{138}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{2}}, {\it{s2\/}})\index{read-an}, {\rm{mc-mem}}\,({\it{s2\/}})\index{mc-mem}, {\sc{qsort-code}}\index{qsort-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{rom-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{116}}, {\rm{mc-pc}}\,({\it{s2\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s2\/}})\index{mc-mem}, {\tt{138}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{116}}, {\rm{mc-pc}}\,({\it{s2\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s2\/}})\index{mc-mem}, {\sc{qsort-code}}\index{qsort-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{16}}, {\rm{read-sp}}\,({\it{s2\/}})\index{read-sp})\index{sub}, {\rm{mc-mem}}\,({\it{s2\/}})\index{mc-mem}, {\tt{68}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\it{a\/}}, {\rm{mc-mem}}\,({\it{s2\/}})\index{mc-mem}, {\tt{4}} $*$ {\it{n\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mem-ilst}}\,({\tt{4}}, {\it{a\/}}, {\rm{mc-mem}}\,({\it{s2\/}})\index{mc-mem}, {\it{n\/}}, {\it{lst\/}})\index{mem-ilst} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{a\/}}, {\tt{4}} $*$ {\it{n\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{16}}, {\rm{read-sp}}\,({\it{s2\/}})\index{read-sp})\index{sub}, {\tt{68}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{3}}, {\it{s2\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $=$ {\rm{nat-to-int}}\,({\rm{read-rn}}\,({\tt{32}}, {\tt{3}}, {\rm{mc-rfile}}\,({\it{s2\/}})\index{mc-rfile})\index{read-rn}, {\tt{32}})\index{nat-to-int}) \\ 
$\wedge$$\;\;\;\;$({\it{r\/}} $=$ {\rm{nat-to-int}}\,({\rm{read-rn}}\,({\tt{32}}, {\tt{4}}, {\rm{mc-rfile}}\,({\it{s2\/}})\index{mc-rfile})\index{read-rn}, {\tt{32}})\index{nat-to-int}) \\ 
$\wedge$$\;\;\;\;$({\it{last\/}} $=$ {\rm{nat-to-int}}\,({\rm{read-rn}}\,({\tt{32}}, {\tt{2}}, {\rm{mc-rfile}}\,({\it{s2\/}})\index{mc-rfile})\index{read-rn}, {\tt{32}})\index{nat-to-int}) \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{r\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{last\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $<$ {\it{r\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{last\/}} $\leq$ {\it{r\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{r\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{int-rangep}}\,({\it{n\/}}, {\tt{32}})\index{int-rangep} \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\tt{4}} $*$ {\it{n\/}}, {\tt{32}})\index{uint-rangep})\-\-
\end{tabbing}

\begin{verbatim}; the conditions of the intermediate state s3.  s3 is the machine 
; state right after the execution of the second JSR instruction, but 
; before the execution of QSORT.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{qsort-s3p} \\  
\=\+{\rm{qsort-s3p}}\,({\it{s\/}}, {\it{s3\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{last\/}})\index{qsort-s3p} \\ 
$=$$\;\;\;\;$(\=\+({\rm{linked-rts-addr}}\,({\it{s3\/}})\index{linked-rts-addr} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\it{s3\/}})\index{linked-a6} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s3\/}})\index{mc-rfile})\index{read-rn}, {\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub})\index{equal*} \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\it{s3\/}})\index{mc-rfile})\index{read-rn}, {\rm{sub}}\,({\tt{32}}, {\tt{52}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub})\index{equal*} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{movem-saved}}\,({\it{s3\/}}, {\tt{4}}, {\tt{20}}, {\tt{5}})\index{movem-saved} \\ 
$=$$\;\;\;\;${\rm{readm-rn}}\,({\tt{32}}, {\tt{'}}{\tt{(}}{\tt{2}}{\tt{ }}{\tt{3}}{\tt{ }}{\tt{4}}{\tt{ }}{\tt{10}}{\tt{ }}{\tt{11}}{\tt{)}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{readm-rn})\- \\ 
$\wedge$$\;\;\;\;$({\rm{mc-status}}\,({\it{s3\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{s3\/}})\index{mc-pc} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{2}}, {\it{s3\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;${\rm{evenp}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{2}}, {\it{s3\/}})\index{read-an})\index{evenp} \\ 
$\wedge$$\;\;\;\;${\rm{evenp}}\,({\rm{rts-addr}}\,({\it{s3\/}})\index{rts-addr})\index{evenp} \\ 
$\wedge$$\;\;\;\;${\rm{rom-addrp}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{2}}, {\it{s3\/}})\index{read-an}, {\rm{mc-mem}}\,({\it{s3\/}})\index{mc-mem}, {\tt{138}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{2}}, {\it{s3\/}})\index{read-an}, {\rm{mc-mem}}\,({\it{s3\/}})\index{mc-mem}, {\sc{qsort-code}}\index{qsort-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{rom-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{128}}, {\rm{rts-addr}}\,({\it{s3\/}})\index{rts-addr})\index{sub}, {\rm{mc-mem}}\,({\it{s3\/}})\index{mc-mem}, {\tt{138}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{128}}, {\rm{rts-addr}}\,({\it{s3\/}})\index{rts-addr})\index{sub}, {\rm{mc-mem}}\,({\it{s3\/}})\index{mc-mem}, {\sc{qsort-code}}\index{qsort-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{read-sp}}\,({\it{s3\/}})\index{read-sp}, {\rm{mc-mem}}\,({\it{s3\/}})\index{mc-mem}, {\tt{68}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\it{a\/}}, {\rm{mc-mem}}\,({\it{s3\/}})\index{mc-mem}, {\tt{4}} $*$ {\it{n\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mem-ilst}}\,({\tt{4}}, {\it{a\/}}, {\rm{mc-mem}}\,({\it{s3\/}})\index{mc-mem}, {\it{n\/}}, {\it{lst\/}})\index{mem-ilst} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{a\/}}, {\tt{4}} $*$ {\it{n\/}}, {\rm{read-sp}}\,({\it{s3\/}})\index{read-sp}, {\tt{68}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{3}}, {\it{s3\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $=$ {\rm{nat-to-int}}\,({\rm{read-rn}}\,({\tt{32}}, {\tt{3}}, {\rm{mc-rfile}}\,({\it{s3\/}})\index{mc-rfile})\index{read-rn}, {\tt{32}})\index{nat-to-int}) \\ 
$\wedge$$\;\;\;\;$({\it{r\/}} $=$ {\rm{nat-to-int}}\,({\rm{read-rn}}\,({\tt{32}}, {\tt{4}}, {\rm{mc-rfile}}\,({\it{s3\/}})\index{mc-rfile})\index{read-rn}, {\tt{32}})\index{nat-to-int}) \\ 
$\wedge$$\;\;\;\;$({\it{last\/}} $=$ {\rm{nat-to-int}}\,({\rm{read-rn}}\,({\tt{32}}, {\tt{2}}, {\rm{mc-rfile}}\,({\it{s3\/}})\index{mc-rfile})\index{read-rn}, {\tt{32}})\index{nat-to-int}) \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $=$ {\rm{read-mem}}\,({\rm{add}}\,({\tt{32}}, {\rm{read-sp}}\,({\it{s3\/}})\index{read-sp}, {\tt{4}})\index{add}, {\rm{mc-mem}}\,({\it{s3\/}})\index{mc-mem}, {\tt{4}})\index{read-mem}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{iread-mem}}\,({\rm{add}}\,({\tt{32}}, {\rm{read-sp}}\,({\it{s3\/}})\index{read-sp}, {\tt{8}})\index{add}, {\rm{mc-mem}}\,({\it{s3\/}})\index{mc-mem}, {\tt{4}})\index{iread-mem} \\ 
$=$$\;\;\;\;$($1\;+$ {\it{last\/}}))\- \\ 
$\wedge$$\;\;\;\;$({\it{r\/}} $=$ {\rm{iread-mem}}\,({\rm{add}}\,({\tt{32}}, {\rm{read-sp}}\,({\it{s3\/}})\index{read-sp}, {\tt{12}})\index{add}, {\rm{mc-mem}}\,({\it{s3\/}})\index{mc-mem}, {\tt{4}})\index{iread-mem}) \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{r\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{last\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $<$ {\it{r\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{last\/}} $\leq$ {\it{r\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{r\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{int-rangep}}\,({\it{n\/}}, {\tt{32}})\index{int-rangep} \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\tt{4}} $*$ {\it{n\/}}, {\tt{32}})\index{uint-rangep})\-\-
\end{tabbing}

\begin{verbatim}; the conditions of the intermediate state s4.  s4 is the machine
; state right after the second recursive call to QSORT.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{qsort-s4p} \\  
\=\+{\rm{qsort-s4p}}\,({\it{s\/}}, {\it{s4\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-s4p} \\ 
$=$$\;\;\;\;$(\=\+({\rm{linked-rts-addr}}\,({\it{s4\/}})\index{linked-rts-addr} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\it{s4\/}})\index{linked-a6} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s4\/}})\index{mc-rfile})\index{read-rn}, {\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub})\index{equal*} \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\it{s4\/}})\index{mc-rfile})\index{read-rn}, {\rm{sub}}\,({\tt{32}}, {\tt{48}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub})\index{equal*} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{movem-saved}}\,({\it{s4\/}}, {\tt{4}}, {\tt{20}}, {\tt{5}})\index{movem-saved} \\ 
$=$$\;\;\;\;${\rm{readm-rn}}\,({\tt{32}}, {\tt{'}}{\tt{(}}{\tt{2}}{\tt{ }}{\tt{3}}{\tt{ }}{\tt{4}}{\tt{ }}{\tt{10}}{\tt{ }}{\tt{11}}{\tt{)}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{readm-rn})\- \\ 
$\wedge$$\;\;\;\;$({\rm{mc-status}}\,({\it{s4\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{evenp}}\,({\rm{mc-pc}}\,({\it{s4\/}})\index{mc-pc})\index{evenp} \\ 
$\wedge$$\;\;\;\;${\rm{rom-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{128}}, {\rm{mc-pc}}\,({\it{s4\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s4\/}})\index{mc-mem}, {\tt{138}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{128}}, {\rm{mc-pc}}\,({\it{s4\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s4\/}})\index{mc-mem}, {\sc{qsort-code}}\index{qsort-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{48}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s4\/}})\index{read-an})\index{sub}, {\rm{mc-mem}}\,({\it{s4\/}})\index{mc-mem}, {\tt{68}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\it{a\/}}, {\rm{mc-mem}}\,({\it{s4\/}})\index{mc-mem}, {\tt{4}} $*$ {\it{n\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mem-ilst}}\,({\tt{4}}, {\it{a\/}}, {\rm{mc-mem}}\,({\it{s4\/}})\index{mc-mem}, {\it{n\/}}, {\it{lst\/}})\index{mem-ilst} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{a\/}}, {\tt{4}} $*$ {\it{n\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{48}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s4\/}})\index{read-an})\index{sub}, {\tt{68}})\index{disjoint})\-\-
\end{tabbing}

\begin{verbatim}; the conditions of the final state.  s5 is the machine state after
; the execution of this QSORT program.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{qsort-s5p} \\  
\=\+{\rm{qsort-s5p}}\,({\it{s\/}}, {\it{s5\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-s5p} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s5\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{s5\/}})\index{mc-pc} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s5\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\- \\ 
$\wedge$$\;\;\;\;$({\rm{read-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\it{s5\/}})\index{mc-rfile})\index{read-rn} $=$ {\rm{add}}\,({\tt{32}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\tt{4}})\index{add}) \\ 
$\wedge$$\;\;\;\;${\rm{mem-ilst}}\,({\tt{4}}, {\it{a\/}}, {\rm{mc-mem}}\,({\it{s5\/}})\index{mc-mem}, {\it{n\/}}, {\it{lst\/}})\index{mem-ilst} \\ 
$\wedge$$\;\;\;\;$({\rm{read-dn}}\,({\tt{32}}, {\tt{2}}, {\it{s5\/}})\index{read-dn} $=$ {\rm{read-dn}}\,({\tt{32}}, {\tt{2}}, {\it{s\/}})\index{read-dn}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-dn}}\,({\tt{32}}, {\tt{3}}, {\it{s5\/}})\index{read-dn} $=$ {\rm{read-dn}}\,({\tt{32}}, {\tt{3}}, {\it{s\/}})\index{read-dn}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-dn}}\,({\tt{32}}, {\tt{4}}, {\it{s5\/}})\index{read-dn} $=$ {\rm{read-dn}}\,({\tt{32}}, {\tt{4}}, {\it{s\/}})\index{read-dn}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-an}}\,({\tt{32}}, {\tt{2}}, {\it{s5\/}})\index{read-an} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{2}}, {\it{s\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-an}}\,({\tt{32}}, {\tt{3}}, {\it{s5\/}})\index{read-an} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{3}}, {\it{s\/}})\index{read-an}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{qsort-sk} \\  
\=\+{\rm{qsort-sk}}\,({\it{s\/}}, {\it{s5\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-sk} \\ 
$\leftrightarrow$$\;\;\;\;$$\forall\;${\it{x\/}}, {\it{k\/}}$\;$\=\+{\bf let }\=\+{\it{sp\/}}{\bf $\;$ be$\;\;$}{\rm{sub}}\,({\tt{32}}, {\rm{qstack}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qstack} $-$ {\tt{16}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{disjoint}}\,({\it{sp\/}}, {\rm{qstack}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qstack}, {\it{x\/}}, {\it{k\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{a\/}}, {\tt{4}} $*$ {\it{n\/}}, {\it{x\/}}, {\it{k\/}})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s5\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem} \\ 
$=$$\;\;\;\;${\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-\-$\;${\bf  endlet}\-\index{forall}\-
\end{tabbing}


\noindent{\sc Event}:   Disable qsort-sk.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  qsort-sk-1 \\ \index{qsort-sk-1}
\=\+{\bf let }\=\+{\it{sp\/}}{\bf $\;$ be$\;\;$}{\rm{sub}}\,({\tt{32}}, {\rm{qstack}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qstack} $-$ {\tt{16}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{qsort-sk}}\,({\it{s\/}}, {\it{s5\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-sk} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{sp\/}}, {\rm{qstack}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qstack}, {\it{x\/}}, {\it{k\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{a\/}}, {\tt{4}} $*$ {\it{n\/}}, {\it{x\/}}, {\it{k\/}})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s5\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-sk-2 \\ \index{qsort-sk-2}
\=\+{\bf let }\=\+{\it{sp\/}}{\bf $\;$ be$\;\;$}{\rm{sub}}\,({\tt{32}}, {\rm{qstack}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qstack} $-$ {\tt{16}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{qsort-sk}}\,({\it{s\/}}, {\it{s5\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-sk} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{sp\/}}, {\rm{qstack}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qstack}, {\it{x\/}}, {\it{opsz\/}} $*$ {\it{k\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{a\/}}, {\tt{4}} $*$ {\it{n\/}}, {\it{x\/}}, {\it{opsz\/}} $*$ {\it{k\/}})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{readm-mem}}\,({\it{opsz\/}}, {\it{x\/}}, {\rm{mc-mem}}\,({\it{s5\/}})\index{mc-mem}, {\it{k\/}})\index{readm-mem} \\ 
$=$$\;\;\;\;${\rm{readm-mem}}\,({\it{opsz\/}}, {\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{readm-mem})\-\-$\;${\bf  endlet}\-
\end{tabbing}


\noindent{\sc Event}:   Disable qsort-sk-1.

\addvspace{18pt}

\noindent{\sc Event}:   Disable qsort-sk-2.

\addvspace{18pt}

\begin{verbatim}; base case: from the initial state to exit (s --> exit).
\end{verbatim}\begin{tabbing}{\sc Theorem}:  qsort-base \\ \index{qsort-base}
\=\+({\rm{qsort-sp}}\,({\it{s\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-sp} $\wedge$ ({\it{l\/}} $\not<$ {\it{r\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{qsort-s5p}}\,({\it{s\/}}, {\rm{stepn}}\,({\it{s\/}}, {\rm{qsort-10}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-10})\index{stepn}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-s5p}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-base-rfile \\ \index{qsort-base-rfile}
\=\+({\rm{qsort-sp}}\,({\it{s\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-sp} $\wedge$ ({\it{l\/}} $\not<$ {\it{r\/}}) $\wedge$ {\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p} $\wedge$ ({\it{oplen\/}} $\leq$ {\tt{32}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{qsort-10}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-10})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-base-mem \\ \index{qsort-base-mem}
\=\+(\=\+{\rm{qsort-sp}}\,({\it{s\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-sp} \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $\not<$ {\it{r\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{sub}}\,({\tt{32}}, {\tt{24}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{40}}, {\it{x\/}}, {\it{k\/}})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{10}})\index{stepn})\index{mc-mem}, {\it{k\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-base-mem-sk \\ \index{qsort-base-mem-sk}
\=\+({\rm{qsort-sp}}\,({\it{s\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-sp} $\wedge$ ({\it{l\/}} $\not<$ {\it{r\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{qsort-sk}}\,({\it{s\/}}, {\rm{stepn}}\,({\it{s\/}}, {\rm{qsort-10}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-10})\index{stepn}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-sk}\-
\end{tabbing}

\begin{verbatim}; induction case: s --> s0 --> s1 --> s2 --> s3 --> s4 --> exit.
; s --> s0:
\end{verbatim}\begin{tabbing}{\sc Theorem}:  add1-int-rangep \\ \index{add1-int-rangep}
({\it{x\/}} $<$ {\rm{nat-to-int}}\,({\it{y\/}}, {\it{n\/}})\index{nat-to-int}) $\rightarrow$ {\rm{int-rangep}}\,($1\;+$ {\it{x\/}}, {\it{n\/}})\index{int-rangep}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mean-bounds \\ \index{mean-bounds}
({\it{i\/}} $<$ {\it{j\/}}) $\rightarrow$ (((({\it{i\/}} $+$ {\it{j\/}}) $\div$ {\tt{2}}) $<$ {\it{j\/}}) $\wedge$ ((({\it{i\/}} $+$ {\it{j\/}}) $\div$ {\tt{2}}) $\not<$ {\it{i\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  int-rangep-plus-1 \\ \index{int-rangep-plus-1}
({\rm{int-rangep}}\,({\tt{2}} $*$ {\it{j\/}}, {\it{n\/}})\index{int-rangep} $\wedge$ ({\it{i\/}} $<$ {\it{j\/}})) $\rightarrow$ {\rm{int-rangep}}\,({\it{i\/}} $+$ {\it{j\/}}, {\it{n\/}})\index{int-rangep}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-s-s0 \\ \index{qsort-s-s0}
\=\+{\bf let }\=\+{\it{lst1\/}}{\bf $\;$ be$\;\;$}{\rm{swap}}\,({\it{l\/}}, ({\it{l\/}} $+$ {\it{r\/}}) $\div$ {\tt{2}}, {\it{lst\/}})\index{swap}\- \\ 
{\bf in} \\ 
\=\+({\rm{qsort-sp}}\,({\it{s\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-sp} $\wedge$ ({\it{l\/}} $<$ {\it{r\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{qsort-s0p}}\,({\it{s\/}}, {\rm{stepn}}\,({\it{s\/}}, {\tt{18}})\index{stepn}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst1\/}}, {\it{l\/}}, $1\;+$ {\it{l\/}})\index{qsort-s0p}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-s-s0-rfile \\ \index{qsort-s-s0-rfile}
\=\+({\rm{qsort-sp}}\,({\it{s\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-sp} $\wedge$ ({\it{l\/}} $<$ {\it{r\/}}) $\wedge$ {\rm{d5-7a4-5p}}\,({\it{rn\/}})\index{d5-7a4-5p}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{18}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-s-s0-mem \\ \index{qsort-s-s0-mem}
\=\+(\=\+{\rm{qsort-sp}}\,({\it{s\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-sp} \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $<$ {\it{r\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{sub}}\,({\tt{32}}, {\tt{52}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{68}}, {\it{x\/}}, {\it{k\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{a\/}}, {\tt{4}} $*$ {\it{n\/}}, {\it{x\/}}, {\it{k\/}})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{18}})\index{stepn})\index{mc-mem}, {\it{k\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-
\end{tabbing}

\begin{verbatim}; s0 --> s1:
; base case (s0 --> s1):
\end{verbatim}\begin{tabbing}{\sc Theorem}:  qsort-s0-s1 \\ \index{qsort-s0-s1}
\=\+({\rm{qsort-s0p}}\,({\it{s\/}}, {\it{s0\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qsort-s0p} $\wedge$ ({\it{r\/}} $<$ {\it{i\/}}) $\wedge$ ({\it{last1\/}} $=$ {\rm{fix}}\,({\it{last\/}}))) \\ 
$\rightarrow$$\;\;\;\;${\rm{qsort-s1p}}\,({\it{s\/}}, {\rm{stepn}}\,({\it{s0\/}}, {\tt{11}})\index{stepn}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\rm{swap}}\,({\it{l\/}}, {\it{last\/}}, {\it{lst\/}})\index{swap}, {\it{last1\/}})\index{qsort-s1p}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-s0-s1-rfile \\ \index{qsort-s0-s1-rfile}
\=\+({\rm{qsort-s0p}}\,({\it{s\/}}, {\it{s0\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qsort-s0p} $\wedge$ ({\it{r\/}} $<$ {\it{i\/}}) $\wedge$ {\rm{d5-7a4-5p}}\,({\it{rn\/}})\index{d5-7a4-5p}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s0\/}}, {\tt{11}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s0\/}})\index{mc-rfile})\index{read-rn})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-s0-s1-mem \\ \index{qsort-s0-s1-mem}
\=\+(\=\+{\rm{qsort-s0p}}\,({\it{s\/}}, {\it{s0\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qsort-s0p} \\ 
$\wedge$$\;\;\;\;$({\it{r\/}} $<$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{sub}}\,({\tt{32}}, {\tt{52}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{68}}, {\it{x\/}}, {\it{k\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{a\/}}, {\tt{4}} $*$ {\it{n\/}}, {\it{x\/}}, {\it{k\/}})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s0\/}}, {\tt{11}})\index{stepn})\index{mc-mem}, {\it{k\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s0\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-
\end{tabbing}

\begin{verbatim}; induction case (s0 --> s0):
\end{verbatim}\begin{tabbing}{\sc Theorem}:  add1-int-rangepxx \\ \index{add1-int-rangepxx}
(({\it{i\/}} $\leq$ {\it{r\/}}) $\wedge$ ({\it{r\/}} $<$ {\it{n\/}}) $\wedge$ {\rm{int-rangep}}\,({\it{n\/}}, {\tt{32}})\index{int-rangep}) $\rightarrow$ {\rm{int-rangep}}\,($1\;+$ {\it{i\/}}, {\tt{32}})\index{int-rangep}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-s0-s0-1 \\ \index{qsort-s0-s0-1}
\=\+(\=\+{\rm{qsort-s0p}}\,({\it{s\/}}, {\it{s0\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qsort-s0p} \\ 
$\wedge$$\;\;\;\;$({\it{r\/}} $\not<$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth}, {\rm{get-nth}}\,({\it{l\/}}, {\it{lst\/}})\index{get-nth})\index{ilessp}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{qsort-s0p}}\,({\it{s\/}}, {\rm{stepn}}\,({\it{s0\/}}, {\tt{6}})\index{stepn}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{last\/}}, $1\;+$ {\it{i\/}})\index{qsort-s0p}\-
\end{tabbing}     

\begin{tabbing}{\sc Theorem}:  qsort-s0-s0-2 \\ \index{qsort-s0-s0-2}
\=\+(\=\+{\rm{qsort-s0p}}\,({\it{s\/}}, {\it{s0\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qsort-s0p} \\ 
$\wedge$$\;\;\;\;$({\it{r\/}} $\not<$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,({\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth}, {\rm{get-nth}}\,({\it{l\/}}, {\it{lst\/}})\index{get-nth})\index{ilessp})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{qsort-s0p}}\,({\it{s\/}}, {\rm{stepn}}\,({\it{s0\/}}, {\tt{10}})\index{stepn}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\rm{swap}}\,($1\;+$ {\it{last\/}}, {\it{i\/}}, {\it{lst\/}})\index{swap}, $1\;+$ {\it{last\/}}, $1\;+$ {\it{i\/}})\index{qsort-s0p}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-s0-s0-rfile-1 \\ \index{qsort-s0-s0-rfile-1}
\=\+(\=\+{\rm{qsort-s0p}}\,({\it{s\/}}, {\it{s0\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qsort-s0p} \\ 
$\wedge$$\;\;\;\;$({\it{r\/}} $\not<$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth}, {\rm{get-nth}}\,({\it{l\/}}, {\it{lst\/}})\index{get-nth})\index{ilessp}) \\ 
$\wedge$$\;\;\;\;${\rm{d5-7a4-5p}}\,({\it{rn\/}})\index{d5-7a4-5p})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s0\/}}, {\tt{6}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s0\/}})\index{mc-rfile})\index{read-rn})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-s0-s0-rfile-2 \\ \index{qsort-s0-s0-rfile-2}
\=\+(\=\+{\rm{qsort-s0p}}\,({\it{s\/}}, {\it{s0\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qsort-s0p} \\ 
$\wedge$$\;\;\;\;$({\it{r\/}} $\not<$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,({\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth}, {\rm{get-nth}}\,({\it{l\/}}, {\it{lst\/}})\index{get-nth})\index{ilessp} \\ 
$\wedge$$\;\;\;\;${\rm{d5-7a4-5p}}\,({\it{rn\/}})\index{d5-7a4-5p})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s0\/}}, {\tt{10}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s0\/}})\index{mc-rfile})\index{read-rn})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-s0-s0-mem-1 \\ \index{qsort-s0-s0-mem-1}
\=\+(\=\+{\rm{qsort-s0p}}\,({\it{s\/}}, {\it{s0\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qsort-s0p} \\ 
$\wedge$$\;\;\;\;$({\it{r\/}} $\not<$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth}, {\rm{get-nth}}\,({\it{l\/}}, {\it{lst\/}})\index{get-nth})\index{ilessp}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s0\/}}, {\tt{6}})\index{stepn})\index{mc-mem}, {\it{k\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s0\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-s0-s0-mem-2 \\ \index{qsort-s0-s0-mem-2}
\=\+(\=\+{\rm{qsort-s0p}}\,({\it{s\/}}, {\it{s0\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qsort-s0p} \\ 
$\wedge$$\;\;\;\;$({\it{r\/}} $\not<$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,({\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth}, {\rm{get-nth}}\,({\it{l\/}}, {\it{lst\/}})\index{get-nth})\index{ilessp} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{a\/}}, {\tt{4}} $*$ {\it{n\/}}, {\it{x\/}}, {\it{k\/}})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s0\/}}, {\tt{10}})\index{stepn})\index{mc-mem}, {\it{k\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s0\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-
\end{tabbing}

\begin{verbatim}; induction hint for the partition.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{qpart-induct} \\  
\=\+{\rm{qpart-induct}}\,({\it{s\/}}, {\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qpart-induct} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{r\/}} $<$ {\it{i\/}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{ilessp}}\,({\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth}, {\rm{get-nth}}\,({\it{l\/}}, {\it{lst\/}})\index{get-nth})\index{ilessp} \\ 
{\bf then }{\rm{qpart-induct}}\,(\=\+{\rm{stepn}}\,({\it{s\/}}, {\tt{10}})\index{stepn}, \\ 
{\it{l\/}}, \\ 
{\it{r\/}}, \\ 
{\rm{swap}}\,($1\;+$ {\it{last\/}}, {\it{i\/}}, {\it{lst\/}})\index{swap}, \\ 
$1\;+$ {\it{last\/}}, \\ 
$1\;+$ {\it{i\/}})\-\index{qpart-induct} \\ 
{\bf else }{\rm{qpart-induct}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn}, {\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{last\/}}, $1\;+$ {\it{i\/}})\index{qpart-induct}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qpart-aux-ct \\ \index{qpart-aux-ct}
\=\+{\rm{qsort-s0p}}\,({\it{s\/}}, {\it{s0\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qsort-s0p} \\ 
$\rightarrow$$\;\;\;\;${\rm{qsort-s1p}}\,(\=\+{\it{s\/}}, \\ 
{\rm{stepn}}\,({\it{s0\/}}, {\rm{qpart-aux-t}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qpart-aux-t})\index{stepn}, \\ 
{\it{a\/}}, \\ 
{\it{l\/}}, \\ 
{\it{r\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{qpart-aux}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qpart-aux}, \\ 
{\rm{qlast-aux}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qlast-aux})\-\index{qsort-s1p}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-s-s1 \\ \index{qsort-s-s1}
\=\+({\rm{qsort-sp}}\,({\it{s\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-sp} $\wedge$ ({\it{l\/}} $<$ {\it{r\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{qsort-s1p}}\,(\=\+{\it{s\/}}, \\ 
{\rm{stepn}}\,({\it{s\/}}, {\rm{qpart-t}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qpart-t})\index{stepn}, \\ 
{\it{a\/}}, \\ 
{\it{l\/}}, \\ 
{\it{r\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qpart}, \\ 
{\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast})\-\index{qsort-s1p}\-
\end{tabbing}      
              
\begin{tabbing}{\sc Theorem}:  qpart-aux-rfile \\ \index{qpart-aux-rfile}
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s0\/}}, {\rm{qpart-aux-t}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qpart-aux-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+({\rm{qsort-s0p}}\,({\it{s\/}}, {\it{s0\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qsort-s0p} $\wedge$ {\rm{d5-7a4-5p}}\,({\it{rn\/}})\index{d5-7a4-5p}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s1\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s0\/}})\index{mc-rfile})\index{read-rn})\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-s-s1-rfile \\ \index{qsort-s-s1-rfile}
\=\+({\rm{qsort-sp}}\,({\it{s\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-sp} $\wedge$ ({\it{l\/}} $<$ {\it{r\/}}) $\wedge$ {\rm{d5-7a4-5p}}\,({\it{rn\/}})\index{d5-7a4-5p}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{qpart-t}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qpart-t})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qpart-aux-mem \\ \index{qpart-aux-mem}
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s0\/}}, {\rm{qpart-aux-t}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qpart-aux-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{qsort-s0p}}\,({\it{s\/}}, {\it{s0\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qsort-s0p} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{sub}}\,({\tt{32}}, {\tt{52}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{68}}, {\it{x\/}}, {\it{k\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{a\/}}, {\tt{4}} $*$ {\it{n\/}}, {\it{x\/}}, {\it{k\/}})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s1\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s0\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-sk-s-s1 \\ \index{qsort-sk-s-s1}
\=\+({\rm{qsort-sp}}\,({\it{s\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-sp} $\wedge$ ({\it{l\/}} $<$ {\it{r\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{qsort-sk}}\,({\it{s\/}}, {\rm{stepn}}\,({\it{s\/}}, {\rm{qpart-t}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qpart-t})\index{stepn}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-sk}\-
\end{tabbing}


\noindent{\sc Event}:   Disable qpart-t.

\addvspace{18pt}

\begin{verbatim}; s2 --> s3:
\end{verbatim}\begin{tabbing}{\sc Theorem}:  qsort-s2-s3 \\ \index{qsort-s2-s3}
\=\+{\bf let }\=\+{\it{qlst\/}}{\bf $\;$ be$\;\;$}{\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qpart}, \\ 
{\it{last\/}}{\bf $\;$ be$\;\;$}{\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast}\- \\ 
{\bf in} \\ 
\=\+{\rm{qsort-s2p}}\,({\it{s\/}}, {\it{s2\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\rm{qsort}}\,({\it{l\/}}, {\it{last\/}} $-\;1$, {\it{qlst\/}})\index{qsort}, {\it{last\/}})\index{qsort-s2p} \\ 
$\rightarrow$$\;\;\;\;${\rm{qsort-s3p}}\,(\=\+{\it{s\/}}, \\ 
{\rm{stepn}}\,({\it{s2\/}}, {\rm{qsort-5}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-5})\index{stepn}, \\ 
{\it{a\/}}, \\ 
{\it{l\/}}, \\ 
{\it{r\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{qsort}}\,({\it{l\/}}, {\it{last\/}} $-\;1$, {\it{qlst\/}})\index{qsort}, \\ 
{\it{last\/}})\-\index{qsort-s3p}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-s2-s3-rfile-la \\ \index{qsort-s2-s3-rfile-la}
\=\+({\rm{qsort-s2p}}\,({\it{s\/}}, {\it{s2\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst1\/}}, {\it{last\/}})\index{qsort-s2p} $\wedge$ {\rm{d5-7a4-5p}}\,({\it{rn\/}})\index{d5-7a4-5p}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s2\/}}, {\tt{5}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s2\/}})\index{mc-rfile})\index{read-rn})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-s2-s3-rfile \\ \index{qsort-s2-s3-rfile}
\=\+{\bf let }\=\+{\it{qlst\/}}{\bf $\;$ be$\;\;$}{\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qpart}, \\ 
{\it{last\/}}{\bf $\;$ be$\;\;$}{\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast}, \\ 
{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\rm{stepn}}\,({\it{s\/}}, {\it{k1\/}})\index{stepn}, {\it{k2\/}})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{qsort-s2p}}\,({\it{s\/}}, {\it{s2\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\rm{qsort}}\,({\it{l\/}}, {\it{last\/}} $-\;1$, {\it{qlst\/}})\index{qsort}, {\it{last\/}})\index{qsort-s2p} \\ 
$\wedge$$\;\;\;\;${\rm{d5-7a4-5p}}\,({\it{rn\/}})\index{d5-7a4-5p})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s2\/}}, {\rm{qsort-5}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-5})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s2\/}})\index{mc-rfile})\index{read-rn})\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-s2-s3-mem \\ \index{qsort-s2-s3-mem}
\=\+(\=\+{\rm{qsort-s2p}}\,({\it{s\/}}, {\it{s2\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{last\/}})\index{qsort-s2p} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{sub}}\,({\tt{32}}, {\tt{52}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{68}}, {\it{x\/}}, {\it{k\/}})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s2\/}}, {\tt{5}})\index{stepn})\index{mc-mem}, {\it{k\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s2\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-sk-s-s3 \\ \index{qsort-sk-s-s3}
\=\+{\bf let }\=\+{\it{lst1\/}}{\bf $\;$ be$\;\;$}{\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qpart}, \\ 
{\it{last\/}}{\bf $\;$ be$\;\;$}{\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{qsort-s2p}}\,({\it{s\/}}, {\it{s2\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\rm{qsort}}\,({\it{l\/}}, {\it{last\/}} $-\;1$, {\it{lst1\/}})\index{qsort}, {\it{last\/}})\index{qsort-s2p} \\ 
$\wedge$$\;\;\;\;${\rm{qsort-sk}}\,({\it{s\/}}, {\it{s2\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-sk})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{qsort-sk}}\,({\it{s\/}}, {\rm{stepn}}\,({\it{s2\/}}, {\rm{qsort-5}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-5})\index{stepn}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-sk}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim}; s4 --> exit:
\end{verbatim}\begin{tabbing}{\sc Theorem}:  qsort-s4-s5 \\ \index{qsort-s4-s5}
\=\+{\bf let }\=\+{\it{qlst\/}}{\bf $\;$ be$\;\;$}{\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qpart}, \\ 
{\it{last\/}}{\bf $\;$ be$\;\;$}{\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast}\- \\ 
{\bf in} \\ 
\=\+{\rm{qsort-s4p}}\,({\it{s\/}}, {\it{s4\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\rm{qsort}}\,($1\;+$ {\it{last\/}}, {\it{r\/}}, {\rm{qsort}}\,({\it{l\/}}, {\it{last\/}} $-\;1$, {\it{qlst\/}})\index{qsort})\index{qsort})\index{qsort-s4p} \\ 
$\rightarrow$$\;\;\;\;${\rm{qsort-s5p}}\,(\=\+{\it{s\/}}, \\ 
{\rm{stepn}}\,({\it{s4\/}}, {\rm{qsort-3}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-3})\index{stepn}, \\ 
{\it{a\/}}, \\ 
{\it{l\/}}, \\ 
{\it{r\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{qsort}}\,($1\;+$ {\it{last\/}}, {\it{r\/}}, {\rm{qsort}}\,({\it{l\/}}, {\it{last\/}} $-\;1$, {\it{qlst\/}})\index{qsort})\index{qsort})\-\index{qsort-s5p}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-s4-s5-rfile-la \\ \index{qsort-s4-s5-rfile-la}
\=\+(\=\+{\rm{qsort-s4p}}\,({\it{s\/}}, {\it{s4\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\rm{qsort}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qsort})\index{qsort-s4p} \\ 
$\wedge$$\;\;\;\;$({\it{oplen\/}} $\leq$ {\tt{32}}) \\ 
$\wedge$$\;\;\;\;${\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s4\/}}, {\tt{3}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{d5-7a4-5p}}\,({\it{rn\/}})\index{d5-7a4-5p}$\;\;${\bf then }{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s4\/}})\index{mc-rfile})\index{read-rn} \\ 
{\bf else }{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-s4-s5-rfile \\ \index{qsort-s4-s5-rfile}
\=\+{\bf let }\=\+{\it{s4\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\rm{stepn}}\,({\rm{stepn}}\,({\rm{stepn}}\,({\it{s\/}}, {\it{k1\/}})\index{stepn}, {\it{k2\/}})\index{stepn}, {\it{k3\/}})\index{stepn}, {\it{k4\/}})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{qsort-s4p}}\,({\it{s\/}}, {\it{s4\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\rm{qsort}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qsort})\index{qsort-s4p} \\ 
$\wedge$$\;\;\;\;$({\it{oplen\/}} $\leq$ {\tt{32}}) \\ 
$\wedge$$\;\;\;\;${\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s4\/}}, {\rm{qsort-3}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-3})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{d5-7a4-5p}}\,({\it{rn\/}})\index{d5-7a4-5p}$\;\;${\bf then }{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s4\/}})\index{mc-rfile})\index{read-rn} \\ 
{\bf else }{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn}$\;${\bf  endif}\-)\-\-$\;${\bf  endlet}\-
\end{tabbing}
       
\begin{tabbing}{\sc Theorem}:  qsort-s4-s5-mem \\ \index{qsort-s4-s5-mem}
\=\+({\rm{qsort-s4p}}\,({\it{s\/}}, {\it{s4\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-s4p} $\wedge$ {\rm{disjoint}}\,({\rm{sub}}\,({\tt{32}}, {\tt{52}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{68}}, {\it{x\/}}, {\it{k\/}})\index{disjoint}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s4\/}}, {\tt{3}})\index{stepn})\index{mc-mem}, {\it{k\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s4\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-sk-s-s5 \\ \index{qsort-sk-s-s5}
\=\+({\rm{qsort-s4p}}\,({\it{s\/}}, {\it{s4\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\rm{qsort}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qsort})\index{qsort-s4p} $\wedge$ {\rm{qsort-sk}}\,({\it{s\/}}, {\it{s4\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-sk}) \\ 
$\rightarrow$$\;\;\;\;${\rm{qsort-sk}}\,({\it{s\/}}, {\rm{stepn}}\,({\it{s4\/}}, {\rm{qsort-3}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-3})\index{stepn}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-sk}\-
\end{tabbing}

\begin{verbatim}; some auxiliary lemmas.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  qlast-aux-0 \\ \index{qlast-aux-0}
({\it{r\/}} $<$ {\it{i\/}}) $\rightarrow$ ({\rm{qlast-aux}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qlast-aux} $=$ {\rm{fix}}\,({\it{last\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qlast-0 \\ \index{qlast-0}
({\it{r\/}} $\leq$ {\it{l\/}}) $\rightarrow$ ({\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast} $=$ {\rm{fix}}\,({\it{l\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qstack-la3 \\ \index{qstack-la3}
({\it{l\/}} $\not<$ {\it{r\/}}) $\rightarrow$ ({\rm{qstack}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qstack} $=$ {\tt{68}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qstack-0 \\ \index{qstack-0}
\=\+({\rm{qstack}}\,({\it{l\/}}, {\tt{-1}}, {\it{lst\/}})\index{qstack} $=$ {\tt{68}}) \\ 
$\wedge$$\;\;\;\;$({\rm{qstack}}\,({\it{l\/}}, {\tt{0}}, {\it{lst\/}})\index{qstack} $=$ {\tt{68}}) \\ 
$\wedge$$\;\;\;\;$({\rm{qstack}}\,({\it{l\/}}, {\it{l\/}}, {\it{lst\/}})\index{qstack} $=$ {\tt{68}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qstack-la4 \\ \index{qstack-la4}
\=\+{\bf let }\=\+{\it{last\/}}{\bf $\;$ be$\;\;$}{\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast}, \\ 
{\it{lst1\/}}{\bf $\;$ be$\;\;$}{\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qpart}\- \\ 
{\bf in} \\ 
{\rm{qstack}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qstack} $\not<$ {\rm{qstack}}\,({\it{l\/}}, {\it{last\/}} $-\;1$, {\it{lst1\/}})\index{qstack}$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim}; s1 --> s2:  the first recursive call.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  qsort-s1-crock \\ \index{qsort-s1-crock}
\=\+((({\it{q1\/}} $+$ {\tt{40}}) $\leq$ {\it{q\/}}) $\wedge$ ({\tt{68}} $\leq$ {\it{q1\/}}) $\wedge$ ({\it{q\/}} $<$ {\rm{exp}}\,({\tt{2}}, {\tt{32}})\index{exp})) \\ 
$\rightarrow$$\;\;\;\;$({\it{q\/}} $\not<$ ({\it{q1\/}} $+$ {\rm{add}}\,(\=\+{\tt{32}}, \\ 
{\tt{4294967256}}, \\ 
{\rm{add}}\,({\tt{32}}, {\rm{neg}}\,({\tt{32}}, {\it{q1\/}} $-$ {\tt{16}})\index{neg}, {\it{q\/}} $-$ {\tt{16}})\index{add})\-\index{add}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qstack-la1\~ \\ \index{qstack-la1\~}
\=\+(({\it{last\/}} $=$ {\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast}) $\wedge$ ({\it{lst1\/}} $=$ {\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qpart}) $\wedge$ ({\it{l\/}} $<$ {\it{r\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{qstack}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qstack} $\not<$ ({\tt{40}} $+$ {\rm{qstack}}\,({\it{l\/}}, {\it{last\/}} $-\;1$, {\it{lst1\/}})\index{qstack}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-s1-s \\ \index{qsort-s1-s}
\=\+{\bf let }\=\+{\it{lst1\/}}{\bf $\;$ be$\;\;$}{\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qpart}, \\ 
{\it{last\/}}{\bf $\;$ be$\;\;$}{\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{qsort-s1p}}\,({\it{s\/}}, {\rm{stepn}}\,({\it{s\/}}, {\it{k\/}})\index{stepn}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst1\/}}, {\it{last\/}})\index{qsort-s1p} \\ 
$\wedge$$\;\;\;\;${\rm{qsort-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-statep})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{qsort-statep}}\,({\rm{stepn}}\,({\it{s\/}}, {\it{k\/}})\index{stepn}, {\it{a\/}}, {\it{l\/}}, {\rm{idifference}}\,({\it{last\/}}, {\tt{1}})\index{idifference}, {\it{n\/}}, {\it{lst1\/}})\index{qsort-statep}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-s1-crock1 \\ \index{qsort-s1-crock1}
\=\+(\=\+({\tt{68}} $\leq$ {\it{q1\/}}) \\ 
$\wedge$$\;\;\;\;$(({\tt{40}} $+$ {\it{q1\/}}) $<$ {\tt{4294967296}}) \\ 
$\wedge$$\;\;\;\;$(({\it{x\/}} $+$ {\it{k\/}}) $\leq$ {\tt{4294967296}}) \\ 
$\wedge$$\;\;\;\;$({\tt{4294967272}} $\leq$ {\it{x\/}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{disjoint}}\,({\rm{add}}\,({\tt{32}}, {\tt{4294967256}}, {\rm{neg}}\,({\tt{32}}, {\it{q1\/}} $-$ {\tt{16}})\index{neg})\index{add}, {\it{q1\/}}, {\it{x\/}}, {\it{k\/}})\index{disjoint}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-s1-crock2-crock \\ \index{qsort-s1-crock2-crock}
\=\+(({\tt{68}} $\leq$ {\it{q1\/}}) $\wedge$ ({\it{q1\/}} $<$ {\tt{4294967256}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{add}}\,({\tt{32}}, {\tt{4294967256}}, {\rm{neg}}\,({\tt{32}}, {\it{q1\/}} $-$ {\tt{16}})\index{neg})\index{add} $\not<$ {\tt{16}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-s1-crock2 \\ \index{qsort-s1-crock2}
\=\+(({\tt{68}} $\leq$ {\it{q1\/}}) $\wedge$ (({\tt{40}} $+$ {\it{q1\/}}) $<$ {\tt{4294967296}}) $\wedge$ (({\it{x\/}} $+$ {\it{k\/}}) $\leq$ {\tt{16}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{disjoint}}\,({\rm{add}}\,({\tt{32}}, {\tt{4294967256}}, {\rm{neg}}\,({\tt{32}}, {\it{q1\/}} $-$ {\tt{16}})\index{neg})\index{add}, {\it{q1\/}}, {\it{x\/}}, {\it{k\/}})\index{disjoint}\-
\end{tabbing}


\noindent{\sc Event}:   Disable qsort-s1-crock2-crock.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  qsort-s1-s2 \\ \index{qsort-s1-s2}
\=\+{\bf let }\=\+{\it{lst1\/}}{\bf $\;$ be$\;\;$}{\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qpart}, \\ 
{\it{last\/}}{\bf $\;$ be$\;\;$}{\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{qsort-s1p}}\,({\it{s\/}}, {\it{s1\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst1\/}}, {\it{last\/}})\index{qsort-s1p} \\ 
$\wedge$$\;\;\;\;${\rm{qsort-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-statep} \\ 
$\wedge$$\;\;\;\;${\rm{qsort-s5p}}\,(\=\+{\it{s1\/}}, \\ 
{\rm{stepn}}\,({\it{s1\/}}, {\it{k\/}})\index{stepn}, \\ 
{\it{a\/}}, \\ 
{\it{l\/}}, \\ 
{\rm{idifference}}\,({\it{last\/}}, {\tt{1}})\index{idifference}, \\ 
{\it{n\/}}, \\ 
{\rm{qsort}}\,({\it{l\/}}, {\it{last\/}} $-\;1$, {\it{lst1\/}})\index{qsort})\-\index{qsort-s5p} \\ 
$\wedge$$\;\;\;\;${\rm{qsort-sk}}\,({\it{s1\/}}, {\rm{stepn}}\,({\it{s1\/}}, {\it{k\/}})\index{stepn}, {\it{a\/}}, {\it{l\/}}, {\rm{idifference}}\,({\it{last\/}}, {\tt{1}})\index{idifference}, {\it{n\/}}, {\it{lst1\/}})\index{qsort-sk})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{qsort-s2p}}\,({\it{s\/}}, {\rm{stepn}}\,({\it{s1\/}}, {\it{k\/}})\index{stepn}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\rm{qsort}}\,({\it{l\/}}, {\it{last\/}} $-\;1$, {\it{lst1\/}})\index{qsort}, {\it{last\/}})\index{qsort-s2p}\-$\;${\bf  endlet}\-
\end{tabbing}


\noindent{\sc Event}:   Disable qsort-s1-crock1.

\addvspace{18pt}

\noindent{\sc Event}:   Disable qsort-s1-crock2.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  qsort-s1-s2-mem \\ \index{qsort-s1-s2-mem}
\=\+{\bf let }\=\+{\it{lst1\/}}{\bf $\;$ be$\;\;$}{\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qpart}, \\ 
{\it{last\/}}{\bf $\;$ be$\;\;$}{\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{qsort-s1p}}\,({\it{s\/}}, {\it{s1\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst1\/}}, {\it{last\/}})\index{qsort-s1p} \\ 
$\wedge$$\;\;\;\;${\rm{qsort-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-statep} \\ 
$\wedge$$\;\;\;\;${\rm{qsort-sk}}\,({\it{s\/}}, {\it{s1\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-sk} \\ 
$\wedge$$\;\;\;\;${\rm{qsort-sk}}\,({\it{s1\/}}, {\rm{stepn}}\,({\it{s1\/}}, {\it{k\/}})\index{stepn}, {\it{a\/}}, {\it{l\/}}, {\rm{idifference}}\,({\it{last\/}}, {\tt{1}})\index{idifference}, {\it{n\/}}, {\it{lst1\/}})\index{qsort-sk} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{a\/}}, {\tt{4}} $*$ {\it{n\/}}, {\it{x\/}}, {\it{k1\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,(\=\+{\rm{sub}}\,({\tt{32}}, {\rm{qstack}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qstack} $-$ {\tt{16}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, \\ 
{\rm{qstack}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qstack}, \\ 
{\it{x\/}}, \\ 
{\it{k1\/}})\-\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s1\/}}, {\it{k\/}})\index{stepn})\index{mc-mem}, {\it{k1\/}})\index{read-mem} \\ 
$=$$\;\;\;\;${\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k1\/}})\index{read-mem})\-\-$\;${\bf  endlet}\-
\end{tabbing}


\noindent{\sc Event}:   Disable qstack-la1\~.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  qsort-sk-s-s2 \\ \index{qsort-sk-s-s2}
\=\+{\bf let }\=\+{\it{lst1\/}}{\bf $\;$ be$\;\;$}{\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qpart}, \\ 
{\it{last\/}}{\bf $\;$ be$\;\;$}{\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{qsort-s1p}}\,({\it{s\/}}, {\it{s1\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst1\/}}, {\it{last\/}})\index{qsort-s1p} \\ 
$\wedge$$\;\;\;\;${\rm{qsort-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-statep} \\ 
$\wedge$$\;\;\;\;${\rm{qsort-sk}}\,({\it{s\/}}, {\it{s1\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-sk} \\ 
$\wedge$$\;\;\;\;${\rm{qsort-sk}}\,({\it{s1\/}}, {\rm{stepn}}\,({\it{s1\/}}, {\it{k\/}})\index{stepn}, {\it{a\/}}, {\it{l\/}}, {\rm{idifference}}\,({\it{last\/}}, {\tt{1}})\index{idifference}, {\it{n\/}}, {\it{lst1\/}})\index{qsort-sk})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{qsort-sk}}\,({\it{s\/}}, {\rm{stepn}}\,({\it{s1\/}}, {\it{k\/}})\index{stepn}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-sk}\-$\;${\bf  endlet}\-
\end{tabbing}


\noindent{\sc Event}:   Disable qsort-s1-s2-mem.

\addvspace{18pt}

\begin{verbatim}; s3 --> s4:  the second recursive call.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  qsort-s3-crock \\ \index{qsort-s3-crock}
\=\+((({\it{q1\/}} $+$ {\tt{52}}) $\leq$ {\it{q\/}}) $\wedge$ ({\tt{68}} $\leq$ {\it{q1\/}}) $\wedge$ ({\it{q\/}} $<$ {\rm{exp}}\,({\tt{2}}, {\tt{32}})\index{exp})) \\ 
$\rightarrow$$\;\;\;\;$({\it{q\/}} $\not<$ ({\it{q1\/}} $+$ {\rm{add}}\,(\=\+{\tt{32}}, \\ 
{\tt{4294967244}}, \\ 
{\rm{add}}\,({\tt{32}}, {\rm{neg}}\,({\tt{32}}, {\it{q1\/}} $-$ {\tt{16}})\index{neg}, {\it{q\/}} $-$ {\tt{16}})\index{add})\-\index{add}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qstack-la2\~ \\ \index{qstack-la2\~}
\=\+(({\it{last\/}} $=$ {\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast}) $\wedge$ ({\it{lst1\/}} $=$ {\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qpart}) $\wedge$ ({\it{l\/}} $<$ {\it{r\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{qstack}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qstack} \\ 
$\not<$$\;\;\;\;$({\tt{52}} $+$ {\rm{qstack}}\,($1\;+$ {\it{last\/}}, {\it{r\/}}, {\rm{qsort}}\,({\it{l\/}}, {\it{last\/}} $-\;1$, {\it{lst1\/}})\index{qsort})\index{qstack}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-s3-s-la \\ \index{qsort-s3-s-la}
\=\+{\bf let }\=\+{\it{lst1\/}}{\bf $\;$ be$\;\;$}{\rm{qsort}}\,({\it{l\/}}, {\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast} $-\;1$, {\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qpart})\index{qsort}, \\ 
{\it{last\/}}{\bf $\;$ be$\;\;$}{\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{qsort-s3p}}\,({\it{s\/}}, {\rm{stepn}}\,({\it{s\/}}, {\it{k\/}})\index{stepn}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst1\/}}, {\it{last\/}})\index{qsort-s3p} \\ 
$\wedge$$\;\;\;\;${\rm{qsort-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-statep})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{qsort-statep}}\,({\rm{stepn}}\,({\it{s\/}}, {\it{k\/}})\index{stepn}, {\it{a\/}}, $1\;+$ {\it{last\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst1\/}})\index{qsort-statep}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-s3-s \\ \index{qsort-s3-s}
\=\+{\bf let }\=\+{\it{lst1\/}}{\bf $\;$ be$\;\;$}{\rm{qsort}}\,({\it{l\/}}, {\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast} $-\;1$, {\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qpart})\index{qsort}, \\ 
{\it{last\/}}{\bf $\;$ be$\;\;$}{\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{qsort-s3p}}\,({\it{s\/}}, {\rm{stepn}}\,({\rm{stepn}}\,({\rm{stepn}}\,({\it{s\/}}, {\it{k1\/}})\index{stepn}, {\it{k2\/}})\index{stepn}, {\it{k3\/}})\index{stepn}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst1\/}}, {\it{last\/}})\index{qsort-s3p} \\ 
$\wedge$$\;\;\;\;${\rm{qsort-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-statep})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{qsort-statep}}\,(\=\+{\rm{stepn}}\,({\rm{stepn}}\,({\rm{stepn}}\,({\it{s\/}}, {\it{k1\/}})\index{stepn}, {\it{k2\/}})\index{stepn}, {\it{k3\/}})\index{stepn}, \\ 
{\it{a\/}}, \\ 
$1\;+$ {\it{last\/}}, \\ 
{\it{r\/}}, \\ 
{\it{n\/}}, \\ 
{\it{lst1\/}})\-\index{qsort-statep}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-s3-crock1 \\ \index{qsort-s3-crock1}
\=\+(\=\+({\tt{68}} $\leq$ {\it{q1\/}}) \\ 
$\wedge$$\;\;\;\;$(({\tt{52}} $+$ {\it{q1\/}}) $<$ {\tt{4294967296}}) \\ 
$\wedge$$\;\;\;\;$(({\it{x\/}} $+$ {\it{k\/}}) $\leq$ {\tt{4294967296}}) \\ 
$\wedge$$\;\;\;\;$({\tt{4294967260}} $\leq$ {\it{x\/}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{disjoint}}\,({\rm{add}}\,({\tt{32}}, {\tt{4294967244}}, {\rm{neg}}\,({\tt{32}}, {\it{q1\/}} $-$ {\tt{16}})\index{neg})\index{add}, {\it{q1\/}}, {\it{x\/}}, {\it{k\/}})\index{disjoint}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-s3-crock2-crock \\ \index{qsort-s3-crock2-crock}
\=\+(({\tt{68}} $\leq$ {\it{q1\/}}) $\wedge$ ({\it{q1\/}} $<$ {\tt{4294967244}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{add}}\,({\tt{32}}, {\tt{4294967244}}, {\rm{neg}}\,({\tt{32}}, {\it{q1\/}} $-$ {\tt{16}})\index{neg})\index{add} $\not<$ {\tt{16}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-s3-crock2 \\ \index{qsort-s3-crock2}
\=\+(({\tt{68}} $\leq$ {\it{q1\/}}) $\wedge$ (({\tt{52}} $+$ {\it{q1\/}}) $<$ {\tt{4294967296}}) $\wedge$ (({\it{x\/}} $+$ {\it{k\/}}) $\leq$ {\tt{16}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{disjoint}}\,({\rm{add}}\,({\tt{32}}, {\tt{4294967244}}, {\rm{neg}}\,({\tt{32}}, {\it{q1\/}} $-$ {\tt{16}})\index{neg})\index{add}, {\it{q1\/}}, {\it{x\/}}, {\it{k\/}})\index{disjoint}\-
\end{tabbing}


\noindent{\sc Event}:   Disable qsort-s3-crock2-crock.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  qsort-s3-s4 \\ \index{qsort-s3-s4}
\=\+{\bf let }\=\+{\it{lst1\/}}{\bf $\;$ be$\;\;$}{\rm{qsort}}\,({\it{l\/}}, {\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast} $-\;1$, {\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qpart})\index{qsort}, \\ 
{\it{last\/}}{\bf $\;$ be$\;\;$}{\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{qsort-s3p}}\,({\it{s\/}}, {\it{s3\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst1\/}}, {\it{last\/}})\index{qsort-s3p} \\ 
$\wedge$$\;\;\;\;${\rm{qsort-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-statep} \\ 
$\wedge$$\;\;\;\;${\rm{qsort-s5p}}\,(\=\+{\it{s3\/}}, \\ 
{\rm{stepn}}\,({\it{s3\/}}, {\it{k\/}})\index{stepn}, \\ 
{\it{a\/}}, \\ 
$1\;+$ {\it{last\/}}, \\ 
{\it{r\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{qsort}}\,($1\;+$ {\it{last\/}}, {\it{r\/}}, {\it{lst1\/}})\index{qsort})\-\index{qsort-s5p} \\ 
$\wedge$$\;\;\;\;${\rm{qsort-sk}}\,({\it{s3\/}}, {\rm{stepn}}\,({\it{s3\/}}, {\it{k\/}})\index{stepn}, {\it{a\/}}, $1\;+$ {\it{last\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst1\/}})\index{qsort-sk})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{qsort-s4p}}\,({\it{s\/}}, {\rm{stepn}}\,({\it{s3\/}}, {\it{k\/}})\index{stepn}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\rm{qsort}}\,($1\;+$ {\it{last\/}}, {\it{r\/}}, {\it{lst1\/}})\index{qsort})\index{qsort-s4p}\-$\;${\bf  endlet}\-
\end{tabbing}


\noindent{\sc Event}:   Disable qsort-s3-crock1.

\addvspace{18pt}

\noindent{\sc Event}:   Disable qsort-s3-crock2.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  qsort-s3-s4-mem \\ \index{qsort-s3-s4-mem}
\=\+{\bf let }\=\+{\it{lst1\/}}{\bf $\;$ be$\;\;$}{\rm{qsort}}\,({\it{l\/}}, {\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast} $-\;1$, {\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qpart})\index{qsort}, \\ 
{\it{last\/}}{\bf $\;$ be$\;\;$}{\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{qsort-s3p}}\,({\it{s\/}}, {\it{s3\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst1\/}}, {\it{last\/}})\index{qsort-s3p} \\ 
$\wedge$$\;\;\;\;${\rm{qsort-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-statep} \\ 
$\wedge$$\;\;\;\;${\rm{qsort-sk}}\,({\it{s\/}}, {\it{s3\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-sk} \\ 
$\wedge$$\;\;\;\;${\rm{qsort-sk}}\,({\it{s3\/}}, {\rm{stepn}}\,({\it{s3\/}}, {\it{k\/}})\index{stepn}, {\it{a\/}}, $1\;+$ {\it{last\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst1\/}})\index{qsort-sk} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{a\/}}, {\tt{4}} $*$ {\it{n\/}}, {\it{x\/}}, {\it{k1\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,(\=\+{\rm{sub}}\,({\tt{32}}, {\rm{qstack}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qstack} $-$ {\tt{16}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, \\ 
{\rm{qstack}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qstack}, \\ 
{\it{x\/}}, \\ 
{\it{k1\/}})\-\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s3\/}}, {\it{k\/}})\index{stepn})\index{mc-mem}, {\it{k1\/}})\index{read-mem} \\ 
$=$$\;\;\;\;${\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k1\/}})\index{read-mem})\-\-$\;${\bf  endlet}\-
\end{tabbing}


\noindent{\sc Event}:   Disable qstack-la2\~.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  qsort-sk-s-s4 \\ \index{qsort-sk-s-s4}
\=\+{\bf let }\=\+{\it{lst1\/}}{\bf $\;$ be$\;\;$}{\rm{qsort}}\,({\it{l\/}}, {\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast} $-\;1$, {\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qpart})\index{qsort}, \\ 
{\it{last\/}}{\bf $\;$ be$\;\;$}{\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{qsort-s3p}}\,({\it{s\/}}, {\it{s3\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst1\/}}, {\it{last\/}})\index{qsort-s3p} \\ 
$\wedge$$\;\;\;\;${\rm{qsort-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-statep} \\ 
$\wedge$$\;\;\;\;${\rm{qsort-sk}}\,({\it{s\/}}, {\it{s3\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-sk} \\ 
$\wedge$$\;\;\;\;${\rm{qsort-sk}}\,({\it{s3\/}}, {\rm{stepn}}\,({\it{s3\/}}, {\it{k\/}})\index{stepn}, {\it{a\/}}, $1\;+$ {\it{last\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst1\/}})\index{qsort-sk})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{qsort-sk}}\,({\it{s\/}}, {\rm{stepn}}\,({\it{s3\/}}, {\it{k\/}})\index{stepn}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-sk}\-$\;${\bf  endlet}\-
\end{tabbing}


\noindent{\sc Event}:   Disable qsort-s3-s4-mem.

\addvspace{18pt}

\begin{verbatim}; the correctness of the QSORT program.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  qsort-t--1 \\ \index{qsort-t--1}
{\rm{qsort-t}}\,({\it{a\/}}, {\it{l\/}}, {\rm{idifference}}\,({\it{r\/}}, {\tt{1}})\index{idifference}, {\it{n\/}}, {\it{lst\/}})\index{qsort-t} $=$ {\rm{qsort-t}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}} $-\;1$, {\it{n\/}}, {\it{lst\/}})\index{qsort-t}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort--1 \\ \index{qsort--1}
{\rm{qsort}}\,({\it{l\/}}, {\rm{idifference}}\,({\it{r\/}}, {\tt{1}})\index{idifference}, {\it{lst\/}})\index{qsort} $=$ {\rm{qsort}}\,({\it{l\/}}, {\it{r\/}} $-\;1$, {\it{lst\/}})\index{qsort}
\end{tabbing}


\noindent{\sc Event}:   Disable qsort-10.

\addvspace{18pt}

\noindent{\sc Event}:   Disable qsort-5.

\addvspace{18pt}

\noindent{\sc Event}:   Disable qsort-3.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  qsort-correctness-la \\ \index{qsort-correctness-la}
\=\+({\rm{qsort-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-statep} $\wedge$ ({\it{oplen\/}} $\leq$ {\tt{32}}) $\wedge$ {\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{qsort-s5p}}\,({\it{s\/}}, {\rm{stepn}}\,({\it{s\/}}, {\rm{qsort-t}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-t})\index{stepn}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\rm{qsort}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qsort})\index{qsort-s5p} \\ 
$\wedge$$\;\;\;\;${\rm{qsort-sk}}\,({\it{s\/}}, {\rm{stepn}}\,({\it{s\/}}, {\rm{qsort-t}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-t})\index{stepn}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-sk} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{qsort-t}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-t})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-correctness \\ \index{qsort-correctness}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{qsort-t}}\,({\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-t})\index{stepn}, \\ 
{\it{sp\/}}{\bf $\;$ be$\;\;$}{\rm{sub}}\,({\tt{32}}, {\rm{qstack}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qstack} $-$ {\tt{16}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}\- \\ 
{\bf in} \\ 
\=\+{\rm{qsort-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{l\/}}, {\it{r\/}}, {\it{n\/}}, {\it{lst\/}})\index{qsort-statep} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{sn\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{sn\/}})\index{mc-pc} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{sn\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\it{sn\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{add}}\,({\tt{32}}, {\rm{read-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn}, {\tt{4}})\index{add})\- \\ 
$\wedge$$\;\;\;\;$(\=\+(({\it{oplen\/}} $\leq$ {\tt{32}}) $\wedge$ {\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{sn\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\rm{disjoint}}\,({\it{sp\/}}, {\rm{qstack}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qstack}, {\it{x\/}}, {\it{k\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{a\/}}, {\tt{4}} $*$ {\it{n\/}}, {\it{x\/}}, {\it{k\/}})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{sn\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem} \\ 
$=$$\;\;\;\;${\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{mem-ilst}}\,({\tt{4}}, {\it{a\/}}, {\rm{mc-mem}}\,({\it{sn\/}})\index{mc-mem}, {\it{n\/}}, {\rm{qsort}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qsort})\index{mem-ilst})\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim}; in the logic, qsort is correct:
;       1. if left <= i <= j <= right,  lst'[i] <= lst'[j].
;       2. for all x,  (count-lst x l r lst) = (count-lst x l r lst').
\end{verbatim}\begin{tabbing}{\sc Theorem}:  put-commute \\ \index{put-commute}
\=\+({\rm{fix}}\,({\it{i\/}}) $\not=$ {\rm{fix}}\,({\it{j\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{put-nth}}\,({\it{v1\/}}, {\it{i\/}}, {\rm{put-nth}}\,({\it{v2\/}}, {\it{j\/}}, {\it{lst\/}})\index{put-nth})\index{put-nth} $=$ {\rm{put-nth}}\,({\it{v2\/}}, {\it{j\/}}, {\rm{put-nth}}\,({\it{v1\/}}, {\it{i\/}}, {\it{lst\/}})\index{put-nth})\index{put-nth})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  swap-put-commute \\ \index{swap-put-commute}
\=\+(({\it{i\/}} $<$ {\it{l\/}}) $\wedge$ ({\it{i\/}} $<$ {\it{r\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{swap}}\,({\it{l\/}}, {\it{r\/}}, {\rm{put-nth}}\,({\it{v\/}}, {\it{i\/}}, {\it{lst\/}})\index{put-nth})\index{swap} $=$ {\rm{put-nth}}\,({\it{v\/}}, {\it{i\/}}, {\rm{swap}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{swap})\index{put-nth})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  swap-commute \\ \index{swap-commute}
\=\+(({\it{i\/}} $<$ {\it{l\/}}) $\wedge$ ({\it{i\/}} $<$ {\it{r\/}}) $\wedge$ ({\it{j\/}} $<$ {\it{l\/}}) $\wedge$ ({\it{j\/}} $<$ {\it{r\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{swap}}\,({\it{l\/}}, {\it{r\/}}, {\rm{swap}}\,({\it{i\/}}, {\it{j\/}}, {\it{lst\/}})\index{swap})\index{swap} $=$ {\rm{swap}}\,({\it{i\/}}, {\it{j\/}}, {\rm{swap}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{swap})\index{swap})\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{sublst-ileq} \\  
\=\+{\rm{sublst-ileq}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{sublst-ileq} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{r\/}} $<$ {\it{l\/}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{ileq}}\,({\it{x\/}}, {\rm{get-nth}}\,({\it{l\/}}, {\it{lst\/}})\index{get-nth})\index{ileq} $\wedge$ {\rm{sublst-ileq}}\,({\it{x\/}}, $1\;+$ {\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{sublst-ileq}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{sublsts-ileq} \\  
\=\+{\rm{sublsts-ileq}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{l1\/}}, {\it{r1\/}}, {\it{lst1\/}})\index{sublsts-ileq} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{r\/}} $<$ {\it{l\/}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }\=\+{\rm{sublst-ileq}}\,({\rm{get-nth}}\,({\it{l\/}}, {\it{lst\/}})\index{get-nth}, {\it{l1\/}}, {\it{r1\/}}, {\it{lst1\/}})\index{sublst-ileq} \\ 
$\wedge$$\;\;\;\;${\rm{sublsts-ileq}}\,($1\;+$ {\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{l1\/}}, {\it{r1\/}}, {\it{lst1\/}})\index{sublsts-ileq}\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sublst-ileq-lemma \\ \index{sublst-ileq-lemma}
\=\+({\rm{sublst-ileq}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{sublst-ileq} $\wedge$ ({\it{l\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $\leq$ {\it{r\/}})) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\rm{get-nth}}\,({\it{j\/}}, {\it{lst\/}})\index{get-nth}, {\it{x\/}})\index{ilessp})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sublsts-ileq-la1 \\ \index{sublsts-ileq-la1}
\=\+({\rm{sublsts-ileq}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{l1\/}}, {\it{r1\/}}, {\it{lst1\/}})\index{sublsts-ileq} $\wedge$ ({\it{l\/}} $\leq$ {\it{i\/}}) $\wedge$ ({\it{i\/}} $\leq$ {\it{r\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{sublst-ileq}}\,({\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth}, {\it{l1\/}}, {\it{r1\/}}, {\it{lst1\/}})\index{sublst-ileq}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sublst-ileq-put \\ \index{sublst-ileq-put}
\=\+({\rm{ileq}}\,({\it{x\/}}, {\it{y\/}})\index{ileq} $\wedge$ {\rm{ileq}}\,({\it{x\/}}, {\rm{get-nth}}\,({\it{j\/}}, {\it{lst\/}})\index{get-nth})\index{ileq}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{sublst-ileq}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\rm{put-nth}}\,({\it{y\/}}, {\it{j\/}}, {\it{lst\/}})\index{put-nth})\index{sublst-ileq} $=$ {\rm{sublst-ileq}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{sublst-ileq})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sublsts-ileq-put \\ \index{sublsts-ileq-put}
\=\+({\rm{sublst-ileq}}\,({\it{y\/}}, {\it{l1\/}}, {\it{r1\/}}, {\it{lst1\/}})\index{sublst-ileq} $\wedge$ {\rm{sublst-ileq}}\,({\rm{get-nth}}\,({\it{j\/}}, {\it{lst\/}})\index{get-nth}, {\it{l1\/}}, {\it{r1\/}}, {\it{lst1\/}})\index{sublst-ileq}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{sublsts-ileq}}\,({\it{l\/}}, {\it{r\/}}, {\rm{put-nth}}\,({\it{y\/}}, {\it{j\/}}, {\it{lst\/}})\index{put-nth}, {\it{l1\/}}, {\it{r1\/}}, {\it{lst1\/}})\index{sublsts-ileq} \\ 
$=$$\;\;\;\;${\rm{sublsts-ileq}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{l1\/}}, {\it{r1\/}}, {\it{lst1\/}})\index{sublsts-ileq})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sublst-ileq-swap-la \\ \index{sublst-ileq-swap-la}
\=\+(\=\+{\rm{sublst-ileq}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{sublst-ileq} \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $\leq$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\leq$ {\it{r\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $\leq$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\leq$ {\it{r\/}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{sublst-ileq}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\rm{swap}}\,({\it{i\/}}, {\it{j\/}}, {\it{lst\/}})\index{swap})\index{sublst-ileq}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sublsts-ileq-swap-la \\ \index{sublsts-ileq-swap-la}
\=\+(\=\+{\rm{sublsts-ileq}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{l1\/}}, {\it{r1\/}}, {\it{lst1\/}})\index{sublsts-ileq} \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $\leq$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\leq$ {\it{r\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $\leq$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\leq$ {\it{r\/}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{sublsts-ileq}}\,({\it{l\/}}, {\it{r\/}}, {\rm{swap}}\,({\it{i\/}}, {\it{j\/}}, {\it{lst\/}})\index{swap}, {\it{l1\/}}, {\it{r1\/}}, {\it{lst1\/}})\index{sublsts-ileq}\-
\end{tabbing}


\noindent{\sc Event}:   Disable swap.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  sublst-ileq-swap-swap \\ \index{sublst-ileq-swap-swap}
{\rm{sublst-ileq}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\rm{swap}}\,({\it{i\/}}, {\it{j\/}}, {\rm{swap}}\,({\it{i\/}}, {\it{j\/}}, {\it{lst\/}})\index{swap})\index{swap})\index{sublst-ileq} $=$ {\rm{sublst-ileq}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{sublst-ileq}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sublst-ileq-swap \\ \index{sublst-ileq-swap}
\=\+(({\it{l\/}} $\leq$ {\it{i\/}}) $\wedge$ ({\it{i\/}} $\leq$ {\it{r\/}}) $\wedge$ ({\it{l\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $\leq$ {\it{r\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{sublst-ileq}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\rm{swap}}\,({\it{i\/}}, {\it{j\/}}, {\it{lst\/}})\index{swap})\index{sublst-ileq} $=$ {\rm{sublst-ileq}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{sublst-ileq})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sublsts-ileq-swap-swap \\ \index{sublsts-ileq-swap-swap}
\=\+{\rm{sublsts-ileq}}\,({\it{l\/}}, {\it{r\/}}, {\rm{swap}}\,({\it{i\/}}, {\it{j\/}}, {\rm{swap}}\,({\it{i\/}}, {\it{j\/}}, {\it{lst\/}})\index{swap})\index{swap}, {\it{l1\/}}, {\it{r1\/}}, {\it{lst1\/}})\index{sublsts-ileq} \\ 
$=$$\;\;\;\;${\rm{sublsts-ileq}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{l1\/}}, {\it{r1\/}}, {\it{lst1\/}})\index{sublsts-ileq}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sublsts-ileq-swap \\ \index{sublsts-ileq-swap}
\=\+(({\it{l\/}} $\leq$ {\it{i\/}}) $\wedge$ ({\it{i\/}} $\leq$ {\it{r\/}}) $\wedge$ ({\it{l\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $\leq$ {\it{r\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{sublsts-ileq}}\,({\it{l\/}}, {\it{r\/}}, {\rm{swap}}\,({\it{i\/}}, {\it{j\/}}, {\it{lst\/}})\index{swap}, {\it{l1\/}}, {\it{r1\/}}, {\it{lst1\/}})\index{sublsts-ileq} \\ 
$=$$\;\;\;\;${\rm{sublsts-ileq}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{l1\/}}, {\it{r1\/}}, {\it{lst1\/}})\index{sublsts-ileq})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sublst-ileq-qpart-aux \\ \index{sublst-ileq-qpart-aux}
\=\+(\=\+({\it{l\/}} $\leq$ {\it{last\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{last\/}} $<$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{last\/}} $\leq$ {\it{r\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $\leq$ {\it{l1\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{l1\/}} $\leq$ {\it{r\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{r1\/}} $\leq$ {\it{r\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{sublst-ileq}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\rm{qpart-aux}}\,({\it{l1\/}}, {\it{r1\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qpart-aux})\index{sublst-ileq} \\ 
$=$$\;\;\;\;${\rm{sublst-ileq}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{sublst-ileq})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sublsts-ileq-qpart-aux \\ \index{sublsts-ileq-qpart-aux}
\=\+(\=\+({\it{l\/}} $\leq$ {\it{last\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{last\/}} $<$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{last\/}} $\leq$ {\it{r2\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $\leq$ {\it{l2\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{l2\/}} $\leq$ {\it{r\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{r2\/}} $\leq$ {\it{r\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{sublsts-ileq}}\,({\it{l\/}}, {\it{r\/}}, {\rm{qpart-aux}}\,({\it{l2\/}}, {\it{r2\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qpart-aux}, {\it{l1\/}}, {\it{r1\/}}, {\it{lst1\/}})\index{sublsts-ileq} \\ 
$=$$\;\;\;\;${\rm{sublsts-ileq}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{l1\/}}, {\it{r1\/}}, {\it{lst1\/}})\index{sublsts-ileq})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sublst-ileq-qsort \\ \index{sublst-ileq-qsort}
\=\+(({\it{l\/}} $\leq$ {\it{l1\/}}) $\wedge$ ({\it{r1\/}} $\leq$ {\it{r\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{sublst-ileq}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\rm{qsort}}\,({\it{l1\/}}, {\it{r1\/}}, {\it{lst\/}})\index{qsort})\index{sublst-ileq} $=$ {\rm{sublst-ileq}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{sublst-ileq})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sublsts-ileq-qsort1 \\ \index{sublsts-ileq-qsort1}
\=\+(({\it{l\/}} $\leq$ {\it{l2\/}}) $\wedge$ ({\it{r2\/}} $\leq$ {\it{r\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{sublsts-ileq}}\,({\it{l\/}}, {\it{r\/}}, {\rm{qsort}}\,({\it{l2\/}}, {\it{r2\/}}, {\it{lst\/}})\index{qsort}, {\it{l1\/}}, {\it{r1\/}}, {\it{lst1\/}})\index{sublsts-ileq} \\ 
$=$$\;\;\;\;${\rm{sublsts-ileq}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{l1\/}}, {\it{r1\/}}, {\it{lst1\/}})\index{sublsts-ileq})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sublsts-ileq-qsort2 \\ \index{sublsts-ileq-qsort2}
\=\+(({\it{l1\/}} $\leq$ {\it{l2\/}}) $\wedge$ ({\it{r2\/}} $\leq$ {\it{r1\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{sublsts-ileq}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{l1\/}}, {\it{r1\/}}, {\rm{qsort}}\,({\it{l2\/}}, {\it{r2\/}}, {\it{lst1\/}})\index{qsort})\index{sublsts-ileq} \\ 
$=$$\;\;\;\;${\rm{sublsts-ileq}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{l1\/}}, {\it{r1\/}}, {\it{lst1\/}})\index{sublsts-ileq})\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{qpartx} \\  
\=\+{\rm{qpartx}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qpartx} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{r\/}} $<$ {\it{i\/}}$\;\;${\bf then }{\it{lst\/}} \\ 
{\bf elseif }{\rm{ilessp}}\,({\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth}, {\rm{get-nth}}\,({\it{l\/}}, {\it{lst\/}})\index{get-nth})\index{ilessp} \\ 
{\bf then }{\rm{qpartx}}\,({\it{l\/}}, {\it{r\/}}, {\rm{swap}}\,($1\;+$ {\it{last\/}}, {\it{i\/}}, {\it{lst\/}})\index{swap}, $1\;+$ {\it{last\/}}, $1\;+$ {\it{i\/}})\index{qpartx} \\ 
{\bf else }{\rm{qpartx}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{last\/}}, $1\;+$ {\it{i\/}})\index{qpartx}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qpart-aux-qpartx \\ \index{qpart-aux-qpartx}
\=\+{\rm{qpart-aux}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qpart-aux} \\ 
$=$$\;\;\;\;${\rm{swap}}\,({\it{l\/}}, {\rm{qlast-aux}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qlast-aux}, {\rm{qpartx}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qpartx})\index{swap}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qpartx-get-1 \\ \index{qpartx-get-1}
\=\+(({\it{last\/}} $<$ {\it{i\/}}) $\wedge$ ({\it{right\/}} $<$ {\it{j\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\rm{qpartx}}\,({\it{left\/}}, {\it{right\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qpartx})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{j\/}}, {\it{lst\/}})\index{get-nth})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qpartx-get-2 \\ \index{qpartx-get-2}
\=\+(({\it{last\/}} $<$ {\it{i\/}}) $\wedge$ ({\it{j\/}} $\leq$ {\it{last\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\rm{qpartx}}\,({\it{left\/}}, {\it{right\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qpartx})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{j\/}}, {\it{lst\/}})\index{get-nth})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qpartx-ilessp-1 \\ \index{qpartx-ilessp-1}
\=\+(\=\+({\it{l\/}} $\leq$ {\it{last\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{last\/}} $<$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{last\/}} $<$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\leq$ {\rm{qlast-aux}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qlast-aux}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{ilessp}}\,({\rm{get-nth}}\,({\it{j\/}}, {\rm{qpartx}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qpartx})\index{get-nth}, {\rm{get-nth}}\,({\it{l\/}}, {\it{lst\/}})\index{get-nth})\index{ilessp}\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{open-sublst-ileq} \\  
\=\+{\rm{open-sublst-ileq}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{open-sublst-ileq} \\ 
$=$$\;\;\;\;$\=\+{\bf if }($1\;+$ {\it{l\/}}) $<$ {\it{r\/}} \\ 
{\bf then }{\rm{ileq}}\,({\it{x\/}}, {\rm{get-nth}}\,($1\;+$ {\it{l\/}}, {\it{lst\/}})\index{get-nth})\index{ileq} $\wedge$ {\rm{open-sublst-ileq}}\,({\it{x\/}}, $1\;+$ {\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{open-sublst-ileq} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  open-sublst-ileq-la0 \\ \index{open-sublst-ileq-la0}
(($1\;+$ {\it{l\/}}) $\not<$ {\it{r\/}}) $\rightarrow$ {\rm{open-sublst-ileq}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{open-sublst-ileq}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  open-sublst-ileq-la1 \\ \index{open-sublst-ileq-la1}
\=\+({\rm{open-sublst-ileq}}\,({\it{x\/}}, {\it{last\/}}, {\it{i\/}}, {\it{lst\/}})\index{open-sublst-ileq} $\wedge$ ({\it{last\/}} $<$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $<$ {\it{i\/}})) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\rm{get-nth}}\,({\it{j\/}}, {\it{lst\/}})\index{get-nth}, {\it{x\/}})\index{ilessp})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  open-sublst-ileq-la2 \\ \index{open-sublst-ileq-la2}
\=\+{\rm{open-sublst-ileq}}\,({\it{x\/}}, {\it{last\/}}, $1\;+$ {\it{i\/}}, {\it{lst\/}})\index{open-sublst-ileq} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{ileq}}\,({\it{x\/}}, {\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth})\index{ileq}$\;\;${\bf then }{\rm{open-sublst-ileq}}\,({\it{x\/}}, {\it{last\/}}, {\it{i\/}}, {\it{lst\/}})\index{open-sublst-ileq} \\ 
{\bf else }($1\;+$ {\it{last\/}}) $\not<$ ($1\;+$ {\it{i\/}})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  open-sublst-ileq-la3 \\ \index{open-sublst-ileq-la3}
\=\+({\it{j\/}} $\leq$ {\it{l\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{open-sublst-ileq}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\rm{put-nth}}\,({\it{v\/}}, {\it{j\/}}, {\it{lst\/}})\index{put-nth})\index{open-sublst-ileq} \\ 
$=$$\;\;\;\;${\rm{open-sublst-ileq}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{open-sublst-ileq})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  open-sublst-ileq-la4 \\ \index{open-sublst-ileq-la4}
\=\+({\it{r\/}} $\leq$ {\it{j\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{open-sublst-ileq}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\rm{put-nth}}\,({\it{v\/}}, {\it{j\/}}, {\it{lst\/}})\index{put-nth})\index{open-sublst-ileq} \\ 
$=$$\;\;\;\;${\rm{open-sublst-ileq}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{open-sublst-ileq})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  open-sublst-ileq-la5 \\ \index{open-sublst-ileq-la5}
\=\+{\rm{open-sublst-ileq}}\,({\it{x\/}}, $1\;+$ {\it{last\/}}, $1\;+$ {\it{i\/}}, {\rm{swap}}\,($1\;+$ {\it{last\/}}, {\it{i\/}}, {\it{lst\/}})\index{swap})\index{open-sublst-ileq} \\ 
$=$$\;\;\;\;${\rm{open-sublst-ileq}}\,({\it{x\/}}, {\it{last\/}}, {\it{i\/}}, {\it{lst\/}})\index{open-sublst-ileq}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qpartx-ilessp-2 \\ \index{qpartx-ilessp-2}
\=\+(\=\+{\rm{open-sublst-ileq}}\,({\rm{get-nth}}\,({\it{l\/}}, {\it{lst\/}})\index{get-nth}, {\it{last\/}}, {\it{i\/}}, {\it{lst\/}})\index{open-sublst-ileq} \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $\leq$ {\it{last\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{last\/}} $<$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{qlast-aux}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qlast-aux} $<$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\leq$ {\it{r\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\rm{get-nth}}\,({\it{j\/}}, {\rm{qpartx}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qpartx})\index{get-nth}, {\rm{get-nth}}\,({\it{l\/}}, {\it{lst\/}})\index{get-nth})\index{ilessp})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  open-sublst-ileq-la6 \\ \index{open-sublst-ileq-la6}
{\rm{open-sublst-ileq}}\,({\rm{get-nth}}\,({\it{l\/}}, {\it{lst\/}})\index{get-nth}, {\it{l\/}}, $1\;+$ {\it{l\/}}, {\it{lst\/}})\index{open-sublst-ileq}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qpart-ilessp-la1-la \\ \index{qpart-ilessp-la1-la}
\=\+(({\it{l\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $<$ {\rm{qlast-aux}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{l\/}}, $1\;+$ {\it{l\/}})\index{qlast-aux})) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\rm{get-nth}}\,({\it{l\/}}, {\it{lst\/}})\index{get-nth}, {\rm{get-nth}}\,({\it{j\/}}, {\rm{qpart-aux}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{l\/}}, $1\;+$ {\it{l\/}})\index{qpart-aux})\index{get-nth})\index{ilessp})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qpart-ilessp-la1 \\ \index{qpart-ilessp-la1}
\=\+(({\it{l\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $\leq$ ({\rm{qlast-aux}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{l\/}}, $1\;+$ {\it{l\/}})\index{qlast-aux} $-\;1$))) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\rm{get-nth}}\,({\it{l\/}}, {\it{lst\/}})\index{get-nth}, {\rm{get-nth}}\,({\it{j\/}}, {\rm{qpart-aux}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{l\/}}, $1\;+$ {\it{l\/}})\index{qpart-aux})\index{get-nth})\index{ilessp})\-
\end{tabbing}     

\begin{tabbing}{\sc Theorem}:  qpart-ilessp-la2 \\ \index{qpart-ilessp-la2}
\=\+(({\rm{qlast-aux}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{l\/}}, $1\;+$ {\it{l\/}})\index{qlast-aux} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $\leq$ {\it{r\/}})) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\rm{get-nth}}\,({\it{j\/}}, {\rm{qpart-aux}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{l\/}}, $1\;+$ {\it{l\/}})\index{qpart-aux})\index{get-nth}, {\rm{get-nth}}\,({\it{l\/}}, {\it{lst\/}})\index{get-nth})\index{ilessp})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qpart-equal \\ \index{qpart-equal}
\=\+(({\it{l\/}} $\leq$ {\it{last\/}}) $\wedge$ ({\it{last\/}} $<$ {\it{i\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{get-nth}}\,({\rm{qlast-aux}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qlast-aux}, {\rm{qpart-aux}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qpart-aux})\index{get-nth} \\ 
$=$$\;\;\;\;${\rm{get-nth}}\,({\it{l\/}}, {\it{lst\/}})\index{get-nth})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-get-1 \\ \index{qsort-get-1}
({\it{j\/}} $<$ {\it{left\/}}) $\rightarrow$ ({\rm{get-nth}}\,({\it{j\/}}, {\rm{qsort}}\,({\it{left\/}}, {\it{right\/}}, {\it{lst\/}})\index{qsort})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{j\/}}, {\it{lst\/}})\index{get-nth})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  get-swap-1 \\ \index{get-swap-1}
(({\it{j\/}} $<$ {\it{i\/}}) $\wedge$ ({\it{k\/}} $<$ {\it{i\/}})) $\rightarrow$ ({\rm{get-nth}}\,({\it{i\/}}, {\rm{swap}}\,({\it{j\/}}, {\it{k\/}}, {\it{lst\/}})\index{swap})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth})
\end{tabbing}
     
\begin{tabbing}{\sc Theorem}:  qlast-aux-swap \\ \index{qlast-aux-swap}
\=\+(({\it{l\/}} $\leq$ {\it{last\/}}) $\wedge$ ({\it{last\/}} $<$ {\it{i\/}}) $\wedge$ ({\it{a\/}} $<$ {\it{l\/}}) $\wedge$ ({\it{b\/}} $<$ {\it{l\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{qlast-aux}}\,({\it{l\/}}, {\it{r\/}}, {\rm{swap}}\,({\it{a\/}}, {\it{b\/}}, {\it{lst\/}})\index{swap}, {\it{last\/}}, {\it{i\/}})\index{qlast-aux} $=$ {\rm{qlast-aux}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qlast-aux})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qlast-swap \\ \index{qlast-swap}
\=\+(({\it{l\/}} $<$ {\it{r\/}}) $\wedge$ ({\it{a\/}} $<$ {\it{l\/}}) $\wedge$ ({\it{b\/}} $<$ {\it{l\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\rm{swap}}\,({\it{a\/}}, {\it{b\/}}, {\it{lst\/}})\index{swap})\index{qlast} $=$ {\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qpart-aux-swap \\ \index{qpart-aux-swap}
\=\+(({\it{l\/}} $\leq$ {\it{last\/}}) $\wedge$ ({\it{last\/}} $<$ {\it{i\/}}) $\wedge$ ({\it{a\/}} $<$ {\it{l\/}}) $\wedge$ ({\it{b\/}} $<$ {\it{l\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{qpart-aux}}\,({\it{l\/}}, {\it{r\/}}, {\rm{swap}}\,({\it{a\/}}, {\it{b\/}}, {\it{lst\/}})\index{swap}, {\it{last\/}}, {\it{i\/}})\index{qpart-aux} \\ 
$=$$\;\;\;\;${\rm{swap}}\,({\it{a\/}}, {\it{b\/}}, {\rm{qpart-aux}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qpart-aux})\index{swap})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qpart-swap \\ \index{qpart-swap}
\=\+(({\it{l\/}} $<$ {\it{r\/}}) $\wedge$ ({\it{a\/}} $<$ {\it{l\/}}) $\wedge$ ({\it{b\/}} $<$ {\it{l\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\rm{swap}}\,({\it{a\/}}, {\it{b\/}}, {\it{lst\/}})\index{swap})\index{qpart} $=$ {\rm{swap}}\,({\it{a\/}}, {\it{b\/}}, {\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qpart})\index{swap})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-swap \\ \index{qsort-swap}
\=\+(({\it{i\/}} $<$ {\it{l\/}}) $\wedge$ ({\it{j\/}} $<$ {\it{l\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{qsort}}\,({\it{l\/}}, {\it{r\/}}, {\rm{swap}}\,({\it{i\/}}, {\it{j\/}}, {\it{lst\/}})\index{swap})\index{qsort} $=$ {\rm{swap}}\,({\it{i\/}}, {\it{j\/}}, {\rm{qsort}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qsort})\index{swap})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-qpartx \\ \index{qsort-qpartx}
\=\+(({\it{l\/}} $\leq$ {\it{r\/}}) $\wedge$ ({\it{l\/}} $\leq$ {\it{last\/}}) $\wedge$ ({\it{last\/}} $<$ {\it{i\/}}) $\wedge$ ({\it{last\/}} $\leq$ {\it{r\/}}) $\wedge$ ({\it{r\/}} $<$ {\it{l1\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{qsort}}\,({\it{l1\/}}, {\it{r1\/}}, {\rm{qpartx}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qpartx})\index{qsort} \\ 
$=$$\;\;\;\;${\rm{qpartx}}\,({\it{l\/}}, {\it{r\/}}, {\rm{qsort}}\,({\it{l1\/}}, {\it{r1\/}}, {\it{lst\/}})\index{qsort}, {\it{last\/}}, {\it{i\/}})\index{qpartx})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-get-2 \\ \index{qsort-get-2}
\=\+({\it{r\/}} $<$ {\it{l1\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{get-nth}}\,({\it{j\/}}, {\rm{qsort}}\,({\it{l1\/}}, {\it{r1\/}}, {\rm{qsort}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qsort})\index{qsort})\index{get-nth} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{r\/}} $<$ {\it{j\/}}$\;\;${\bf then }{\rm{get-nth}}\,({\it{j\/}}, {\rm{qsort}}\,({\it{l1\/}}, {\it{r1\/}}, {\it{lst\/}})\index{qsort})\index{get-nth} \\ 
{\bf else }{\rm{get-nth}}\,({\it{j\/}}, {\rm{qsort}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qsort})\index{get-nth}$\;${\bf  endif}\-)\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable qpart-aux-qpartx.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  ilessp-trans \\ \index{ilessp-trans}
({\rm{ilessp}}\,({\it{a\/}}, {\it{b\/}})\index{ilessp} $\wedge$ {\rm{ileq}}\,({\it{b\/}}, {\it{c\/}})\index{ileq}) $\rightarrow$ {\rm{ilessp}}\,({\it{a\/}}, {\it{c\/}})\index{ilessp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qpart-ilessp \\ \index{qpart-ilessp}
\=\+(\=\+({\it{l\/}} $\leq$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\leq$ {\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast}) \\ 
$\wedge$$\;\;\;\;$({\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast} $\leq$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\leq$ {\it{r\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\rm{get-nth}}\,({\it{j\/}}, {\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qpart})\index{get-nth}, {\rm{get-nth}}\,({\it{i\/}}, {\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qpart})\index{get-nth})\index{ilessp})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-get3 \\ \index{qsort-get3}
\=\+{\rm{get-nth}}\,({\it{j\/}}, {\rm{qsort}}\,($1\;+$ {\it{last\/}}, {\it{r\/}}, {\rm{qsort}}\,({\it{l\/}}, {\it{last\/}} $-\;1$, {\it{lst\/}})\index{qsort})\index{qsort})\index{get-nth} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{j\/}} $\leq$ ({\it{last\/}} $-\;1$)$\;\;${\bf then }{\rm{get-nth}}\,({\it{j\/}}, {\rm{qsort}}\,({\it{l\/}}, {\it{last\/}} $-\;1$, {\it{lst\/}})\index{qsort})\index{get-nth} \\ 
{\bf else }{\rm{get-nth}}\,({\it{j\/}}, {\rm{qsort}}\,($1\;+$ {\it{last\/}}, {\it{r\/}}, {\it{lst\/}})\index{qsort})\index{get-nth}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sublsts-ileq-la2 \\ \index{sublsts-ileq-la2}
\=\+(\=\+{\rm{sublsts-ileq}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{l1\/}}, {\it{r1\/}}, {\it{lst1\/}})\index{sublsts-ileq} \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $\leq$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\leq$ {\it{r\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{l1\/}} $\leq$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\leq$ {\it{r1\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\rm{get-nth}}\,({\it{j\/}}, {\it{lst1\/}})\index{get-nth}, {\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth})\index{ilessp})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qpart-ilessp-closed-1 \\ \index{qpart-ilessp-closed-1}
\=\+({\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast} $\leq$ {\it{last\/}}) \\ 
$\rightarrow$$\;\;\;\;${\rm{sublst-ileq}}\,(\=\+{\rm{get-nth}}\,({\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast}, {\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qpart})\index{get-nth}, \\ 
{\it{last\/}}, \\ 
{\it{r\/}}, \\ 
{\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qpart})\-\index{sublst-ileq}\-
\end{tabbing}
             
\begin{tabbing}{\sc Theorem}:  qsort-ilessp-1 \\ \index{qsort-ilessp-1}
\=\+{\bf let }\=\+{\it{lst1\/}}{\bf $\;$ be$\;\;$}{\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qpart}, \\ 
{\it{last\/}}{\bf $\;$ be$\;\;$}{\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast}\- \\ 
{\bf in} \\ 
\=\+(({\it{last\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $\leq$ {\it{r\/}})) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,(\=\+{\rm{get-nth}}\,({\it{j\/}}, {\rm{qsort}}\,($1\;+$ {\it{last\/}}, {\it{r\/}}, {\it{lst1\/}})\index{qsort})\index{get-nth}, \\ 
{\rm{get-nth}}\,({\it{last\/}}, {\it{lst1\/}})\index{get-nth})\-\index{ilessp})\-$\;${\bf  endlet}\-
\end{tabbing}     

\begin{tabbing}{\sc Theorem}:  qpart-ilessp-closed-2 \\ \index{qpart-ilessp-closed-2}
\=\+{\bf let }\=\+{\it{lst1\/}}{\bf $\;$ be$\;\;$}{\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qpart}\- \\ 
{\bf in} \\ 
\=\+(\=\+({\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast} $\leq$ {\it{last\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $\leq$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\leq$ ({\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast} $-\;1$)))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{sublst-ileq}}\,({\rm{get-nth}}\,({\it{j\/}}, {\it{lst1\/}})\index{get-nth}, {\it{last\/}}, {\it{r\/}}, {\it{lst1\/}})\index{sublst-ileq}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qpart-ilessp-closed-3 \\ \index{qpart-ilessp-closed-3}
\=\+{\bf let }\=\+{\it{last\/}}{\bf $\;$ be$\;\;$}{\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast}, \\ 
{\it{lst1\/}}{\bf $\;$ be$\;\;$}{\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qpart}\- \\ 
{\bf in} \\ 
({\it{l\/}} $\leq$ {\it{l1\/}}) $\rightarrow$ {\rm{sublsts-ileq}}\,({\it{l1\/}}, {\it{last\/}} $-\;1$, {\it{lst1\/}}, {\it{last\/}}, {\it{r\/}}, {\it{lst1\/}})\index{sublsts-ileq}$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-ilessp-2 \\ \index{qsort-ilessp-2}
\=\+{\bf let }\=\+{\it{lst1\/}}{\bf $\;$ be$\;\;$}{\rm{qpart}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qpart}, \\ 
{\it{last\/}}{\bf $\;$ be$\;\;$}{\rm{qlast}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qlast}\- \\ 
{\bf in} \\ 
\=\+(({\it{l\/}} $\leq$ {\it{i\/}}) $\wedge$ ({\it{i\/}} $\leq$ ({\it{last\/}} $-\;1$)) $\wedge$ ({\it{last\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $\leq$ {\it{r\/}})) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,(\=\+{\rm{get-nth}}\,({\it{j\/}}, {\rm{qsort}}\,($1\;+$ {\it{last\/}}, {\it{r\/}}, {\it{lst1\/}})\index{qsort})\index{get-nth}, \\ 
{\rm{get-nth}}\,({\it{i\/}}, {\rm{qsort}}\,({\it{l\/}}, {\it{last\/}} $-\;1$, {\it{lst1\/}})\index{qsort})\index{get-nth})\-\index{ilessp})\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-ordered \\ \index{qsort-ordered}
\=\+(({\it{left\/}} $\leq$ {\it{i\/}}) $\wedge$ ({\it{i\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $\leq$ {\it{right\/}})) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,(\=\+{\rm{get-nth}}\,({\it{j\/}}, {\rm{qsort}}\,({\it{left\/}}, {\it{right\/}}, {\it{lst\/}})\index{qsort})\index{get-nth}, \\ 
{\rm{get-nth}}\,({\it{i\/}}, {\rm{qsort}}\,({\it{left\/}}, {\it{right\/}}, {\it{lst\/}})\index{qsort})\index{get-nth})\-\index{ilessp})\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{orderedp1} \\  
\=\+{\rm{orderedp1}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{orderedp1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{r\/}} $\leq$ {\it{l\/}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }\=\+{\rm{ileq}}\,({\rm{get-nth}}\,({\it{l\/}}, {\it{lst\/}})\index{get-nth}, {\rm{get-nth}}\,($1\;+$ {\it{l\/}}, {\it{lst\/}})\index{get-nth})\index{ileq} \\ 
$\wedge$$\;\;\;\;${\rm{orderedp1}}\,($1\;+$ {\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{orderedp1}\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-orderedp1-la \\ \index{qsort-orderedp1-la}
({\it{left\/}} $\leq$ {\it{left1\/}}) $\rightarrow$ {\rm{orderedp1}}\,({\it{left1\/}}, {\it{right\/}}, {\rm{qsort}}\,({\it{left\/}}, {\it{right\/}}, {\it{lst\/}})\index{qsort})\index{orderedp1}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qsort-orderedp1 \\ \index{qsort-orderedp1}
{\rm{orderedp1}}\,({\it{left\/}}, {\it{right\/}}, {\rm{qsort}}\,({\it{left\/}}, {\it{right\/}}, {\it{lst\/}})\index{qsort})\index{orderedp1}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{transwap}$\;\;$
{\rm{transwap}}\,({\it{i\/}}, {\it{lst\/}})\index{transwap} $=$ {\rm{swap}}\,({\it{i\/}}, $1\;+$ {\it{i\/}}, {\it{lst\/}})\index{swap}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{lst-eq} \\  
\=\+{\rm{lst-eq}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{lst1\/}})\index{lst-eq} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{r\/}} $<$ {\it{l\/}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }\=\+({\rm{get-nth}}\,({\it{l\/}}, {\it{lst\/}})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{l\/}}, {\it{lst1\/}})\index{get-nth}) \\ 
$\wedge$$\;\;\;\;${\rm{lst-eq}}\,($1\;+$ {\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{lst1\/}})\index{lst-eq}\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{count-lst} \\  
\=\+{\rm{count-lst}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{count-lst} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{r\/}} $<$ {\it{l\/}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{x\/}} $=$ {\rm{get-nth}}\,({\it{l\/}}, {\it{lst\/}})\index{get-nth}$\;\;${\bf then }$1\;+$ {\rm{count-lst}}\,({\it{x\/}}, $1\;+$ {\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{count-lst} \\ 
{\bf else }{\rm{count-lst}}\,({\it{x\/}}, $1\;+$ {\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{count-lst}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  count-lst-0 \\ \index{count-lst-0}
({\it{l\/}} $\not\in\;${\bf{N}}${}$) $\rightarrow$ ({\rm{count-lst}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{count-lst} $=$ {\rm{count-lst}}\,({\it{x\/}}, {\tt{0}}, {\it{r\/}}, {\it{lst\/}})\index{count-lst})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  count-swapii \\ \index{count-swapii}
{\rm{count-lst}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\rm{swap}}\,({\it{i\/}}, {\it{i\/}}, {\it{lst\/}})\index{swap})\index{count-lst} $=$ {\rm{count-lst}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{count-lst}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  count-lst-put-1 \\ \index{count-lst-put-1}
({\it{i\/}} $<$ {\it{l\/}}) $\rightarrow$ ({\rm{count-lst}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\rm{put-nth}}\,({\it{v\/}}, {\it{i\/}}, {\it{lst\/}})\index{put-nth})\index{count-lst} $=$ {\rm{count-lst}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{count-lst})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  count-lst-swap-1 \\ \index{count-lst-swap-1}
\=\+(({\it{i\/}} $<$ {\it{l\/}}) $\wedge$ ({\it{j\/}} $<$ {\it{l\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{count-lst}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\rm{swap}}\,({\it{i\/}}, {\it{j\/}}, {\it{lst\/}})\index{swap})\index{count-lst} $=$ {\rm{count-lst}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{count-lst})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  count-transwap-0 \\ \index{count-transwap-0}
({\it{l\/}} $<$ {\it{r\/}}) $\rightarrow$ ({\rm{count-lst}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\rm{swap}}\,({\it{l\/}}, $1\;+$ {\it{l\/}}, {\it{lst\/}})\index{swap})\index{count-lst} $=$ {\rm{count-lst}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{count-lst})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  swap-0 \\ \index{swap-0}
\=\+({\it{i\/}} $\not\in\;${\bf{N}}${}$) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{swap}}\,({\it{i\/}}, {\it{j\/}}, {\it{lst\/}})\index{swap} $=$ {\rm{swap}}\,({\tt{0}}, {\it{j\/}}, {\it{lst\/}})\index{swap}) \\ 
$\wedge$$\;\;\;\;$({\rm{swap}}\,({\it{j\/}}, {\it{i\/}}, {\it{lst\/}})\index{swap} $=$ {\rm{swap}}\,({\it{j\/}}, {\tt{0}}, {\it{lst\/}})\index{swap}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  count-transwap \\ \index{count-transwap}
\=\+(({\it{l\/}} $\leq$ {\it{i\/}}) $\wedge$ ({\it{i\/}} $<$ {\it{r\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{count-lst}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\rm{transwap}}\,({\it{i\/}}, {\it{lst\/}})\index{transwap})\index{count-lst} $=$ {\rm{count-lst}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{count-lst})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  swap-rec-la \\ \index{swap-rec-la}
\=\+({\it{i\/}} $\leq$ {\it{j\/}}) \\ 
$\rightarrow$$\;\;\;\;${\rm{lst-eq}}\,({\it{l\/}}, {\it{r\/}}, {\rm{swap}}\,({\it{i\/}}, $1\;+$ {\it{j\/}}, {\it{lst\/}})\index{swap}, {\rm{swap}}\,({\it{i\/}}, {\it{j\/}}, {\rm{swap}}\,({\it{j\/}}, $1\;+$ {\it{j\/}}, {\rm{swap}}\,({\it{i\/}}, {\it{j\/}}, {\it{lst\/}})\index{swap})\index{swap})\index{swap})\index{lst-eq}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  count-lst-eq \\ \index{count-lst-eq}
{\rm{lst-eq}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}}, {\it{lst1\/}})\index{lst-eq} $\rightarrow$ ({\rm{count-lst}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{count-lst} $=$ {\rm{count-lst}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\it{lst1\/}})\index{count-lst})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  count-lst-swap-rec \\ \index{count-lst-swap-rec}
\=\+({\it{i\/}} $\leq$ {\it{j\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{count-lst}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\rm{swap}}\,({\it{i\/}}, $1\;+$ {\it{j\/}}, {\it{lst\/}})\index{swap})\index{count-lst} \\ 
$=$$\;\;\;\;${\rm{count-lst}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\rm{swap}}\,({\it{i\/}}, {\it{j\/}}, {\rm{transwap}}\,({\it{j\/}}, {\rm{swap}}\,({\it{i\/}}, {\it{j\/}}, {\it{lst\/}})\index{swap})\index{transwap})\index{swap})\index{count-lst})\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{swap-induct} \\  
\=\+{\rm{swap-induct}}\,({\it{i\/}}, {\it{j\/}}, {\it{lst\/}})\index{swap-induct} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{j\/}} $\leq$ {\it{i\/}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }\=\+{\rm{swap-induct}}\,({\it{i\/}}, {\it{j\/}} $-\;1$, {\rm{transwap}}\,({\it{j\/}} $-\;1$, {\rm{swap}}\,({\it{i\/}}, {\it{j\/}} $-\;1$, {\it{lst\/}})\index{swap})\index{transwap})\index{swap-induct} \\ 
$\wedge$$\;\;\;\;${\rm{swap-induct}}\,({\it{i\/}}, {\it{j\/}} $-\;1$, {\it{lst\/}})\index{swap-induct}\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  count-lst-swap \\ \index{count-lst-swap}
\=\+(({\it{l\/}} $\leq$ {\it{i\/}}) $\wedge$ ({\it{i\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $\leq$ {\it{r\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{count-lst}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\rm{swap}}\,({\it{i\/}}, {\it{j\/}}, {\it{lst\/}})\index{swap})\index{count-lst} $=$ {\rm{count-lst}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{count-lst})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  count-lst-qpart-aux \\ \index{count-lst-qpart-aux}
\=\+(\=\+({\it{l1\/}} $\leq$ {\it{last\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{last\/}} $<$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{last\/}} $\leq$ {\it{r1\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $\leq$ {\it{l1\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{l1\/}} $\leq$ {\it{r\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{r1\/}} $\leq$ {\it{r\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{count-lst}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\rm{qpart-aux}}\,({\it{l1\/}}, {\it{r1\/}}, {\it{lst\/}}, {\it{last\/}}, {\it{i\/}})\index{qpart-aux})\index{count-lst} \\ 
$=$$\;\;\;\;${\rm{count-lst}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{count-lst})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  count-lst-qsort-la \\ \index{count-lst-qsort-la}
\=\+(({\it{l\/}} $\leq$ {\it{l1\/}}) $\wedge$ ({\it{r1\/}} $\leq$ {\it{r\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{count-lst}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\rm{qsort}}\,({\it{l1\/}}, {\it{r1\/}}, {\it{lst\/}})\index{qsort})\index{count-lst} $=$ {\rm{count-lst}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{count-lst})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  count-lst-qsort \\ \index{count-lst-qsort}
{\rm{count-lst}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\rm{qsort}}\,({\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{qsort})\index{count-lst} $=$ {\rm{count-lst}}\,({\it{x\/}}, {\it{l\/}}, {\it{r\/}}, {\it{lst\/}})\index{count-lst}
\end{tabbing}

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