\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 version of our
; majority vote algorithm.  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 a\$0\index{a\$0}\/} of 0 arguments.

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


\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 i\$1\index{i\$1}\/} of 0 arguments.

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{cnt} \\  
\=\+{\rm{cnt}}\,({\it{x\/}}, {\it{a\/}}, {\it{i\/}}, {\it{n\/}})\index{cnt} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{n\/}} $\simeq {\tt{0}}$) $\vee$ ({\it{n\/}} $<$ {\it{i\/}})$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\rm{zeqp}}\,({\it{x\/}}, {\rm{elt1}}\,({\it{a\/}}, {\it{n\/}})\index{elt1})\index{zeqp}$\;\;${\bf then }$1\;+$ {\rm{cnt}}\,({\it{x\/}}, {\it{a\/}}, {\it{i\/}}, {\it{n\/}} $-\;1$)\index{cnt} \\ 
{\bf else }{\rm{cnt}}\,({\it{x\/}}, {\it{a\/}}, {\it{i\/}}, {\it{n\/}} $-\;1$)\index{cnt}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Axiom}:  input-conditions \\ \index{input-conditions}
\=\+(({\tt{'}}{\tt{0}} $<$ {\it{j\/}}) $\wedge$ (({\sc{n\$0}}\index{n\$0} $\not<$ {\it{j\/}}) $\wedge$ ($\neg$ {\rm{negativep}}\,({\rm{elt1}}\,({\it{a\/}}, {\it{j\/}})\index{elt1})))) \\ 
$\rightarrow$$\;\;\;\;$({\rm{elt1}}\,({\it{a\/}}, {\it{j\/}})\index{elt1} $\in\;${\bf{N}}${}$)\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{global-hyps} \\  
\=\+{\sc{global-hyps}}\index{global-hyps} \\ 
$=$$\;\;\;\;$(\=\+({\sc{n\$0}}\index{n\$0} $\not=$ {\tt{'}}{\tt{0}}) \\ 
$\wedge$$\;\;\;\;$(\=\+(($1\;+$ {\sc{n\$0}}\index{n\$0}) $<$ {\sc{least-inexpressible-positive-integer}}\index{least-inexpressible-positive-inte!ger}) \\ 
$\wedge$$\;\;\;\;$({\sc{n\$0}}\index{n\$0} $\in\;${\bf{N}}${}$))\-)\-\-
\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-0 \\ \index{difference-0}
({\it{x\/}} $\not<$ {\it{y\/}}) $\rightarrow$ (({\it{y\/}} $-$ {\it{x\/}}) $=$ {\tt{0}})
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  lessp-x-1 \\ \index{lessp-x-1}
({\it{x\/}} $<$ {\tt{1}}) $=$ ({\it{x\/}} $\simeq {\tt{0}}$)
\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}:  quotient-by-2-bound \\ \index{quotient-by-2-bound}
{\it{x\/}} $\not<$ ({\it{x\/}} $\div$ {\tt{2}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-quotient-rewrite \\ \index{lessp-quotient-rewrite}
(({\it{n\/}} $\div$ {\tt{2}}) $<$ {\it{m\/}}) $=$ ({\it{n\/}} $<$ ({\it{m\/}} $+$ {\it{m\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  znormalize-zero \\ \index{znormalize-zero}
({\it{x\/}} $\in\;${\bf{N}}${}$) $\rightarrow$ (({\rm{znormalize}}\,({\it{x\/}})\index{znormalize} $=$ {\tt{0}}) $=$ ({\it{x\/}} $=$ {\tt{0}}))
\end{tabbing}


\noindent{\sc Event}:   Disable znormalize.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  cnt-bound \\ \index{cnt-bound}
{\it{n\/}} $\not<$ {\rm{cnt}}\,({\it{x\/}}, {\it{a\/}}, {\tt{1}}, {\it{n\/}})\index{cnt}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  input-definedness \\ \index{input-definedness}
{\sc{global-hyps}}\index{global-hyps} $\rightarrow$ {\tt{'}}{\tt{*1*true}}
\end{tabbing}

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

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

\begin{tabbing}{\sc Axiom}:  assignment \\ \index{assignment}
\=\+({\sc{boole\$1}}\index{boole\$1} $=$ {\sc{boole\$0}}\index{boole\$0}) \\ 
$\wedge$$\;\;\;\;$(({\sc{cand\$1}}\index{cand\$1} $=$ {\sc{cand\$0}}\index{cand\$0}) $\wedge$ (({\sc{i\$1}}\index{i\$1} $=$ {\sc{i\$0}}\index{i\$0}) $\wedge$ ({\sc{k\$1}}\index{k\$1} $=$ {\tt{'}}{\tt{0}})))\-
\end{tabbing}

\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{tabbing}{\sc Axiom}:  assignment1 \\ \index{assignment1}
\=\+({\sc{boole\$2}}\index{boole\$2} $=$ {\sc{boole\$1}}\index{boole\$1}) \\ 
$\wedge$$\;\;\;\;$(({\sc{cand\$2}}\index{cand\$2} $=$ {\sc{cand\$1}}\index{cand\$1}) $\wedge$ (({\sc{i\$2}}\index{i\$2} $=$ {\tt{'}}{\tt{1}}) $\wedge$ ({\sc{k\$2}}\index{k\$2} $=$ {\sc{k\$1}}\index{k\$1})))\-
\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 Axiom}:  effects-of-undefiner \\ \index{effects-of-undefiner}
({\sc{boole\$3}}\index{boole\$3} $=$ {\sc{boole\$2}}\index{boole\$2}) $\wedge$ (({\sc{cand\$3}}\index{cand\$3} $=$ {\sc{cand\$2}}\index{cand\$2}) $\wedge$ ({\sc{k\$3}}\index{k\$3} $=$ {\sc{k\$2}}\index{k\$2}))
\end{tabbing}

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

\begin{tabbing}{\sc Axiom}:  assignment2 \\ \index{assignment2}
\=\+({\sc{boole\$4}}\index{boole\$4} $=$ {\tt{'}}{\tt{*1*false}}) \\ 
$\wedge$$\;\;\;\;$(({\sc{cand\$4}}\index{cand\$4} $=$ {\sc{cand\$3}}\index{cand\$3}) $\wedge$ (({\sc{i\$4}}\index{i\$4} $=$ {\sc{i\$3}}\index{i\$3}) $\wedge$ ({\sc{k\$4}}\index{k\$4} $=$ {\sc{k\$3}}\index{k\$3})))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  output \\ \index{output}
\=\+({\rm{zeqp}}\,({\sc{k\$3}}\index{k\$3}, {\tt{'}}{\tt{0}})\index{zeqp} $\wedge$ ({\sc{i\$2}}\index{i\$2} $\wedge$ ({\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp} $\wedge$ {\sc{global-hyps}}\index{global-hyps}))) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(({\sc{boole\$4}}\index{boole\$4} $=$ {\tt{'}}{\tt{*1*true}}) $\vee$ ({\sc{boole\$4}}\index{boole\$4} $=$ {\tt{'}}{\tt{*1*false}})) \\ 
$\wedge$$\;\;\;\;$\=\+{\bf if }{\sc{boole\$4}}\index{boole\$4} \\ 
{\bf then }\=\+{\rm{znumberp}}\,({\sc{cand\$4}}\index{cand\$4})\index{znumberp} \\ 
$\wedge$$\;\;\;\;$(({\sc{n\$0}}\index{n\$0} $\div$ {\tt{'}}{\tt{2}}) $<$ {\rm{cnt}}\,({\sc{cand\$4}}\index{cand\$4}, {\sc{a\$0}}\index{a\$0}, {\tt{'}}{\tt{1}}, {\sc{n\$0}}\index{n\$0})\index{cnt})\- \\ 
{\bf else }({\sc{n\$0}}\index{n\$0} $\div$ {\tt{'}}{\tt{2}}) $\not<$ {\rm{cnt}}\,({\it{x\/}}, {\sc{a\$0}}\index{a\$0}, {\tt{'}}{\tt{1}}, {\sc{n\$0}}\index{n\$0})\index{cnt}$\;${\bf  endif}\-)\-\-
\end{tabbing}

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

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

\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}:  assignment2 \\ \index{assignment2}
\=\+({\sc{boole\$4}}\index{boole\$4} $=$ {\tt{'}}{\tt{*1*true}}) \\ 
$\wedge$$\;\;\;\;$(({\sc{cand\$4}}\index{cand\$4} $=$ {\sc{cand\$3}}\index{cand\$3}) $\wedge$ (({\sc{i\$4}}\index{i\$4} $=$ {\sc{i\$3}}\index{i\$3}) $\wedge$ ({\sc{k\$4}}\index{k\$4} $=$ {\sc{k\$3}}\index{k\$3})))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  input-cond-of-zquotient \\ \index{input-cond-of-zquotient}
\=\+(($\neg$ {\rm{zeqp}}\,({\sc{k\$3}}\index{k\$3}, {\tt{'}}{\tt{0}})\index{zeqp}) $\wedge$ ({\sc{i\$2}}\index{i\$2} $\wedge$ ({\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\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{n\$0}}\index{n\$0}, {\tt{'}}{\tt{2}})\index{zquotient})\index{expressible-znumberp})\-
\end{tabbing}

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

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

\begin{tabbing}{\sc Theorem}:  output \\ \index{output}
\=\+(\=\+{\rm{zgreaterp}}\,({\sc{k\$4}}\index{k\$4}, {\rm{zquotient}}\,({\sc{n\$0}}\index{n\$0}, {\tt{'}}{\tt{2}})\index{zquotient})\index{zgreaterp} \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zeqp}}\,({\sc{k\$3}}\index{k\$3}, {\tt{'}}{\tt{0}})\index{zeqp}) \\ 
$\wedge$$\;\;\;\;$({\sc{i\$2}}\index{i\$2} $\wedge$ ({\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp} $\wedge$ {\sc{global-hyps}}\index{global-hyps})))\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(({\sc{boole\$4}}\index{boole\$4} $=$ {\tt{'}}{\tt{*1*true}}) $\vee$ ({\sc{boole\$4}}\index{boole\$4} $=$ {\tt{'}}{\tt{*1*false}})) \\ 
$\wedge$$\;\;\;\;$\=\+{\bf if }{\sc{boole\$4}}\index{boole\$4} \\ 
{\bf then }\=\+{\rm{znumberp}}\,({\sc{cand\$4}}\index{cand\$4})\index{znumberp} \\ 
$\wedge$$\;\;\;\;$(({\sc{n\$0}}\index{n\$0} $\div$ {\tt{'}}{\tt{2}}) $<$ {\rm{cnt}}\,({\sc{cand\$4}}\index{cand\$4}, {\sc{a\$0}}\index{a\$0}, {\tt{'}}{\tt{1}}, {\sc{n\$0}}\index{n\$0})\index{cnt})\- \\ 
{\bf else }({\sc{n\$0}}\index{n\$0} $\div$ {\tt{'}}{\tt{2}}) $\not<$ {\rm{cnt}}\,({\it{x\/}}, {\sc{a\$0}}\index{a\$0}, {\tt{'}}{\tt{1}}, {\sc{n\$0}}\index{n\$0})\index{cnt}$\;${\bf  endif}\-)\-\-
\end{tabbing}

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

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

\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 Axiom}:  assignment3 \\ \index{assignment3}
\=\+({\sc{boole\$5}}\index{boole\$5} $=$ {\sc{boole\$4}}\index{boole\$4}) \\ 
$\wedge$$\;\;\;\;$(({\sc{cand\$5}}\index{cand\$5} $=$ {\sc{cand\$4}}\index{cand\$4}) $\wedge$ (({\sc{i\$5}}\index{i\$5} $=$ {\sc{i\$4}}\index{i\$4}) $\wedge$ ({\sc{k\$5}}\index{k\$5} $=$ {\tt{'}}{\tt{0}})))\-
\end{tabbing}

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

\begin{tabbing}{\sc Axiom}:  assignment4 \\ \index{assignment4}
\=\+({\sc{boole\$6}}\index{boole\$6} $=$ {\sc{boole\$5}}\index{boole\$5}) \\ 
$\wedge$$\;\;\;\;$(({\sc{cand\$6}}\index{cand\$6} $=$ {\sc{cand\$5}}\index{cand\$5}) $\wedge$ (({\sc{i\$6}}\index{i\$6} $=$ {\tt{'}}{\tt{1}}) $\wedge$ ({\sc{k\$6}}\index{k\$6} $=$ {\sc{k\$5}}\index{k\$5})))\-
\end{tabbing}

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

\begin{tabbing}{\sc Axiom}:  effects-of-undefiner1 \\ \index{effects-of-undefiner1}
({\sc{boole\$7}}\index{boole\$7} $=$ {\sc{boole\$6}}\index{boole\$6}) $\wedge$ (({\sc{cand\$7}}\index{cand\$7} $=$ {\sc{cand\$6}}\index{cand\$6}) $\wedge$ ({\sc{k\$7}}\index{k\$7} $=$ {\sc{k\$6}}\index{k\$6}))
\end{tabbing}

\begin{tabbing}{\sc Axiom}:  assignment5 \\ \index{assignment5}
\=\+({\sc{boole\$8}}\index{boole\$8} $=$ {\tt{'}}{\tt{*1*false}}) \\ 
$\wedge$$\;\;\;\;$(({\sc{cand\$8}}\index{cand\$8} $=$ {\sc{cand\$7}}\index{cand\$7}) $\wedge$ (({\sc{i\$8}}\index{i\$8} $=$ {\sc{i\$7}}\index{i\$7}) $\wedge$ ({\sc{k\$8}}\index{k\$8} $=$ {\sc{k\$7}}\index{k\$7})))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  output \\ \index{output}
\=\+(\=\+{\sc{i\$6}}\index{i\$6} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{zgreaterp}}\,({\sc{i\$6}}\index{i\$6}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp} \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{k\$4}}\index{k\$4}, {\rm{zquotient}}\,({\sc{n\$0}}\index{n\$0}, {\tt{'}}{\tt{2}})\index{zquotient})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zeqp}}\,({\sc{k\$3}}\index{k\$3}, {\tt{'}}{\tt{0}})\index{zeqp}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\sc{i\$2}}\index{i\$2} \\ 
$\wedge$$\;\;\;\;$({\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp} $\wedge$ {\sc{global-hyps}}\index{global-hyps}))\-)\-)\-)\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(({\sc{boole\$8}}\index{boole\$8} $=$ {\tt{'}}{\tt{*1*true}}) $\vee$ ({\sc{boole\$8}}\index{boole\$8} $=$ {\tt{'}}{\tt{*1*false}})) \\ 
$\wedge$$\;\;\;\;$\=\+{\bf if }{\sc{boole\$8}}\index{boole\$8} \\ 
{\bf then }\=\+{\rm{znumberp}}\,({\sc{cand\$8}}\index{cand\$8})\index{znumberp} \\ 
$\wedge$$\;\;\;\;$(({\sc{n\$0}}\index{n\$0} $\div$ {\tt{'}}{\tt{2}}) $<$ {\rm{cnt}}\,({\sc{cand\$8}}\index{cand\$8}, {\sc{a\$0}}\index{a\$0}, {\tt{'}}{\tt{1}}, {\sc{n\$0}}\index{n\$0})\index{cnt})\- \\ 
{\bf else }({\sc{n\$0}}\index{n\$0} $\div$ {\tt{'}}{\tt{2}}) $\not<$ {\rm{cnt}}\,({\it{x\/}}, {\sc{a\$0}}\index{a\$0}, {\tt{'}}{\tt{1}}, {\sc{n\$0}}\index{n\$0})\index{cnt}$\;${\bf  endif}\-)\-\-
\end{tabbing}

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

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

\addvspace{18pt}

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

\begin{tabbing}{\sc Theorem}:  array-bounds-check-for-a \\ \index{array-bounds-check-for-a}
\=\+(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{i\$6}}\index{i\$6}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{k\$4}}\index{k\$4}, {\rm{zquotient}}\,({\sc{n\$0}}\index{n\$0}, {\tt{'}}{\tt{2}})\index{zquotient})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zeqp}}\,({\sc{k\$3}}\index{k\$3}, {\tt{'}}{\tt{0}})\index{zeqp}) \\ 
$\wedge$$\;\;\;\;$({\sc{i\$2}}\index{i\$2} $\wedge$ ({\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp} $\wedge$ {\sc{global-hyps}}\index{global-hyps})))\-)\-)\- \\ 
$\rightarrow$$\;\;\;\;$(({\tt{'}}{\tt{0}} $<$ {\sc{i\$6}}\index{i\$6}) $\wedge$ ({\sc{n\$0}}\index{n\$0} $\not<$ {\sc{i\$6}}\index{i\$6}))\-
\end{tabbing}

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

\end{verbatim}\begin{tabbing}{\sc Theorem}:  definedness \\ \index{definedness}
\=\+(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{i\$6}}\index{i\$6}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{k\$4}}\index{k\$4}, {\rm{zquotient}}\,({\sc{n\$0}}\index{n\$0}, {\tt{'}}{\tt{2}})\index{zquotient})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zeqp}}\,({\sc{k\$3}}\index{k\$3}, {\tt{'}}{\tt{0}})\index{zeqp}) \\ 
$\wedge$$\;\;\;\;$({\sc{i\$2}}\index{i\$2} $\wedge$ ({\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp} $\wedge$ {\sc{global-hyps}}\index{global-hyps})))\-)\-)\- \\ 
$\rightarrow$$\;\;\;\;${\rm{znumberp}}\,({\sc{cand\$6}}\index{cand\$6})\index{znumberp}\-
\end{tabbing}

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

\end{verbatim}\begin{tabbing}{\sc Theorem}:  definedness1 \\ \index{definedness1}
\=\+(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{i\$6}}\index{i\$6}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{k\$4}}\index{k\$4}, {\rm{zquotient}}\,({\sc{n\$0}}\index{n\$0}, {\tt{'}}{\tt{2}})\index{zquotient})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zeqp}}\,({\sc{k\$3}}\index{k\$3}, {\tt{'}}{\tt{0}})\index{zeqp}) \\ 
$\wedge$$\;\;\;\;$({\sc{i\$2}}\index{i\$2} $\wedge$ ({\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp} $\wedge$ {\sc{global-hyps}}\index{global-hyps})))\-)\-)\- \\ 
$\rightarrow$$\;\;\;\;${\rm{znumberp}}\,({\rm{elt1}}\,({\sc{a\$0}}\index{a\$0}, {\sc{i\$6}}\index{i\$6})\index{elt1})\index{znumberp}\-
\end{tabbing}

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

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

\begin{tabbing}{\sc Theorem}:  phase2-invrt \\ \index{phase2-invrt}
\=\+(\=\+{\rm{zneqp}}\,({\sc{cand\$6}}\index{cand\$6}, {\rm{elt1}}\,({\sc{a\$0}}\index{a\$0}, {\sc{i\$6}}\index{i\$6})\index{elt1})\index{zneqp} \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{i\$6}}\index{i\$6}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{k\$4}}\index{k\$4}, {\rm{zquotient}}\,({\sc{n\$0}}\index{n\$0}, {\tt{'}}{\tt{2}})\index{zquotient})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zeqp}}\,({\sc{k\$3}}\index{k\$3}, {\tt{'}}{\tt{0}})\index{zeqp}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\sc{i\$2}}\index{i\$2} \\ 
$\wedge$$\;\;\;\;$({\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp} $\wedge$ {\sc{global-hyps}}\index{global-hyps}))\-)\-)\-)\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+({\sc{i\$6}}\index{i\$6} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{i\$6}}\index{i\$6} $\not=$ {\tt{'}}{\tt{0}}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{boole\$6}}\index{boole\$6} $=$ {\tt{'}}{\tt{*1*true}}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{n\$0}}\index{n\$0} $\not<$ {\sc{i\$6}}\index{i\$6}) \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+($\neg$ {\rm{negativep}}\,({\sc{cand\$6}}\index{cand\$6})) \\ 
$\rightarrow$$\;\;\;\;$({\sc{cand\$6}}\index{cand\$6} $\in\;${\bf{N}}${}$))\- \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\rm{zneqp}}\,({\it{x\/}}, {\sc{cand\$6}}\index{cand\$6})\index{zneqp} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\sc{n\$0}}\index{n\$0} \\ 
$\not<$$\;\;\;\;$(\=\+{\tt{'}}{\tt{2}} \\ 
$*$$\;\;\;\;${\rm{cnt}}\,(\=\+{\it{x\/}}, \\ 
{\sc{a\$0}}\index{a\$0}, \\ 
{\tt{'}}{\tt{1}}, \\ 
{\sc{n\$0}}\index{n\$0})\-\index{cnt})\-)\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\sc{n\$0}}\index{n\$0} \\ 
$\not<$$\;\;\;\;$(\=\+{\tt{'}}{\tt{2}} \\ 
$*$$\;\;\;\;${\rm{cnt}}\,(\=\+{\sc{cand\$6}}\index{cand\$6}, \\ 
{\sc{a\$0}}\index{a\$0}, \\ 
{\tt{'}}{\tt{1}}, \\ 
{\sc{i\$6}}\index{i\$6})\-\index{cnt})\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\sc{k\$6}}\index{k\$6} \\ 
$=$$\;\;\;\;${\rm{cnt}}\,(\=\+{\sc{cand\$6}}\index{cand\$6}, \\ 
{\sc{a\$0}}\index{a\$0}, \\ 
{\tt{'}}{\tt{1}}, \\ 
{\sc{i\$6}}\index{i\$6})\-\index{cnt})\-)\-)\-)\-)\-)\-)\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{lex}}\,(\=\+{\rm{cons}}\,(($1\;+$ {\sc{n\$0}}\index{n\$0}) $-$ {\sc{i\$6}}\index{i\$6}, {\tt{'}}{\tt{nil}}), \\ 
{\rm{cons}}\,($1\;+$ ($1\;+$ ({\sc{n\$0}}\index{n\$0} $+$ {\sc{n\$0}}\index{n\$0})), {\tt{'}}{\tt{nil}}))\-\index{lex})\-\-
\end{tabbing}

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

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

\addvspace{18pt}

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

\begin{tabbing}{\sc Theorem}:  input-cond-of-zplus \\ \index{input-cond-of-zplus}
\=\+(\=\+($\neg$ {\rm{zneqp}}\,({\sc{cand\$6}}\index{cand\$6}, {\rm{elt1}}\,({\sc{a\$0}}\index{a\$0}, {\sc{i\$6}}\index{i\$6})\index{elt1})\index{zneqp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{i\$6}}\index{i\$6}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{k\$4}}\index{k\$4}, {\rm{zquotient}}\,({\sc{n\$0}}\index{n\$0}, {\tt{'}}{\tt{2}})\index{zquotient})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zeqp}}\,({\sc{k\$3}}\index{k\$3}, {\tt{'}}{\tt{0}})\index{zeqp}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\sc{i\$2}}\index{i\$2} \\ 
$\wedge$$\;\;\;\;$({\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp} $\wedge$ {\sc{global-hyps}}\index{global-hyps}))\-)\-)\-)\-)\- \\ 
$\rightarrow$$\;\;\;\;${\rm{expressible-znumberp}}\,({\rm{zplus}}\,({\sc{k\$6}}\index{k\$6}, {\tt{'}}{\tt{1}})\index{zplus})\index{expressible-znumberp}\-
\end{tabbing}

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

\end{verbatim}\begin{tabbing}{\sc Axiom}:  assignment5 \\ \index{assignment5}
\=\+({\sc{boole\$7}}\index{boole\$7} $=$ {\sc{boole\$6}}\index{boole\$6}) \\ 
$\wedge$$\;\;\;\;$(({\sc{cand\$7}}\index{cand\$7} $=$ {\sc{cand\$6}}\index{cand\$6}) $\wedge$ (({\sc{i\$7}}\index{i\$7} $=$ {\sc{i\$6}}\index{i\$6}) $\wedge$ ({\sc{k\$7}}\index{k\$7} $=$ {\rm{zplus}}\,({\sc{k\$6}}\index{k\$6}, {\tt{'}}{\tt{1}})\index{zplus})))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  input-cond-of-zquotient1 \\ \index{input-cond-of-zquotient1}
\=\+(\=\+($\neg$ {\rm{zneqp}}\,({\sc{cand\$6}}\index{cand\$6}, {\rm{elt1}}\,({\sc{a\$0}}\index{a\$0}, {\sc{i\$6}}\index{i\$6})\index{elt1})\index{zneqp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{i\$6}}\index{i\$6}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{k\$4}}\index{k\$4}, {\rm{zquotient}}\,({\sc{n\$0}}\index{n\$0}, {\tt{'}}{\tt{2}})\index{zquotient})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zeqp}}\,({\sc{k\$3}}\index{k\$3}, {\tt{'}}{\tt{0}})\index{zeqp}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\sc{i\$2}}\index{i\$2} \\ 
$\wedge$$\;\;\;\;$({\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\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{n\$0}}\index{n\$0}, {\tt{'}}{\tt{2}})\index{zquotient})\index{expressible-znumberp})\-
\end{tabbing}

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

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

\begin{tabbing}{\sc Theorem}:  output \\ \index{output}
\=\+(\=\+{\rm{zgreaterp}}\,({\sc{k\$7}}\index{k\$7}, {\rm{zquotient}}\,({\sc{n\$0}}\index{n\$0}, {\tt{'}}{\tt{2}})\index{zquotient})\index{zgreaterp} \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zneqp}}\,({\sc{cand\$6}}\index{cand\$6}, {\rm{elt1}}\,({\sc{a\$0}}\index{a\$0}, {\sc{i\$6}}\index{i\$6})\index{elt1})\index{zneqp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{i\$6}}\index{i\$6}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{k\$4}}\index{k\$4}, {\rm{zquotient}}\,({\sc{n\$0}}\index{n\$0}, {\tt{'}}{\tt{2}})\index{zquotient})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zeqp}}\,({\sc{k\$3}}\index{k\$3}, {\tt{'}}{\tt{0}})\index{zeqp}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\sc{i\$2}}\index{i\$2} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp} \\ 
$\wedge$$\;\;\;\;${\sc{global-hyps}}\index{global-hyps})\-)\-)\-)\-)\-)\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(({\sc{boole\$7}}\index{boole\$7} $=$ {\tt{'}}{\tt{*1*true}}) $\vee$ ({\sc{boole\$7}}\index{boole\$7} $=$ {\tt{'}}{\tt{*1*false}})) \\ 
$\wedge$$\;\;\;\;$\=\+{\bf if }{\sc{boole\$7}}\index{boole\$7} \\ 
{\bf then }\=\+{\rm{znumberp}}\,({\sc{cand\$7}}\index{cand\$7})\index{znumberp} \\ 
$\wedge$$\;\;\;\;$(({\sc{n\$0}}\index{n\$0} $\div$ {\tt{'}}{\tt{2}}) $<$ {\rm{cnt}}\,({\sc{cand\$7}}\index{cand\$7}, {\sc{a\$0}}\index{a\$0}, {\tt{'}}{\tt{1}}, {\sc{n\$0}}\index{n\$0})\index{cnt})\- \\ 
{\bf else }({\sc{n\$0}}\index{n\$0} $\div$ {\tt{'}}{\tt{2}}) $\not<$ {\rm{cnt}}\,({\it{x\/}}, {\sc{a\$0}}\index{a\$0}, {\tt{'}}{\tt{1}}, {\sc{n\$0}}\index{n\$0})\index{cnt}$\;${\bf  endif}\-)\-\-
\end{tabbing}

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

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

\addvspace{18pt}

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

\begin{tabbing}{\sc Theorem}:  phase2-invrt \\ \index{phase2-invrt}
\=\+(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{k\$7}}\index{k\$7}, {\rm{zquotient}}\,({\sc{n\$0}}\index{n\$0}, {\tt{'}}{\tt{2}})\index{zquotient})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zneqp}}\,({\sc{cand\$6}}\index{cand\$6}, {\rm{elt1}}\,({\sc{a\$0}}\index{a\$0}, {\sc{i\$6}}\index{i\$6})\index{elt1})\index{zneqp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{i\$6}}\index{i\$6}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{k\$4}}\index{k\$4}, {\rm{zquotient}}\,({\sc{n\$0}}\index{n\$0}, {\tt{'}}{\tt{2}})\index{zquotient})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zeqp}}\,({\sc{k\$3}}\index{k\$3}, {\tt{'}}{\tt{0}})\index{zeqp}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\sc{i\$2}}\index{i\$2} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp} \\ 
$\wedge$$\;\;\;\;${\sc{global-hyps}}\index{global-hyps})\-)\-)\-)\-)\-)\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+({\sc{i\$7}}\index{i\$7} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{i\$7}}\index{i\$7} $\not=$ {\tt{'}}{\tt{0}}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{boole\$7}}\index{boole\$7} $=$ {\tt{'}}{\tt{*1*true}}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{n\$0}}\index{n\$0} $\not<$ {\sc{i\$7}}\index{i\$7}) \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+($\neg$ {\rm{negativep}}\,({\sc{cand\$7}}\index{cand\$7})) \\ 
$\rightarrow$$\;\;\;\;$({\sc{cand\$7}}\index{cand\$7} $\in\;${\bf{N}}${}$))\- \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\rm{zneqp}}\,({\it{x\/}}, {\sc{cand\$7}}\index{cand\$7})\index{zneqp} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\sc{n\$0}}\index{n\$0} \\ 
$\not<$$\;\;\;\;$(\=\+{\tt{'}}{\tt{2}} \\ 
$*$$\;\;\;\;${\rm{cnt}}\,(\=\+{\it{x\/}}, \\ 
{\sc{a\$0}}\index{a\$0}, \\ 
{\tt{'}}{\tt{1}}, \\ 
{\sc{n\$0}}\index{n\$0})\-\index{cnt})\-)\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\sc{n\$0}}\index{n\$0} \\ 
$\not<$$\;\;\;\;$(\=\+{\tt{'}}{\tt{2}} \\ 
$*$$\;\;\;\;${\rm{cnt}}\,(\=\+{\sc{cand\$7}}\index{cand\$7}, \\ 
{\sc{a\$0}}\index{a\$0}, \\ 
{\tt{'}}{\tt{1}}, \\ 
{\sc{i\$7}}\index{i\$7})\-\index{cnt})\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\sc{k\$7}}\index{k\$7} \\ 
$=$$\;\;\;\;${\rm{cnt}}\,(\=\+{\sc{cand\$7}}\index{cand\$7}, \\ 
{\sc{a\$0}}\index{a\$0}, \\ 
{\tt{'}}{\tt{1}}, \\ 
{\sc{i\$7}}\index{i\$7})\-\index{cnt})\-)\-)\-)\-)\-)\-)\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{lex}}\,(\=\+{\rm{cons}}\,(($1\;+$ {\sc{n\$0}}\index{n\$0}) $-$ {\sc{i\$7}}\index{i\$7}, {\tt{'}}{\tt{nil}}), \\ 
{\rm{cons}}\,($1\;+$ ($1\;+$ ({\sc{n\$0}}\index{n\$0} $+$ {\sc{n\$0}}\index{n\$0})), {\tt{'}}{\tt{nil}}))\-\index{lex})\-\-
\end{tabbing}

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

\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{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}:  array-bounds-check-for-a \\ \index{array-bounds-check-for-a}
\=\+({\rm{zeqp}}\,({\sc{k\$2}}\index{k\$2}, {\tt{'}}{\tt{0}})\index{zeqp} $\wedge$ (($\neg$ {\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) $\wedge$ {\sc{global-hyps}}\index{global-hyps})) \\ 
$\rightarrow$$\;\;\;\;$(({\tt{'}}{\tt{0}} $<$ {\sc{i\$2}}\index{i\$2}) $\wedge$ ({\sc{n\$0}}\index{n\$0} $\not<$ {\sc{i\$2}}\index{i\$2}))\-
\end{tabbing}

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

\end{verbatim}\begin{tabbing}{\sc Theorem}:  definedness \\ \index{definedness}
\=\+({\rm{zeqp}}\,({\sc{k\$2}}\index{k\$2}, {\tt{'}}{\tt{0}})\index{zeqp} $\wedge$ (($\neg$ {\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) $\wedge$ {\sc{global-hyps}}\index{global-hyps})) \\ 
$\rightarrow$$\;\;\;\;${\rm{znumberp}}\,({\rm{elt1}}\,({\sc{a\$0}}\index{a\$0}, {\sc{i\$2}}\index{i\$2})\index{elt1})\index{znumberp}\-
\end{tabbing}

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

\end{verbatim}\begin{tabbing}{\sc Axiom}:  assignment2 \\ \index{assignment2}
\=\+({\sc{boole\$3}}\index{boole\$3} $=$ {\sc{boole\$2}}\index{boole\$2}) \\ 
$\wedge$$\;\;\;\;$(({\sc{cand\$3}}\index{cand\$3} $=$ {\rm{elt1}}\,({\sc{a\$0}}\index{a\$0}, {\sc{i\$2}}\index{i\$2})\index{elt1}) $\wedge$ (({\sc{i\$3}}\index{i\$3} $=$ {\sc{i\$2}}\index{i\$2}) $\wedge$ ({\sc{k\$3}}\index{k\$3} $=$ {\sc{k\$2}}\index{k\$2})))\-
\end{tabbing}

\begin{tabbing}{\sc Axiom}:  assignment3 \\ \index{assignment3}
\=\+({\sc{boole\$4}}\index{boole\$4} $=$ {\sc{boole\$3}}\index{boole\$3}) \\ 
$\wedge$$\;\;\;\;$(({\sc{cand\$4}}\index{cand\$4} $=$ {\sc{cand\$3}}\index{cand\$3}) $\wedge$ (({\sc{i\$4}}\index{i\$4} $=$ {\sc{i\$3}}\index{i\$3}) $\wedge$ ({\sc{k\$4}}\index{k\$4} $=$ {\tt{'}}{\tt{1}})))\-
\end{tabbing}

%\item 
\begin{verbatim}


(PROVE-LEMMA PHASE1-INVRT NIL
 (IMPLIES
  (AND (ZEQP (K$2) '0)
       (AND (NOT (ZGREATERP (I$2) (N$0)))
            (GLOBAL-HYPS)))
  (AND
   (AND
    (NUMBERP (I$4))
    (AND
     (NOT (EQUAL (I$4) '0))
     (AND
      (NUMBERP (K$4))
      (AND
       (NOT (LESSP (I$4) (K$4)))
       (AND
        (NOT (LESSP (N$0) (I$4)))
        (AND
         (IMPLIES (NOT (NEGATIVEP (CAND$4)))
                  (NUMBERP (CAND$4)))
         (AND
          (NOT (LESSP (CNT (CAND$4) (A$0) '1 (I$4))
                      (K$4)))
          (AND
           (IMPLIES
                  (ZEQP X (CAND$4))
                  (NOT (LESSP (PLUS (I$4) (K$4))
                              (TIMES '2 (CNT X (A$0) '1 (I$4))))))
           (IMPLIES
            (ZNEQP X (CAND$4))
            (NOT
             (LESSP
                   (I$4)
                   (PLUS (K$4)
                         (TIMES '2
                                (CNT X (A$0) '1 (I$4)))))))))))))))
   (LEX (CONS (ADD1 (PLUS (N$0)
                          (DIFFERENCE (ADD1 (N$0)) (I$4))))
              'NIL)
        (CONS (ADD1 (ADD1 (PLUS (N$0) (N$0))))
              'NIL)))))
\end{verbatim}


\begin{verbatim}#| (COMMENT INPUT F F 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}:  array-bounds-check-for-a \\ \index{array-bounds-check-for-a}
\=\+(($\neg$ {\rm{zeqp}}\,({\sc{k\$2}}\index{k\$2}, {\tt{'}}{\tt{0}})\index{zeqp}) $\wedge$ (($\neg$ {\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) $\wedge$ {\sc{global-hyps}}\index{global-hyps})) \\ 
$\rightarrow$$\;\;\;\;$(({\tt{'}}{\tt{0}} $<$ {\sc{i\$2}}\index{i\$2}) $\wedge$ ({\sc{n\$0}}\index{n\$0} $\not<$ {\sc{i\$2}}\index{i\$2}))\-
\end{tabbing}

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

\end{verbatim}\begin{tabbing}{\sc Theorem}:  definedness \\ \index{definedness}
\=\+(($\neg$ {\rm{zeqp}}\,({\sc{k\$2}}\index{k\$2}, {\tt{'}}{\tt{0}})\index{zeqp}) $\wedge$ (($\neg$ {\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) $\wedge$ {\sc{global-hyps}}\index{global-hyps})) \\ 
$\rightarrow$$\;\;\;\;${\rm{znumberp}}\,({\sc{cand\$2}}\index{cand\$2})\index{znumberp}\-
\end{tabbing}

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

\end{verbatim}\begin{tabbing}{\sc Theorem}:  definedness1 \\ \index{definedness1}
\=\+(($\neg$ {\rm{zeqp}}\,({\sc{k\$2}}\index{k\$2}, {\tt{'}}{\tt{0}})\index{zeqp}) $\wedge$ (($\neg$ {\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) $\wedge$ {\sc{global-hyps}}\index{global-hyps})) \\ 
$\rightarrow$$\;\;\;\;${\rm{znumberp}}\,({\rm{elt1}}\,({\sc{a\$0}}\index{a\$0}, {\sc{i\$2}}\index{i\$2})\index{elt1})\index{znumberp}\-
\end{tabbing}

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

; (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-zplus \\ \index{input-cond-of-zplus}
\=\+(\=\+{\rm{zeqp}}\,({\sc{cand\$2}}\index{cand\$2}, {\rm{elt1}}\,({\sc{a\$0}}\index{a\$0}, {\sc{i\$2}}\index{i\$2})\index{elt1})\index{zeqp} \\ 
$\wedge$$\;\;\;\;$(($\neg$ {\rm{zeqp}}\,({\sc{k\$2}}\index{k\$2}, {\tt{'}}{\tt{0}})\index{zeqp}) $\wedge$ (($\neg$ {\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) $\wedge$ {\sc{global-hyps}}\index{global-hyps})))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{expressible-znumberp}}\,({\rm{zplus}}\,({\sc{k\$2}}\index{k\$2}, {\tt{'}}{\tt{1}})\index{zplus})\index{expressible-znumberp}\-
\end{tabbing}

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

\end{verbatim}\begin{tabbing}{\sc Axiom}:  assignment2 \\ \index{assignment2}
\=\+({\sc{boole\$3}}\index{boole\$3} $=$ {\sc{boole\$2}}\index{boole\$2}) \\ 
$\wedge$$\;\;\;\;$(({\sc{cand\$3}}\index{cand\$3} $=$ {\sc{cand\$2}}\index{cand\$2}) $\wedge$ (({\sc{i\$3}}\index{i\$3} $=$ {\sc{i\$2}}\index{i\$2}) $\wedge$ ({\sc{k\$3}}\index{k\$3} $=$ {\rm{zplus}}\,({\sc{k\$2}}\index{k\$2}, {\tt{'}}{\tt{1}})\index{zplus})))\-
\end{tabbing}

%\item 
\begin{verbatim}


(PROVE-LEMMA PHASE1-INVRT NIL
 (IMPLIES
  (AND (ZEQP (CAND$2) (ELT1 (A$0) (I$2)))
       (AND (NOT (ZEQP (K$2) '0))
            (AND (NOT (ZGREATERP (I$2) (N$0)))
                 (GLOBAL-HYPS))))
  (AND
   (AND
    (NUMBERP (I$3))
    (AND
     (NOT (EQUAL (I$3) '0))
     (AND
      (NUMBERP (K$3))
      (AND
       (NOT (LESSP (I$3) (K$3)))
       (AND
        (NOT (LESSP (N$0) (I$3)))
        (AND
         (IMPLIES (NOT (NEGATIVEP (CAND$3)))
                  (NUMBERP (CAND$3)))
         (AND
          (NOT (LESSP (CNT (CAND$3) (A$0) '1 (I$3))
                      (K$3)))
          (AND
           (IMPLIES
                  (ZEQP X (CAND$3))
                  (NOT (LESSP (PLUS (I$3) (K$3))
                              (TIMES '2 (CNT X (A$0) '1 (I$3))))))
           (IMPLIES
            (ZNEQP X (CAND$3))
            (NOT
             (LESSP
                   (I$3)
                   (PLUS (K$3)
                         (TIMES '2
                                (CNT X (A$0) '1 (I$3)))))))))))))))
   (LEX (CONS (ADD1 (PLUS (N$0)
                          (DIFFERENCE (ADD1 (N$0)) (I$3))))
              'NIL)
        (CONS (ADD1 (ADD1 (PLUS (N$0) (N$0))))
              'NIL)))))
\end{verbatim}


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

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

\addvspace{18pt}

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

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

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

\end{verbatim}\begin{tabbing}{\sc Axiom}:  assignment2 \\ \index{assignment2}
\=\+({\sc{boole\$3}}\index{boole\$3} $=$ {\sc{boole\$2}}\index{boole\$2}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{cand\$3}}\index{cand\$3} $=$ {\sc{cand\$2}}\index{cand\$2}) \\ 
$\wedge$$\;\;\;\;$(({\sc{i\$3}}\index{i\$3} $=$ {\sc{i\$2}}\index{i\$2}) $\wedge$ ({\sc{k\$3}}\index{k\$3} $=$ {\rm{zdifference}}\,({\sc{k\$2}}\index{k\$2}, {\tt{'}}{\tt{1}})\index{zdifference})))\-\-
\end{tabbing}

%\item 
\begin{verbatim}


(PROVE-LEMMA PHASE1-INVRT NIL
 (IMPLIES
  (AND (NOT (ZEQP (CAND$2) (ELT1 (A$0) (I$2))))
       (AND (NOT (ZEQP (K$2) '0))
            (AND (NOT (ZGREATERP (I$2) (N$0)))
                 (GLOBAL-HYPS))))
  (AND
   (AND
    (NUMBERP (I$3))
    (AND
     (NOT (EQUAL (I$3) '0))
     (AND
      (NUMBERP (K$3))
      (AND
       (NOT (LESSP (I$3) (K$3)))
       (AND
        (NOT (LESSP (N$0) (I$3)))
        (AND
         (IMPLIES (NOT (NEGATIVEP (CAND$3)))
                  (NUMBERP (CAND$3)))
         (AND
          (NOT (LESSP (CNT (CAND$3) (A$0) '1 (I$3))
                      (K$3)))
          (AND
           (IMPLIES
                  (ZEQP X (CAND$3))
                  (NOT (LESSP (PLUS (I$3) (K$3))
                              (TIMES '2 (CNT X (A$0) '1 (I$3))))))
           (IMPLIES
            (ZNEQP X (CAND$3))
            (NOT
             (LESSP
                   (I$3)
                   (PLUS (K$3)
                         (TIMES '2
                                (CNT X (A$0) '1 (I$3)))))))))))))))
   (LEX (CONS (ADD1 (PLUS (N$0)
                          (DIFFERENCE (ADD1 (N$0)) (I$3))))
              'NIL)
        (CONS (ADD1 (ADD1 (PLUS (N$0) (N$0))))
              'NIL)))))
\end{verbatim}


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

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

\addvspace{18pt}

\begin{tabbing}{\sc Axiom}:  paths-from-phase1-invrt \\ \index{paths-from-phase1-invrt}
\=\+({\rm{zeqp}}\,({\it{x\/}}, {\sc{cand\$1}}\index{cand\$1})\index{zeqp} $\rightarrow$ (({\sc{i\$1}}\index{i\$1} $+$ {\sc{k\$1}}\index{k\$1}) $\not<$ ({\tt{'}}{\tt{2}} $*$ {\rm{cnt}}\,({\it{x\/}}, {\sc{a\$0}}\index{a\$0}, {\tt{'}}{\tt{1}}, {\sc{i\$1}}\index{i\$1})\index{cnt}))) \\ 
$\wedge$$\;\;\;\;$({\rm{zneqp}}\,({\it{x\/}}, {\sc{cand\$1}}\index{cand\$1})\index{zneqp} $\rightarrow$ ({\sc{i\$1}}\index{i\$1} $\not<$ ({\sc{k\$1}}\index{k\$1} $+$ ({\tt{'}}{\tt{2}} $*$ {\rm{cnt}}\,({\it{x\/}}, {\sc{a\$0}}\index{a\$0}, {\tt{'}}{\tt{1}}, {\sc{i\$1}}\index{i\$1})\index{cnt}))))\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{path-hyps} \\  
\=\+{\sc{path-hyps}}\index{path-hyps} \\ 
$=$$\;\;\;\;$(\=\+{\sc{global-hyps}}\index{global-hyps} \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{i\$1}}\index{i\$1} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{i\$1}}\index{i\$1} $\not=$ {\tt{'}}{\tt{0}}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{k\$1}}\index{k\$1} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{i\$1}}\index{i\$1} $\not<$ {\sc{k\$1}}\index{k\$1}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{n\$0}}\index{n\$0} $\not<$ {\sc{i\$1}}\index{i\$1}) \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+($\neg$ {\rm{negativep}}\,({\sc{cand\$1}}\index{cand\$1})) \\ 
$\rightarrow$$\;\;\;\;$({\sc{cand\$1}}\index{cand\$1} $\in\;${\bf{N}}${}$))\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{cnt}}\,(\=\+{\sc{cand\$1}}\index{cand\$1}, \\ 
{\sc{a\$0}}\index{a\$0}, \\ 
{\tt{'}}{\tt{1}}, \\ 
{\sc{i\$1}}\index{i\$1})\-\index{cnt} \\ 
$\not<$$\;\;\;\;${\sc{k\$1}}\index{k\$1})\-)\-)\-)\-)\-)\-)\-)\-\-
\end{tabbing}

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

\begin{verbatim}#| (COMMENT PHASE1-INVRT) |#

\end{verbatim}\begin{tabbing}{\sc Theorem}:  input-cond-of-zplus \\ \index{input-cond-of-zplus}
{\sc{path-hyps}}\index{path-hyps} $\rightarrow$ {\rm{expressible-znumberp}}\,({\rm{zplus}}\,({\sc{i\$1}}\index{i\$1}, {\tt{'}}{\tt{1}})\index{zplus})\index{expressible-znumberp}
\end{tabbing}

\begin{verbatim}#| (COMMENT PHASE1-INVRT) |#

\end{verbatim}\begin{tabbing}{\sc Axiom}:  assignment3 \\ \index{assignment3}
\=\+({\sc{boole\$2}}\index{boole\$2} $=$ {\sc{boole\$1}}\index{boole\$1}) \\ 
$\wedge$$\;\;\;\;$(({\sc{cand\$2}}\index{cand\$2} $=$ {\sc{cand\$1}}\index{cand\$1}) $\wedge$ (({\sc{i\$2}}\index{i\$2} $=$ {\rm{zplus}}\,({\sc{i\$1}}\index{i\$1}, {\tt{'}}{\tt{1}})\index{zplus}) $\wedge$ ({\sc{k\$2}}\index{k\$2} $=$ {\sc{k\$1}}\index{k\$1})))\-
\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 Axiom}:  effects-of-undefiner \\ \index{effects-of-undefiner}
({\sc{boole\$3}}\index{boole\$3} $=$ {\sc{boole\$2}}\index{boole\$2}) $\wedge$ (({\sc{cand\$3}}\index{cand\$3} $=$ {\sc{cand\$2}}\index{cand\$2}) $\wedge$ ({\sc{k\$3}}\index{k\$3} $=$ {\sc{k\$2}}\index{k\$2}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  definedness3 \\ \index{definedness3}
({\sc{i\$2}}\index{i\$2} $\wedge$ ({\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp} $\wedge$ {\sc{path-hyps}}\index{path-hyps})) $\rightarrow$ {\rm{znumberp}}\,({\sc{k\$3}}\index{k\$3})\index{znumberp}
\end{tabbing}

\begin{verbatim}#| (COMMENT PHASE1-INVRT T) |#

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

\begin{tabbing}{\sc Axiom}:  assignment4 \\ \index{assignment4}
\=\+({\sc{boole\$4}}\index{boole\$4} $=$ {\tt{'}}{\tt{*1*false}}) \\ 
$\wedge$$\;\;\;\;$(({\sc{cand\$4}}\index{cand\$4} $=$ {\sc{cand\$3}}\index{cand\$3}) $\wedge$ (({\sc{i\$4}}\index{i\$4} $=$ {\sc{i\$3}}\index{i\$3}) $\wedge$ ({\sc{k\$4}}\index{k\$4} $=$ {\sc{k\$3}}\index{k\$3})))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  compound-invrt \\ \index{compound-invrt}
({\sc{k\$1}}\index{k\$1} $=$ {\tt{0}}) $\rightarrow$ ({\sc{i\$1}}\index{i\$1} $\not<$ ({\tt{2}} $*$ {\rm{cnt}}\,({\it{x\/}}, {\sc{a\$0}}\index{a\$0}, {\tt{1}}, {\sc{i\$1}}\index{i\$1})\index{cnt}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  output \\ \index{output}
\=\+({\rm{zeqp}}\,({\sc{k\$3}}\index{k\$3}, {\tt{'}}{\tt{0}})\index{zeqp} $\wedge$ ({\sc{i\$2}}\index{i\$2} $\wedge$ ({\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp} $\wedge$ {\sc{path-hyps}}\index{path-hyps}))) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(({\sc{boole\$4}}\index{boole\$4} $=$ {\tt{'}}{\tt{*1*true}}) $\vee$ ({\sc{boole\$4}}\index{boole\$4} $=$ {\tt{'}}{\tt{*1*false}})) \\ 
$\wedge$$\;\;\;\;$\=\+{\bf if }{\sc{boole\$4}}\index{boole\$4} \\ 
{\bf then }\=\+{\rm{znumberp}}\,({\sc{cand\$4}}\index{cand\$4})\index{znumberp} \\ 
$\wedge$$\;\;\;\;$(({\sc{n\$0}}\index{n\$0} $\div$ {\tt{'}}{\tt{2}}) $<$ {\rm{cnt}}\,({\sc{cand\$4}}\index{cand\$4}, {\sc{a\$0}}\index{a\$0}, {\tt{'}}{\tt{1}}, {\sc{n\$0}}\index{n\$0})\index{cnt})\- \\ 
{\bf else }({\sc{n\$0}}\index{n\$0} $\div$ {\tt{'}}{\tt{2}}) $\not<$ {\rm{cnt}}\,({\it{x\/}}, {\sc{a\$0}}\index{a\$0}, {\tt{'}}{\tt{1}}, {\sc{n\$0}}\index{n\$0})\index{cnt}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{verbatim}#| (COMMENT PHASE1-INVRT T T) |#

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

\addvspace{18pt}

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

\begin{tabbing}{\sc Axiom}:  assignment4 \\ \index{assignment4}
\=\+({\sc{boole\$4}}\index{boole\$4} $=$ {\tt{'}}{\tt{*1*true}}) \\ 
$\wedge$$\;\;\;\;$(({\sc{cand\$4}}\index{cand\$4} $=$ {\sc{cand\$3}}\index{cand\$3}) $\wedge$ (({\sc{i\$4}}\index{i\$4} $=$ {\sc{i\$3}}\index{i\$3}) $\wedge$ ({\sc{k\$4}}\index{k\$4} $=$ {\sc{k\$3}}\index{k\$3})))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  input-cond-of-zquotient \\ \index{input-cond-of-zquotient}
\=\+(($\neg$ {\rm{zeqp}}\,({\sc{k\$3}}\index{k\$3}, {\tt{'}}{\tt{0}})\index{zeqp}) $\wedge$ ({\sc{i\$2}}\index{i\$2} $\wedge$ ({\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp} $\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}}\,({\sc{n\$0}}\index{n\$0}, {\tt{'}}{\tt{2}})\index{zquotient})\index{expressible-znumberp})\-
\end{tabbing}

\begin{verbatim}#| (COMMENT PHASE1-INVRT T F) |#

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

\begin{tabbing}{\sc Theorem}:  output \\ \index{output}
\=\+(\=\+{\rm{zgreaterp}}\,({\sc{k\$4}}\index{k\$4}, {\rm{zquotient}}\,({\sc{n\$0}}\index{n\$0}, {\tt{'}}{\tt{2}})\index{zquotient})\index{zgreaterp} \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zeqp}}\,({\sc{k\$3}}\index{k\$3}, {\tt{'}}{\tt{0}})\index{zeqp}) \\ 
$\wedge$$\;\;\;\;$({\sc{i\$2}}\index{i\$2} $\wedge$ ({\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp} $\wedge$ {\sc{path-hyps}}\index{path-hyps})))\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(({\sc{boole\$4}}\index{boole\$4} $=$ {\tt{'}}{\tt{*1*true}}) $\vee$ ({\sc{boole\$4}}\index{boole\$4} $=$ {\tt{'}}{\tt{*1*false}})) \\ 
$\wedge$$\;\;\;\;$\=\+{\bf if }{\sc{boole\$4}}\index{boole\$4} \\ 
{\bf then }\=\+{\rm{znumberp}}\,({\sc{cand\$4}}\index{cand\$4})\index{znumberp} \\ 
$\wedge$$\;\;\;\;$(({\sc{n\$0}}\index{n\$0} $\div$ {\tt{'}}{\tt{2}}) $<$ {\rm{cnt}}\,({\sc{cand\$4}}\index{cand\$4}, {\sc{a\$0}}\index{a\$0}, {\tt{'}}{\tt{1}}, {\sc{n\$0}}\index{n\$0})\index{cnt})\- \\ 
{\bf else }({\sc{n\$0}}\index{n\$0} $\div$ {\tt{'}}{\tt{2}}) $\not<$ {\rm{cnt}}\,({\it{x\/}}, {\sc{a\$0}}\index{a\$0}, {\tt{'}}{\tt{1}}, {\sc{n\$0}}\index{n\$0})\index{cnt}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{verbatim}#| (COMMENT PHASE1-INVRT T F T) |#

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

\addvspace{18pt}

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

\begin{tabbing}{\sc Axiom}:  assignment5 \\ \index{assignment5}
\=\+({\sc{boole\$5}}\index{boole\$5} $=$ {\sc{boole\$4}}\index{boole\$4}) \\ 
$\wedge$$\;\;\;\;$(({\sc{cand\$5}}\index{cand\$5} $=$ {\sc{cand\$4}}\index{cand\$4}) $\wedge$ (({\sc{i\$5}}\index{i\$5} $=$ {\sc{i\$4}}\index{i\$4}) $\wedge$ ({\sc{k\$5}}\index{k\$5} $=$ {\tt{'}}{\tt{0}})))\-
\end{tabbing}

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

\begin{tabbing}{\sc Axiom}:  assignment6 \\ \index{assignment6}
\=\+({\sc{boole\$6}}\index{boole\$6} $=$ {\sc{boole\$5}}\index{boole\$5}) \\ 
$\wedge$$\;\;\;\;$(({\sc{cand\$6}}\index{cand\$6} $=$ {\sc{cand\$5}}\index{cand\$5}) $\wedge$ (({\sc{i\$6}}\index{i\$6} $=$ {\tt{'}}{\tt{1}}) $\wedge$ ({\sc{k\$6}}\index{k\$6} $=$ {\sc{k\$5}}\index{k\$5})))\-
\end{tabbing}

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

\begin{tabbing}{\sc Axiom}:  effects-of-undefiner1 \\ \index{effects-of-undefiner1}
({\sc{boole\$7}}\index{boole\$7} $=$ {\sc{boole\$6}}\index{boole\$6}) $\wedge$ (({\sc{cand\$7}}\index{cand\$7} $=$ {\sc{cand\$6}}\index{cand\$6}) $\wedge$ ({\sc{k\$7}}\index{k\$7} $=$ {\sc{k\$6}}\index{k\$6}))
\end{tabbing}

\begin{tabbing}{\sc Axiom}:  assignment7 \\ \index{assignment7}
\=\+({\sc{boole\$8}}\index{boole\$8} $=$ {\tt{'}}{\tt{*1*false}}) \\ 
$\wedge$$\;\;\;\;$(({\sc{cand\$8}}\index{cand\$8} $=$ {\sc{cand\$7}}\index{cand\$7}) $\wedge$ (({\sc{i\$8}}\index{i\$8} $=$ {\sc{i\$7}}\index{i\$7}) $\wedge$ ({\sc{k\$8}}\index{k\$8} $=$ {\sc{k\$7}}\index{k\$7})))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  output \\ \index{output}
\=\+(\=\+{\sc{i\$6}}\index{i\$6} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{zgreaterp}}\,({\sc{i\$6}}\index{i\$6}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp} \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{k\$4}}\index{k\$4}, {\rm{zquotient}}\,({\sc{n\$0}}\index{n\$0}, {\tt{'}}{\tt{2}})\index{zquotient})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zeqp}}\,({\sc{k\$3}}\index{k\$3}, {\tt{'}}{\tt{0}})\index{zeqp}) \\ 
$\wedge$$\;\;\;\;$({\sc{i\$2}}\index{i\$2} $\wedge$ ({\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp} $\wedge$ {\sc{path-hyps}}\index{path-hyps})))\-)\-)\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(({\sc{boole\$8}}\index{boole\$8} $=$ {\tt{'}}{\tt{*1*true}}) $\vee$ ({\sc{boole\$8}}\index{boole\$8} $=$ {\tt{'}}{\tt{*1*false}})) \\ 
$\wedge$$\;\;\;\;$\=\+{\bf if }{\sc{boole\$8}}\index{boole\$8} \\ 
{\bf then }\=\+{\rm{znumberp}}\,({\sc{cand\$8}}\index{cand\$8})\index{znumberp} \\ 
$\wedge$$\;\;\;\;$(({\sc{n\$0}}\index{n\$0} $\div$ {\tt{'}}{\tt{2}}) $<$ {\rm{cnt}}\,({\sc{cand\$8}}\index{cand\$8}, {\sc{a\$0}}\index{a\$0}, {\tt{'}}{\tt{1}}, {\sc{n\$0}}\index{n\$0})\index{cnt})\- \\ 
{\bf else }({\sc{n\$0}}\index{n\$0} $\div$ {\tt{'}}{\tt{2}}) $\not<$ {\rm{cnt}}\,({\it{x\/}}, {\sc{a\$0}}\index{a\$0}, {\tt{'}}{\tt{1}}, {\sc{n\$0}}\index{n\$0})\index{cnt}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{verbatim}#| (COMMENT PHASE1-INVRT T F F F T) |#

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

\addvspace{18pt}

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

\begin{tabbing}{\sc Theorem}:  array-bounds-check-for-a1 \\ \index{array-bounds-check-for-a1}
\=\+(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{i\$6}}\index{i\$6}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{k\$4}}\index{k\$4}, {\rm{zquotient}}\,({\sc{n\$0}}\index{n\$0}, {\tt{'}}{\tt{2}})\index{zquotient})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zeqp}}\,({\sc{k\$3}}\index{k\$3}, {\tt{'}}{\tt{0}})\index{zeqp}) \\ 
$\wedge$$\;\;\;\;$({\sc{i\$2}}\index{i\$2} $\wedge$ ({\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp} $\wedge$ {\sc{path-hyps}}\index{path-hyps})))\-)\-)\- \\ 
$\rightarrow$$\;\;\;\;$(({\tt{'}}{\tt{0}} $<$ {\sc{i\$6}}\index{i\$6}) $\wedge$ ({\sc{n\$0}}\index{n\$0} $\not<$ {\sc{i\$6}}\index{i\$6}))\-
\end{tabbing}

\begin{verbatim}#| (COMMENT PHASE1-INVRT T F F F F) |#

\end{verbatim}\begin{tabbing}{\sc Theorem}:  definedness4 \\ \index{definedness4}
\=\+(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{i\$6}}\index{i\$6}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{k\$4}}\index{k\$4}, {\rm{zquotient}}\,({\sc{n\$0}}\index{n\$0}, {\tt{'}}{\tt{2}})\index{zquotient})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zeqp}}\,({\sc{k\$3}}\index{k\$3}, {\tt{'}}{\tt{0}})\index{zeqp}) \\ 
$\wedge$$\;\;\;\;$({\sc{i\$2}}\index{i\$2} $\wedge$ ({\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp} $\wedge$ {\sc{path-hyps}}\index{path-hyps})))\-)\-)\- \\ 
$\rightarrow$$\;\;\;\;${\rm{znumberp}}\,({\sc{cand\$6}}\index{cand\$6})\index{znumberp}\-
\end{tabbing}

\begin{verbatim}#| (COMMENT PHASE1-INVRT T F F F F) |#

\end{verbatim}\begin{tabbing}{\sc Theorem}:  definedness5 \\ \index{definedness5}
\=\+(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{i\$6}}\index{i\$6}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{k\$4}}\index{k\$4}, {\rm{zquotient}}\,({\sc{n\$0}}\index{n\$0}, {\tt{'}}{\tt{2}})\index{zquotient})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zeqp}}\,({\sc{k\$3}}\index{k\$3}, {\tt{'}}{\tt{0}})\index{zeqp}) \\ 
$\wedge$$\;\;\;\;$({\sc{i\$2}}\index{i\$2} $\wedge$ ({\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp} $\wedge$ {\sc{path-hyps}}\index{path-hyps})))\-)\-)\- \\ 
$\rightarrow$$\;\;\;\;${\rm{znumberp}}\,({\rm{elt1}}\,({\sc{a\$0}}\index{a\$0}, {\sc{i\$6}}\index{i\$6})\index{elt1})\index{znumberp}\-
\end{tabbing}

\begin{verbatim}#| (COMMENT PHASE1-INVRT T F F F F) |#

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

\begin{tabbing}{\sc Theorem}:  phase2-invrt \\ \index{phase2-invrt}
\=\+(\=\+{\rm{zneqp}}\,({\sc{cand\$6}}\index{cand\$6}, {\rm{elt1}}\,({\sc{a\$0}}\index{a\$0}, {\sc{i\$6}}\index{i\$6})\index{elt1})\index{zneqp} \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{i\$6}}\index{i\$6}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{k\$4}}\index{k\$4}, {\rm{zquotient}}\,({\sc{n\$0}}\index{n\$0}, {\tt{'}}{\tt{2}})\index{zquotient})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zeqp}}\,({\sc{k\$3}}\index{k\$3}, {\tt{'}}{\tt{0}})\index{zeqp}) \\ 
$\wedge$$\;\;\;\;$({\sc{i\$2}}\index{i\$2} $\wedge$ ({\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp} $\wedge$ {\sc{path-hyps}}\index{path-hyps})))\-)\-)\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+({\sc{i\$6}}\index{i\$6} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{i\$6}}\index{i\$6} $\not=$ {\tt{'}}{\tt{0}}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{boole\$6}}\index{boole\$6} $=$ {\tt{'}}{\tt{*1*true}}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{n\$0}}\index{n\$0} $\not<$ {\sc{i\$6}}\index{i\$6}) \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+($\neg$ {\rm{negativep}}\,({\sc{cand\$6}}\index{cand\$6})) \\ 
$\rightarrow$$\;\;\;\;$({\sc{cand\$6}}\index{cand\$6} $\in\;${\bf{N}}${}$))\- \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\rm{zneqp}}\,({\it{x\/}}, {\sc{cand\$6}}\index{cand\$6})\index{zneqp} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\sc{n\$0}}\index{n\$0} \\ 
$\not<$$\;\;\;\;$(\=\+{\tt{'}}{\tt{2}} \\ 
$*$$\;\;\;\;${\rm{cnt}}\,(\=\+{\it{x\/}}, \\ 
{\sc{a\$0}}\index{a\$0}, \\ 
{\tt{'}}{\tt{1}}, \\ 
{\sc{n\$0}}\index{n\$0})\-\index{cnt})\-)\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\sc{n\$0}}\index{n\$0} \\ 
$\not<$$\;\;\;\;$(\=\+{\tt{'}}{\tt{2}} \\ 
$*$$\;\;\;\;${\rm{cnt}}\,(\=\+{\sc{cand\$6}}\index{cand\$6}, \\ 
{\sc{a\$0}}\index{a\$0}, \\ 
{\tt{'}}{\tt{1}}, \\ 
{\sc{i\$6}}\index{i\$6})\-\index{cnt})\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\sc{k\$6}}\index{k\$6} \\ 
$=$$\;\;\;\;${\rm{cnt}}\,(\=\+{\sc{cand\$6}}\index{cand\$6}, \\ 
{\sc{a\$0}}\index{a\$0}, \\ 
{\tt{'}}{\tt{1}}, \\ 
{\sc{i\$6}}\index{i\$6})\-\index{cnt})\-)\-)\-)\-)\-)\-)\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{lex}}\,(\=\+{\rm{cons}}\,(($1\;+$ {\sc{n\$0}}\index{n\$0}) $-$ {\sc{i\$6}}\index{i\$6}, {\tt{'}}{\tt{nil}}), \\ 
{\rm{cons}}\,($1\;+$ ({\sc{n\$0}}\index{n\$0} $+$ (($1\;+$ {\sc{n\$0}}\index{n\$0}) $-$ {\sc{i\$1}}\index{i\$1})), {\tt{'}}{\tt{nil}}))\-\index{lex})\-\-
\end{tabbing}

\begin{verbatim}#| (COMMENT PHASE1-INVRT T F F F F T) |#

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

\addvspace{18pt}

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

\begin{tabbing}{\sc Theorem}:  input-cond-of-zplus1 \\ \index{input-cond-of-zplus1}
\=\+(\=\+($\neg$ {\rm{zneqp}}\,({\sc{cand\$6}}\index{cand\$6}, {\rm{elt1}}\,({\sc{a\$0}}\index{a\$0}, {\sc{i\$6}}\index{i\$6})\index{elt1})\index{zneqp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{i\$6}}\index{i\$6}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{k\$4}}\index{k\$4}, {\rm{zquotient}}\,({\sc{n\$0}}\index{n\$0}, {\tt{'}}{\tt{2}})\index{zquotient})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zeqp}}\,({\sc{k\$3}}\index{k\$3}, {\tt{'}}{\tt{0}})\index{zeqp}) \\ 
$\wedge$$\;\;\;\;$({\sc{i\$2}}\index{i\$2} $\wedge$ ({\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp} $\wedge$ {\sc{path-hyps}}\index{path-hyps})))\-)\-)\-)\- \\ 
$\rightarrow$$\;\;\;\;${\rm{expressible-znumberp}}\,({\rm{zplus}}\,({\sc{k\$6}}\index{k\$6}, {\tt{'}}{\tt{1}})\index{zplus})\index{expressible-znumberp}\-
\end{tabbing}

\begin{verbatim}#| (COMMENT PHASE1-INVRT T F F F F F) |#

\end{verbatim}\begin{tabbing}{\sc Axiom}:  assignment7 \\ \index{assignment7}
\=\+({\sc{boole\$7}}\index{boole\$7} $=$ {\sc{boole\$6}}\index{boole\$6}) \\ 
$\wedge$$\;\;\;\;$(({\sc{cand\$7}}\index{cand\$7} $=$ {\sc{cand\$6}}\index{cand\$6}) $\wedge$ (({\sc{i\$7}}\index{i\$7} $=$ {\sc{i\$6}}\index{i\$6}) $\wedge$ ({\sc{k\$7}}\index{k\$7} $=$ {\rm{zplus}}\,({\sc{k\$6}}\index{k\$6}, {\tt{'}}{\tt{1}})\index{zplus})))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  input-cond-of-zquotient1 \\ \index{input-cond-of-zquotient1}
\=\+(\=\+($\neg$ {\rm{zneqp}}\,({\sc{cand\$6}}\index{cand\$6}, {\rm{elt1}}\,({\sc{a\$0}}\index{a\$0}, {\sc{i\$6}}\index{i\$6})\index{elt1})\index{zneqp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{i\$6}}\index{i\$6}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{k\$4}}\index{k\$4}, {\rm{zquotient}}\,({\sc{n\$0}}\index{n\$0}, {\tt{'}}{\tt{2}})\index{zquotient})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zeqp}}\,({\sc{k\$3}}\index{k\$3}, {\tt{'}}{\tt{0}})\index{zeqp}) \\ 
$\wedge$$\;\;\;\;$({\sc{i\$2}}\index{i\$2} $\wedge$ ({\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp} $\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}}\,({\sc{n\$0}}\index{n\$0}, {\tt{'}}{\tt{2}})\index{zquotient})\index{expressible-znumberp})\-
\end{tabbing}

\begin{verbatim}#| (COMMENT PHASE1-INVRT T F F F F F) |#

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

\begin{tabbing}{\sc Theorem}:  output \\ \index{output}
\=\+(\=\+{\rm{zgreaterp}}\,({\sc{k\$7}}\index{k\$7}, {\rm{zquotient}}\,({\sc{n\$0}}\index{n\$0}, {\tt{'}}{\tt{2}})\index{zquotient})\index{zgreaterp} \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zneqp}}\,({\sc{cand\$6}}\index{cand\$6}, {\rm{elt1}}\,({\sc{a\$0}}\index{a\$0}, {\sc{i\$6}}\index{i\$6})\index{elt1})\index{zneqp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{i\$6}}\index{i\$6}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{k\$4}}\index{k\$4}, {\rm{zquotient}}\,({\sc{n\$0}}\index{n\$0}, {\tt{'}}{\tt{2}})\index{zquotient})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zeqp}}\,({\sc{k\$3}}\index{k\$3}, {\tt{'}}{\tt{0}})\index{zeqp}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\sc{i\$2}}\index{i\$2} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp} \\ 
$\wedge$$\;\;\;\;${\sc{path-hyps}}\index{path-hyps})\-)\-)\-)\-)\-)\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(({\sc{boole\$7}}\index{boole\$7} $=$ {\tt{'}}{\tt{*1*true}}) $\vee$ ({\sc{boole\$7}}\index{boole\$7} $=$ {\tt{'}}{\tt{*1*false}})) \\ 
$\wedge$$\;\;\;\;$\=\+{\bf if }{\sc{boole\$7}}\index{boole\$7} \\ 
{\bf then }\=\+{\rm{znumberp}}\,({\sc{cand\$7}}\index{cand\$7})\index{znumberp} \\ 
$\wedge$$\;\;\;\;$(({\sc{n\$0}}\index{n\$0} $\div$ {\tt{'}}{\tt{2}}) $<$ {\rm{cnt}}\,({\sc{cand\$7}}\index{cand\$7}, {\sc{a\$0}}\index{a\$0}, {\tt{'}}{\tt{1}}, {\sc{n\$0}}\index{n\$0})\index{cnt})\- \\ 
{\bf else }({\sc{n\$0}}\index{n\$0} $\div$ {\tt{'}}{\tt{2}}) $\not<$ {\rm{cnt}}\,({\it{x\/}}, {\sc{a\$0}}\index{a\$0}, {\tt{'}}{\tt{1}}, {\sc{n\$0}}\index{n\$0})\index{cnt}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{verbatim}#| (COMMENT PHASE1-INVRT T F F F F F T) |#

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

\addvspace{18pt}

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

\begin{tabbing}{\sc Theorem}:  phase2-invrt \\ \index{phase2-invrt}
\=\+(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{k\$7}}\index{k\$7}, {\rm{zquotient}}\,({\sc{n\$0}}\index{n\$0}, {\tt{'}}{\tt{2}})\index{zquotient})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zneqp}}\,({\sc{cand\$6}}\index{cand\$6}, {\rm{elt1}}\,({\sc{a\$0}}\index{a\$0}, {\sc{i\$6}}\index{i\$6})\index{elt1})\index{zneqp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{i\$6}}\index{i\$6}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{k\$4}}\index{k\$4}, {\rm{zquotient}}\,({\sc{n\$0}}\index{n\$0}, {\tt{'}}{\tt{2}})\index{zquotient})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zeqp}}\,({\sc{k\$3}}\index{k\$3}, {\tt{'}}{\tt{0}})\index{zeqp}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\sc{i\$2}}\index{i\$2} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp} \\ 
$\wedge$$\;\;\;\;${\sc{path-hyps}}\index{path-hyps})\-)\-)\-)\-)\-)\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+({\sc{i\$7}}\index{i\$7} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{i\$7}}\index{i\$7} $\not=$ {\tt{'}}{\tt{0}}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{boole\$7}}\index{boole\$7} $=$ {\tt{'}}{\tt{*1*true}}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{n\$0}}\index{n\$0} $\not<$ {\sc{i\$7}}\index{i\$7}) \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+($\neg$ {\rm{negativep}}\,({\sc{cand\$7}}\index{cand\$7})) \\ 
$\rightarrow$$\;\;\;\;$({\sc{cand\$7}}\index{cand\$7} $\in\;${\bf{N}}${}$))\- \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\rm{zneqp}}\,({\it{x\/}}, {\sc{cand\$7}}\index{cand\$7})\index{zneqp} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\sc{n\$0}}\index{n\$0} \\ 
$\not<$$\;\;\;\;$(\=\+{\tt{'}}{\tt{2}} \\ 
$*$$\;\;\;\;${\rm{cnt}}\,(\=\+{\it{x\/}}, \\ 
{\sc{a\$0}}\index{a\$0}, \\ 
{\tt{'}}{\tt{1}}, \\ 
{\sc{n\$0}}\index{n\$0})\-\index{cnt})\-)\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\sc{n\$0}}\index{n\$0} \\ 
$\not<$$\;\;\;\;$(\=\+{\tt{'}}{\tt{2}} \\ 
$*$$\;\;\;\;${\rm{cnt}}\,(\=\+{\sc{cand\$7}}\index{cand\$7}, \\ 
{\sc{a\$0}}\index{a\$0}, \\ 
{\tt{'}}{\tt{1}}, \\ 
{\sc{i\$7}}\index{i\$7})\-\index{cnt})\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\sc{k\$7}}\index{k\$7} \\ 
$=$$\;\;\;\;${\rm{cnt}}\,(\=\+{\sc{cand\$7}}\index{cand\$7}, \\ 
{\sc{a\$0}}\index{a\$0}, \\ 
{\tt{'}}{\tt{1}}, \\ 
{\sc{i\$7}}\index{i\$7})\-\index{cnt})\-)\-)\-)\-)\-)\-)\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{lex}}\,(\=\+{\rm{cons}}\,(($1\;+$ {\sc{n\$0}}\index{n\$0}) $-$ {\sc{i\$7}}\index{i\$7}, {\tt{'}}{\tt{nil}}), \\ 
{\rm{cons}}\,($1\;+$ ({\sc{n\$0}}\index{n\$0} $+$ (($1\;+$ {\sc{n\$0}}\index{n\$0}) $-$ {\sc{i\$1}}\index{i\$1})), {\tt{'}}{\tt{nil}}))\-\index{lex})\-\-
\end{tabbing}

\begin{verbatim}#| (COMMENT PHASE1-INVRT T F F F F F F) |#

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

\addvspace{18pt}

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

\begin{tabbing}{\sc Theorem}:  definedness3 \\ \index{definedness3}
(($\neg$ {\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) $\wedge$ {\sc{path-hyps}}\index{path-hyps}) $\rightarrow$ {\rm{znumberp}}\,({\sc{k\$2}}\index{k\$2})\index{znumberp}
\end{tabbing}

\begin{verbatim}#| (COMMENT PHASE1-INVRT F) |#

; (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}:  array-bounds-check-for-a1 \\ \index{array-bounds-check-for-a1}
\=\+({\rm{zeqp}}\,({\sc{k\$2}}\index{k\$2}, {\tt{'}}{\tt{0}})\index{zeqp} $\wedge$ (($\neg$ {\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) $\wedge$ {\sc{path-hyps}}\index{path-hyps})) \\ 
$\rightarrow$$\;\;\;\;$(({\tt{'}}{\tt{0}} $<$ {\sc{i\$2}}\index{i\$2}) $\wedge$ ({\sc{n\$0}}\index{n\$0} $\not<$ {\sc{i\$2}}\index{i\$2}))\-
\end{tabbing}

\begin{verbatim}#| (COMMENT PHASE1-INVRT F T) |#

\end{verbatim}\begin{tabbing}{\sc Theorem}:  definedness4 \\ \index{definedness4}
\=\+({\rm{zeqp}}\,({\sc{k\$2}}\index{k\$2}, {\tt{'}}{\tt{0}})\index{zeqp} $\wedge$ (($\neg$ {\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) $\wedge$ {\sc{path-hyps}}\index{path-hyps})) \\ 
$\rightarrow$$\;\;\;\;${\rm{znumberp}}\,({\rm{elt1}}\,({\sc{a\$0}}\index{a\$0}, {\sc{i\$2}}\index{i\$2})\index{elt1})\index{znumberp}\-
\end{tabbing}

\begin{verbatim}#| (COMMENT PHASE1-INVRT F T) |#

\end{verbatim}\begin{tabbing}{\sc Axiom}:  assignment4 \\ \index{assignment4}
\=\+({\sc{boole\$3}}\index{boole\$3} $=$ {\sc{boole\$2}}\index{boole\$2}) \\ 
$\wedge$$\;\;\;\;$(({\sc{cand\$3}}\index{cand\$3} $=$ {\rm{elt1}}\,({\sc{a\$0}}\index{a\$0}, {\sc{i\$2}}\index{i\$2})\index{elt1}) $\wedge$ (({\sc{i\$3}}\index{i\$3} $=$ {\sc{i\$2}}\index{i\$2}) $\wedge$ ({\sc{k\$3}}\index{k\$3} $=$ {\sc{k\$2}}\index{k\$2})))\-
\end{tabbing}

\begin{tabbing}{\sc Axiom}:  assignment5 \\ \index{assignment5}
\=\+({\sc{boole\$4}}\index{boole\$4} $=$ {\sc{boole\$3}}\index{boole\$3}) \\ 
$\wedge$$\;\;\;\;$(({\sc{cand\$4}}\index{cand\$4} $=$ {\sc{cand\$3}}\index{cand\$3}) $\wedge$ (({\sc{i\$4}}\index{i\$4} $=$ {\sc{i\$3}}\index{i\$3}) $\wedge$ ({\sc{k\$4}}\index{k\$4} $=$ {\tt{'}}{\tt{1}})))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  compound-invrt \\ \index{compound-invrt}
({\sc{k\$1}}\index{k\$1} $=$ {\tt{0}}) $\rightarrow$ ({\sc{i\$1}}\index{i\$1} $\not<$ ({\tt{2}} $*$ {\rm{cnt}}\,({\it{x\/}}, {\sc{a\$0}}\index{a\$0}, {\tt{1}}, {\sc{i\$1}}\index{i\$1})\index{cnt}))
\end{tabbing}

%\item 
\begin{verbatim}


(PROVE-LEMMA PHASE1-INVRT1 NIL
 (IMPLIES
  (AND (ZEQP (K$2) '0)
       (AND (NOT (ZGREATERP (I$2) (N$0)))
            (PATH-HYPS)))
  (AND
   (AND
    (NUMBERP (I$4))
    (AND
     (NOT (EQUAL (I$4) '0))
     (AND
      (NUMBERP (K$4))
      (AND
       (NOT (LESSP (I$4) (K$4)))
       (AND
        (NOT (LESSP (N$0) (I$4)))
        (AND
         (IMPLIES (NOT (NEGATIVEP (CAND$4)))
                  (NUMBERP (CAND$4)))
         (AND
          (NOT (LESSP (CNT (CAND$4) (A$0) '1 (I$4))
                      (K$4)))
          (AND
           (IMPLIES
                  (ZEQP X (CAND$4))
                  (NOT (LESSP (PLUS (I$4) (K$4))
                              (TIMES '2 (CNT X (A$0) '1 (I$4))))))
           (IMPLIES
            (ZNEQP X (CAND$4))
            (NOT
             (LESSP
                   (I$4)
                   (PLUS (K$4)
                         (TIMES '2
                                (CNT X (A$0) '1 (I$4)))))))))))))))
   (LEX (CONS (ADD1 (PLUS (N$0)
                          (DIFFERENCE (ADD1 (N$0)) (I$4))))
              'NIL)
        (CONS (ADD1 (PLUS (N$0)
                          (DIFFERENCE (ADD1 (N$0)) (I$1))))
              'NIL)))))
\end{verbatim}


\begin{verbatim}#| (COMMENT PHASE1-INVRT F T) |#

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

\addvspace{18pt}

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

\begin{tabbing}{\sc Theorem}:  array-bounds-check-for-a1 \\ \index{array-bounds-check-for-a1}
\=\+(($\neg$ {\rm{zeqp}}\,({\sc{k\$2}}\index{k\$2}, {\tt{'}}{\tt{0}})\index{zeqp}) $\wedge$ (($\neg$ {\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) $\wedge$ {\sc{path-hyps}}\index{path-hyps})) \\ 
$\rightarrow$$\;\;\;\;$(({\tt{'}}{\tt{0}} $<$ {\sc{i\$2}}\index{i\$2}) $\wedge$ ({\sc{n\$0}}\index{n\$0} $\not<$ {\sc{i\$2}}\index{i\$2}))\-
\end{tabbing}

\begin{verbatim}#| (COMMENT PHASE1-INVRT F F) |#

\end{verbatim}\begin{tabbing}{\sc Theorem}:  definedness4 \\ \index{definedness4}
\=\+(($\neg$ {\rm{zeqp}}\,({\sc{k\$2}}\index{k\$2}, {\tt{'}}{\tt{0}})\index{zeqp}) $\wedge$ (($\neg$ {\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) $\wedge$ {\sc{path-hyps}}\index{path-hyps})) \\ 
$\rightarrow$$\;\;\;\;${\rm{znumberp}}\,({\sc{cand\$2}}\index{cand\$2})\index{znumberp}\-
\end{tabbing}

\begin{verbatim}#| (COMMENT PHASE1-INVRT F F) |#

\end{verbatim}\begin{tabbing}{\sc Theorem}:  definedness5 \\ \index{definedness5}
\=\+(($\neg$ {\rm{zeqp}}\,({\sc{k\$2}}\index{k\$2}, {\tt{'}}{\tt{0}})\index{zeqp}) $\wedge$ (($\neg$ {\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) $\wedge$ {\sc{path-hyps}}\index{path-hyps})) \\ 
$\rightarrow$$\;\;\;\;${\rm{znumberp}}\,({\rm{elt1}}\,({\sc{a\$0}}\index{a\$0}, {\sc{i\$2}}\index{i\$2})\index{elt1})\index{znumberp}\-
\end{tabbing}

\begin{verbatim}#| (COMMENT PHASE1-INVRT F F) |#

; (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-zplus1 \\ \index{input-cond-of-zplus1}
\=\+(\=\+{\rm{zeqp}}\,({\sc{cand\$2}}\index{cand\$2}, {\rm{elt1}}\,({\sc{a\$0}}\index{a\$0}, {\sc{i\$2}}\index{i\$2})\index{elt1})\index{zeqp} \\ 
$\wedge$$\;\;\;\;$(($\neg$ {\rm{zeqp}}\,({\sc{k\$2}}\index{k\$2}, {\tt{'}}{\tt{0}})\index{zeqp}) $\wedge$ (($\neg$ {\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) $\wedge$ {\sc{path-hyps}}\index{path-hyps})))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{expressible-znumberp}}\,({\rm{zplus}}\,({\sc{k\$2}}\index{k\$2}, {\tt{'}}{\tt{1}})\index{zplus})\index{expressible-znumberp}\-
\end{tabbing}

\begin{verbatim}#| (COMMENT PHASE1-INVRT F F T) |#

\end{verbatim}\begin{tabbing}{\sc Axiom}:  assignment4 \\ \index{assignment4}
\=\+({\sc{boole\$3}}\index{boole\$3} $=$ {\sc{boole\$2}}\index{boole\$2}) \\ 
$\wedge$$\;\;\;\;$(({\sc{cand\$3}}\index{cand\$3} $=$ {\sc{cand\$2}}\index{cand\$2}) $\wedge$ (({\sc{i\$3}}\index{i\$3} $=$ {\sc{i\$2}}\index{i\$2}) $\wedge$ ({\sc{k\$3}}\index{k\$3} $=$ {\rm{zplus}}\,({\sc{k\$2}}\index{k\$2}, {\tt{'}}{\tt{1}})\index{zplus})))\-
\end{tabbing}

%\item 
\begin{verbatim}


(PROVE-LEMMA PHASE1-INVRT1 NIL
 (IMPLIES
  (AND (ZEQP (CAND$2) (ELT1 (A$0) (I$2)))
       (AND (NOT (ZEQP (K$2) '0))
            (AND (NOT (ZGREATERP (I$2) (N$0)))
                 (PATH-HYPS))))
  (AND
   (AND
    (NUMBERP (I$3))
    (AND
     (NOT (EQUAL (I$3) '0))
     (AND
      (NUMBERP (K$3))
      (AND
       (NOT (LESSP (I$3) (K$3)))
       (AND
        (NOT (LESSP (N$0) (I$3)))
        (AND
         (IMPLIES (NOT (NEGATIVEP (CAND$3)))
                  (NUMBERP (CAND$3)))
         (AND
          (NOT (LESSP (CNT (CAND$3) (A$0) '1 (I$3))
                      (K$3)))
          (AND
           (IMPLIES
                  (ZEQP X (CAND$3))
                  (NOT (LESSP (PLUS (I$3) (K$3))
                              (TIMES '2 (CNT X (A$0) '1 (I$3))))))
           (IMPLIES
            (ZNEQP X (CAND$3))
            (NOT
             (LESSP
                   (I$3)
                   (PLUS (K$3)
                         (TIMES '2
                                (CNT X (A$0) '1 (I$3)))))))))))))))
   (LEX (CONS (ADD1 (PLUS (N$0)
                          (DIFFERENCE (ADD1 (N$0)) (I$3))))
              'NIL)
        (CONS (ADD1 (PLUS (N$0)
                          (DIFFERENCE (ADD1 (N$0)) (I$1))))
              'NIL)))))
\end{verbatim}


\begin{verbatim}#| (COMMENT PHASE1-INVRT F F T) |#

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

\addvspace{18pt}

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

\begin{tabbing}{\sc Theorem}:  input-cond-of-zdifference1 \\ \index{input-cond-of-zdifference1}
\=\+(\=\+($\neg$ {\rm{zeqp}}\,({\sc{cand\$2}}\index{cand\$2}, {\rm{elt1}}\,({\sc{a\$0}}\index{a\$0}, {\sc{i\$2}}\index{i\$2})\index{elt1})\index{zeqp}) \\ 
$\wedge$$\;\;\;\;$(($\neg$ {\rm{zeqp}}\,({\sc{k\$2}}\index{k\$2}, {\tt{'}}{\tt{0}})\index{zeqp}) $\wedge$ (($\neg$ {\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) $\wedge$ {\sc{path-hyps}}\index{path-hyps})))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{expressible-znumberp}}\,({\rm{zdifference}}\,({\sc{k\$2}}\index{k\$2}, {\tt{'}}{\tt{1}})\index{zdifference})\index{expressible-znumberp}\-
\end{tabbing}

\begin{verbatim}#| (COMMENT PHASE1-INVRT F F F) |#

\end{verbatim}\begin{tabbing}{\sc Axiom}:  assignment4 \\ \index{assignment4}
\=\+({\sc{boole\$3}}\index{boole\$3} $=$ {\sc{boole\$2}}\index{boole\$2}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{cand\$3}}\index{cand\$3} $=$ {\sc{cand\$2}}\index{cand\$2}) \\ 
$\wedge$$\;\;\;\;$(({\sc{i\$3}}\index{i\$3} $=$ {\sc{i\$2}}\index{i\$2}) $\wedge$ ({\sc{k\$3}}\index{k\$3} $=$ {\rm{zdifference}}\,({\sc{k\$2}}\index{k\$2}, {\tt{'}}{\tt{1}})\index{zdifference})))\-\-
\end{tabbing}

%\item 
\begin{verbatim}


(PROVE-LEMMA PHASE1-INVRT1 NIL
 (IMPLIES
  (AND (NOT (ZEQP (CAND$2) (ELT1 (A$0) (I$2))))
       (AND (NOT (ZEQP (K$2) '0))
            (AND (NOT (ZGREATERP (I$2) (N$0)))
                 (PATH-HYPS))))
  (AND
   (AND
    (NUMBERP (I$3))
    (AND
     (NOT (EQUAL (I$3) '0))
     (AND
      (NUMBERP (K$3))
      (AND
       (NOT (LESSP (I$3) (K$3)))
       (AND
        (NOT (LESSP (N$0) (I$3)))
        (AND
         (IMPLIES (NOT (NEGATIVEP (CAND$3)))
                  (NUMBERP (CAND$3)))
         (AND
          (NOT (LESSP (CNT (CAND$3) (A$0) '1 (I$3))
                      (K$3)))
          (AND
           (IMPLIES
                  (ZEQP X (CAND$3))
                  (NOT (LESSP (PLUS (I$3) (K$3))
                              (TIMES '2 (CNT X (A$0) '1 (I$3))))))
           (IMPLIES
            (ZNEQP X (CAND$3))
            (NOT
             (LESSP
                   (I$3)
                   (PLUS (K$3)
                         (TIMES '2
                                (CNT X (A$0) '1 (I$3)))))))))))))))
   (LEX (CONS (ADD1 (PLUS (N$0)
                          (DIFFERENCE (ADD1 (N$0)) (I$3))))
              'NIL)
        (CONS (ADD1 (PLUS (N$0)
                          (DIFFERENCE (ADD1 (N$0)) (I$1))))
              'NIL)))))
\end{verbatim}


\begin{verbatim}#| (COMMENT PHASE1-INVRT F F F) |#

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

\addvspace{18pt}

\begin{tabbing}{\sc Axiom}:  paths-from-phase2-invrt \\ \index{paths-from-phase2-invrt}
\=\+({\sc{boole\$1}}\index{boole\$1} $=$ {\tt{'}}{\tt{*1*true}}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\rm{zneqp}}\,({\it{x\/}}, {\sc{cand\$1}}\index{cand\$1})\index{zneqp} $\rightarrow$ ({\sc{n\$0}}\index{n\$0} $\not<$ ({\tt{'}}{\tt{2}} $*$ {\rm{cnt}}\,({\it{x\/}}, {\sc{a\$0}}\index{a\$0}, {\tt{'}}{\tt{1}}, {\sc{n\$0}}\index{n\$0})\index{cnt}))) \\ 
$\wedge$$\;\;\;\;$({\sc{k\$1}}\index{k\$1} $=$ {\rm{cnt}}\,({\sc{cand\$1}}\index{cand\$1}, {\sc{a\$0}}\index{a\$0}, {\tt{'}}{\tt{1}}, {\sc{i\$1}}\index{i\$1})\index{cnt}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{path-hyps} \\  
\=\+{\sc{path-hyps}}\index{path-hyps} \\ 
$=$$\;\;\;\;$(\=\+{\sc{global-hyps}}\index{global-hyps} \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{i\$1}}\index{i\$1} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{i\$1}}\index{i\$1} $\not=$ {\tt{'}}{\tt{0}}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{n\$0}}\index{n\$0} $\not<$ {\sc{i\$1}}\index{i\$1}) \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+($\neg$ {\rm{negativep}}\,({\sc{cand\$1}}\index{cand\$1})) \\ 
$\rightarrow$$\;\;\;\;$({\sc{cand\$1}}\index{cand\$1} $\in\;${\bf{N}}${}$))\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\sc{n\$0}}\index{n\$0} \\ 
$\not<$$\;\;\;\;$(\=\+{\tt{'}}{\tt{2}} \\ 
$*$$\;\;\;\;${\rm{cnt}}\,(\=\+{\sc{cand\$1}}\index{cand\$1}, \\ 
{\sc{a\$0}}\index{a\$0}, \\ 
{\tt{'}}{\tt{1}}, \\ 
{\sc{i\$1}}\index{i\$1})\-\index{cnt})\-)\-)\-)\-)\-)\-)\-\-
\end{tabbing}

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

\begin{verbatim}#| (COMMENT PHASE2-INVRT) |#

\end{verbatim}\begin{tabbing}{\sc Theorem}:  input-cond-of-zplus \\ \index{input-cond-of-zplus}
{\sc{path-hyps}}\index{path-hyps} $\rightarrow$ {\rm{expressible-znumberp}}\,({\rm{zplus}}\,({\sc{i\$1}}\index{i\$1}, {\tt{'}}{\tt{1}})\index{zplus})\index{expressible-znumberp}
\end{tabbing}

\begin{verbatim}#| (COMMENT PHASE2-INVRT) |#

\end{verbatim}\begin{tabbing}{\sc Axiom}:  assignment3 \\ \index{assignment3}
\=\+({\sc{boole\$2}}\index{boole\$2} $=$ {\sc{boole\$1}}\index{boole\$1}) \\ 
$\wedge$$\;\;\;\;$(({\sc{cand\$2}}\index{cand\$2} $=$ {\sc{cand\$1}}\index{cand\$1}) $\wedge$ (({\sc{i\$2}}\index{i\$2} $=$ {\rm{zplus}}\,({\sc{i\$1}}\index{i\$1}, {\tt{'}}{\tt{1}})\index{zplus}) $\wedge$ ({\sc{k\$2}}\index{k\$2} $=$ {\sc{k\$1}}\index{k\$1})))\-
\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 Axiom}:  effects-of-undefiner \\ \index{effects-of-undefiner}
({\sc{boole\$3}}\index{boole\$3} $=$ {\sc{boole\$2}}\index{boole\$2}) $\wedge$ (({\sc{cand\$3}}\index{cand\$3} $=$ {\sc{cand\$2}}\index{cand\$2}) $\wedge$ ({\sc{k\$3}}\index{k\$3} $=$ {\sc{k\$2}}\index{k\$2}))
\end{tabbing}

\begin{tabbing}{\sc Axiom}:  assignment4 \\ \index{assignment4}
\=\+({\sc{boole\$4}}\index{boole\$4} $=$ {\tt{'}}{\tt{*1*false}}) \\ 
$\wedge$$\;\;\;\;$(({\sc{cand\$4}}\index{cand\$4} $=$ {\sc{cand\$3}}\index{cand\$3}) $\wedge$ (({\sc{i\$4}}\index{i\$4} $=$ {\sc{i\$3}}\index{i\$3}) $\wedge$ ({\sc{k\$4}}\index{k\$4} $=$ {\sc{k\$3}}\index{k\$3})))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  zeqp-is-a-congruence-relation-wrt-cnt-arg-1 \\ \index{zeqp-is-a-congruence-relation-w!rt-cnt-arg-1}
({\rm{znormalize}}\,({\it{x\/}})\index{znormalize} $=$ {\rm{znormalize}}\,({\it{y\/}})\index{znormalize}) $\rightarrow$ ({\rm{cnt}}\,({\it{x\/}}, {\it{a\/}}, {\it{i\/}}, {\it{j\/}})\index{cnt} $\not<$ {\rm{cnt}}\,({\it{y\/}}, {\it{a\/}}, {\it{i\/}}, {\it{j\/}})\index{cnt})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  phase-2-hint \\ \index{phase-2-hint}
\=\+({\sc{n\$0}}\index{n\$0} $\not<$ ({\rm{cnt}}\,({\sc{cand\$1}}\index{cand\$1}, {\sc{a\$0}}\index{a\$0}, {\tt{1}}, {\sc{n\$0}}\index{n\$0})\index{cnt} $+$ {\rm{cnt}}\,({\sc{cand\$1}}\index{cand\$1}, {\sc{a\$0}}\index{a\$0}, {\tt{1}}, {\sc{n\$0}}\index{n\$0})\index{cnt})) \\ 
$\rightarrow$$\;\;\;\;$({\sc{n\$0}}\index{n\$0} $\not<$ ({\rm{cnt}}\,({\it{x\/}}, {\sc{a\$0}}\index{a\$0}, {\tt{1}}, {\sc{n\$0}}\index{n\$0})\index{cnt} $+$ {\rm{cnt}}\,({\it{x\/}}, {\sc{a\$0}}\index{a\$0}, {\tt{1}}, {\sc{n\$0}}\index{n\$0})\index{cnt}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  output \\ \index{output}
\=\+({\sc{i\$2}}\index{i\$2} $\wedge$ ({\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp} $\wedge$ {\sc{path-hyps}}\index{path-hyps})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(({\sc{boole\$4}}\index{boole\$4} $=$ {\tt{'}}{\tt{*1*true}}) $\vee$ ({\sc{boole\$4}}\index{boole\$4} $=$ {\tt{'}}{\tt{*1*false}})) \\ 
$\wedge$$\;\;\;\;$\=\+{\bf if }{\sc{boole\$4}}\index{boole\$4} \\ 
{\bf then }\=\+{\rm{znumberp}}\,({\sc{cand\$4}}\index{cand\$4})\index{znumberp} \\ 
$\wedge$$\;\;\;\;$(({\sc{n\$0}}\index{n\$0} $\div$ {\tt{'}}{\tt{2}}) $<$ {\rm{cnt}}\,({\sc{cand\$4}}\index{cand\$4}, {\sc{a\$0}}\index{a\$0}, {\tt{'}}{\tt{1}}, {\sc{n\$0}}\index{n\$0})\index{cnt})\- \\ 
{\bf else }({\sc{n\$0}}\index{n\$0} $\div$ {\tt{'}}{\tt{2}}) $\not<$ {\rm{cnt}}\,({\it{x\/}}, {\sc{a\$0}}\index{a\$0}, {\tt{'}}{\tt{1}}, {\sc{n\$0}}\index{n\$0})\index{cnt}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{verbatim}#| (COMMENT PHASE2-INVRT T) |#

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

\addvspace{18pt}

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

\begin{tabbing}{\sc Theorem}:  array-bounds-check-for-a1 \\ \index{array-bounds-check-for-a1}
\=\+(($\neg$ {\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) $\wedge$ {\sc{path-hyps}}\index{path-hyps}) \\ 
$\rightarrow$$\;\;\;\;$(({\tt{'}}{\tt{0}} $<$ {\sc{i\$2}}\index{i\$2}) $\wedge$ ({\sc{n\$0}}\index{n\$0} $\not<$ {\sc{i\$2}}\index{i\$2}))\-
\end{tabbing}

\begin{verbatim}#| (COMMENT PHASE2-INVRT F) |#

\end{verbatim}\begin{tabbing}{\sc Theorem}:  definedness3 \\ \index{definedness3}
(($\neg$ {\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) $\wedge$ {\sc{path-hyps}}\index{path-hyps}) $\rightarrow$ {\rm{znumberp}}\,({\sc{cand\$2}}\index{cand\$2})\index{znumberp}
\end{tabbing}

\begin{verbatim}#| (COMMENT PHASE2-INVRT F) |#

\end{verbatim}\begin{tabbing}{\sc Theorem}:  definedness4 \\ \index{definedness4}
(($\neg$ {\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) $\wedge$ {\sc{path-hyps}}\index{path-hyps}) $\rightarrow$ {\rm{znumberp}}\,({\rm{elt1}}\,({\sc{a\$0}}\index{a\$0}, {\sc{i\$2}}\index{i\$2})\index{elt1})\index{znumberp}
\end{tabbing}

\begin{verbatim}#| (COMMENT PHASE2-INVRT F) |#

; (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}:  phase2-invrt1 \\ \index{phase2-invrt1}
\=\+({\rm{zneqp}}\,({\sc{cand\$2}}\index{cand\$2}, {\rm{elt1}}\,({\sc{a\$0}}\index{a\$0}, {\sc{i\$2}}\index{i\$2})\index{elt1})\index{zneqp} $\wedge$ (($\neg$ {\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) $\wedge$ {\sc{path-hyps}}\index{path-hyps})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+({\sc{i\$2}}\index{i\$2} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{i\$2}}\index{i\$2} $\not=$ {\tt{'}}{\tt{0}}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{boole\$2}}\index{boole\$2} $=$ {\tt{'}}{\tt{*1*true}}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{n\$0}}\index{n\$0} $\not<$ {\sc{i\$2}}\index{i\$2}) \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+($\neg$ {\rm{negativep}}\,({\sc{cand\$2}}\index{cand\$2})) \\ 
$\rightarrow$$\;\;\;\;$({\sc{cand\$2}}\index{cand\$2} $\in\;${\bf{N}}${}$))\- \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\rm{zneqp}}\,({\it{x\/}}, {\sc{cand\$2}}\index{cand\$2})\index{zneqp} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\sc{n\$0}}\index{n\$0} \\ 
$\not<$$\;\;\;\;$(\=\+{\tt{'}}{\tt{2}} \\ 
$*$$\;\;\;\;${\rm{cnt}}\,(\=\+{\it{x\/}}, \\ 
{\sc{a\$0}}\index{a\$0}, \\ 
{\tt{'}}{\tt{1}}, \\ 
{\sc{n\$0}}\index{n\$0})\-\index{cnt})\-)\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\sc{n\$0}}\index{n\$0} \\ 
$\not<$$\;\;\;\;$(\=\+{\tt{'}}{\tt{2}} \\ 
$*$$\;\;\;\;${\rm{cnt}}\,(\=\+{\sc{cand\$2}}\index{cand\$2}, \\ 
{\sc{a\$0}}\index{a\$0}, \\ 
{\tt{'}}{\tt{1}}, \\ 
{\sc{i\$2}}\index{i\$2})\-\index{cnt})\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\sc{k\$2}}\index{k\$2} \\ 
$=$$\;\;\;\;${\rm{cnt}}\,(\=\+{\sc{cand\$2}}\index{cand\$2}, \\ 
{\sc{a\$0}}\index{a\$0}, \\ 
{\tt{'}}{\tt{1}}, \\ 
{\sc{i\$2}}\index{i\$2})\-\index{cnt})\-)\-)\-)\-)\-)\-)\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{lex}}\,(\=\+{\rm{cons}}\,(($1\;+$ {\sc{n\$0}}\index{n\$0}) $-$ {\sc{i\$2}}\index{i\$2}, {\tt{'}}{\tt{nil}}), \\ 
{\rm{cons}}\,(($1\;+$ {\sc{n\$0}}\index{n\$0}) $-$ {\sc{i\$1}}\index{i\$1}, {\tt{'}}{\tt{nil}}))\-\index{lex})\-\-
\end{tabbing}

\begin{verbatim}#| (COMMENT PHASE2-INVRT F T) |#

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

\addvspace{18pt}

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

\begin{tabbing}{\sc Theorem}:  definedness5 \\ \index{definedness5}
\=\+(\=\+($\neg$ {\rm{zneqp}}\,({\sc{cand\$2}}\index{cand\$2}, {\rm{elt1}}\,({\sc{a\$0}}\index{a\$0}, {\sc{i\$2}}\index{i\$2})\index{elt1})\index{zneqp}) \\ 
$\wedge$$\;\;\;\;$(($\neg$ {\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) $\wedge$ {\sc{path-hyps}}\index{path-hyps}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{znumberp}}\,({\sc{k\$2}}\index{k\$2})\index{znumberp}\-
\end{tabbing}

\begin{verbatim}#| (COMMENT PHASE2-INVRT F F) |#

\end{verbatim}\begin{tabbing}{\sc Theorem}:  input-cond-of-zplus1 \\ \index{input-cond-of-zplus1}
\=\+(\=\+($\neg$ {\rm{zneqp}}\,({\sc{cand\$2}}\index{cand\$2}, {\rm{elt1}}\,({\sc{a\$0}}\index{a\$0}, {\sc{i\$2}}\index{i\$2})\index{elt1})\index{zneqp}) \\ 
$\wedge$$\;\;\;\;$(($\neg$ {\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) $\wedge$ {\sc{path-hyps}}\index{path-hyps}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{expressible-znumberp}}\,({\rm{zplus}}\,({\sc{k\$2}}\index{k\$2}, {\tt{'}}{\tt{1}})\index{zplus})\index{expressible-znumberp}\-
\end{tabbing}

\begin{verbatim}#| (COMMENT PHASE2-INVRT F F) |#

\end{verbatim}\begin{tabbing}{\sc Axiom}:  assignment4 \\ \index{assignment4}
\=\+({\sc{boole\$3}}\index{boole\$3} $=$ {\sc{boole\$2}}\index{boole\$2}) \\ 
$\wedge$$\;\;\;\;$(({\sc{cand\$3}}\index{cand\$3} $=$ {\sc{cand\$2}}\index{cand\$2}) $\wedge$ (({\sc{i\$3}}\index{i\$3} $=$ {\sc{i\$2}}\index{i\$2}) $\wedge$ ({\sc{k\$3}}\index{k\$3} $=$ {\rm{zplus}}\,({\sc{k\$2}}\index{k\$2}, {\tt{'}}{\tt{1}})\index{zplus})))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  cnt-grows \\ \index{cnt-grows}
\=\+(({\sc{i\$1}}\index{i\$1} $<$ {\it{n\/}}) $\wedge$ {\rm{zeqp}}\,({\it{x\/}}, {\rm{elt1}}\,({\it{a\/}}, $1\;+$ {\sc{i\$1}}\index{i\$1})\index{elt1})\index{zeqp}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{cnt}}\,({\it{x\/}}, {\it{a\/}}, {\tt{1}}, {\sc{i\$1}}\index{i\$1})\index{cnt} $<$ {\rm{cnt}}\,({\it{x\/}}, {\it{a\/}}, {\tt{1}}, {\it{n\/}})\index{cnt})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  input-cond-of-zquotient \\ \index{input-cond-of-zquotient}
\=\+(\=\+($\neg$ {\rm{zneqp}}\,({\sc{cand\$2}}\index{cand\$2}, {\rm{elt1}}\,({\sc{a\$0}}\index{a\$0}, {\sc{i\$2}}\index{i\$2})\index{elt1})\index{zneqp}) \\ 
$\wedge$$\;\;\;\;$(($\neg$ {\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) $\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}}\,({\sc{n\$0}}\index{n\$0}, {\tt{'}}{\tt{2}})\index{zquotient})\index{expressible-znumberp})\-
\end{tabbing}

\begin{verbatim}#| (COMMENT PHASE2-INVRT F F) |#

; (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}:  output \\ \index{output}
\=\+(\=\+{\rm{zgreaterp}}\,({\sc{k\$3}}\index{k\$3}, {\rm{zquotient}}\,({\sc{n\$0}}\index{n\$0}, {\tt{'}}{\tt{2}})\index{zquotient})\index{zgreaterp} \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zneqp}}\,({\sc{cand\$2}}\index{cand\$2}, {\rm{elt1}}\,({\sc{a\$0}}\index{a\$0}, {\sc{i\$2}}\index{i\$2})\index{elt1})\index{zneqp}) \\ 
$\wedge$$\;\;\;\;$(($\neg$ {\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) $\wedge$ {\sc{path-hyps}}\index{path-hyps}))\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(({\sc{boole\$3}}\index{boole\$3} $=$ {\tt{'}}{\tt{*1*true}}) $\vee$ ({\sc{boole\$3}}\index{boole\$3} $=$ {\tt{'}}{\tt{*1*false}})) \\ 
$\wedge$$\;\;\;\;$\=\+{\bf if }{\sc{boole\$3}}\index{boole\$3} \\ 
{\bf then }\=\+{\rm{znumberp}}\,({\sc{cand\$3}}\index{cand\$3})\index{znumberp} \\ 
$\wedge$$\;\;\;\;$(({\sc{n\$0}}\index{n\$0} $\div$ {\tt{'}}{\tt{2}}) $<$ {\rm{cnt}}\,({\sc{cand\$3}}\index{cand\$3}, {\sc{a\$0}}\index{a\$0}, {\tt{'}}{\tt{1}}, {\sc{n\$0}}\index{n\$0})\index{cnt})\- \\ 
{\bf else }({\sc{n\$0}}\index{n\$0} $\div$ {\tt{'}}{\tt{2}}) $\not<$ {\rm{cnt}}\,({\it{x\/}}, {\sc{a\$0}}\index{a\$0}, {\tt{'}}{\tt{1}}, {\sc{n\$0}}\index{n\$0})\index{cnt}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{verbatim}#| (COMMENT PHASE2-INVRT F F T) |#

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

\addvspace{18pt}

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

\begin{tabbing}{\sc Theorem}:  phase2-invrt1 \\ \index{phase2-invrt1}
\=\+(\=\+($\neg$ {\rm{zgreaterp}}\,({\sc{k\$3}}\index{k\$3}, {\rm{zquotient}}\,({\sc{n\$0}}\index{n\$0}, {\tt{'}}{\tt{2}})\index{zquotient})\index{zgreaterp}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{zneqp}}\,({\sc{cand\$2}}\index{cand\$2}, {\rm{elt1}}\,({\sc{a\$0}}\index{a\$0}, {\sc{i\$2}}\index{i\$2})\index{elt1})\index{zneqp}) \\ 
$\wedge$$\;\;\;\;$(($\neg$ {\rm{zgreaterp}}\,({\sc{i\$2}}\index{i\$2}, {\sc{n\$0}}\index{n\$0})\index{zgreaterp}) $\wedge$ {\sc{path-hyps}}\index{path-hyps}))\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+({\sc{i\$3}}\index{i\$3} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{i\$3}}\index{i\$3} $\not=$ {\tt{'}}{\tt{0}}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{boole\$3}}\index{boole\$3} $=$ {\tt{'}}{\tt{*1*true}}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{n\$0}}\index{n\$0} $\not<$ {\sc{i\$3}}\index{i\$3}) \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+($\neg$ {\rm{negativep}}\,({\sc{cand\$3}}\index{cand\$3})) \\ 
$\rightarrow$$\;\;\;\;$({\sc{cand\$3}}\index{cand\$3} $\in\;${\bf{N}}${}$))\- \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\rm{zneqp}}\,({\it{x\/}}, {\sc{cand\$3}}\index{cand\$3})\index{zneqp} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\sc{n\$0}}\index{n\$0} \\ 
$\not<$$\;\;\;\;$(\=\+{\tt{'}}{\tt{2}} \\ 
$*$$\;\;\;\;${\rm{cnt}}\,(\=\+{\it{x\/}}, \\ 
{\sc{a\$0}}\index{a\$0}, \\ 
{\tt{'}}{\tt{1}}, \\ 
{\sc{n\$0}}\index{n\$0})\-\index{cnt})\-)\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\sc{n\$0}}\index{n\$0} \\ 
$\not<$$\;\;\;\;$(\=\+{\tt{'}}{\tt{2}} \\ 
$*$$\;\;\;\;${\rm{cnt}}\,(\=\+{\sc{cand\$3}}\index{cand\$3}, \\ 
{\sc{a\$0}}\index{a\$0}, \\ 
{\tt{'}}{\tt{1}}, \\ 
{\sc{i\$3}}\index{i\$3})\-\index{cnt})\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\sc{k\$3}}\index{k\$3} \\ 
$=$$\;\;\;\;${\rm{cnt}}\,(\=\+{\sc{cand\$3}}\index{cand\$3}, \\ 
{\sc{a\$0}}\index{a\$0}, \\ 
{\tt{'}}{\tt{1}}, \\ 
{\sc{i\$3}}\index{i\$3})\-\index{cnt})\-)\-)\-)\-)\-)\-)\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{lex}}\,(\=\+{\rm{cons}}\,(($1\;+$ {\sc{n\$0}}\index{n\$0}) $-$ {\sc{i\$3}}\index{i\$3}, {\tt{'}}{\tt{nil}}), \\ 
{\rm{cons}}\,(($1\;+$ {\sc{n\$0}}\index{n\$0}) $-$ {\sc{i\$1}}\index{i\$1}, {\tt{'}}{\tt{nil}}))\-\index{lex})\-\-
\end{tabbing}

\begin{verbatim}#| (COMMENT PHASE2-INVRT F F F) |#

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

\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.
        (CNT X A I N)
           =
        (IF (OR (ZEROP N) (LESSP N I))
            0
            (IF (ZEQP X (ELT1 A N))
                (ADD1 (CNT X A I (SUB1 N)))
                (CNT X A I (SUB1 N))))
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        (FORTRAN-COMMENT USEFUL-LEMMAS)
@END(VERBATIM)
@END(GROUP)


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

Specification for routine MJRTY

The input assertion:
        (AND (IMPLIES (AND (LESSP 0 J)
                           (NOT (LESSP (N STATE) J))
                           (NOT (NEGATIVEP (ELT1 A J))))
                      (NUMBERP (ELT1 A J)))
             (NUMBERP (N STATE))
             (NOT (EQUAL (N STATE) 0))
             (LESSP (ADD1 (N STATE))
                    (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))


The output assertion:
        (AND (OR (EQUAL (BOOLE NEWSTATE) (TRUE))
                 (EQUAL (BOOLE NEWSTATE) (FALSE)))
             (IF (BOOLE NEWSTATE)
                 (AND (ZNUMBERP (CAND NEWSTATE))
                      (LESSP (QUOTIENT (N STATE) 2)
                             (CNT (CAND NEWSTATE)
                                  (A STATE)
                                  1
                                  (N STATE))))
                 (NOT (LESSP (QUOTIENT (N STATE) 2)
                             (CNT X (A STATE) 1 (N STATE))))))
\end{verbatim}
\newpage
\begin{verbatim}

      END
      SUBROUTINE MJRTY(A, N, BOOLE, CAND)
      INTEGER N
      INTEGER A
      LOGICAL BOOLE
      INTEGER CAND
      INTEGER I
      INTEGER K
      DIMENSION A(N)
      K = 0
C     THE FOLLOWING DO IMPLEMENTS THE PAIRING PHASE. CAND IS THE CURRENT
C     LY LEADING CANDIDATE AND K IS THE NUMBER OF UNPAIRED VOTES FOR CAN
C     D. 
      DO 100 I = 1, N
C     DOJUNK PHASE1-HINT
      IF ((K .EQ. 0)) GOTO 50
      IF ((CAND .EQ. A(I))) GOTO 75
      K = (K - 1)
      GOTO 100
50    CAND = A(I)
      K = 1
C     XXX PHASE1-INVRT-F-T
      GOTO 100
75    K = (K + 1)
100   CONTINUE
      IF ((K .EQ. 0)) GOTO 300
      BOOLE = .TRUE.
      IF ((K .GT. (N / 2))) RETURN
C     WE NOW ENTER THE COUNTING PHASE. BOOLE IS SET TO TRUE IN ANTICIPAT
C     ION OF FINDING CAND IN THE MAJORITY. K IS USED AS THE RUNNING TALL
C     Y FOR CAND. WE EXIT AS SOON AS K EXCEEDS N/2. 
      K = 0
      DO 200 I = 1, N
C     DOJUNK PHASE2
      IF ((CAND .NE. A(I))) GOTO 200
      K = (K + 1)
C     XXX OUTPUT-HINT
      IF ((K .GT. (N / 2))) RETURN
200   CONTINUE
300   BOOLE = .FALSE.
C     XXX HINT-FOR-PHASE1-INVRT-T-T
C     XXX HINT-FOR-PHASE2-INVRT-T
      RETURN
      END


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

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  DIFFERENCE-0 (rewrite):
        (IMPLIES (NOT (LESSP X Y))
                 (EQUAL (DIFFERENCE Y X) 0))
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  DIFFERENCE-1 (rewrite):
        (EQUAL (DIFFERENCE X 1) (SUB1 X))
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  LESSP-X-1 (rewrite):
        (EQUAL (LESSP X 1) (ZEROP X))
@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.  QUOTIENT-BY-2-BOUND (rewrite):
        (NOT (LESSP X (QUOTIENT X 2)))
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  LESSP-QUOTIENT-REWRITE (rewrite):
        (EQUAL (LESSP (QUOTIENT N 2) M)
               (LESSP N (PLUS M M)))
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  ZNORMALIZE-ZERO (rewrite):
        (IMPLIES (NUMBERP X)
                 (EQUAL (EQUAL (ZNORMALIZE X) 0)
                        (EQUAL X 0)))
@END(VERBATIM)
@END(GROUP)

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

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  CNT-BOUND (rewrite):
        (NOT (LESSP N (CNT X A 1 N)))
@END(VERBATIM)
@END(GROUP)


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

Hints for routine MJRTY

                              

The input clock:
        (LIST (ADD1 (ADD1 (PLUS (N (START)) (N (START))))))

The DO junk named PHASE1-HINT:
        ((BUMP PHASE1-INVRT))

The invariant and clock named PHASE1-INVRT.

        (AND
         (NUMBERP (I STATE))
         (NOT (EQUAL (I STATE) 0))
         (NUMBERP (K STATE))
         (NOT (LESSP (I STATE) (K STATE)))
         (NOT (LESSP (N (START)) (I STATE)))
         (IMPLIES (NOT (NEGATIVEP (CAND STATE)))
                  (NUMBERP (CAND STATE)))
         (NOT (LESSP (CNT (CAND STATE)
                          (A STATE)
                          1
                          (I STATE))
                     (K STATE)))
         (IMPLIES
                (ZEQP X (CAND STATE))
                (NOT (LESSP (PLUS (I STATE) (K STATE))
                            (TIMES 2
                                   (CNT X (A STATE) 1 (I STATE))))))
         (IMPLIES
          (ZNEQP X (CAND STATE))
          (NOT
             (LESSP (I STATE)
                    (PLUS (K STATE)
                          (TIMES 2
                                 (CNT X (A STATE) 1 (I STATE))))))))

        (LIST (ADD1 (PLUS (N (START))
                          (DIFFERENCE (ADD1 (N (START)))
                                      (I STATE)))))

The XXX named PHASE1-INVRT-F-T:
        Path encryption:
        ((PHASE1-INVRT F T))
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  COMPOUND-INVRT (rewrite):
        (IMPLIES (EQUAL (K$1) 0)
                 (NOT (LESSP (I$1)
                             (TIMES 2 (CNT X (A$0) 1 (I$1))))))
        Hints:  Consider:
                 PATHS-FROM-PHASE1-INVRT
                Enable  PATHS-FROM-PHASE1-INVRT
@END(VERBATIM)
@END(GROUP)



The DO junk named PHASE2:
        ((BUMP PHASE2-INVRT))

The invariant and clock named PHASE2-INVRT.

        (AND
         (NUMBERP (I STATE))
         (NOT (EQUAL (I STATE) 0))
         (EQUAL (BOOLE STATE) (TRUE))
         (NOT (LESSP (N (START)) (I STATE)))
         (IMPLIES (NOT (NEGATIVEP (CAND STATE)))
                  (NUMBERP (CAND STATE)))
         (IMPLIES
              (ZNEQP X (CAND STATE))
              (NOT (LESSP (N (START))
                          (TIMES 2
                                 (CNT X (A STATE) 1 (N (START)))))))
         (NOT (LESSP (N (START))
                     (TIMES 2
                            (CNT (CAND STATE)
                                 (A STATE)
                                 1
                                 (I STATE)))))
         (EQUAL (K STATE)
                (CNT (CAND STATE)
                     (A STATE)
                     1
                     (I STATE))))

        (LIST (DIFFERENCE (ADD1 (N (START)))
                          (I STATE)))

The XXX named OUTPUT-HINT:
        Path encryption:
        ((PHASE2-INVRT F F))
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  CNT-GROWS (rewrite):
        (IMPLIES (AND (LESSP (I$1) N)
                      (ZEQP X (ELT1 A (ADD1 (I$1)))))
                 (LESSP (CNT X A 1 (I$1))
                        (CNT X A 1 N)))
        Hint:  Induct as for (PLUS N I).
@END(VERBATIM)
@END(GROUP)



The XXX named HINT-FOR-PHASE1-INVRT-T-T:
        Path encryption:
        ((PHASE1-INVRT T T))
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  COMPOUND-INVRT (rewrite):
        (IMPLIES (EQUAL (K$1) 0)
                 (NOT (LESSP (I$1)
                             (TIMES 2 (CNT X (A$0) 1 (I$1))))))
        Hints:  Consider:
                 PATHS-FROM-PHASE1-INVRT
                Enable PATHS-FROM-PHASE1-INVRT
@END(VERBATIM)
@END(GROUP)



The XXX named HINT-FOR-PHASE2-INVRT-T:
        Path encryption:
        ((PHASE2-INVRT T))
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  ZEQP-IS-A-CONGRUENCE-RELATION-WRT-CNT-ARG-1 (rewrite):
        (IMPLIES (EQUAL (ZNORMALIZE X) (ZNORMALIZE Y))
                 (NOT (LESSP (CNT X A I J) (CNT Y A I J))))
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  PHASE-2-HINT (rewrite):
        (IMPLIES (NOT (LESSP (N$0)
                             (PLUS (CNT (CAND$1) (A$0) 1 (N$0))
                                   (CNT (CAND$1) (A$0) 1 (N$0)))))
                 (NOT (LESSP (N$0)
                             (PLUS (CNT X (A$0) 1 (N$0))
                                   (CNT X (A$0) 1 (N$0))))))
        Hints:  Consider:
                 PATHS-FROM-PHASE2-INVRT
                Enable PATHS-FROM-PHASE2-INVRT
@END(VERBATIM)
@END(GROUP)

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