\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.

|#

;         Proof of the Correctness of a Binary Search Program
;
\end{verbatim}
\noindent{\sc Event}:   Start with the library {\tt{"mc20-2"}} using the compiled version.

\addvspace{18pt}
\begin{verbatim}#|
The following C function BSEARCH determines if a given value x occurs
in the sorted array a.

/* from K&R */
/* bsearch:  find x in a[0] <= a[1] <= ... <= a[n-1] */
int bsearch (int x, int a[], int n)
{
  int low, high, mid;

  low = 0;
  high = n;
  while (low < high) {
    mid = (low + high) / 2;
    if (x < a[mid])
      high = mid;
    else if (x > a[mid])
      low = mid + 1;
    else return mid;
  }
  return -1;
}

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

0x22f0 <bsearch>:       linkw a6,#0
0x22f4 <bsearch+4>:     moveml d2-d3,sp@-
0x22f8 <bsearch+8>:     movel a6@(8),d3
0x22fc <bsearch+12>:    moveal a6@(12),a0
0x2300 <bsearch+16>:    clrl d1
0x2302 <bsearch+18>:    movel a6@(16),d2
0x2306 <bsearch+22>:    cmpl d1,d2
0x2308 <bsearch+24>:    ble 0x232a <bsearch+58>
0x230a <bsearch+26>:    movel d1,d0
0x230c <bsearch+28>:    addl d2,d0
0x230e <bsearch+30>:    bpl 0x2312 <bsearch+34>
0x2310 <bsearch+32>:    addql #1,d0
0x2312 <bsearch+34>:    asrl #1,d0
0x2314 <bsearch+36>:    cmpl 0(a0)[d0.l*4],d3
0x2318 <bsearch+40>:    bge 0x231e <bsearch+46>
0x231a <bsearch+42>:    movel d0,d2
0x231c <bsearch+44>:    bra 0x2306 <bsearch+22>
0x231e <bsearch+46>:    cmpl 0(a0)[d0.l*4],d3
0x2322 <bsearch+50>:    ble 0x232c <bsearch+60>
0x2324 <bsearch+52>:    movel d0,d1
0x2326 <bsearch+54>:    addql #1,d1
0x2328 <bsearch+56>:    bra 0x2306 <bsearch+22>
0x232a <bsearch+58>:    movel #-1,d0
0x232c <bsearch+60>:    moveml a6@(-8),d2-d3
0x2332 <bsearch+66>:    unlk a6
0x2334 <bsearch+68>:    rts

The machine code of the above program is:

<bsearch>:       0x4e56  0x0000  0x48e7  0x3000  0x262e  0x0008  0x206e  0x000c
<bsearch+16>:    0x4281  0x242e  0x0010  0xb481  0x6f20  0x2001  0xd082  0x6a02
<bsearch+32>:    0x5280  0xe280  0xb6b0  0x0c00  0x6c04  0x2400  0x60e8  0xb6b0
<bsearch+48>:    0x0c00  0x6f08  0x2200  0x5281  0x60dc  0x70ff  0x4cee  0x000c
<bsearch+64>:    0xfff8  0x4e5e  0x4e75

In the Logic, this is:

'(78      86      0       0       72      231     48      0
  38      46      0       8       32      110     0       12
  66      129     36      46      0       16      180     129
  111     32      32      1       208     130     106     2
  82      128     226     128     182     176     12      0
  108     4       36      0       96      232     182     176
  12      0       111     8       34      0       82      129
  96      220     112     255     76      238     0       12
  255     248     78      94      78      117)

|#

; in the logic, the above program is defined by (bsearch-code).
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{bsearch-code} \\  
\=\+{\sc{bsearch-code}}\index{bsearch-code} \\ 
$=$$\;\;\;\;${\tt{'}}{\tt{(}}\=\+{\tt{78}}{\tt{ }}{\tt{86}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{72}}{\tt{ }}{\tt{231}}{\tt{ }}{\tt{48}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{38}}{\tt{ }}{\tt{46}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{8}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{110}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{12}}{\tt{ }}{\tt{66}}{\tt{ }}{\tt{129}} \\ 
{\tt{36}}{\tt{ }}{\tt{46}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{16}}{\tt{ }}{\tt{180}}{\tt{ }}{\tt{129}}{\tt{ }}{\tt{111}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{1}}{\tt{ }}{\tt{208}}{\tt{ }}{\tt{130}}{\tt{ }}{\tt{106}}{\tt{ }}{\tt{2}}{\tt{ }}{\tt{82}}{\tt{ }}{\tt{128}} \\ 
{\tt{226}}{\tt{ }}{\tt{128}}{\tt{ }}{\tt{182}}{\tt{ }}{\tt{176}}{\tt{ }}{\tt{12}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{108}}{\tt{ }}{\tt{4}}{\tt{ }}{\tt{36}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{96}}{\tt{ }}{\tt{232}}{\tt{ }}{\tt{182}}{\tt{ }}{\tt{176}}{\tt{ }}{\tt{12}}{\tt{ }}{\tt{0}} \\ 
{\tt{111}}{\tt{ }}{\tt{8}}{\tt{ }}{\tt{34}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{82}}{\tt{ }}{\tt{129}}{\tt{ }}{\tt{96}}{\tt{ }}{\tt{220}}{\tt{ }}{\tt{112}}{\tt{ }}{\tt{255}}{\tt{ }}{\tt{76}}{\tt{ }}{\tt{238}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{12}}{\tt{ }}{\tt{255}}{\tt{ }}{\tt{248}} \\ 
{\tt{78}}{\tt{ }}{\tt{94}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{117}}{\tt{)}}\-\-
\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}:  ilessp-lessp \\ \index{ilessp-lessp}
(({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{y\/}} $\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}

\begin{verbatim}; bsearch1 is a function in the logic to simulate the loop of the
; above code.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{bsearch1} \\  
\=\+{\rm{bsearch1}}\,({\it{x\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{j\/}})\index{bsearch1} \\ 
$=$$\;\;\;\;$\=\+{\bf let }\=\+{\it{k\/}}{\bf $\;$ be$\;\;$}({\it{i\/}} $+$ {\it{j\/}}) $\div$ {\tt{2}}\- \\ 
{\bf in} \\ 
\=\+{\bf if }{\it{i\/}} $<$ {\it{j\/}} \\ 
{\bf then }\=\+{\bf if }{\rm{ilessp}}\,({\it{x\/}}, {\rm{get-nth}}\,({\it{k\/}}, {\it{lst\/}})\index{get-nth})\index{ilessp}$\;\;${\bf then }{\rm{bsearch1}}\,({\it{x\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{k\/}})\index{bsearch1} \\ 
{\bf elseif }{\rm{ilessp}}\,({\rm{get-nth}}\,({\it{k\/}}, {\it{lst\/}})\index{get-nth}, {\it{x\/}})\index{ilessp} \\ 
{\bf then }{\rm{bsearch1}}\,({\it{x\/}}, {\it{lst\/}}, $1\;+$ {\it{k\/}}, {\it{j\/}})\index{bsearch1} \\ 
{\bf else }{\it{k\/}}$\;${\bf  endif}\- \\ 
{\bf else }{\tt{-1}}$\;${\bf  endif}\-$\;${\bf  endlet}\-\-
\end{tabbing}

\begin{verbatim}; bsearch is a function in the logic to simulate the above code.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{bsearch}$\;\;$
{\rm{bsearch}}\,({\it{x\/}}, {\it{n\/}}, {\it{lst\/}})\index{bsearch} $=$ {\rm{bsearch1}}\,({\it{x\/}}, {\it{lst\/}}, {\tt{0}}, {\it{n\/}})\index{bsearch1}
\end{tabbing}

\begin{verbatim}; the computation time of the loop.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{bsearch1-t} \\  
\=\+{\rm{bsearch1-t}}\,({\it{x\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{j\/}})\index{bsearch1-t} \\ 
$=$$\;\;\;\;$\=\+{\bf let }\=\+{\it{k\/}}{\bf $\;$ be$\;\;$}({\it{i\/}} $+$ {\it{j\/}}) $\div$ {\tt{2}}\- \\ 
{\bf in} \\ 
\=\+{\bf if }{\it{i\/}} $<$ {\it{j\/}} \\ 
{\bf then }\=\+{\bf if }{\rm{ilessp}}\,({\it{x\/}}, {\rm{get-nth}}\,({\it{k\/}}, {\it{lst\/}})\index{get-nth})\index{ilessp} \\ 
{\bf then }{\rm{splus}}\,({\tt{10}}, {\rm{bsearch1-t}}\,({\it{x\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{k\/}})\index{bsearch1-t})\index{splus} \\ 
{\bf elseif }{\rm{ilessp}}\,({\rm{get-nth}}\,({\it{k\/}}, {\it{lst\/}})\index{get-nth}, {\it{x\/}})\index{ilessp} \\ 
{\bf then }{\rm{splus}}\,({\tt{13}}, {\rm{bsearch1-t}}\,({\it{x\/}}, {\it{lst\/}}, $1\;+$ {\it{k\/}}, {\it{j\/}})\index{bsearch1-t})\index{splus} \\ 
{\bf else }{\tt{13}}$\;${\bf  endif}\- \\ 
{\bf else }{\tt{6}}$\;${\bf  endif}\-$\;${\bf  endlet}\-\-
\end{tabbing}

\begin{verbatim}; the computation time of the code.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{bsearch-t} \\  
{\rm{bsearch-t}}\,({\it{x\/}}, {\it{n\/}}, {\it{lst\/}})\index{bsearch-t} $=$ {\rm{splus}}\,({\tt{6}}, {\rm{bsearch1-t}}\,({\it{x\/}}, {\it{lst\/}}, {\tt{0}}, {\it{n\/}})\index{bsearch1-t})\index{splus}
\end{tabbing}

\begin{verbatim}; an induction hint.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{bsearch-induct} \\  
\=\+{\rm{bsearch-induct}}\,({\it{s\/}}, {\it{x\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{j\/}})\index{bsearch-induct} \\ 
$=$$\;\;\;\;$\=\+{\bf let }\=\+{\it{k\/}}{\bf $\;$ be$\;\;$}({\it{i\/}} $+$ {\it{j\/}}) $\div$ {\tt{2}}\- \\ 
{\bf in} \\ 
\=\+{\bf if }{\it{i\/}} $<$ {\it{j\/}} \\ 
{\bf then }\=\+{\bf if }{\rm{ilessp}}\,({\it{x\/}}, {\rm{get-nth}}\,({\it{k\/}}, {\it{lst\/}})\index{get-nth})\index{ilessp} \\ 
{\bf then }{\rm{bsearch-induct}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{10}})\index{stepn}, {\it{x\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{k\/}})\index{bsearch-induct} \\ 
{\bf elseif }{\rm{ilessp}}\,({\rm{get-nth}}\,({\it{k\/}}, {\it{lst\/}})\index{get-nth}, {\it{x\/}})\index{ilessp} \\ 
{\bf then }{\rm{bsearch-induct}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{13}})\index{stepn}, {\it{x\/}}, {\it{lst\/}}, $1\;+$ {\it{k\/}}, {\it{j\/}})\index{bsearch-induct} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\- \\ 
{\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{bsearch-statep} \\  
\=\+{\rm{bsearch-statep}}\,({\it{s\/}}, {\it{x\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{bsearch-statep} \\ 
$=$$\;\;\;\;$(\=\+({\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{70}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{bsearch-code}}\index{bsearch-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{12}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{28}})\index{ram-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{disjoint}}\,({\rm{sub}}\,({\tt{32}}, {\tt{12}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{28}}, {\it{a\/}}, {\tt{4}} $*$ {\it{n\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $=$ {\rm{read-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{read-mem}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $=$ {\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{x\/}} $=$ {\rm{iread-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{iread-mem}) \\ 
$\wedge$$\;\;\;\;${\rm{int-rangep}}\,({\tt{2}} $*$ {\it{n\/}}, {\tt{32}})\index{int-rangep} \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\in\;${\bf{N}}${}$))\-\-
\end{tabbing}

\begin{verbatim}; the conditions of an intermediate state.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{bsearch-s0p} \\  
\=\+{\rm{bsearch-s0p}}\,({\it{s\/}}, {\it{x\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{j\/}})\index{bsearch-s0p} \\ 
$=$$\;\;\;\;$(\=\+({\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{sub}}\,({\tt{32}}, {\tt{22}}, {\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{70}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{22}}, {\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{bsearch-code}}\index{bsearch-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{8}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{28}})\index{ram-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{disjoint}}\,({\rm{sub}}\,({\tt{32}}, {\tt{8}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{28}}, {\it{a\/}}, {\tt{4}} $*$ {\it{n\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{0}}, {\it{s\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $=$ {\rm{nat-to-int}}\,({\rm{read-dn}}\,({\tt{32}}, {\tt{1}}, {\it{s\/}})\index{read-dn}, {\tt{32}})\index{nat-to-int}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $=$ {\rm{nat-to-int}}\,({\rm{read-dn}}\,({\tt{32}}, {\tt{2}}, {\it{s\/}})\index{read-dn}, {\tt{32}})\index{nat-to-int}) \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $=$ {\rm{nat-to-int}}\,({\rm{read-dn}}\,({\tt{32}}, {\tt{3}}, {\it{s\/}})\index{read-dn}, {\tt{32}})\index{nat-to-int}) \\ 
$\wedge$$\;\;\;\;${\rm{int-rangep}}\,({\tt{2}} $*$ {\it{j\/}}, {\tt{32}})\index{int-rangep} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\leq$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\leq$ {\it{n\/}}))\-\-
\end{tabbing}

\begin{verbatim}; the initial segment.  From the initial state to s0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  bsearch-s-s0p \\ \index{bsearch-s-s0p}
{\rm{bsearch-statep}}\,({\it{s\/}}, {\it{x\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{bsearch-statep} $\rightarrow$ {\rm{bsearch-s0p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn}, {\it{x\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\tt{0}}, {\it{n\/}})\index{bsearch-s0p}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bsearch-s-s0 \\ \index{bsearch-s-s0}
\=\+{\rm{bsearch-statep}}\,({\it{s\/}}, {\it{x\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{bsearch-statep} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn})\index{linked-a6} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{movem-saved}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn}, {\tt{4}}, {\tt{8}}, {\tt{2}})\index{movem-saved} \\ 
$=$$\;\;\;\;${\rm{readm-rn}}\,({\tt{32}}, {\tt{'}}{\tt{(}}{\tt{2}}{\tt{ }}{\tt{3}}{\tt{)}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{readm-rn})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bsearch-s-s0-rfile \\ \index{bsearch-s-s0-rfile}
\=\+({\rm{bsearch-statep}}\,({\it{s\/}}, {\it{x\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{bsearch-statep} $\wedge$ {\rm{d4-7a2-5p}}\,({\it{rn\/}})\index{d4-7a2-5p}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\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}:  bsearch-s-s0-mem \\ \index{bsearch-s-s0-mem}
\=\+({\rm{bsearch-statep}}\,({\it{s\/}}, {\it{x\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{bsearch-statep} $\wedge$ {\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{12}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{28}})\index{disjoint}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\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}; from s0 to s0 (induction case), from s0 to exit (base case).
; base case: s0 --> sn.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  bsearch-s0-sn-base1 \\ \index{bsearch-s0-sn-base1}
\=\+({\rm{bsearch-s0p}}\,({\it{s\/}}, {\it{x\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{j\/}})\index{bsearch-s0p} $\wedge$ ({\it{i\/}} $\not<$ {\it{j\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn})\index{mc-pc} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{iread-dn}}\,({\tt{32}}, {\tt{0}}, {\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn})\index{iread-dn} $=$ {\tt{-1}}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn})\index{mc-rfile})\index{read-rn} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{add}}\,({\tt{32}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}, {\tt{8}})\index{add})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn})\index{mc-mem}, {\it{l\/}})\index{read-mem} \\ 
$=$$\;\;\;\;${\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{l\/}})\index{read-mem})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bsearch-s0-sn-rfile-base1 \\ \index{bsearch-s0-sn-rfile-base1}
\=\+(\=\+{\rm{bsearch-s0p}}\,({\it{s\/}}, {\it{x\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{j\/}})\index{bsearch-s0p} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not<$ {\it{j\/}}) \\ 
$\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\/}}, {\tt{6}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{d4-7a2-5p}}\,({\it{rn\/}})\index{d4-7a2-5p}$\;\;${\bf then }{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn} \\ 
{\bf else }{\rm{get-vlst}}\,({\it{oplen\/}}, {\tt{0}}, {\it{rn\/}}, {\tt{'}}{\tt{(}}{\tt{2}}{\tt{ }}{\tt{3}}{\tt{)}}, {\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{8}}, {\tt{2}})\index{movem-saved})\index{get-vlst}$\;${\bf  endif}\-)\-\-
\end{tabbing}


\noindent{\sc Event}:   Enable iplus.

\addvspace{18pt}

\noindent{\sc Event}:   Enable iquotient.

\addvspace{18pt}

\noindent{\sc Event}:   Disable quotient.

\addvspace{18pt}

\noindent{\sc Event}:   Disable remainder.

\addvspace{18pt}

\noindent{\sc Event}:   Disable times.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  bsearch-crock \\ \index{bsearch-crock}
({\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}:  bsearch-s0-sn-base2 \\ \index{bsearch-s0-sn-base2}
\=\+{\bf let }\=\+{\it{k\/}}{\bf $\;$ be$\;\;$}({\it{i\/}} $+$ {\it{j\/}}) $\div$ {\tt{2}}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{bsearch-s0p}}\,({\it{s\/}}, {\it{x\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{j\/}})\index{bsearch-s0p} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\it{x\/}}, {\rm{get-nth}}\,({\it{k\/}}, {\it{lst\/}})\index{get-nth})\index{ilessp}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\rm{get-nth}}\,({\it{k\/}}, {\it{lst\/}})\index{get-nth}, {\it{x\/}})\index{ilessp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{13}})\index{stepn})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{13}})\index{stepn})\index{mc-pc} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{iread-dn}}\,({\tt{32}}, {\tt{0}}, {\rm{stepn}}\,({\it{s\/}}, {\tt{13}})\index{stepn})\index{iread-dn} $=$ (({\it{i\/}} $+$ {\it{j\/}}) $\div$ {\tt{2}})) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{13}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{13}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{add}}\,({\tt{32}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}, {\tt{8}})\index{add})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{13}})\index{stepn})\index{mc-mem}, {\it{l\/}})\index{read-mem} \\ 
$=$$\;\;\;\;${\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{l\/}})\index{read-mem})\-)\-\-$\;${\bf  endlet}\-
\end{tabbing}		     

\begin{tabbing}{\sc Theorem}:  bsearch1-s0-sn-rfile-base2 \\ \index{bsearch1-s0-sn-rfile-base2}
\=\+{\bf let }\=\+{\it{k\/}}{\bf $\;$ be$\;\;$}({\it{i\/}} $+$ {\it{j\/}}) $\div$ {\tt{2}}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{bsearch-s0p}}\,({\it{s\/}}, {\it{x\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{j\/}})\index{bsearch-s0p} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\it{x\/}}, {\rm{get-nth}}\,({\it{k\/}}, {\it{lst\/}})\index{get-nth})\index{ilessp}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\rm{get-nth}}\,({\it{k\/}}, {\it{lst\/}})\index{get-nth}, {\it{x\/}})\index{ilessp}) \\ 
$\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\/}}, {\tt{13}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{d4-7a2-5p}}\,({\it{rn\/}})\index{d4-7a2-5p}$\;\;${\bf then }{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn} \\ 
{\bf else }{\rm{get-vlst}}\,(\=\+{\it{oplen\/}}, \\ 
{\tt{0}}, \\ 
{\it{rn\/}}, \\ 
{\tt{'}}{\tt{(}}{\tt{2}}{\tt{ }}{\tt{3}}{\tt{)}}, \\ 
{\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{8}}, {\tt{2}})\index{movem-saved})\-\index{get-vlst}$\;${\bf  endif}\-)\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim}; from s0 to s0 (induction case).
\end{verbatim}\begin{tabbing}{\sc Theorem}:  bsearch-s0-s0-1 \\ \index{bsearch-s0-s0-1}
\=\+{\bf let }\=\+{\it{k\/}}{\bf $\;$ be$\;\;$}({\it{i\/}} $+$ {\it{j\/}}) $\div$ {\tt{2}}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{bsearch-s0p}}\,({\it{s\/}}, {\it{x\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{j\/}})\index{bsearch-s0p} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,({\it{x\/}}, {\rm{get-nth}}\,({\it{k\/}}, {\it{lst\/}})\index{get-nth})\index{ilessp})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{bsearch-s0p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{10}})\index{stepn}, {\it{x\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{k\/}})\index{bsearch-s0p} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{10}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\- \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{10}})\index{stepn})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{10}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{movem-saved}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{10}})\index{stepn}, {\tt{4}}, {\tt{8}}, {\tt{2}})\index{movem-saved} \\ 
$=$$\;\;\;\;${\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{8}}, {\tt{2}})\index{movem-saved})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{10}})\index{stepn})\index{mc-mem}, {\it{l\/}})\index{read-mem} \\ 
$=$$\;\;\;\;${\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{l\/}})\index{read-mem})\-)\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bsearch-s0-s0-rfile1 \\ \index{bsearch-s0-s0-rfile1}
\=\+{\bf let }\=\+{\it{k\/}}{\bf $\;$ be$\;\;$}({\it{i\/}} $+$ {\it{j\/}}) $\div$ {\tt{2}}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{bsearch-s0p}}\,({\it{s\/}}, {\it{x\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{j\/}})\index{bsearch-s0p} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,({\it{x\/}}, {\rm{get-nth}}\,({\it{k\/}}, {\it{lst\/}})\index{get-nth})\index{ilessp} \\ 
$\wedge$$\;\;\;\;${\rm{d4-7a2-5p}}\,({\it{rn\/}})\index{d4-7a2-5p})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{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})\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bsearch-s0-s0-2 \\ \index{bsearch-s0-s0-2}
\=\+{\bf let }\=\+{\it{k\/}}{\bf $\;$ be$\;\;$}({\it{i\/}} $+$ {\it{j\/}}) $\div$ {\tt{2}}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{bsearch-s0p}}\,({\it{s\/}}, {\it{x\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{j\/}})\index{bsearch-s0p} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\it{x\/}}, {\rm{get-nth}}\,({\it{k\/}}, {\it{lst\/}})\index{get-nth})\index{ilessp}) \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,({\rm{get-nth}}\,({\it{k\/}}, {\it{lst\/}})\index{get-nth}, {\it{x\/}})\index{ilessp})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{bsearch-s0p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{13}})\index{stepn}, {\it{x\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, $1\;+$ {\it{k\/}}, {\it{j\/}})\index{bsearch-s0p} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{13}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\- \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{13}})\index{stepn})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{13}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{movem-saved}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{13}})\index{stepn}, {\tt{4}}, {\tt{8}}, {\tt{2}})\index{movem-saved} \\ 
$=$$\;\;\;\;${\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{8}}, {\tt{2}})\index{movem-saved})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{13}})\index{stepn})\index{mc-mem}, {\it{l\/}})\index{read-mem} \\ 
$=$$\;\;\;\;${\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{l\/}})\index{read-mem})\-)\-\-$\;${\bf  endlet}\-
\end{tabbing}		     

\begin{tabbing}{\sc Theorem}:  bsearch1-s0-s0-rfile2 \\ \index{bsearch1-s0-s0-rfile2}
\=\+{\bf let }\=\+{\it{k\/}}{\bf $\;$ be$\;\;$}({\it{i\/}} $+$ {\it{j\/}}) $\div$ {\tt{2}}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{bsearch-s0p}}\,({\it{s\/}}, {\it{x\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{j\/}})\index{bsearch-s0p} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\it{x\/}}, {\rm{get-nth}}\,({\it{k\/}}, {\it{lst\/}})\index{get-nth})\index{ilessp}) \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,({\rm{get-nth}}\,({\it{k\/}}, {\it{lst\/}})\index{get-nth}, {\it{x\/}})\index{ilessp} \\ 
$\wedge$$\;\;\;\;${\rm{d4-7a2-5p}}\,({\it{rn\/}})\index{d4-7a2-5p})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{13}})\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})\-\-$\;${\bf  endlet}\-
\end{tabbing}


\noindent{\sc Event}:   Disable bsearch-statep.

\addvspace{18pt}

\noindent{\sc Event}:   Disable bsearch-s0p.

\addvspace{18pt}

\begin{verbatim}; put together. s0 --> sn
\end{verbatim}\begin{tabbing}{\sc Theorem}:  bsearch-s0-sn \\ \index{bsearch-s0-sn}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{bsearch1-t}}\,({\it{x\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{j\/}})\index{bsearch1-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{bsearch-s0p}}\,({\it{s\/}}, {\it{x\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{j\/}})\index{bsearch-s0p} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{sn\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{sn\/}})\index{mc-pc} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{iread-dn}}\,({\tt{32}}, {\tt{0}}, {\it{sn\/}})\index{iread-dn} $=$ {\rm{bsearch1}}\,({\it{x\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{j\/}})\index{bsearch1}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{sn\/}})\index{mc-rfile})\index{read-rn} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\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-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}, {\tt{8}})\index{add})\- \\ 
$\wedge$$\;\;\;\;$({\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}))\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bsearch-s0-sn-rfile \\ \index{bsearch-s0-sn-rfile}
\=\+({\rm{bsearch-s0p}}\,({\it{s\/}}, {\it{x\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{j\/}})\index{bsearch-s0p} $\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{bsearch1-t}}\,({\it{x\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{j\/}})\index{bsearch1-t})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{d4-7a2-5p}}\,({\it{rn\/}})\index{d4-7a2-5p}$\;\;${\bf then }{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn} \\ 
{\bf else }{\rm{get-vlst}}\,({\it{oplen\/}}, {\tt{0}}, {\it{rn\/}}, {\tt{'}}{\tt{(}}{\tt{2}}{\tt{ }}{\tt{3}}{\tt{)}}, {\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{8}}, {\tt{2}})\index{movem-saved})\index{get-vlst}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{verbatim}; the correctness statement of this BSEARCH program.
; after an execution of this program,  the machine state satisfies:
;  0. normal exit.
;  1. the program counter is returned to the next instruction of the caller.
;  2. the result -- (bsearch x n lst), is stored in the register D0.
;  3. a6, used by LINK, is restored to its original value.
;  4. a7, the stack pointer, is updated correctly to pop off one frame.
;  5. the registers d2-d7 and a2-a5 maintain their original values.
;  6. the memory is only locally changed wrt this program.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  bsearch-correctness \\ \index{bsearch-correctness}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{bsearch-t}}\,({\it{x\/}}, {\it{n\/}}, {\it{lst\/}})\index{bsearch-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{bsearch-statep}}\,({\it{s\/}}, {\it{x\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{bsearch-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-sp}}\,({\it{s\/}})\index{read-sp}, {\tt{4}})\index{add})\- \\ 
$\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}}\,({\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{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{12}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{28}})\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{iread-dn}}\,({\tt{32}}, {\tt{0}}, {\it{sn\/}})\index{iread-dn} $=$ {\rm{bsearch}}\,({\it{x\/}}, {\it{n\/}}, {\it{lst\/}})\index{bsearch}))\-\-$\;${\bf  endlet}\-
\end{tabbing}


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

\addvspace{18pt}

\begin{verbatim}; in the logic, bsearch has these properties:
;      1. if it returns a nonnegative integer i, then lst[i] = x.
;      2. if it returns -1, then x is not in lst.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{member1} \\  
\=\+{\rm{member1}}\,({\it{x\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{j\/}})\index{member1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $<$ {\it{j\/}} \\ 
{\bf then }\=\+{\bf if }{\it{x\/}} $=$ {\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{member1}}\,({\it{x\/}}, {\it{lst\/}}, $1\;+$ {\it{i\/}}, {\it{j\/}})\index{member1}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{orderedp} \\  
\=\+{\rm{orderedp}}\,({\it{lst\/}})\index{orderedp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{lst\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{cdr}}\,({\it{lst\/}}) $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{ileq}}\,({\rm{car}}\,({\it{lst\/}}), {\rm{cadr}}\,({\it{lst\/}}))\index{ileq} $\wedge$ {\rm{orderedp}}\,({\rm{cdr}}\,({\it{lst\/}}))\index{orderedp}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  leq-trans \\ \index{leq-trans}
(($\neg$ {\rm{ilessp}}\,({\it{x\/}}, {\it{y\/}})\index{ilessp}) $\wedge$ ($\neg$ {\rm{ilessp}}\,({\it{y\/}}, {\it{z\/}})\index{ilessp})) $\rightarrow$ ($\neg$ {\rm{ilessp}}\,({\it{x\/}}, {\it{z\/}})\index{ilessp})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  int-equal \\ \index{int-equal}
\=\+({\rm{integerp}}\,({\it{x\/}})\index{integerp} $\wedge$ {\rm{integerp}}\,({\it{y\/}})\index{integerp} $\wedge$ ($\neg$ {\rm{ilessp}}\,({\it{x\/}}, {\it{y\/}})\index{ilessp}) $\wedge$ ($\neg$ {\rm{ilessp}}\,({\it{y\/}}, {\it{x\/}})\index{ilessp})) \\ 
$\rightarrow$$\;\;\;\;$(({\it{x\/}} $=$ {\it{y\/}}) $=$ {\bf{t}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  orderedp-ordered \\ \index{orderedp-ordered}
\=\+({\rm{orderedp}}\,({\it{lst\/}})\index{orderedp} $\wedge$ ({\it{i\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $<$ {\rm{len}}\,({\it{lst\/}})\index{len})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{ilessp}}\,({\rm{get-nth}}\,({\it{j\/}}, {\it{lst\/}})\index{get-nth}, {\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth})\index{ilessp} $=$ {\bf{f}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bsearch1-found \\ \index{bsearch1-found}
\=\+(({\rm{bsearch1}}\,({\it{x\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{j\/}})\index{bsearch1} $\not=$ {\tt{-1}}) $\wedge$ {\rm{lst-integerp}}\,({\it{lst\/}})\index{lst-integerp} $\wedge$ {\rm{integerp}}\,({\it{x\/}})\index{integerp}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{get-nth}}\,({\rm{bsearch1}}\,({\it{x\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{j\/}})\index{bsearch1}, {\it{lst\/}})\index{get-nth} $=$ {\it{x\/}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bsearch1-not-found-1 \\ \index{bsearch1-not-found-1}
\=\+(\=\+{\rm{orderedp}}\,({\it{lst\/}})\index{orderedp} \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,({\rm{get-nth}}\,({\it{k\/}}, {\it{lst\/}})\index{get-nth}, {\it{x\/}})\index{ilessp} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\leq$ {\it{k\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $<$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\leq$ {\rm{len}}\,({\it{lst\/}})\index{len}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{member1}}\,({\it{x\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{j\/}})\index{member1} $=$ {\rm{member1}}\,({\it{x\/}}, {\it{lst\/}}, $1\;+$ {\it{k\/}}, {\it{j\/}})\index{member1})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bsearch1-not-found-2-lemma \\ \index{bsearch1-not-found-2-lemma}
\=\+(\=\+{\rm{orderedp}}\,({\it{lst\/}})\index{orderedp} \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,({\it{x\/}}, {\rm{get-nth}}\,({\it{k\/}}, {\it{lst\/}})\index{get-nth})\index{ilessp} \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $\leq$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ {\rm{len}}\,({\it{lst\/}})\index{len}))\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{member1}}\,({\it{x\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{j\/}})\index{member1})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bsearch1-not-found-2 \\ \index{bsearch1-not-found-2}
\=\+(\=\+{\rm{orderedp}}\,({\it{lst\/}})\index{orderedp} \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,({\it{x\/}}, {\rm{get-nth}}\,({\it{k\/}}, {\it{lst\/}})\index{get-nth})\index{ilessp} \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $<$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\leq$ {\rm{len}}\,({\it{lst\/}})\index{len}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{member1}}\,({\it{x\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{j\/}})\index{member1} $=$ {\rm{member1}}\,({\it{x\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{k\/}})\index{member1})\-
\end{tabbing}


\noindent{\sc Event}:   Disable bsearch1-not-found-2-lemma.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  bsearch1-not-found \\ \index{bsearch1-not-found}
\=\+(\=\+({\rm{bsearch1}}\,({\it{x\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{j\/}})\index{bsearch1} $=$ {\tt{-1}}) \\ 
$\wedge$$\;\;\;\;${\rm{orderedp}}\,({\it{lst\/}})\index{orderedp} \\ 
$\wedge$$\;\;\;\;${\rm{lst-integerp}}\,({\it{lst\/}})\index{lst-integerp} \\ 
$\wedge$$\;\;\;\;${\rm{integerp}}\,({\it{x\/}})\index{integerp} \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\leq$ {\rm{len}}\,({\it{lst\/}})\index{len}))\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{member1}}\,({\it{x\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{j\/}})\index{member1})\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{member2} \\  
\=\+{\rm{member2}}\,({\it{x\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{j\/}})\index{member2} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $<$ {\it{j\/}} \\ 
{\bf then }\=\+{\bf if }{\it{x\/}} $=$ {\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{member2}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{lst\/}}), {\it{i\/}}, {\it{j\/}} $-\;1$)\index{member2}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member2-member \\ \index{member2-member}
{\rm{member2}}\,({\it{x\/}}, {\it{lst\/}}, {\tt{0}}, {\rm{len}}\,({\it{lst\/}})\index{len})\index{member2} $=$ ({\it{x\/}} $\in$ {\it{lst\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member2-lemma \\ \index{member2-lemma}
({\it{x\/}} $\not=$ {\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth}) $\rightarrow$ ({\rm{member2}}\,({\it{x\/}}, {\it{lst\/}}, $1\;+$ {\it{i\/}}, {\it{j\/}})\index{member2} $=$ {\rm{member2}}\,({\it{x\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{j\/}})\index{member2})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member1-member2 \\ \index{member1-member2}
{\rm{member1}}\,({\it{x\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{j\/}})\index{member1} $=$ {\rm{member2}}\,({\it{x\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{j\/}})\index{member2}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bsearch-found \\ \index{bsearch-found}
\=\+(({\rm{bsearch}}\,({\it{x\/}}, {\it{n\/}}, {\it{lst\/}})\index{bsearch} $\not=$ {\tt{-1}}) $\wedge$ {\rm{lst-integerp}}\,({\it{lst\/}})\index{lst-integerp} $\wedge$ {\rm{integerp}}\,({\it{x\/}})\index{integerp}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{get-nth}}\,({\rm{bsearch}}\,({\it{x\/}}, {\it{n\/}}, {\it{lst\/}})\index{bsearch}, {\it{lst\/}})\index{get-nth} $=$ {\it{x\/}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bsearch-not-found \\ \index{bsearch-not-found}
\=\+(\=\+({\rm{bsearch}}\,({\it{x\/}}, {\rm{len}}\,({\it{lst\/}})\index{len}, {\it{lst\/}})\index{bsearch} $=$ {\tt{-1}}) \\ 
$\wedge$$\;\;\;\;${\rm{orderedp}}\,({\it{lst\/}})\index{orderedp} \\ 
$\wedge$$\;\;\;\;${\rm{lst-integerp}}\,({\it{lst\/}})\index{lst-integerp} \\ 
$\wedge$$\;\;\;\;${\rm{integerp}}\,({\it{x\/}})\index{integerp})\- \\ 
$\rightarrow$$\;\;\;\;$({\it{x\/}} $\not\in$ {\it{lst\/}})\-
\end{tabbing}

\begin{verbatim}; an upper bound.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  bsearch1-t-0 \\ \index{bsearch1-t-0}
{\rm{bsearch1-t}}\,({\it{x\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{i\/}})\index{bsearch1-t} $=$ {\tt{6}}
\end{tabbing}
	    
\begin{tabbing}{\sc Theorem}:  bsearch1-t-crock \\ \index{bsearch1-t-crock}
\=\+(\=\+({\it{i\/}} $<$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\tt{26}} $+$ ({\tt{13}} $*$ {\rm{log}}\,({\tt{2}}, ({\it{j\/}} $-\;1$) $-$ (({\it{i\/}} $+$ {\it{j\/}}) $\div$ {\tt{2}}))\index{log})) \\ 
$\not<$$\;\;\;\;${\rm{bsearch1-t}}\,({\it{x\/}}, {\it{lst\/}}, $1\;+$ (({\it{i\/}} $+$ {\it{j\/}}) $\div$ {\tt{2}}), {\it{j\/}})\index{bsearch1-t})\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+({\tt{26}} $+$ ({\tt{13}} $*$ {\rm{log}}\,({\tt{2}}, {\it{j\/}} $-$ {\it{i\/}})\index{log})) \\ 
$<$$\;\;\;\;$({\tt{13}} $+$ {\rm{bsearch1-t}}\,({\it{x\/}}, {\it{lst\/}}, $1\;+$ (({\it{i\/}} $+$ {\it{j\/}}) $\div$ {\tt{2}}), {\it{j\/}})\index{bsearch1-t}))\- \\ 
$=$$\;\;\;\;${\bf{f}})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bsearch1-t-ubound \\ \index{bsearch1-t-ubound}
({\tt{26}} $+$ ({\tt{13}} $*$ {\rm{log}}\,({\tt{2}}, {\it{j\/}} $-$ {\it{i\/}})\index{log})) $\not<$ {\rm{bsearch1-t}}\,({\it{x\/}}, {\it{lst\/}}, {\it{i\/}}, {\it{j\/}})\index{bsearch1-t}
\end{tabbing}


\noindent{\sc Event}:   Disable bsearch1-t-crock.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  bsearch-t-ubound-la \\ \index{bsearch-t-ubound-la}
{\rm{bsearch-t}}\,({\it{x\/}}, {\it{n\/}}, {\it{lst\/}})\index{bsearch-t} $\leq$ ({\tt{32}} $+$ ({\tt{13}} $*$ {\rm{log}}\,({\tt{2}}, {\it{n\/}})\index{log}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bsearch-t-ubound \\ \index{bsearch-t-ubound}
({\it{n\/}} $<$ {\rm{exp}}\,({\tt{2}}, {\tt{31}})\index{exp}) $\rightarrow$ ({\rm{bsearch-t}}\,({\it{x\/}}, {\it{n\/}}, {\it{lst\/}})\index{bsearch-t} $\leq$ {\tt{435}})
\end{tabbing}

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