\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 Robert S. Boyer and J Strother Moore.  All Rights
 Reserved.

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

 NO WARRANTY

 Robert S. Boyer and J Strother Moore PROVIDE 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 Robert S. Boyer or J Strother Moore 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.

|#

; This is the list of verification conditions for a FORTRAN square
; root program.  For the details of the algorithm, see the comment at
; the end of the file.  Boyer and Moore.

; This list of events has been further edited, for processing by
; DO-FILE, by (1) inserting the following NOTE-LIB, (2) commenting out
; each FORTRAN-COMMENT and following the comment with the
; corresponding macroexpansion, and (3) by commenting out each
; (COMMENT ...).

\end{verbatim}
\noindent{\sc Event}:   Start with the library {\tt{"fortran"}} using the compiled version.

\addvspace{18pt}

\begin{verbatim}; (FORTRAN-COMMENT FORTRAN)
\end{verbatim}\begin{tabbing}{\sc Axiom}:  fortran \\ \index{fortran}
{\bf{t}}
\end{tabbing}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}

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

\begin{tabbing}{\sc Axiom}:  input-conditions \\ \index{input-conditions}
{\tt{'}}{\tt{*1*true}}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{global-hyps} \\  
\=\+{\sc{global-hyps}}\index{global-hyps} \\ 
$=$$\;\;\;\;$(\=\+({\sc{i\$0}}\index{i\$0} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{i\$0}}\index{i\$0} $<$ {\sc{least-inexpressible-positive-integer}}\index{least-inexpressible-positive-inte!ger}) \\ 
$\wedge$$\;\;\;\;${\rm{znumberp}}\,({\sc{i\$0}}\index{i\$0})\index{znumberp})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  plus-1 \\ \index{plus-1}
({\tt{1}} $+$ {\it{x\/}}) $=$ ($1\;+$ {\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  difference-2 \\ \index{difference-2}
(($1\;+$ ($1\;+$ {\it{x\/}})) $-$ {\tt{2}}) $=$ {\rm{fix}}\,({\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-by-2 \\ \index{quotient-by-2}
(({\it{a\/}} $\div$ {\tt{2}}) $+$ ({\it{a\/}} $\div$ {\tt{2}})) $\not<$ ({\it{a\/}} $-\;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}:  lessp-remainder2 \\ \index{lessp-remainder2}
(({\it{x\/}} ${}${\bf{mod}}${}$ {\it{y\/}}) $<$ {\it{y\/}}) $=$ ({\it{y\/}} $\not\simeq {\tt{0}}$)
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-quotient-elim \\ \index{remainder-quotient-elim}
(({\it{y\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{x\/}} $\in\;${\bf{N}}${}$)) $\rightarrow$ ((({\it{x\/}} ${}${\bf{mod}}${}$ {\it{y\/}}) $+$ ({\it{y\/}} $*$ ({\it{x\/}} $\div$ {\it{y\/}}))) $=$ {\it{x\/}})
\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}


\noindent{\sc Event}:   Disable sq.

\addvspace{18pt}

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


\noindent{\sc Event}:   Enable sq.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  lessp-times-cancellation-restated-for-linear \\ \index{lessp-times-cancellation-restate!d-for-linear}
({\it{i\/}} $\not<$ {\it{j\/}}) $\rightarrow$ (({\it{a\/}} $*$ {\it{i\/}}) $\not<$ ({\it{a\/}} $*$ {\it{j\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  multiply-thru-by-divisor \\ \index{multiply-thru-by-divisor}
({\it{a\/}} $<$ ({\it{b\/}} $*$ {\it{c\/}})) $\rightarrow$ ((({\it{a\/}} $\div$ {\it{b\/}}) $<$ {\it{c\/}}) $=$ {\bf{t}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  times-greaterp-zero \\ \index{times-greaterp-zero}
(({\it{x\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{y\/}} $\not\simeq {\tt{0}}$)) $\rightarrow$ ({\tt{0}} $<$ ({\it{x\/}} $*$ {\it{y\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-shrinks \\ \index{quotient-shrinks}
{\it{i\/}} $\not<$ ({\it{i\/}} $\div$ {\it{j\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-shrinks-fast \\ \index{quotient-shrinks-fast}
{\it{i\/}} $\not<$ ({\tt{2}} $*$ ({\it{i\/}} $\div$ {\tt{2}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-by-1 \\ \index{quotient-by-1}
({\it{i\/}} $\div$ {\tt{1}}) $=$ {\rm{fix}}\,({\it{i\/}})
\end{tabbing}

\begin{verbatim}; (FORTRAN-COMMENT INPUT)
\end{verbatim}\begin{tabbing}{\sc Axiom}:  input \\ \index{input}
{\bf{t}}
\end{tabbing}

\begin{verbatim}; (FORTRAN-COMMENT LOGICAL-IF-T)
\end{verbatim}\begin{tabbing}{\sc Axiom}:  logical-if-t \\ \index{logical-if-t}
{\bf{t}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  stop \\ \index{stop}
($\neg$ {\rm{zlessp}}\,({\sc{i\$0}}\index{i\$0}, {\tt{'}}{\tt{0}})\index{zlessp}) $\vee$ ($\neg$ {\sc{global-hyps}}\index{global-hyps})
\end{tabbing}

\begin{verbatim}#| (COMMENT INPUT T) |#

\end{verbatim}
\noindent{\sc Event}:   Undo back through the event named `logical-if-t'.

\addvspace{18pt}

\begin{verbatim}; (FORTRAN-COMMENT LOGICAL-IF-F)
\end{verbatim}\begin{tabbing}{\sc Axiom}:  logical-if-f \\ \index{logical-if-f}
{\bf{t}}
\end{tabbing}

\begin{verbatim}; (FORTRAN-COMMENT LOGICAL-IF-T)
\end{verbatim}\begin{tabbing}{\sc Axiom}:  logical-if-t \\ \index{logical-if-t}
{\bf{t}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  input-cond-of-zquotient \\ \index{input-cond-of-zquotient}
\=\+({\rm{zgreaterp}}\,({\sc{i\$0}}\index{i\$0}, {\tt{'}}{\tt{1}})\index{zgreaterp} $\wedge$ {\sc{global-hyps}}\index{global-hyps}) \\ 
$\rightarrow$$\;\;\;\;$(($\neg$ {\rm{zeqp}}\,({\tt{'}}{\tt{2}}, {\tt{'}}{\tt{0}})\index{zeqp}) $\wedge$ {\rm{expressible-znumberp}}\,({\rm{zquotient}}\,({\sc{i\$0}}\index{i\$0}, {\tt{'}}{\tt{2}})\index{zquotient})\index{expressible-znumberp})\-
\end{tabbing}

\begin{verbatim}#| (COMMENT INPUT F T) |#

\end{verbatim}\begin{tabbing}{\sc Axiom}:  assignment \\ \index{assignment}
{\sc{isqrt\$1}}\index{isqrt\$1} $=$ {\rm{zquotient}}\,({\sc{i\$0}}\index{i\$0}, {\tt{'}}{\tt{2}})\index{zquotient}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lp \\ \index{lp}
\=\+({\rm{zgreaterp}}\,({\sc{i\$0}}\index{i\$0}, {\tt{'}}{\tt{1}})\index{zgreaterp} $\wedge$ {\sc{global-hyps}}\index{global-hyps}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+({\tt{'}}{\tt{0}} $<$ {\sc{isqrt\$1}}\index{isqrt\$1}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{i\$0}}\index{i\$0} $\not<$ ({\tt{'}}{\tt{2}} $*$ {\sc{isqrt\$1}}\index{isqrt\$1})) \\ 
$\wedge$$\;\;\;\;$(({\sc{isqrt\$1}}\index{isqrt\$1} $\in\;${\bf{N}}${}$) $\wedge$ ({\sc{i\$0}}\index{i\$0} $<$ {\rm{sq}}\,($1\;+$ {\sc{isqrt\$1}}\index{isqrt\$1})\index{sq})))\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{lex}}\,({\rm{cons}}\,({\sc{isqrt\$1}}\index{isqrt\$1}, {\tt{'}}{\tt{nil}}), {\rm{cons}}\,({\sc{i\$0}}\index{i\$0}, {\tt{'}}{\tt{nil}}))\index{lex})\-\-
\end{tabbing}

\begin{verbatim}#| (COMMENT INPUT F T) |#

\end{verbatim}
\noindent{\sc Event}:   Undo back through the event named `logical-if-t'.

\addvspace{18pt}

\begin{verbatim}; (FORTRAN-COMMENT LOGICAL-IF-F1)
\end{verbatim}\begin{tabbing}{\sc Axiom}:  logical-if-f1 \\ \index{logical-if-f1}
{\bf{t}}
\end{tabbing}

\begin{tabbing}{\sc Axiom}:  assignment \\ \index{assignment}
{\sc{isqrt\$1}}\index{isqrt\$1} $=$ {\sc{i\$0}}\index{i\$0}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  output \\ \index{output}
\=\+(($\neg$ {\rm{zgreaterp}}\,({\sc{i\$0}}\index{i\$0}, {\tt{'}}{\tt{1}})\index{zgreaterp}) $\wedge$ {\sc{global-hyps}}\index{global-hyps}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{znumberp}}\,({\sc{isqrt\$1}}\index{isqrt\$1})\index{znumberp} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{zgreatereqp}}\,({\sc{isqrt\$1}}\index{isqrt\$1}, {\tt{'}}{\tt{0}})\index{zgreatereqp} \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{i\$0}}\index{i\$0} $\not<$ {\rm{sq}}\,({\sc{isqrt\$1}}\index{isqrt\$1})\index{sq}) \\ 
$\wedge$$\;\;\;\;$({\sc{i\$0}}\index{i\$0} $<$ {\rm{sq}}\,({\tt{'}}{\tt{1}} $+$ {\sc{isqrt\$1}}\index{isqrt\$1})\index{sq}))\-)\-)\-\-
\end{tabbing}

\begin{verbatim}#| (COMMENT INPUT F F) |#

\end{verbatim}
\noindent{\sc Event}:   Undo back through the event named `input'.

\addvspace{18pt}

\begin{tabbing}{\sc Axiom}:  paths-from-lp \\ \index{paths-from-lp}
{\tt{'}}{\tt{*1*true}}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{path-hyps} \\  
\=\+{\sc{path-hyps}}\index{path-hyps} \\ 
$=$$\;\;\;\;$(\=\+{\sc{global-hyps}}\index{global-hyps} \\ 
$\wedge$$\;\;\;\;$(\=\+({\tt{'}}{\tt{0}} $<$ {\sc{isqrt\$1}}\index{isqrt\$1}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{i\$0}}\index{i\$0} $\not<$ ({\tt{'}}{\tt{2}} $*$ {\sc{isqrt\$1}}\index{isqrt\$1})) \\ 
$\wedge$$\;\;\;\;$(({\sc{isqrt\$1}}\index{isqrt\$1} $\in\;${\bf{N}}${}$) $\wedge$ ({\sc{i\$0}}\index{i\$0} $<$ {\rm{sq}}\,($1\;+$ {\sc{isqrt\$1}}\index{isqrt\$1})\index{sq})))\-)\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  definedness \\ \index{definedness}
{\sc{path-hyps}}\index{path-hyps} $\rightarrow$ {\rm{znumberp}}\,({\sc{isqrt\$1}}\index{isqrt\$1})\index{znumberp}
\end{tabbing}

\begin{verbatim}#| (COMMENT LP) |#

\end{verbatim}\begin{tabbing}{\sc Theorem}:  input-cond-of-zquotient \\ \index{input-cond-of-zquotient}
\=\+{\sc{path-hyps}}\index{path-hyps} \\ 
$\rightarrow$$\;\;\;\;$(\=\+($\neg$ {\rm{zeqp}}\,({\sc{isqrt\$1}}\index{isqrt\$1}, {\tt{'}}{\tt{0}})\index{zeqp}) \\ 
$\wedge$$\;\;\;\;${\rm{expressible-znumberp}}\,({\rm{zquotient}}\,({\sc{i\$0}}\index{i\$0}, {\sc{isqrt\$1}}\index{isqrt\$1})\index{zquotient})\index{expressible-znumberp})\-\-
\end{tabbing}

\begin{verbatim}#| (COMMENT LP) |#

; (FORTRAN-COMMENT LOGICAL-IF-T)
\end{verbatim}\begin{tabbing}{\sc Axiom}:  logical-if-t \\ \index{logical-if-t}
{\bf{t}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  output1 \\ \index{output1}
\=\+({\rm{zgreatereqp}}\,({\rm{zquotient}}\,({\sc{i\$0}}\index{i\$0}, {\sc{isqrt\$1}}\index{isqrt\$1})\index{zquotient}, {\sc{isqrt\$1}}\index{isqrt\$1})\index{zgreatereqp} $\wedge$ {\sc{path-hyps}}\index{path-hyps}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{znumberp}}\,({\sc{isqrt\$1}}\index{isqrt\$1})\index{znumberp} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{zgreatereqp}}\,({\sc{isqrt\$1}}\index{isqrt\$1}, {\tt{'}}{\tt{0}})\index{zgreatereqp} \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{i\$0}}\index{i\$0} $\not<$ {\rm{sq}}\,({\sc{isqrt\$1}}\index{isqrt\$1})\index{sq}) \\ 
$\wedge$$\;\;\;\;$({\sc{i\$0}}\index{i\$0} $<$ {\rm{sq}}\,({\tt{'}}{\tt{1}} $+$ {\sc{isqrt\$1}}\index{isqrt\$1})\index{sq}))\-)\-)\-\-
\end{tabbing}

\begin{verbatim}#| (COMMENT LP T) |#

\end{verbatim}
\noindent{\sc Event}:   Undo back through the event named `logical-if-t'.

\addvspace{18pt}

\begin{verbatim}; (FORTRAN-COMMENT LOGICAL-IF-F2)
\end{verbatim}\begin{tabbing}{\sc Axiom}:  logical-if-f2 \\ \index{logical-if-f2}
{\bf{t}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  input-cond-of-zquotient1 \\ \index{input-cond-of-zquotient1}
\=\+(($\neg$ {\rm{zgreatereqp}}\,({\rm{zquotient}}\,({\sc{i\$0}}\index{i\$0}, {\sc{isqrt\$1}}\index{isqrt\$1})\index{zquotient}, {\sc{isqrt\$1}}\index{isqrt\$1})\index{zgreatereqp}) $\wedge$ {\sc{path-hyps}}\index{path-hyps}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+($\neg$ {\rm{zeqp}}\,({\sc{isqrt\$1}}\index{isqrt\$1}, {\tt{'}}{\tt{0}})\index{zeqp}) \\ 
$\wedge$$\;\;\;\;${\rm{expressible-znumberp}}\,({\rm{zquotient}}\,({\sc{i\$0}}\index{i\$0}, {\sc{isqrt\$1}}\index{isqrt\$1})\index{zquotient})\index{expressible-znumberp})\-\-
\end{tabbing}

\begin{verbatim}#| (COMMENT LP F) |#

\end{verbatim}\begin{tabbing}{\sc Theorem}:  input-cond-of-zplus \\ \index{input-cond-of-zplus}
\=\+(($\neg$ {\rm{zgreatereqp}}\,({\rm{zquotient}}\,({\sc{i\$0}}\index{i\$0}, {\sc{isqrt\$1}}\index{isqrt\$1})\index{zquotient}, {\sc{isqrt\$1}}\index{isqrt\$1})\index{zgreatereqp}) $\wedge$ {\sc{path-hyps}}\index{path-hyps}) \\ 
$\rightarrow$$\;\;\;\;${\rm{expressible-znumberp}}\,({\rm{zplus}}\,({\sc{isqrt\$1}}\index{isqrt\$1}, {\rm{zquotient}}\,({\sc{i\$0}}\index{i\$0}, {\sc{isqrt\$1}}\index{isqrt\$1})\index{zquotient})\index{zplus})\index{expressible-znumberp}\-
\end{tabbing}

\begin{verbatim}#| (COMMENT LP F) |#

\end{verbatim}\begin{tabbing}{\sc Theorem}:  input-cond-of-zquotient2 \\ \index{input-cond-of-zquotient2}
\=\+(($\neg$ {\rm{zgreatereqp}}\,({\rm{zquotient}}\,({\sc{i\$0}}\index{i\$0}, {\sc{isqrt\$1}}\index{isqrt\$1})\index{zquotient}, {\sc{isqrt\$1}}\index{isqrt\$1})\index{zgreatereqp}) $\wedge$ {\sc{path-hyps}}\index{path-hyps}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+($\neg$ {\rm{zeqp}}\,({\tt{'}}{\tt{2}}, {\tt{'}}{\tt{0}})\index{zeqp}) \\ 
$\wedge$$\;\;\;\;${\rm{expressible-znumberp}}\,({\rm{zquotient}}\,(\=\+{\rm{zplus}}\,(\=\+{\sc{isqrt\$1}}\index{isqrt\$1}, \\ 
{\rm{zquotient}}\,({\sc{i\$0}}\index{i\$0}, {\sc{isqrt\$1}}\index{isqrt\$1})\index{zquotient})\-\index{zplus}, \\ 
{\tt{'}}{\tt{2}})\-\index{zquotient})\index{expressible-znumberp})\-\-
\end{tabbing}

\begin{verbatim}#| (COMMENT LP F) |#

\end{verbatim}\begin{tabbing}{\sc Axiom}:  assignment1 \\ \index{assignment1}
{\sc{isqrt\$2}}\index{isqrt\$2} $=$ {\rm{zquotient}}\,({\rm{zplus}}\,({\sc{isqrt\$1}}\index{isqrt\$1}, {\rm{zquotient}}\,({\sc{i\$0}}\index{i\$0}, {\sc{isqrt\$1}}\index{isqrt\$1})\index{zquotient})\index{zplus}, {\tt{'}}{\tt{2}})\index{zquotient}
\end{tabbing}


\noindent{\sc Event}:   Disable sq.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  lp1 \\ \index{lp1}
\=\+(($\neg$ {\rm{zgreatereqp}}\,({\rm{zquotient}}\,({\sc{i\$0}}\index{i\$0}, {\sc{isqrt\$1}}\index{isqrt\$1})\index{zquotient}, {\sc{isqrt\$1}}\index{isqrt\$1})\index{zgreatereqp}) $\wedge$ {\sc{path-hyps}}\index{path-hyps}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+({\tt{'}}{\tt{0}} $<$ {\sc{isqrt\$2}}\index{isqrt\$2}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{i\$0}}\index{i\$0} $\not<$ ({\tt{'}}{\tt{2}} $*$ {\sc{isqrt\$2}}\index{isqrt\$2})) \\ 
$\wedge$$\;\;\;\;$(({\sc{isqrt\$2}}\index{isqrt\$2} $\in\;${\bf{N}}${}$) $\wedge$ ({\sc{i\$0}}\index{i\$0} $<$ {\rm{sq}}\,($1\;+$ {\sc{isqrt\$2}}\index{isqrt\$2})\index{sq})))\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{lex}}\,({\rm{cons}}\,({\sc{isqrt\$2}}\index{isqrt\$2}, {\tt{'}}{\tt{nil}}), {\rm{cons}}\,({\sc{isqrt\$1}}\index{isqrt\$1}, {\tt{'}}{\tt{nil}}))\index{lex})\-\-
\end{tabbing}

\begin{verbatim}#| (COMMENT LP F) |#

\end{verbatim}
\noindent{\sc Event}:   Undo back through the event named `paths-from-lp'.

\addvspace{18pt}


\noindent{\sc Event}:   Undo back through the event named `fortran'.

\addvspace{18pt}


\begin{verbatim}#|



The correctness of the program depends upon the following events:

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Definition.
        (SQ I)
           =
        (TIMES I I)
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        (FORTRAN-COMMENT ISQRT-STUFF)
@END(VERBATIM)
@END(GROUP)


\end{verbatim}
\newpage
\begin{verbatim}

Specification for routine ISQRT

The input assertion:
        (AND (NUMBERP (I STATE))
             (LESSP (I STATE)
                    (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))


The output assertion:
        (AND (ZGREATEREQP ANS 0)
             (NOT (LESSP (I STATE) (SQ ANS)))
             (LESSP (I STATE) (SQ (PLUS 1 ANS))))
\end{verbatim}
\newpage
\begin{verbatim}

      END
      INTEGER FUNCTION ISQRT(I)
      INTEGER I
C     CALCULATE THE SQUARE ROOT OF I USING THE NEWTON METHOD. 
      IF ((I .LT. 0)) STOP
      IF ((I .GT. 1)) GOTO 100
      ISQRT = I
      RETURN
C     ISQRT TAKES ON INCREASINGLY SMALLER VALUES AND CONVERGES TO THE SQ
C     UARE ROOT OF I. THE FIRST APPROXIMATION IS ONE HALF I, WHICH IS NO
C     T LESS THAN THE SQUARE ROOT OF I WHEN 1 IS LESS THAN I. 
100   ISQRT = (I / 2)
200   CONTINUE
C     ASSERTION LP
      IF (((I / ISQRT) .GE. ISQRT)) RETURN
      ISQRT = ((ISQRT + (I / ISQRT)) / 2)
C     XXX SQ-REWRITE-OFF-AGAIN
      GOTO 200
      END


The XXX at ISQRT-STUFF.
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  PLUS-1 (rewrite):
        (EQUAL (PLUS 1 X) (ADD1 X))
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  DIFFERENCE-2 (rewrite):
        (EQUAL (DIFFERENCE (ADD1 (ADD1 X)) 2)
               (FIX X))
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  QUOTIENT-BY-2 (rewrite):
        (NOT (LESSP (PLUS (QUOTIENT A 2) (QUOTIENT A 2))
                    (SUB1 A)))
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  MAIN-TRICK (rewrite):
        (NOT (LESSP (SQ (ADD1 (QUOTIENT (PLUS J K) 2)))
                    (PLUS (TIMES J K) J)))
        Hint:  Induct as for (LESSP J K).
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  LESSP-REMAINDER2 (rewrite and generalize):
        (EQUAL (LESSP (REMAINDER X Y) Y)
               (NOT (ZEROP Y)))
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  REMAINDER-QUOTIENT-ELIM (elimination):
        (IMPLIES (AND (NOT (ZEROP Y)) (NUMBERP X))
                 (EQUAL (PLUS (REMAINDER X Y)
                              (TIMES Y (QUOTIENT X Y)))
                        X))
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  SQ-ADD1-NON-ZERO (rewrite):
        (NOT (EQUAL (SQ (ADD1 X)) 0))
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Enable SQ.
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  MAIN (rewrite):
        (IMPLIES (NOT (ZEROP J))
                 (LESSP I
                        (SQ (ADD1 (QUOTIENT (PLUS J (QUOTIENT I J))
                                            2)))))
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Disable SQ.
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  LESSP-TIMES-CANCELLATION-RESTATED-FOR-LINEAR (rewrite):
        (IMPLIES (NOT (LESSP I J))
                 (NOT (LESSP (TIMES A I) (TIMES A J))))
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  MULTIPLY-THRU-BY-DIVISOR (rewrite):
        (IMPLIES (LESSP A (TIMES B C))
                 (EQUAL (LESSP (QUOTIENT A B) C) T))
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  TIMES-GREATERP-ZERO (rewrite):
        (IMPLIES (AND (NOT (ZEROP X)) (NOT (ZEROP Y)))
                 (LESSP 0 (TIMES X Y)))
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  QUOTIENT-SHRINKS (rewrite):
        (NOT (LESSP I (QUOTIENT I J)))
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  QUOTIENT-SHRINKS-FAST (rewrite):
        (NOT (LESSP I (TIMES 2 (QUOTIENT I 2))))
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  QUOTIENT-BY-1 (rewrite):
        (EQUAL (QUOTIENT I 1) (FIX I))
@END(VERBATIM)
@END(GROUP)


\end{verbatim}
\newpage
\begin{verbatim}

Hints for routine ISQRT

                              

The input clock:
        (LIST (I (START)))

The invariant and clock named LP.

        (AND (LESSP 0 (ISQRT STATE))
             (NOT (LESSP (I STATE)
                         (TIMES 2 (ISQRT STATE))))
             (NUMBERP (ISQRT STATE))
             (LESSP (I STATE)
                    (SQ (ADD1 (ISQRT STATE)))))

        (LIST (ISQRT STATE))

The XXX named SQ-REWRITE-OFF-AGAIN:
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Enable SQ.
@END(VERBATIM)
@END(GROUP)

|#
\end{verbatim}
%\end{list}
\printindex
\end{document}
