\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 an Integer Square Root Program
;
\end{verbatim}
\noindent{\sc Event}:   Start with the library {\tt{"mc20-2"}} using the compiled version.

\addvspace{18pt}
\begin{verbatim}#|
This is a revisit to our ISQRT proof.  Dr. Don Good talked with 
Dr. Steve Zeigler, vice president for Ada products at Verdix, and
they agreed to let me publicize the machine codes generated by 
their present Ada compiler.

The following Ada function ISQRT computes the integer square root of a 
given nonnegative integer i.  This is our third proof about ISQRT.

function isqrt (i:integer) return integer is
  j : integer := (i / 2);
 begin
  while ((i / j) < j) loop
    j := (j + (i / j)) / 2;
  end loop;
  return j;
 end isqrt;

Here is the MC68020 assembly code of the above ISQRT program.  The code
is from Dr. Steve Zeigler and generated by their present Ada compiler.

   1  function isqrt (i:integer) return integer is
      00000: link.w      a6, #-04
   2     j : integer := (i / 2);
      00004: move.l      d2, d1
      00006: bge.b       06    -> 0e
      00008: addi.l      #01, d1
      0000e: asr.l       #01, d1
   3  begin
   4     while not ((i / j) >= j) loop
      00010: move.l      d2, d0
      00012: divsl.l     d1, d0:d0
      00016: trapv       
      00018: cmp.l       d0, d1
      0001a: ble.b       01c    -> 038
   5         j := (j + (i / j)) / 2;
      0001c: add.l       d1, d0
      0001e: trapv       
      00020: move.l      d0, d1
      00022: bge.b       06    -> 02a
      00024: addi.l      #01, d1
      0002a: asr.l       #01, d1
   4     while not ((i / j) >= j) loop
      0002c: move.l      d2, d0
      0002e: divsl.l     d1, d0:d0
      00032: trapv       
   6  end loop;
      00034: cmp.l       d0, d1
      00036: bgt.b       -01c    -> 01c
   7  return j;
      00038: move.l      d1, d0
      0003a: unlk        a6
      0003c: rts         
   8 end isqrt;

0x4e56  0xfffc  0x2202  0x6c06  0x0681  0x0000  0x0001  0xe281
0x2002  0x4c41  0x0800  0x4e76  0xb280  0x6f1c  0xd081  0x4e76
0x2200  0x6c06  0x0681  0x0000  0x0001  0xe281  0x2002  0x4c41
0x0800  0x4e76  0xb280  0x6ee4  0x2001  0x4e5e  0x4e75

'(78      86      255     252     34      2       108     6
  6       129     0       0       0       1       226     129
  32      2       76      65      8       0       78      118
  178     128     111     28      208     129     78      118
  34      0       108     6       6       129     0       0
  0       1       226     129     32      2       76      65
  8       0       78      118     178     128     110     228
  32      1       78      94      78      117)
|#

; in the logic, the above program is defined by (isqrt-code).
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{isqrt-code} \\  
\=\+{\sc{isqrt-code}}\index{isqrt-code} \\ 
$=$$\;\;\;\;${\tt{'}}{\tt{(}}\=\+{\tt{78}}{\tt{ }}{\tt{86}}{\tt{ }}{\tt{255}}{\tt{ }}{\tt{252}}{\tt{ }}{\tt{34}}{\tt{ }}{\tt{2}}{\tt{ }}{\tt{108}}{\tt{ }}{\tt{6}}{\tt{ }}{\tt{6}}{\tt{ }}{\tt{129}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{1}}{\tt{ }}{\tt{226}}{\tt{ }}{\tt{129}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{2}} \\ 
{\tt{76}}{\tt{ }}{\tt{65}}{\tt{ }}{\tt{8}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{118}}{\tt{ }}{\tt{178}}{\tt{ }}{\tt{128}}{\tt{ }}{\tt{111}}{\tt{ }}{\tt{28}}{\tt{ }}{\tt{208}}{\tt{ }}{\tt{129}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{118}}{\tt{ }}{\tt{34}}{\tt{ }}{\tt{0}} \\ 
{\tt{108}}{\tt{ }}{\tt{6}}{\tt{ }}{\tt{6}}{\tt{ }}{\tt{129}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{1}}{\tt{ }}{\tt{226}}{\tt{ }}{\tt{129}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{2}}{\tt{ }}{\tt{76}}{\tt{ }}{\tt{65}}{\tt{ }}{\tt{8}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{118}} \\ 
{\tt{178}}{\tt{ }}{\tt{128}}{\tt{ }}{\tt{110}}{\tt{ }}{\tt{228}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{1}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{94}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{117}}{\tt{)}}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{sq}$\;\;$
{\rm{sq}}\,({\it{x\/}})\index{sq} $=$ ({\it{x\/}} $*$ {\it{x\/}})
\end{tabbing}

\begin{verbatim}; isqrt1 is a function in the Logic simulating the loop of the above code.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{isqrt1} \\  
\=\+{\rm{isqrt1}}\,({\it{i\/}}, {\it{j\/}})\index{isqrt1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{j\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{fix}}\,({\it{i\/}}) \\ 
{\bf elseif }({\it{i\/}} $\div$ {\it{j\/}}) $<$ {\it{j\/}}$\;\;${\bf then }{\rm{isqrt1}}\,({\it{i\/}}, ({\it{j\/}} $+$ ({\it{i\/}} $\div$ {\it{j\/}})) $\div$ {\tt{2}})\index{isqrt1} \\ 
{\bf else }{\rm{fix}}\,({\it{j\/}})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; isqrt specifies the semantics of ISQRT in the Logic.  To see why
; the function isqrt computes the square root for any nonnegative 
; integer input, please refer to the proof in file isqrt.events.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{isqrt} \\  
\=\+{\rm{isqrt}}\,({\it{i\/}})\index{isqrt} \\ 
$=$$\;\;\;\;$\=\+{\bf let }\=\+{\it{j1\/}}{\bf $\;$ be$\;\;$}(({\it{i\/}} $\div$ {\tt{2}}) $+$ ({\it{i\/}} $\div$ ({\it{i\/}} $\div$ {\tt{2}}))) $\div$ {\tt{2}}\- \\ 
{\bf in} \\ 
\=\+{\bf if }{\it{i\/}} $<$ {\rm{sq}}\,({\it{i\/}} $\div$ {\tt{2}})\index{sq}$\;\;${\bf then }{\rm{isqrt1}}\,({\it{i\/}}, {\it{j1\/}})\index{isqrt1} \\ 
{\bf else }{\it{i\/}} $\div$ {\tt{2}}$\;${\bf  endif}\-$\;${\bf  endlet}\-\-
\end{tabbing}

\begin{verbatim}; the computation time of this program.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{isqrt1-t} \\  
\=\+{\rm{isqrt1-t}}\,({\it{i\/}}, {\it{j\/}})\index{isqrt1-t} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{j\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }({\it{i\/}} $\div$ {\it{j\/}}) $<$ {\it{j\/}} \\ 
{\bf then }{\rm{splus}}\,({\tt{10}}, {\rm{isqrt1-t}}\,({\it{i\/}}, ({\it{j\/}} $+$ ({\it{i\/}} $\div$ {\it{j\/}})) $\div$ {\tt{2}})\index{isqrt1-t})\index{splus} \\ 
{\bf else }{\tt{8}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{isqrt-t} \\  
\=\+{\rm{isqrt-t}}\,({\it{i\/}})\index{isqrt-t} \\ 
$=$$\;\;\;\;$\=\+{\bf let }\=\+{\it{j1\/}}{\bf $\;$ be$\;\;$}(({\it{i\/}} $\div$ {\tt{2}}) $+$ ({\it{i\/}} $\div$ ({\it{i\/}} $\div$ {\tt{2}}))) $\div$ {\tt{2}}\- \\ 
{\bf in} \\ 
\=\+{\bf if }{\it{i\/}} $<$ {\rm{sq}}\,({\it{i\/}} $\div$ {\tt{2}})\index{sq}$\;\;${\bf then }{\rm{splus}}\,({\tt{14}}, {\rm{isqrt1-t}}\,({\it{i\/}}, {\it{j1\/}})\index{isqrt1-t})\index{splus} \\ 
{\bf else }{\tt{12}}$\;${\bf  endif}\-$\;${\bf  endlet}\-\-
\end{tabbing}

\begin{verbatim}; enable a few functions.
\end{verbatim}
\noindent{\sc Event}:   Enable iplus.

\addvspace{18pt}

\noindent{\sc Event}:   Enable integerp.

\addvspace{18pt}

\noindent{\sc Event}:   Enable iquotient.

\addvspace{18pt}

\noindent{\sc Event}:   Enable ilessp.

\addvspace{18pt}

\begin{verbatim}; disable a few functions.
\end{verbatim}
\noindent{\sc Event}:   Disable remainder.

\addvspace{18pt}

\noindent{\sc Event}:   Disable quotient.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  isqrt-no-overflow \\ \index{isqrt-no-overflow}
\=\+({\rm{int-rangep}}\,({\tt{2}} $*$ {\it{j\/}}, {\it{n\/}})\index{int-rangep} $\wedge$ (({\it{i\/}} $\div$ {\it{j\/}}) $<$ {\it{j\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{int-rangep}}\,({\it{j\/}} $+$ ({\it{i\/}} $\div$ {\it{j\/}}), {\it{n\/}})\index{int-rangep}\-
\end{tabbing}

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

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

\begin{verbatim}; an induction hint.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{isqrt-induct} \\  
\=\+{\rm{isqrt-induct}}\,({\it{s\/}}, {\it{i\/}}, {\it{j\/}})\index{isqrt-induct} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{j\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }({\it{i\/}} $\div$ {\it{j\/}}) $<$ {\it{j\/}} \\ 
{\bf then }{\rm{isqrt-induct}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{10}})\index{stepn}, {\it{i\/}}, ({\it{j\/}} $+$ ({\it{i\/}} $\div$ {\it{j\/}})) $\div$ {\tt{2}})\index{isqrt-induct} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; the properties of the initial state.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{isqrt-statep} \\  
\=\+{\rm{isqrt-statep}}\,({\it{s\/}}, {\it{i\/}})\index{isqrt-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{isqrt-code}}\index{isqrt-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{8}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{12}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $=$ {\rm{iread-dn}}\,({\tt{32}}, {\tt{2}}, {\it{s\/}})\index{iread-dn}) \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,({\tt{1}}, {\it{i\/}})\index{ilessp})\-\-
\end{tabbing}

\begin{verbatim}; an intermediate state s0.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{isqrt-s0p} \\  
\=\+{\rm{isqrt-s0p}}\,({\it{s\/}}, {\it{i\/}}, {\it{j\/}})\index{isqrt-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{44}}, {\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{44}}, {\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{isqrt-code}}\index{isqrt-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{12}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $=$ {\rm{iread-dn}}\,({\tt{32}}, {\tt{2}}, {\it{s\/}})\index{iread-dn}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $=$ {\rm{iread-dn}}\,({\tt{32}}, {\tt{1}}, {\it{s\/}})\index{iread-dn}) \\ 
$\wedge$$\;\;\;\;${\rm{int-rangep}}\,({\tt{2}} $*$ {\it{j\/}}, {\tt{32}})\index{int-rangep} \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,({\tt{1}}, {\it{i\/}})\index{ilessp} \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,({\tt{0}}, {\it{j\/}})\index{ilessp})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  initial-j-int-rangep \\ \index{initial-j-int-rangep}
{\rm{int-rangep}}\,({\it{i\/}}, {\it{n\/}})\index{int-rangep} $\rightarrow$ {\rm{int-rangep}}\,({\tt{2}} $*$ ({\it{i\/}} $\div$ {\tt{2}}), {\it{n\/}})\index{int-rangep}
\end{tabbing}

\begin{verbatim}; from the initial state to exit.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  isqrt-s-exit \\ \index{isqrt-s-exit}
\=\+({\rm{isqrt-statep}}\,({\it{s\/}}, {\it{i\/}})\index{isqrt-statep} $\wedge$ ({\it{i\/}} $\not<$ (({\it{i\/}} $\div$ {\tt{2}}) $*$ ({\it{i\/}} $\div$ {\tt{2}})))) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{12}})\index{stepn})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{12}})\index{stepn})\index{mc-pc} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{iread-dn}}\,({\tt{32}}, {\tt{0}}, {\rm{stepn}}\,({\it{s\/}}, {\tt{12}})\index{stepn})\index{iread-dn} $=$ ({\it{i\/}} $\div$ {\tt{2}})) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{12}})\index{stepn})\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}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{12}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{add}}\,({\tt{32}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\tt{4}})\index{add})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  isqrt-s-exit-rfile \\ \index{isqrt-s-exit-rfile}
\=\+({\rm{isqrt-statep}}\,({\it{s\/}}, {\it{i\/}})\index{isqrt-statep} $\wedge$ ({\it{i\/}} $\not<$ (({\it{i\/}} $\div$ {\tt{2}}) $*$ ({\it{i\/}} $\div$ {\tt{2}}))) $\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{s\/}}, {\tt{12}})\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}:  isqrt-s-exit-mem \\ \index{isqrt-s-exit-mem}
\=\+(\=\+{\rm{isqrt-statep}}\,({\it{s\/}}, {\it{i\/}})\index{isqrt-statep} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not<$ (({\it{i\/}} $\div$ {\tt{2}}) $*$ ({\it{i\/}} $\div$ {\tt{2}}))) \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{8}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{12}})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{12}})\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 the initial state to s0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  isqrt-s-s0 \\ \index{isqrt-s-s0}
\=\+{\bf let }\=\+{\it{j1\/}}{\bf $\;$ be$\;\;$}(({\it{i\/}} $\div$ {\tt{2}}) $+$ ({\it{i\/}} $\div$ ({\it{i\/}} $\div$ {\tt{2}}))) $\div$ {\tt{2}}\- \\ 
{\bf in} \\ 
\=\+({\rm{isqrt-statep}}\,({\it{s\/}}, {\it{i\/}})\index{isqrt-statep} $\wedge$ ({\it{i\/}} $<$ (({\it{i\/}} $\div$ {\tt{2}}) $*$ ({\it{i\/}} $\div$ {\tt{2}})))) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{isqrt-s0p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{14}})\index{stepn}, {\it{i\/}}, {\it{j1\/}})\index{isqrt-s0p} \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{14}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{14}})\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{14}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub})\-)\-\-$\;${\bf  endlet}\-
\end{tabbing}     

\begin{tabbing}{\sc Theorem}:  isqrt-s-s0-rfile \\ \index{isqrt-s-s0-rfile}
\=\+({\rm{isqrt-statep}}\,({\it{s\/}}, {\it{i\/}})\index{isqrt-statep} $\wedge$ ({\it{i\/}} $<$ (({\it{i\/}} $\div$ {\tt{2}}) $*$ ({\it{i\/}} $\div$ {\tt{2}}))) $\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{s\/}}, {\tt{14}})\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}:  isqrt-s-s0-mem \\ \index{isqrt-s-s0-mem}
\=\+(\=\+{\rm{isqrt-statep}}\,({\it{s\/}}, {\it{i\/}})\index{isqrt-statep} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ (({\it{i\/}} $\div$ {\tt{2}}) $*$ ({\it{i\/}} $\div$ {\tt{2}}))) \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{8}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{12}})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{14}})\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 exit (base case), or from s0 to s0 (induction case).
; base case: s0 --> exit.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  isqrt-s0-exit-base \\ \index{isqrt-s0-exit-base}
\=\+({\rm{isqrt-s0p}}\,({\it{s\/}}, {\it{i\/}}, {\it{j\/}})\index{isqrt-s0p} $\wedge$ (({\it{i\/}} $\div$ {\it{j\/}}) $\not<$ {\it{j\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\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{8}})\index{stepn})\index{iread-dn} $=$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\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{8}})\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})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  isqrt1-s0-exit-rfile-base \\ \index{isqrt1-s0-exit-rfile-base}
\=\+({\rm{isqrt-s0p}}\,({\it{s\/}}, {\it{i\/}}, {\it{j\/}})\index{isqrt-s0p} $\wedge$ (({\it{i\/}} $\div$ {\it{j\/}}) $\not<$ {\it{j\/}}) $\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{s\/}}, {\tt{8}})\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}:  isqrt1-s0-exit-mem-base \\ \index{isqrt1-s0-exit-mem-base}
\=\+({\rm{isqrt-s0p}}\,({\it{s\/}}, {\it{i\/}}, {\it{j\/}})\index{isqrt-s0p} $\wedge$ (({\it{i\/}} $\div$ {\it{j\/}}) $\not<$ {\it{j\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\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}; induction case: s0 --> s0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  isqrt-s0-s0 \\ \index{isqrt-s0-s0}
\=\+({\rm{isqrt-s0p}}\,({\it{s\/}}, {\it{i\/}}, {\it{j\/}})\index{isqrt-s0p} $\wedge$ (({\it{i\/}} $\div$ {\it{j\/}}) $<$ {\it{j\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{isqrt-s0p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{10}})\index{stepn}, {\it{i\/}}, ({\it{j\/}} $+$ ({\it{i\/}} $\div$ {\it{j\/}})) $\div$ {\tt{2}})\index{isqrt-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}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  isqrt-s0-s0-rfile \\ \index{isqrt-s0-s0-rfile}
\=\+({\rm{isqrt-s0p}}\,({\it{s\/}}, {\it{i\/}}, {\it{j\/}})\index{isqrt-s0p} $\wedge$ (({\it{i\/}} $\div$ {\it{j\/}}) $<$ {\it{j\/}}) $\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{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})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  isqrt-s0-s0-mem \\ \index{isqrt-s0-s0-mem}
\=\+(\=\+{\rm{isqrt-s0p}}\,({\it{s\/}}, {\it{i\/}}, {\it{j\/}})\index{isqrt-s0p} \\ 
$\wedge$$\;\;\;\;$(({\it{i\/}} $\div$ {\it{j\/}}) $<$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{8}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{20}})\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}:  isqrt-s0p-j\_nonzerop \\ \index{isqrt-s0p-j\_nonzerop}
{\rm{isqrt-s0p}}\,({\it{s\/}}, {\it{i\/}}, {\it{j\/}})\index{isqrt-s0p} $\rightarrow$ (({\it{j\/}} $\not=$ {\tt{0}}) $\wedge$ ({\it{j\/}} $\in\;${\bf{N}}${}$))
\end{tabbing}


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

\addvspace{18pt}

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

\addvspace{18pt}

\begin{verbatim}; put together:  s0 --> exit.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  isqrt-s0-exit \\ \index{isqrt-s0-exit}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{isqrt1-t}}\,({\it{i\/}}, {\it{j\/}})\index{isqrt1-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{isqrt-s0p}}\,({\it{s\/}}, {\it{i\/}}, {\it{j\/}})\index{isqrt-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{isqrt1}}\,({\it{i\/}}, {\it{j\/}})\index{isqrt1}) \\ 
$\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})\-)\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  isqrt-s0-exit-rfile \\ \index{isqrt-s0-exit-rfile}
\=\+({\rm{isqrt-s0p}}\,({\it{s\/}}, {\it{i\/}}, {\it{j\/}})\index{isqrt-s0p} $\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{s\/}}, {\rm{isqrt1-t}}\,({\it{i\/}}, {\it{j\/}})\index{isqrt1-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}:  isqrt-s0-exit-mem \\ \index{isqrt-s0-exit-mem}
\=\+({\rm{isqrt-s0p}}\,({\it{s\/}}, {\it{i\/}}, {\it{j\/}})\index{isqrt-s0p} $\wedge$ {\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{8}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{20}})\index{disjoint}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{isqrt1-t}}\,({\it{i\/}}, {\it{j\/}})\index{isqrt1-t})\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}


\noindent{\sc Event}:   Disable isqrt-s0p-j\_nonzerop.

\addvspace{18pt}

\begin{verbatim}; ISQRT program is correct.
; after an execution of this program,  the machine state satisfies:
;  0. normal exit.
;  1. the pc is returned to the next instruction of the caller.
;  2. the result -- ISQRT(i), is stored in D0.
;  3. a6, used by LINK, is restored to its original content.
;  4. the stack pointer sp(a7) is updated correctly to pop off one frame.
; the registers not touched by this program still have their original values.
; the memory is correctly changed -- the local effect on memory.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  isqrt-correctness \\ \index{isqrt-correctness}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{isqrt-t}}\,({\it{i\/}})\index{isqrt-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{isqrt-statep}}\,({\it{s\/}}, {\it{i\/}})\index{isqrt-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-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}) \\ 
$\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{7}}, {\it{s\/}})\index{read-an}, {\tt{4}})\index{add})\- \\ 
$\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{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{12}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{20}})\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{isqrt}}\,({\it{i\/}})\index{isqrt}))\-\-$\;${\bf  endlet}\-
\end{tabbing}


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

\addvspace{18pt}

\begin{verbatim}; start to prove isqrt correct.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  isqrt1-lower-bound \\ \index{isqrt1-lower-bound}
({\it{j\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ ({\it{i\/}} $\not<$ {\rm{sq}}\,({\rm{isqrt1}}\,({\it{i\/}}, {\it{j\/}})\index{isqrt1})\index{sq})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-by-2 \\ \index{quotient-by-2}
(({\it{x\/}} $\div$ {\tt{2}}) $+$ ({\it{x\/}} $\div$ {\tt{2}})) $\not<$ ({\it{x\/}} $-\;1$)
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  main-trick \\ \index{main-trick}
{\rm{sq}}\,($1\;+$ (({\it{j\/}} $+$ {\it{k\/}}) $\div$ {\tt{2}}))\index{sq} $\not<$ (({\it{j\/}} $*$ {\it{k\/}}) $+$ {\it{j\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sq-add1-non-zero \\ \index{sq-add1-non-zero}
{\rm{sq}}\,($1\;+$ {\it{x\/}})\index{sq} $\not=$ {\tt{0}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  main \\ \index{main}
({\it{j\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ ({\it{i\/}} $<$ {\rm{sq}}\,($1\;+$ (({\it{j\/}} $+$ ({\it{i\/}} $\div$ {\it{j\/}})) $\div$ {\tt{2}}))\index{sq})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  isqrt1-upper-bound \\ \index{isqrt1-upper-bound}
({\it{i\/}} $<$ {\rm{sq}}\,($1\;+$ {\it{j\/}})\index{sq}) $\rightarrow$ ({\it{i\/}} $<$ {\rm{sq}}\,($1\;+$ {\rm{isqrt1}}\,({\it{i\/}}, {\it{j\/}})\index{isqrt1})\index{sq})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  isqrt-$>$isqrt1 \\ \index{isqrt-$>$isqrt1}
({\tt{1}} $<$ {\it{i\/}}) $\rightarrow$ ({\it{i\/}} $<$ {\rm{sq}}\,($1\;+$ ({\it{i\/}} $\div$ {\tt{2}}))\index{sq})
\end{tabbing}

\begin{verbatim}; (isqrt i) is the square root of i:  (isqrt i)^2 <= i < [(isqrt i)+1]^2.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  isqrt-logic-correctness \\ \index{isqrt-logic-correctness}
({\tt{1}} $<$ {\it{i\/}}) $\rightarrow$ (({\it{i\/}} $<$ {\rm{sq}}\,($1\;+$ {\rm{isqrt}}\,({\it{i\/}})\index{isqrt})\index{sq}) $\wedge$ ({\it{i\/}} $\not<$ {\rm{sq}}\,({\rm{isqrt}}\,({\it{i\/}})\index{isqrt})\index{sq}))
\end{tabbing}

\begin{verbatim}; a simple time analysis.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  quotient-mono-1 \\ \index{quotient-mono-1}
(({\it{y\/}} $\leq$ {\it{z\/}}) $\wedge$ ({\it{y\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{z\/}} $\not\simeq {\tt{0}}$)) $\rightarrow$ (({\it{x\/}} $\div$ {\it{y\/}}) $\not<$ ({\it{x\/}} $\div$ {\it{z\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mean-lessp-1 \\ \index{mean-lessp-1}
({\it{x\/}} $\not<$ {\it{y\/}}) $\rightarrow$ ({\it{x\/}} $\not<$ (({\it{x\/}} $+$ {\it{y\/}}) $\div$ {\tt{2}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  isqrt1-t-la-0 \\ \index{isqrt1-t-la-0}
\=\+{\bf let }\=\+{\it{j1\/}}{\bf $\;$ be$\;\;$}({\it{j\/}} $+$ ({\it{i\/}} $\div$ {\it{j\/}})) $\div$ {\tt{2}}\- \\ 
{\bf in} \\ 
\=\+((({\it{i\/}} $\div$ {\it{j\/}}) $\leq$ {\it{j\/}}) $\wedge$ ({\tt{1}} $<$ {\it{i\/}}) $\wedge$ ({\tt{0}} $<$ {\it{j\/}})) \\ 
$\rightarrow$$\;\;\;\;$(({\it{x\/}} $-$ ({\it{i\/}} $\div$ {\it{j\/}})) $\not<$ ({\it{x\/}} $-$ ({\it{i\/}} $\div$ {\it{j1\/}})))\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mean-difference-1-1 \\ \index{mean-difference-1-1}
({\it{i\/}} $\leq$ {\it{j\/}}) $\rightarrow$ (((({\it{j\/}} $+$ {\it{i\/}}) $\div$ {\tt{2}}) $-$ {\it{i\/}}) $=$ (({\it{j\/}} $-$ {\it{i\/}}) $\div$ {\tt{2}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  isqrt1-t-la-1 \\ \index{isqrt1-t-la-1}
\=\+{\bf let }\=\+{\it{j1\/}}{\bf $\;$ be$\;\;$}({\it{j\/}} $+$ ({\it{i\/}} $\div$ {\it{j\/}})) $\div$ {\tt{2}}\- \\ 
{\bf in} \\ 
\=\+((({\it{i\/}} $\div$ {\it{j\/}}) $<$ {\it{j\/}}) $\wedge$ ({\tt{1}} $<$ {\it{i\/}}) $\wedge$ ({\tt{0}} $<$ {\it{j\/}})) \\ 
$\rightarrow$$\;\;\;\;$((({\it{j\/}} $-$ ({\it{i\/}} $\div$ {\it{j\/}})) $\div$ {\tt{2}}) $\not<$ ({\it{j1\/}} $-$ ({\it{i\/}} $\div$ {\it{j1\/}})))\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  isqrt1-t-la-2 \\ \index{isqrt1-t-la-2}
\=\+{\bf let }\=\+{\it{j1\/}}{\bf $\;$ be$\;\;$}({\it{j\/}} $+$ ({\it{i\/}} $\div$ {\it{j\/}})) $\div$ {\tt{2}}\- \\ 
{\bf in} \\ 
\=\+((({\it{i\/}} $\div$ {\it{j\/}}) $<$ {\it{j\/}}) $\wedge$ ({\tt{1}} $<$ {\it{i\/}}) $\wedge$ ({\tt{0}} $<$ {\it{j\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{log}}\,({\tt{2}}, ({\it{j\/}} $-$ ({\it{i\/}} $\div$ {\it{j\/}})) $\div$ {\tt{2}})\index{log} $\not<$ {\rm{log}}\,({\tt{2}}, {\it{j1\/}} $-$ ({\it{i\/}} $\div$ {\it{j1\/}}))\index{log})\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  isqrt-t1-ubound \\ \index{isqrt-t1-ubound}
\=\+(({\tt{1}} $<$ {\it{i\/}}) $\wedge$ ({\tt{0}} $<$ {\it{j\/}})) \\ 
$\rightarrow$$\;\;\;\;$(({\tt{18}} $+$ ({\tt{10}} $*$ {\rm{log}}\,({\tt{2}}, {\it{j\/}} $-$ ({\it{i\/}} $\div$ {\it{j\/}}))\index{log})) $\not<$ {\rm{isqrt1-t}}\,({\it{i\/}}, {\it{j\/}})\index{isqrt1-t})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  isqrt-t-$>$isqrt1-t \\ \index{isqrt-t-$>$isqrt1-t}
({\tt{1}} $<$ {\it{i\/}}) $\rightarrow$ (({\tt{4}} $+$ {\rm{isqrt1-t}}\,({\it{i\/}}, {\it{i\/}} $\div$ {\tt{2}})\index{isqrt1-t}) $\not<$ {\rm{isqrt-t}}\,({\it{i\/}})\index{isqrt-t})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  log-mono \\ \index{log-mono}
{\rm{log}}\,({\it{b\/}}, {\it{y\/}})\index{log} $\not<$ {\rm{log}}\,({\it{b\/}}, {\it{y\/}} $-$ {\it{x\/}})\index{log}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  isqrt-t-ubound-la \\ \index{isqrt-t-ubound-la}
({\tt{1}} $<$ {\it{i\/}}) $\rightarrow$ (({\tt{12}} $+$ ({\tt{10}} $*$ {\rm{log}}\,({\tt{2}}, {\it{i\/}})\index{log})) $\not<$ {\rm{isqrt-t}}\,({\it{i\/}})\index{isqrt-t})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  isqrt-t-ubound \\ \index{isqrt-t-ubound}
(({\it{i\/}} $<$ {\rm{exp}}\,({\tt{2}}, {\tt{31}})\index{exp}) $\wedge$ ({\tt{1}} $<$ {\it{i\/}})) $\rightarrow$ ({\rm{isqrt-t}}\,({\it{i\/}})\index{isqrt-t} $\leq$ {\tt{322}})
\end{tabbing}

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