\documentstyle[makeidx]{article}
\makeindex
%\setlength{\oddsidemargin}{.5in}
%\setlength{\evensidemargin}{.5in}
%\setlength{\textwidth}{5.8in}
\begin{document}
%\setlength{\parindent}{0pt}
%\newcounter{bean}
%\begin{list}{\arabic{bean}.}{\usecounter{bean}\setlength{\leftmargin}{0pt}\setlength{\rightmargin}{0pt}\setlength{\listparindent}{20pt}\setlength{\parsep}{5pt}}
%\item[]

\begin{verbatim}#|

 Copyright (C) 1994 by Robert S. Boyer and J Strother Moore.  All Rights
 Reserved.

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

 NO WARRANTY

 Robert S. Boyer and J Strother Moore PROVIDE ABSOLUTELY NO WARRANTY.  THE
 EVENT SCRIPT IS PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS
 OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF
 MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO
 THE QUALITY AND PERFORMANCE OF THE SCRIPT IS WITH YOU.  SHOULD THE SCRIPT
 PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR
 CORRECTION.

 IN NO EVENT WILL Robert S. Boyer or J Strother Moore BE LIABLE TO YOU FOR ANY
 DAMAGES, ANY LOST PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR
 CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT
 (INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE
 OR LOSSES SUSTAINED BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE
 POSSIBILITY OF SUCH DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.

|#

; This is the list of verification conditions for a FORTRAN
; version of our fast string searching 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 blk-delta1\$0\index{blk-delta1\$0}\/} of 0 arguments.

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


\noindent{\sc Event}:   Introduce the function symbol {\it c\$4\index{c\$4}\/} 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 maxi\$0\index{maxi\$0}\/} of 0 arguments.

\addvspace{18pt}


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

\addvspace{18pt}

\begin{tabbing}{\sc Axiom}:  asize\&-numberp \\ \index{asize\&-numberp}
{\sc{asize\&}}\index{asize\&} $\in\;${\bf{N}}${}$
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{delta1} \\  
\=\+{\rm{delta1}}\,({\it{a\/}}, {\it{c\/}}, {\it{maxi\/}})\index{delta1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{maxi\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{c\/}} $=$ {\rm{elt1}}\,({\it{a\/}}, {\it{maxi\/}})\index{elt1}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }$1\;+$ {\rm{delta1}}\,({\it{a\/}}, {\it{c\/}}, {\it{maxi\/}} $-\;1$)\index{delta1}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{stringp} \\  
\=\+{\rm{stringp}}\,({\it{a\/}}, {\it{i\/}}, {\it{size\/}})\index{stringp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }\=\+({\rm{elt1}}\,({\it{a\/}}, {\it{i\/}})\index{elt1} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{elt1}}\,({\it{a\/}}, {\it{i\/}})\index{elt1} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{size\/}} $\not<$ {\rm{elt1}}\,({\it{a\/}}, {\it{i\/}})\index{elt1}) \\ 
$\wedge$$\;\;\;\;${\rm{stringp}}\,({\it{a\/}}, {\it{i\/}} $-\;1$, {\it{size\/}})\index{stringp}\-$\;${\bf  endif}\-\-
\end{tabbing}

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

\begin{tabbing}{\sc Definition}:\index{global-hyps} \\  
\=\+{\sc{global-hyps}}\index{global-hyps} \\ 
$=$$\;\;\;\;$(\=\+({\sc{asize\&}}\index{asize\&} $\not=$ {\tt{'}}{\tt{0}}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{stringp}}\,({\sc{a\$0}}\index{a\$0}, {\sc{maxi\$0}}\index{maxi\$0}, {\sc{asize\&}}\index{asize\&})\index{stringp} \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{maxi\$0}}\index{maxi\$0} $\not=$ {\tt{'}}{\tt{0}}) \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+($1\;+$ {\sc{asize\&}}\index{asize\&}) \\ 
$<$$\;\;\;\;${\sc{least-inexpressible-positive-integer}}\index{least-inexpressible-positive-inte!ger})\- \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+($1\;+$ {\sc{maxi\$0}}\index{maxi\$0}) \\ 
$<$$\;\;\;\;${\sc{least-inexpressible-positive-integer}}\index{least-inexpressible-positive-inte!ger})\- \\ 
$\wedge$$\;\;\;\;$({\sc{maxi\$0}}\index{maxi\$0} $\in\;${\bf{N}}${}$))\-)\-)\-)\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  stringp-is-a-univ-quantifier \\ \index{stringp-is-a-univ-quantifier}
\=\+({\rm{stringp}}\,({\it{a\/}}, {\it{i\/}}, {\sc{asize\&}}\index{asize\&})\index{stringp} $\wedge$ ({\it{j\/}} $\not=$ {\tt{0}}) $\wedge$ ({\it{j\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{i\/}} $\not<$ {\it{j\/}})) \\ 
$\rightarrow$$\;\;\;\;$(({\rm{elt1}}\,({\it{a\/}}, {\it{j\/}})\index{elt1} $\in\;${\bf{N}}${}$) $\wedge$ ({\sc{asize\&}}\index{asize\&} $\not<$ {\rm{elt1}}\,({\it{a\/}}, {\it{j\/}})\index{elt1}) $\wedge$ ({\rm{elt1}}\,({\it{a\/}}, {\it{j\/}})\index{elt1} $\not=$ {\tt{0}}))\-
\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{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}:  assignment \\ \index{assignment}
({\sc{i\$1}}\index{i\$1} $=$ {\tt{'}}{\tt{1}}) $\wedge$ (({\sc{c\$1}}\index{c\$1} $=$ {\sc{c\$0}}\index{c\$0}) $\wedge$ ({\sc{blk-delta1\$1}}\index{blk-delta1\$1} $=$ {\sc{blk-delta1\$0}}\index{blk-delta1\$0}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  pass1-invrt \\ \index{pass1-invrt}
\=\+{\sc{global-hyps}}\index{global-hyps} \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+({\sc{i\$1}}\index{i\$1} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{i\$1}}\index{i\$1} $\not=$ {\tt{'}}{\tt{0}}) \\ 
$\wedge$$\;\;\;\;$(\=\+(($1\;+$ {\sc{asize\&}}\index{asize\&}) $\not<$ {\sc{i\$1}}\index{i\$1}) \\ 
$\wedge$$\;\;\;\;$(\=\+(({\it{j\/}} $\in\;${\bf{N}}${}$) $\wedge$ (({\it{j\/}} $\not=$ {\tt{'}}{\tt{0}}) $\wedge$ ({\it{j\/}} $<$ {\sc{i\$1}}\index{i\$1}))) \\ 
$\rightarrow$$\;\;\;\;$({\rm{elt1}}\,({\sc{blk-delta1\$1}}\index{blk-delta1\$1}, {\it{j\/}})\index{elt1} $=$ {\sc{maxi\$0}}\index{maxi\$0}))\-)\-)\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{lex}}\,(\=\+{\rm{cons}}\,(({\tt{'}}{\tt{2}} $+$ ({\sc{asize\&}}\index{asize\&} $+$ {\sc{maxi\$0}}\index{maxi\$0})) $-$ {\sc{i\$1}}\index{i\$1}, {\tt{'}}{\tt{nil}}), \\ 
{\rm{cons}}\,({\tt{'}}{\tt{2}} $+$ ({\sc{asize\&}}\index{asize\&} $+$ {\sc{maxi\$0}}\index{maxi\$0}), {\tt{'}}{\tt{nil}}))\-\index{lex})\-\-
\end{tabbing}

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

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

\addvspace{18pt}

\begin{tabbing}{\sc Axiom}:  paths-from-pass1-invrt \\ \index{paths-from-pass1-invrt}
\=\+(({\it{j\/}} $\in\;${\bf{N}}${}$) $\wedge$ (({\it{j\/}} $\not=$ {\tt{'}}{\tt{0}}) $\wedge$ ({\it{j\/}} $<$ {\sc{i\$1}}\index{i\$1}))) \\ 
$\rightarrow$$\;\;\;\;$({\rm{elt1}}\,({\sc{blk-delta1\$1}}\index{blk-delta1\$1}, {\it{j\/}})\index{elt1} $=$ {\sc{maxi\$0}}\index{maxi\$0})\-
\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$ (($1\;+$ {\sc{asize\&}}\index{asize\&}) $\not<$ {\sc{i\$1}}\index{i\$1}))))\-\-
\end{tabbing}

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

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

; (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{c\$2}}\index{c\$2} $=$ {\sc{c\$1}}\index{c\$1}) $\wedge$ ({\sc{blk-delta1\$2}}\index{blk-delta1\$2} $=$ {\sc{blk-delta1\$1}}\index{blk-delta1\$1})
\end{tabbing}

\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}:  assignment1 \\ \index{assignment1}
({\sc{i\$3}}\index{i\$3} $=$ {\tt{'}}{\tt{1}}) $\wedge$ (({\sc{c\$3}}\index{c\$3} $=$ {\sc{c\$2}}\index{c\$2}) $\wedge$ ({\sc{blk-delta1\$3}}\index{blk-delta1\$3} $=$ {\sc{blk-delta1\$2}}\index{blk-delta1\$2}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  pass2-invrt \\ \index{pass2-invrt}
\=\+({\sc{i\$1}}\index{i\$1} $\wedge$ ({\rm{zgreaterp}}\,({\sc{i\$1}}\index{i\$1}, {\sc{asize\&}}\index{asize\&})\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$$\;\;\;\;$(\=\+(($1\;+$ {\sc{maxi\$0}}\index{maxi\$0}) $\not<$ {\sc{i\$3}}\index{i\$3}) \\ 
$\wedge$$\;\;\;\;$(\=\+(({\it{j\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\sc{asize\&}}\index{asize\&} $\not<$ {\it{j\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{elt1}}\,({\sc{blk-delta1\$3}}\index{blk-delta1\$3}, {\it{j\/}})\index{elt1} \\ 
$=$$\;\;\;\;$(\=\+{\rm{delta1}}\,({\sc{a\$0}}\index{a\$0}, {\it{j\/}}, {\sc{i\$3}}\index{i\$3} $-\;1$)\index{delta1} \\ 
$+$$\;\;\;\;$(\=\+{\sc{maxi\$0}}\index{maxi\$0} \\ 
$-$$\;\;\;\;$({\sc{i\$3}}\index{i\$3} $-\;1$))\-)\-)\-)\-)\-)\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{lex}}\,(\=\+{\rm{cons}}\,(($1\;+$ {\sc{maxi\$0}}\index{maxi\$0}) $-$ {\sc{i\$3}}\index{i\$3}, {\tt{'}}{\tt{nil}}), \\ 
{\rm{cons}}\,(({\tt{'}}{\tt{2}} $+$ ({\sc{asize\&}}\index{asize\&} $+$ {\sc{maxi\$0}}\index{maxi\$0})) $-$ {\sc{i\$1}}\index{i\$1}, {\tt{'}}{\tt{nil}}))\-\index{lex})\-\-
\end{tabbing}

\begin{verbatim}#| (COMMENT PASS1-INVRT T 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{tabbing}{\sc Theorem}:  array-bounds-check-for-delta1 \\ \index{array-bounds-check-for-delta1}
\=\+(($\neg$ {\rm{zgreaterp}}\,({\sc{i\$1}}\index{i\$1}, {\sc{asize\&}}\index{asize\&})\index{zgreaterp}) $\wedge$ {\sc{path-hyps}}\index{path-hyps}) \\ 
$\rightarrow$$\;\;\;\;$(({\tt{'}}{\tt{0}} $<$ {\sc{i\$1}}\index{i\$1}) $\wedge$ ({\sc{asize\&}}\index{asize\&} $\not<$ {\sc{i\$1}}\index{i\$1}))\-
\end{tabbing}

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

\end{verbatim}\begin{tabbing}{\sc Axiom}:  assignment1 \\ \index{assignment1}
\=\+({\sc{i\$2}}\index{i\$2} $=$ {\sc{i\$1}}\index{i\$1}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{c\$2}}\index{c\$2} $=$ {\sc{c\$1}}\index{c\$1}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{elt1}}\,({\sc{blk-delta1\$2}}\index{blk-delta1\$2}, {\it{i\/}})\index{elt1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $=$ {\sc{i\$1}}\index{i\$1}$\;\;${\bf then }{\sc{maxi\$0}}\index{maxi\$0} \\ 
{\bf else }{\rm{elt1}}\,({\sc{blk-delta1\$1}}\index{blk-delta1\$1}, {\it{i\/}})\index{elt1}$\;${\bf  endif}\-)\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  input-cond-of-zplus \\ \index{input-cond-of-zplus}
\=\+(\=\+{\rm{almost-equal1}}\,({\sc{blk-delta1\$1}}\index{blk-delta1\$1}, {\sc{blk-delta1\$2}}\index{blk-delta1\$2}, {\tt{'}}{\tt{1}}, {\sc{asize\&}}\index{asize\&}, {\sc{i\$1}}\index{i\$1}, {\sc{maxi\$0}}\index{maxi\$0})\index{almost-equal1} \\ 
$\wedge$$\;\;\;\;$(($\neg$ {\rm{zgreaterp}}\,({\sc{i\$1}}\index{i\$1}, {\sc{asize\&}}\index{asize\&})\index{zgreaterp}) $\wedge$ {\sc{path-hyps}}\index{path-hyps}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{expressible-znumberp}}\,({\rm{zplus}}\,({\sc{i\$2}}\index{i\$2}, {\tt{'}}{\tt{1}})\index{zplus})\index{expressible-znumberp}\-
\end{tabbing}

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

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

\begin{tabbing}{\sc Theorem}:  pass1-invrt1 \\ \index{pass1-invrt1}
\=\+(\=\+{\rm{almost-equal1}}\,({\sc{blk-delta1\$1}}\index{blk-delta1\$1}, {\sc{blk-delta1\$2}}\index{blk-delta1\$2}, {\tt{'}}{\tt{1}}, {\sc{asize\&}}\index{asize\&}, {\sc{i\$1}}\index{i\$1}, {\sc{maxi\$0}}\index{maxi\$0})\index{almost-equal1} \\ 
$\wedge$$\;\;\;\;$(($\neg$ {\rm{zgreaterp}}\,({\sc{i\$1}}\index{i\$1}, {\sc{asize\&}}\index{asize\&})\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$$\;\;\;\;$(\=\+(($1\;+$ {\sc{asize\&}}\index{asize\&}) $\not<$ {\sc{i\$3}}\index{i\$3}) \\ 
$\wedge$$\;\;\;\;$(\=\+(({\it{j\/}} $\in\;${\bf{N}}${}$) $\wedge$ (({\it{j\/}} $\not=$ {\tt{'}}{\tt{0}}) $\wedge$ ({\it{j\/}} $<$ {\sc{i\$3}}\index{i\$3}))) \\ 
$\rightarrow$$\;\;\;\;$({\rm{elt1}}\,({\sc{blk-delta1\$3}}\index{blk-delta1\$3}, {\it{j\/}})\index{elt1} $=$ {\sc{maxi\$0}}\index{maxi\$0}))\-)\-)\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{lex}}\,(\=\+{\rm{cons}}\,(({\tt{'}}{\tt{2}} $+$ ({\sc{asize\&}}\index{asize\&} $+$ {\sc{maxi\$0}}\index{maxi\$0})) $-$ {\sc{i\$3}}\index{i\$3}, {\tt{'}}{\tt{nil}}), \\ 
{\rm{cons}}\,(({\tt{'}}{\tt{2}} $+$ ({\sc{asize\&}}\index{asize\&} $+$ {\sc{maxi\$0}}\index{maxi\$0})) $-$ {\sc{i\$1}}\index{i\$1}, {\tt{'}}{\tt{nil}}))\-\index{lex})\-\-
\end{tabbing}

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

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

\addvspace{18pt}

\begin{tabbing}{\sc Axiom}:  paths-from-pass2-invrt \\ \index{paths-from-pass2-invrt}
\=\+(({\it{j\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\sc{asize\&}}\index{asize\&} $\not<$ {\it{j\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{elt1}}\,({\sc{blk-delta1\$1}}\index{blk-delta1\$1}, {\it{j\/}})\index{elt1} \\ 
$=$$\;\;\;\;$({\rm{delta1}}\,({\sc{a\$0}}\index{a\$0}, {\it{j\/}}, {\sc{i\$1}}\index{i\$1} $-\;1$)\index{delta1} $+$ ({\sc{maxi\$0}}\index{maxi\$0} $-$ ({\sc{i\$1}}\index{i\$1} $-\;1$))))\-\-
\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$ (($1\;+$ {\sc{maxi\$0}}\index{maxi\$0}) $\not<$ {\sc{i\$1}}\index{i\$1}))))\-\-
\end{tabbing}

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

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

; (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{c\$2}}\index{c\$2} $=$ {\sc{c\$1}}\index{c\$1}) $\wedge$ ({\sc{blk-delta1\$2}}\index{blk-delta1\$2} $=$ {\sc{blk-delta1\$1}}\index{blk-delta1\$1})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  output \\ \index{output}
\=\+({\sc{i\$1}}\index{i\$1} $\wedge$ ({\rm{zgreaterp}}\,({\sc{i\$1}}\index{i\$1}, {\sc{maxi\$0}}\index{maxi\$0})\index{zgreaterp} $\wedge$ {\sc{path-hyps}}\index{path-hyps})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(({\it{c\/}} $\in\;${\bf{N}}${}$) $\wedge$ (({\it{c\/}} $\not=$ {\tt{'}}{\tt{0}}) $\wedge$ ({\sc{asize\&}}\index{asize\&} $\not<$ {\it{c\/}}))) \\ 
$\rightarrow$$\;\;\;\;$({\rm{elt1}}\,({\sc{blk-delta1\$2}}\index{blk-delta1\$2}, {\it{c\/}})\index{elt1} $=$ {\rm{delta1}}\,({\sc{a\$0}}\index{a\$0}, {\it{c\/}}, {\sc{maxi\$0}}\index{maxi\$0})\index{delta1}))\-\-
\end{tabbing}

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

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

\addvspace{18pt}

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

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

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

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

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

\end{verbatim}\begin{tabbing}{\sc Axiom}:  assignment1 \\ \index{assignment1}
\=\+({\sc{i\$2}}\index{i\$2} $=$ {\sc{i\$1}}\index{i\$1}) \\ 
$\wedge$$\;\;\;\;$(({\sc{c\$2}}\index{c\$2} $=$ {\rm{elt1}}\,({\sc{a\$0}}\index{a\$0}, {\sc{i\$1}}\index{i\$1})\index{elt1}) $\wedge$ ({\sc{blk-delta1\$2}}\index{blk-delta1\$2} $=$ {\sc{blk-delta1\$1}}\index{blk-delta1\$1}))\-
\end{tabbing}

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

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

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

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

\end{verbatim}\begin{tabbing}{\sc Axiom}:  assignment2 \\ \index{assignment2}
\=\+({\sc{i\$3}}\index{i\$3} $=$ {\sc{i\$2}}\index{i\$2}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{c\$3}}\index{c\$3} $=$ {\sc{c\$2}}\index{c\$2}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{elt1}}\,({\sc{blk-delta1\$3}}\index{blk-delta1\$3}, {\it{i\/}})\index{elt1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $=$ {\sc{c\$2}}\index{c\$2}$\;\;${\bf then }{\rm{zdifference}}\,({\sc{maxi\$0}}\index{maxi\$0}, {\sc{i\$2}}\index{i\$2})\index{zdifference} \\ 
{\bf else }{\rm{elt1}}\,({\sc{blk-delta1\$2}}\index{blk-delta1\$2}, {\it{i\/}})\index{elt1}$\;${\bf  endif}\-)\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  input-cond-of-zplus \\ \index{input-cond-of-zplus}
\=\+(\=\+{\rm{almost-equal1}}\,(\=\+{\sc{blk-delta1\$2}}\index{blk-delta1\$2}, \\ 
{\sc{blk-delta1\$3}}\index{blk-delta1\$3}, \\ 
{\tt{'}}{\tt{1}}, \\ 
{\sc{asize\&}}\index{asize\&}, \\ 
{\sc{c\$2}}\index{c\$2}, \\ 
{\rm{zdifference}}\,({\sc{maxi\$0}}\index{maxi\$0}, {\sc{i\$2}}\index{i\$2})\index{zdifference})\-\index{almost-equal1} \\ 
$\wedge$$\;\;\;\;$(($\neg$ {\rm{zgreaterp}}\,({\sc{i\$1}}\index{i\$1}, {\sc{maxi\$0}}\index{maxi\$0})\index{zgreaterp}) $\wedge$ {\sc{path-hyps}}\index{path-hyps}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{expressible-znumberp}}\,({\rm{zplus}}\,({\sc{i\$3}}\index{i\$3}, {\tt{'}}{\tt{1}})\index{zplus})\index{expressible-znumberp}\-
\end{tabbing}

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

\end{verbatim}\begin{tabbing}{\sc Axiom}:  assignment3 \\ \index{assignment3}
\=\+({\sc{i\$4}}\index{i\$4} $=$ {\rm{zplus}}\,({\sc{i\$3}}\index{i\$3}, {\tt{'}}{\tt{1}})\index{zplus}) \\ 
$\wedge$$\;\;\;\;$(({\sc{c\$4}}\index{c\$4} $=$ {\sc{c\$3}}\index{c\$3}) $\wedge$ ({\sc{blk-delta1\$4}}\index{blk-delta1\$4} $=$ {\sc{blk-delta1\$3}}\index{blk-delta1\$3}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  delta1-skip \\ \index{delta1-skip}
\=\+(({\it{j\/}} $\not=$ {\rm{elt1}}\,({\it{pat\/}}, {\it{i\/}})\index{elt1}) $\wedge$ ({\it{i\/}} $\not\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;$({\rm{delta1}}\,({\it{pat\/}}, {\it{j\/}}, {\it{i\/}})\index{delta1} $=$ ($1\;+$ {\rm{delta1}}\,({\it{pat\/}}, {\it{j\/}}, {\it{i\/}} $-\;1$)\index{delta1}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  pass2-invrt1 \\ \index{pass2-invrt1}
\=\+(\=\+{\rm{almost-equal1}}\,(\=\+{\sc{blk-delta1\$2}}\index{blk-delta1\$2}, \\ 
{\sc{blk-delta1\$3}}\index{blk-delta1\$3}, \\ 
{\tt{'}}{\tt{1}}, \\ 
{\sc{asize\&}}\index{asize\&}, \\ 
{\sc{c\$2}}\index{c\$2}, \\ 
{\rm{zdifference}}\,({\sc{maxi\$0}}\index{maxi\$0}, {\sc{i\$2}}\index{i\$2})\index{zdifference})\-\index{almost-equal1} \\ 
$\wedge$$\;\;\;\;$(($\neg$ {\rm{zgreaterp}}\,({\sc{i\$1}}\index{i\$1}, {\sc{maxi\$0}}\index{maxi\$0})\index{zgreaterp}) $\wedge$ {\sc{path-hyps}}\index{path-hyps}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+({\sc{i\$4}}\index{i\$4} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{i\$4}}\index{i\$4} $\not=$ {\tt{'}}{\tt{0}}) \\ 
$\wedge$$\;\;\;\;$(\=\+(($1\;+$ {\sc{maxi\$0}}\index{maxi\$0}) $\not<$ {\sc{i\$4}}\index{i\$4}) \\ 
$\wedge$$\;\;\;\;$(\=\+(({\it{j\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\sc{asize\&}}\index{asize\&} $\not<$ {\it{j\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{elt1}}\,({\sc{blk-delta1\$4}}\index{blk-delta1\$4}, {\it{j\/}})\index{elt1} \\ 
$=$$\;\;\;\;$(\=\+{\rm{delta1}}\,({\sc{a\$0}}\index{a\$0}, {\it{j\/}}, {\sc{i\$4}}\index{i\$4} $-\;1$)\index{delta1} \\ 
$+$$\;\;\;\;$(\=\+{\sc{maxi\$0}}\index{maxi\$0} \\ 
$-$$\;\;\;\;$({\sc{i\$4}}\index{i\$4} $-\;1$))\-)\-)\-)\-)\-)\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{lex}}\,(\=\+{\rm{cons}}\,(($1\;+$ {\sc{maxi\$0}}\index{maxi\$0}) $-$ {\sc{i\$4}}\index{i\$4}, {\tt{'}}{\tt{nil}}), \\ 
{\rm{cons}}\,(($1\;+$ {\sc{maxi\$0}}\index{maxi\$0}) $-$ {\sc{i\$1}}\index{i\$1}, {\tt{'}}{\tt{nil}}))\-\index{lex})\-\-
\end{tabbing}

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

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

\addvspace{18pt}


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

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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


\noindent{\sc Event}:   Introduce the function symbol {\it c\$4\index{c\$4}\/} 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 j\$0\index{j\$0}\/} of 0 arguments.

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}


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

\addvspace{18pt}

\begin{tabbing}{\sc Axiom}:  asize\&-numberp \\ \index{asize\&-numberp}
{\sc{asize\&}}\index{asize\&} $\in\;${\bf{N}}${}$
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{delta1} \\  
\=\+{\rm{delta1}}\,({\it{a\/}}, {\it{c\/}}, {\it{maxi\/}})\index{delta1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{maxi\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{c\/}} $=$ {\rm{elt1}}\,({\it{a\/}}, {\it{maxi\/}})\index{elt1}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }$1\;+$ {\rm{delta1}}\,({\it{a\/}}, {\it{c\/}}, {\it{maxi\/}} $-\;1$)\index{delta1}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{stringp} \\  
\=\+{\rm{stringp}}\,({\it{a\/}}, {\it{i\/}}, {\it{size\/}})\index{stringp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }\=\+({\rm{elt1}}\,({\it{a\/}}, {\it{i\/}})\index{elt1} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{elt1}}\,({\it{a\/}}, {\it{i\/}})\index{elt1} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{size\/}} $\not<$ {\rm{elt1}}\,({\it{a\/}}, {\it{i\/}})\index{elt1}) \\ 
$\wedge$$\;\;\;\;${\rm{stringp}}\,({\it{a\/}}, {\it{i\/}} $-\;1$, {\it{size\/}})\index{stringp}\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  stringp-is-a-univ-quantifier \\ \index{stringp-is-a-univ-quantifier}
\=\+({\rm{stringp}}\,({\it{a\/}}, {\it{i\/}}, {\sc{asize\&}}\index{asize\&})\index{stringp} $\wedge$ ({\it{j\/}} $\not=$ {\tt{0}}) $\wedge$ ({\it{j\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{i\/}} $\not<$ {\it{j\/}})) \\ 
$\rightarrow$$\;\;\;\;$(({\rm{elt1}}\,({\it{a\/}}, {\it{j\/}})\index{elt1} $\in\;${\bf{N}}${}$) $\wedge$ ({\sc{asize\&}}\index{asize\&} $\not<$ {\rm{elt1}}\,({\it{a\/}}, {\it{j\/}})\index{elt1}) $\wedge$ ({\rm{elt1}}\,({\it{a\/}}, {\it{j\/}})\index{elt1} $\not=$ {\tt{0}}))\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{match} \\  
\=\+{\rm{match}}\,({\it{pat\/}}, {\it{j\/}}, {\it{patlen\/}}, {\it{str\/}}, {\it{i\/}}, {\it{strlen\/}})\index{match} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{patlen\/}} $<$ {\it{j\/}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\it{strlen\/}} $<$ {\it{i\/}}$\;\;${\bf then }{\bf{f}} \\ 
{\bf else }\=\+({\rm{elt1}}\,({\it{pat\/}}, {\it{j\/}})\index{elt1} $=$ {\rm{elt1}}\,({\it{str\/}}, {\it{i\/}})\index{elt1}) \\ 
$\wedge$$\;\;\;\;${\rm{match}}\,({\it{pat\/}}, $1\;+$ {\it{j\/}}, {\it{patlen\/}}, {\it{str\/}}, $1\;+$ {\it{i\/}}, {\it{strlen\/}})\index{match}\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{search} \\  
\=\+{\rm{search}}\,({\it{pat\/}}, {\it{str\/}}, {\it{patlen\/}}, {\it{strlen\/}}, {\it{i\/}})\index{search} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{strlen\/}} $<$ {\it{i\/}}$\;\;${\bf then }$1\;+$ {\it{strlen\/}} \\ 
{\bf elseif }{\rm{match}}\,({\it{pat\/}}, {\tt{1}}, {\it{patlen\/}}, {\it{str\/}}, {\it{i\/}}, {\it{strlen\/}})\index{match}$\;\;${\bf then }{\it{i\/}} \\ 
{\bf else }{\rm{search}}\,({\it{pat\/}}, {\it{str\/}}, {\it{patlen\/}}, {\it{strlen\/}}, $1\;+$ {\it{i\/}})\index{search}$\;${\bf  endif}\-\-
\end{tabbing}

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

\begin{tabbing}{\sc Definition}:\index{global-hyps} \\  
\=\+{\sc{global-hyps}}\index{global-hyps} \\ 
$=$$\;\;\;\;$(\=\+({\sc{asize\&}}\index{asize\&} $\not=$ {\tt{'}}{\tt{0}}) \\ 
$\wedge$$\;\;\;\;$(\=\+(($1\;+$ {\sc{asize\&}}\index{asize\&}) $<$ {\sc{least-inexpressible-positive-integer}}\index{least-inexpressible-positive-inte!ger}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{stringp}}\,({\sc{pat\$0}}\index{pat\$0}, {\sc{patlen\$0}}\index{patlen\$0}, {\sc{asize\&}}\index{asize\&})\index{stringp} \\ 
$\wedge$$\;\;\;\;$(\=\+({\tt{'}}{\tt{0}} $<$ {\sc{patlen\$0}}\index{patlen\$0}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{stringp}}\,({\sc{str\$0}}\index{str\$0}, {\sc{strlen\$0}}\index{strlen\$0}, {\sc{asize\&}}\index{asize\&})\index{stringp} \\ 
$\wedge$$\;\;\;\;$(\=\+({\tt{'}}{\tt{0}} $<$ {\sc{strlen\$0}}\index{strlen\$0}) \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+(\=\+{\sc{patlen\$0}}\index{patlen\$0} \\ 
$+$$\;\;\;\;${\sc{strlen\$0}}\index{strlen\$0})\- \\ 
$<$$\;\;\;\;${\sc{least-inexpressible-positive-integer}}\index{least-inexpressible-positive-inte!ger})\- \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{patlen\$0}}\index{patlen\$0} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\sc{strlen\$0}}\index{strlen\$0} $\in\;${\bf{N}}${}$))\-)\-)\-)\-)\-)\-)\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  search-non-zero \\ \index{search-non-zero}
({\it{i\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ ({\tt{0}} $<$ {\rm{search}}\,({\it{pat\/}}, {\it{str\/}}, {\it{patlen\/}}, {\it{strlen\/}}, {\it{i\/}})\index{search})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  match-at-patlen \\ \index{match-at-patlen}
({\it{patlen\/}} $<$ {\it{j\/}}) $\rightarrow$ {\rm{match}}\,({\it{pat\/}}, {\it{j\/}}, {\it{patlen\/}}, {\it{str\/}}, {\it{i\/}}, {\it{strlen\/}})\index{match}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  match-at-strlen \\ \index{match-at-strlen}
({\it{strlen\/}} $<$ {\it{i\/}}) $\rightarrow$ ({\rm{match}}\,({\it{pat\/}}, {\it{j\/}}, {\it{patlen\/}}, {\it{str\/}}, {\it{i\/}}, {\it{strlen\/}})\index{match} $=$ ({\it{patlen\/}} $<$ {\it{j\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  match-needs-patlen-chars \\ \index{match-needs-patlen-chars}
\=\+(\=\+({\it{patlen\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{strlen\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{patlen\/}} $\not<$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{strlen\/}} $\not<$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;$(({\it{j\/}} $+$ {\it{strlen\/}}) $<$ ({\it{i\/}} $+$ {\it{patlen\/}})))\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{match}}\,({\it{pat\/}}, {\it{j\/}}, {\it{patlen\/}}, {\it{str\/}}, {\it{i\/}}, {\it{strlen\/}})\index{match})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  search-boundary \\ \index{search-boundary}
\=\+(\=\+({\it{patlen\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{strlen\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{strlen\/}} $\not<$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;$(($1\;+$ {\it{strlen\/}}) $<$ ({\it{patlen\/}} $+$ {\rm{search}}\,({\it{pat\/}}, {\it{str\/}}, {\it{patlen\/}}, {\it{strlen\/}}, {\it{i\/}})\index{search})))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{search}}\,({\it{pat\/}}, {\it{str\/}}, {\it{patlen\/}}, {\it{strlen\/}}, {\it{i\/}})\index{search} $=$ ($1\;+$ {\it{strlen\/}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  delta1-lesseqp-patlen \\ \index{delta1-lesseqp-patlen}
{\it{patlen\/}} $\not<$ {\rm{delta1}}\,({\it{pat\/}}, {\it{char\/}}, {\it{patlen\/}})\index{delta1}
\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 Theorem}:  call-of-setup \\ \index{call-of-setup}
\=\+({\sc{patlen\$0}}\index{patlen\$0} $\wedge$ {\sc{global-hyps}}\index{global-hyps}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{stringp}}\,({\sc{pat\$0}}\index{pat\$0}, {\sc{patlen\$0}}\index{patlen\$0}, {\sc{asize\&}}\index{asize\&})\index{stringp} \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{patlen\$0}}\index{patlen\$0} $\not=$ {\tt{'}}{\tt{0}}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{patlen\$0}}\index{patlen\$0} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+($1\;+$ {\sc{asize\&}}\index{asize\&}) \\ 
$<$$\;\;\;\;${\sc{least-inexpressible-positive-integer}}\index{least-inexpressible-positive-inte!ger})\- \\ 
$\wedge$$\;\;\;\;$(\=\+($1\;+$ {\sc{patlen\$0}}\index{patlen\$0}) \\ 
$<$$\;\;\;\;${\sc{least-inexpressible-positive-integer}}\index{least-inexpressible-positive-inte!ger})\-)\-)\-)\-)\-\-
\end{tabbing}

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

\end{verbatim}\begin{tabbing}{\sc Axiom}:  effects-of-setup \\ \index{effects-of-setup}
\=\+(\=\+(({\it{c\/}} $\in\;${\bf{N}}${}$) $\wedge$ (({\it{c\/}} $\not=$ {\tt{'}}{\tt{0}}) $\wedge$ ({\sc{asize\&}}\index{asize\&} $\not<$ {\it{c\/}}))) \\ 
$\rightarrow$$\;\;\;\;$({\rm{elt1}}\,({\sc{blk-delta1\$1}}\index{blk-delta1\$1}, {\it{c\/}})\index{elt1} $=$ {\rm{delta1}}\,({\sc{pat\$0}}\index{pat\$0}, {\it{c\/}}, {\sc{patlen\$0}}\index{patlen\$0})\index{delta1}))\- \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{i\$1}}\index{i\$1} $=$ {\sc{i\$0}}\index{i\$0}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{j\$1}}\index{j\$1} $=$ {\sc{j\$0}}\index{j\$0}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{c\$1}}\index{c\$1} $=$ {\sc{c\$0}}\index{c\$0}) \\ 
$\wedge$$\;\;\;\;$(({\sc{nexti\$1}}\index{nexti\$1} $=$ {\sc{nexti\$0}}\index{nexti\$0}) $\wedge$ ({\sc{x\$1}}\index{x\$1} $=$ {\sc{x\$0}}\index{x\$0})))\-)\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Axiom}:  assignment \\ \index{assignment}
\=\+({\sc{i\$2}}\index{i\$2} $=$ {\sc{patlen\$0}}\index{patlen\$0}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{j\$2}}\index{j\$2} $=$ {\sc{j\$1}}\index{j\$1}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{c\$2}}\index{c\$2} $=$ {\sc{c\$1}}\index{c\$1}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{nexti\$2}}\index{nexti\$2} $=$ {\sc{nexti\$1}}\index{nexti\$1}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{x\$2}}\index{x\$2} $=$ {\sc{x\$1}}\index{x\$1}) \\ 
$\wedge$$\;\;\;\;$({\sc{blk-delta1\$2}}\index{blk-delta1\$2} $=$ {\sc{blk-delta1\$1}}\index{blk-delta1\$1}))\-)\-)\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  outer-invrt \\ \index{outer-invrt}
\=\+({\sc{patlen\$0}}\index{patlen\$0} $\wedge$ {\sc{global-hyps}}\index{global-hyps}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+({\sc{i\$2}}\index{i\$2} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{i\$2}}\index{i\$2} $\not<$ {\sc{patlen\$0}}\index{patlen\$0}) \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\sc{i\$2}}\index{i\$2} \\ 
$<$$\;\;\;\;$(\=\+{\sc{patlen\$0}}\index{patlen\$0} \\ 
$+$$\;\;\;\;${\rm{search}}\,(\=\+{\sc{pat\$0}}\index{pat\$0}, \\ 
{\sc{str\$0}}\index{str\$0}, \\ 
{\sc{patlen\$0}}\index{patlen\$0}, \\ 
{\sc{strlen\$0}}\index{strlen\$0}, \\ 
{\tt{'}}{\tt{1}})\-\index{search})\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+({\it{c\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$(({\it{c\/}} $\not=$ {\tt{'}}{\tt{0}}) $\wedge$ ({\sc{asize\&}}\index{asize\&} $\not<$ {\it{c\/}})))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{elt1}}\,({\sc{blk-delta1\$2}}\index{blk-delta1\$2}, {\it{c\/}})\index{elt1} \\ 
$=$$\;\;\;\;${\rm{delta1}}\,({\sc{pat\$0}}\index{pat\$0}, {\it{c\/}}, {\sc{patlen\$0}}\index{patlen\$0})\index{delta1})\-)\-)\-)\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{lex}}\,(\=\+{\rm{cons}}\,(\=\+({\tt{'}}{\tt{1}} $+$ ({\sc{strlen\$0}}\index{strlen\$0} $+$ {\sc{patlen\$0}}\index{patlen\$0})) $-$ {\sc{i\$2}}\index{i\$2}, \\ 
{\rm{cons}}\,($1\;+$ {\sc{patlen\$0}}\index{patlen\$0}, {\tt{'}}{\tt{nil}}))\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{1}} $+$ ({\sc{strlen\$0}}\index{strlen\$0} $+$ {\sc{patlen\$0}}\index{patlen\$0}), \\ 
{\rm{cons}}\,($1\;+$ {\sc{patlen\$0}}\index{patlen\$0}, {\tt{'}}{\tt{nil}}))\-)\-\index{lex})\-\-
\end{tabbing}

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

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

\addvspace{18pt}

\begin{tabbing}{\sc Axiom}:  paths-from-outer-invrt \\ \index{paths-from-outer-invrt}
\=\+(({\it{c\/}} $\in\;${\bf{N}}${}$) $\wedge$ (({\it{c\/}} $\not=$ {\tt{'}}{\tt{0}}) $\wedge$ ({\sc{asize\&}}\index{asize\&} $\not<$ {\it{c\/}}))) \\ 
$\rightarrow$$\;\;\;\;$({\rm{elt1}}\,({\sc{blk-delta1\$1}}\index{blk-delta1\$1}, {\it{c\/}})\index{elt1} $=$ {\rm{delta1}}\,({\sc{pat\$0}}\index{pat\$0}, {\it{c\/}}, {\sc{patlen\$0}}\index{patlen\$0})\index{delta1})\-
\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<$ {\sc{patlen\$0}}\index{patlen\$0}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\sc{i\$1}}\index{i\$1} \\ 
$<$$\;\;\;\;$(\=\+{\sc{patlen\$0}}\index{patlen\$0} \\ 
$+$$\;\;\;\;${\rm{search}}\,(\=\+{\sc{pat\$0}}\index{pat\$0}, \\ 
{\sc{str\$0}}\index{str\$0}, \\ 
{\sc{patlen\$0}}\index{patlen\$0}, \\ 
{\sc{strlen\$0}}\index{strlen\$0}, \\ 
{\tt{'}}{\tt{1}})\-\index{search})\-)\-)\-)\-)\-\-
\end{tabbing}

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

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

; (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{zgreaterp}}\,({\sc{i\$1}}\index{i\$1}, {\sc{strlen\$0}}\index{strlen\$0})\index{zgreaterp} $\wedge$ {\sc{path-hyps}}\index{path-hyps}) \\ 
$\rightarrow$$\;\;\;\;${\rm{expressible-znumberp}}\,({\rm{zplus}}\,({\sc{strlen\$0}}\index{strlen\$0}, {\tt{'}}{\tt{1}})\index{zplus})\index{expressible-znumberp}\-
\end{tabbing}

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

\end{verbatim}\begin{tabbing}{\sc Axiom}:  assignment1 \\ \index{assignment1}
\=\+({\sc{i\$2}}\index{i\$2} $=$ {\sc{i\$1}}\index{i\$1}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{j\$2}}\index{j\$2} $=$ {\sc{j\$1}}\index{j\$1}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{c\$2}}\index{c\$2} $=$ {\sc{c\$1}}\index{c\$1}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{nexti\$2}}\index{nexti\$2} $=$ {\sc{nexti\$1}}\index{nexti\$1}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{x\$2}}\index{x\$2} $=$ {\rm{zplus}}\,({\sc{strlen\$0}}\index{strlen\$0}, {\tt{'}}{\tt{1}})\index{zplus}) \\ 
$\wedge$$\;\;\;\;$({\sc{blk-delta1\$2}}\index{blk-delta1\$2} $=$ {\sc{blk-delta1\$1}}\index{blk-delta1\$1}))\-)\-)\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  output \\ \index{output}
\=\+({\rm{zgreaterp}}\,({\sc{i\$1}}\index{i\$1}, {\sc{strlen\$0}}\index{strlen\$0})\index{zgreaterp} $\wedge$ {\sc{path-hyps}}\index{path-hyps}) \\ 
$\rightarrow$$\;\;\;\;$({\sc{x\$2}}\index{x\$2} $=$ {\rm{search}}\,({\sc{pat\$0}}\index{pat\$0}, {\sc{str\$0}}\index{str\$0}, {\sc{patlen\$0}}\index{patlen\$0}, {\sc{strlen\$0}}\index{strlen\$0}, {\tt{'}}{\tt{1}})\index{search})\-
\end{tabbing}

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

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

\addvspace{18pt}

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

\begin{tabbing}{\sc Axiom}:  assignment1 \\ \index{assignment1}
\=\+({\sc{i\$2}}\index{i\$2} $=$ {\sc{i\$1}}\index{i\$1}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{j\$2}}\index{j\$2} $=$ {\sc{patlen\$0}}\index{patlen\$0}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{c\$2}}\index{c\$2} $=$ {\sc{c\$1}}\index{c\$1}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{nexti\$2}}\index{nexti\$2} $=$ {\sc{nexti\$1}}\index{nexti\$1}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{x\$2}}\index{x\$2} $=$ {\sc{x\$1}}\index{x\$1}) \\ 
$\wedge$$\;\;\;\;$({\sc{blk-delta1\$2}}\index{blk-delta1\$2} $=$ {\sc{blk-delta1\$1}}\index{blk-delta1\$1}))\-)\-)\-)\-\-
\end{tabbing}

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

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

\end{verbatim}\begin{tabbing}{\sc Axiom}:  assignment2 \\ \index{assignment2}
\=\+({\sc{i\$3}}\index{i\$3} $=$ {\sc{i\$2}}\index{i\$2}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{j\$3}}\index{j\$3} $=$ {\sc{j\$2}}\index{j\$2}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{c\$3}}\index{c\$3} $=$ {\sc{c\$2}}\index{c\$2}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{nexti\$3}}\index{nexti\$3} $=$ {\rm{zplus}}\,({\tt{'}}{\tt{1}}, {\sc{i\$2}}\index{i\$2})\index{zplus}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{x\$3}}\index{x\$3} $=$ {\sc{x\$2}}\index{x\$2}) \\ 
$\wedge$$\;\;\;\;$({\sc{blk-delta1\$3}}\index{blk-delta1\$3} $=$ {\sc{blk-delta1\$2}}\index{blk-delta1\$2}))\-)\-)\-)\-\-
\end{tabbing}

%\item 
\begin{verbatim}


(PROVE-LEMMA INNER-INVRT NIL
 (IMPLIES
  (AND (NOT (ZGREATERP (I$1) (STRLEN$0)))
       (PATH-HYPS))
  (AND
   (AND
    (NOT (LESSP (NEXTI$3) (ADD1 (PATLEN$0))))
    (AND
     (LESSP (NEXTI$3)
            (ADD1 (PLUS (PATLEN$0)
                        (SEARCH (PAT$0)
                                (STR$0)
                                (PATLEN$0)
                                (STRLEN$0)
                                '1))))
     (AND
      (IMPLIES (AND (NUMBERP C)
                    (AND (NOT (EQUAL C '0))
                         (NOT (LESSP (ASIZE&) C))))
               (EQUAL (ELT1 (BLK-DELTA1$3) C)
                      (DELTA1 (PAT$0) C (PATLEN$0))))
      (AND
       (NUMBERP (I$3))
       (AND
        (NOT (EQUAL (I$3) '0))
        (AND
         (NUMBERP (J$3))
         (AND
          (NOT (EQUAL (J$3) '0))
          (AND
           (NUMBERP (NEXTI$3))
           (AND
            (NOT (LESSP (PATLEN$0) (J$3)))
            (AND
             (NOT (LESSP (STRLEN$0) (I$3)))
             (AND
              (EQUAL (NEXTI$3)
                     (PLUS (ADD1 (PATLEN$0))
                           (DIFFERENCE (I$3) (J$3))))
              (AND
               (NOT (LESSP (ADD1 (STRLEN$0)) (NEXTI$3)))
               (AND
                  (NOT (LESSP (I$3) (J$3)))
                  (AND (MATCH (PAT$0)
                              (ADD1 (J$3))
                              (PATLEN$0)
                              (STR$0)
                              (ADD1 (I$3))
                              (STRLEN$0))
                       (AND (NUMBERP (ELT1 (BLK-DELTA1$3)
                                           (ELT1 (STR$0) (I$3))))
                            (AND (NUMBERP (ELT1 (STR$0) (I$3)))
                                 (NUMBERP (ELT1 (PAT$0) (J$3)))))))))))))))))))
   (LEX (CONS (DIFFERENCE (PLUS '1
                                (PLUS (STRLEN$0) (PATLEN$0)))
                          (SUB1 (NEXTI$3)))
              (CONS (J$3) 'NIL))
        (CONS (DIFFERENCE (PLUS '1
                                (PLUS (STRLEN$0) (PATLEN$0)))
                          (I$1))
              (CONS (ADD1 (PATLEN$0)) 'NIL))))))
\end{verbatim}


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

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

\addvspace{18pt}

\begin{tabbing}{\sc Axiom}:  paths-from-inner-invrt \\ \index{paths-from-inner-invrt}
\=\+(\=\+(({\it{c\/}} $\in\;${\bf{N}}${}$) $\wedge$ (({\it{c\/}} $\not=$ {\tt{'}}{\tt{0}}) $\wedge$ ({\sc{asize\&}}\index{asize\&} $\not<$ {\it{c\/}}))) \\ 
$\rightarrow$$\;\;\;\;$({\rm{elt1}}\,({\sc{blk-delta1\$1}}\index{blk-delta1\$1}, {\it{c\/}})\index{elt1} $=$ {\rm{delta1}}\,({\sc{pat\$0}}\index{pat\$0}, {\it{c\/}}, {\sc{patlen\$0}}\index{patlen\$0})\index{delta1}))\- \\ 
$\wedge$$\;\;\;\;$({\sc{nexti\$1}}\index{nexti\$1} $=$ (($1\;+$ {\sc{patlen\$0}}\index{patlen\$0}) $+$ ({\sc{i\$1}}\index{i\$1} $-$ {\sc{j\$1}}\index{j\$1})))\-
\end{tabbing}

%\item 
\begin{verbatim}


(DEFN PATH-HYPS NIL
 (AND
  (GLOBAL-HYPS)
  (AND
   (NOT (LESSP (NEXTI$1) (ADD1 (PATLEN$0))))
   (AND
    (LESSP (NEXTI$1)
           (ADD1 (PLUS (PATLEN$0)
                       (SEARCH (PAT$0)
                               (STR$0)
                               (PATLEN$0)
                               (STRLEN$0)
                               '1))))
    (AND
     (NUMBERP (I$1))
     (AND
      (NOT (EQUAL (I$1) '0))
      (AND
       (NUMBERP (J$1))
       (AND
        (NOT (EQUAL (J$1) '0))
        (AND
         (NUMBERP (NEXTI$1))
         (AND
          (NOT (LESSP (PATLEN$0) (J$1)))
          (AND
           (NOT (LESSP (STRLEN$0) (I$1)))
           (AND
             (NOT (LESSP (ADD1 (STRLEN$0)) (NEXTI$1)))
             (AND (NOT (LESSP (I$1) (J$1)))
                  (AND (MATCH (PAT$0)
                              (ADD1 (J$1))
                              (PATLEN$0)
                              (STR$0)
                              (ADD1 (I$1))
                              (STRLEN$0))
                       (AND (NUMBERP (ELT1 (BLK-DELTA1$1)
                                           (ELT1 (STR$0) (I$1))))
                            (AND (NUMBERP (ELT1 (STR$0) (I$1)))
                                 (NUMBERP (ELT1 (PAT$0) (J$1)))))))))))))))))))
\end{verbatim}


\begin{tabbing}{\sc Theorem}:  array-bounds-check-for-str \\ \index{array-bounds-check-for-str}
{\sc{path-hyps}}\index{path-hyps} $\rightarrow$ (({\tt{'}}{\tt{0}} $<$ {\sc{i\$1}}\index{i\$1}) $\wedge$ ({\sc{strlen\$0}}\index{strlen\$0} $\not<$ {\sc{i\$1}}\index{i\$1}))
\end{tabbing}

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

\end{verbatim}\begin{tabbing}{\sc Theorem}:  definedness \\ \index{definedness}
{\sc{path-hyps}}\index{path-hyps} $\rightarrow$ {\rm{znumberp}}\,({\rm{elt1}}\,({\sc{str\$0}}\index{str\$0}, {\sc{i\$1}}\index{i\$1})\index{elt1})\index{znumberp}
\end{tabbing}

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

\end{verbatim}\begin{tabbing}{\sc Axiom}:  assignment1 \\ \index{assignment1}
\=\+({\sc{i\$2}}\index{i\$2} $=$ {\sc{i\$1}}\index{i\$1}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{j\$2}}\index{j\$2} $=$ {\sc{j\$1}}\index{j\$1}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{c\$2}}\index{c\$2} $=$ {\rm{elt1}}\,({\sc{str\$0}}\index{str\$0}, {\sc{i\$1}}\index{i\$1})\index{elt1}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{nexti\$2}}\index{nexti\$2} $=$ {\sc{nexti\$1}}\index{nexti\$1}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{x\$2}}\index{x\$2} $=$ {\sc{x\$1}}\index{x\$1}) \\ 
$\wedge$$\;\;\;\;$({\sc{blk-delta1\$2}}\index{blk-delta1\$2} $=$ {\sc{blk-delta1\$1}}\index{blk-delta1\$1}))\-)\-)\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  array-bounds-check-for-pat \\ \index{array-bounds-check-for-pat}
{\sc{path-hyps}}\index{path-hyps} $\rightarrow$ (({\tt{'}}{\tt{0}} $<$ {\sc{j\$2}}\index{j\$2}) $\wedge$ ({\sc{patlen\$0}}\index{patlen\$0} $\not<$ {\sc{j\$2}}\index{j\$2}))
\end{tabbing}

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

\end{verbatim}\begin{tabbing}{\sc Theorem}:  definedness1 \\ \index{definedness1}
{\sc{path-hyps}}\index{path-hyps} $\rightarrow$ {\rm{znumberp}}\,({\rm{elt1}}\,({\sc{pat\$0}}\index{pat\$0}, {\sc{j\$2}}\index{j\$2})\index{elt1})\index{znumberp}
\end{tabbing}

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

; (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-delta1 \\ \index{array-bounds-check-for-delta1}
\=\+({\rm{zneqp}}\,({\sc{c\$2}}\index{c\$2}, {\rm{elt1}}\,({\sc{pat\$0}}\index{pat\$0}, {\sc{j\$2}}\index{j\$2})\index{elt1})\index{zneqp} $\wedge$ {\sc{path-hyps}}\index{path-hyps}) \\ 
$\rightarrow$$\;\;\;\;$(({\tt{'}}{\tt{0}} $<$ {\sc{c\$2}}\index{c\$2}) $\wedge$ ({\sc{asize\&}}\index{asize\&} $\not<$ {\sc{c\$2}}\index{c\$2}))\-
\end{tabbing}

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

\end{verbatim}\begin{tabbing}{\sc Theorem}:  definedness2 \\ \index{definedness2}
\=\+({\rm{zneqp}}\,({\sc{c\$2}}\index{c\$2}, {\rm{elt1}}\,({\sc{pat\$0}}\index{pat\$0}, {\sc{j\$2}}\index{j\$2})\index{elt1})\index{zneqp} $\wedge$ {\sc{path-hyps}}\index{path-hyps}) \\ 
$\rightarrow$$\;\;\;\;${\rm{znumberp}}\,({\rm{elt1}}\,({\sc{blk-delta1\$2}}\index{blk-delta1\$2}, {\sc{c\$2}}\index{c\$2})\index{elt1})\index{znumberp}\-
\end{tabbing}

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

\end{verbatim}\begin{tabbing}{\sc Theorem}:  input-cond-of-zplus \\ \index{input-cond-of-zplus}
\=\+({\rm{zneqp}}\,({\sc{c\$2}}\index{c\$2}, {\rm{elt1}}\,({\sc{pat\$0}}\index{pat\$0}, {\sc{j\$2}}\index{j\$2})\index{elt1})\index{zneqp} $\wedge$ {\sc{path-hyps}}\index{path-hyps}) \\ 
$\rightarrow$$\;\;\;\;${\rm{expressible-znumberp}}\,({\rm{zplus}}\,({\sc{i\$2}}\index{i\$2}, {\rm{elt1}}\,({\sc{blk-delta1\$2}}\index{blk-delta1\$2}, {\sc{c\$2}}\index{c\$2})\index{elt1})\index{zplus})\index{expressible-znumberp}\-
\end{tabbing}

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

\end{verbatim}\begin{tabbing}{\sc Theorem}:  definedness3 \\ \index{definedness3}
({\rm{zneqp}}\,({\sc{c\$2}}\index{c\$2}, {\rm{elt1}}\,({\sc{pat\$0}}\index{pat\$0}, {\sc{j\$2}}\index{j\$2})\index{elt1})\index{zneqp} $\wedge$ {\sc{path-hyps}}\index{path-hyps}) $\rightarrow$ {\rm{znumberp}}\,({\sc{nexti\$2}}\index{nexti\$2})\index{znumberp}
\end{tabbing}

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

\end{verbatim}\begin{tabbing}{\sc Axiom}:  assignment2 \\ \index{assignment2}
\=\+({\sc{i\$3}}\index{i\$3} $=$ {\rm{max0}}\,({\rm{zplus}}\,({\sc{i\$2}}\index{i\$2}, {\rm{elt1}}\,({\sc{blk-delta1\$2}}\index{blk-delta1\$2}, {\sc{c\$2}}\index{c\$2})\index{elt1})\index{zplus}, {\sc{nexti\$2}}\index{nexti\$2})\index{max0}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{j\$3}}\index{j\$3} $=$ {\sc{j\$2}}\index{j\$2}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{c\$3}}\index{c\$3} $=$ {\sc{c\$2}}\index{c\$2}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{nexti\$3}}\index{nexti\$3} $=$ {\sc{nexti\$2}}\index{nexti\$2}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{x\$3}}\index{x\$3} $=$ {\sc{x\$2}}\index{x\$2}) \\ 
$\wedge$$\;\;\;\;$({\sc{blk-delta1\$3}}\index{blk-delta1\$3} $=$ {\sc{blk-delta1\$2}}\index{blk-delta1\$2}))\-)\-)\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  delta1-plus-j-lesseqp-patlen \\ \index{delta1-plus-j-lesseqp-patlen}
\=\+(({\it{j\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{j\/}} $\not=$ {\tt{0}}) $\wedge$ ({\it{patlen\/}} $\not<$ {\it{j\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\it{patlen\/}} $\not<$ ({\it{j\/}} $+$ {\rm{delta1}}\,({\it{pat\/}}, {\rm{elt1}}\,({\it{pat\/}}, {\it{j\/}})\index{elt1}, {\it{patlen\/}})\index{delta1}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  difference-plus-id \\ \index{difference-plus-id}
(({\it{k\/}} $+$ {\it{j\/}}) $-$ {\it{j\/}}) $=$ {\rm{fix}}\,({\it{k\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  match-implies-eq-chars \\ \index{match-implies-eq-chars}
\=\+(\=\+{\rm{match}}\,({\it{pat\/}}, {\it{j\/}}, {\it{patlen\/}}, {\it{str\/}}, {\it{k\/}}, {\it{strlen\/}})\index{match} \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{patlen\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{strlen\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{strlen\/}} $\not<$ {\it{k\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{patlen\/}} $\not<$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $\not<$ {\it{k\/}}) \\ 
$\wedge$$\;\;\;\;$(({\it{k\/}} $+$ {\it{patlen\/}}) $\not<$ ({\it{j\/}} $+$ {\it{l\/}})))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{elt1}}\,({\it{str\/}}, {\it{l\/}})\index{elt1} $=$ {\rm{elt1}}\,({\it{pat\/}}, ({\it{j\/}} $+$ {\it{l\/}}) $-$ {\it{k\/}})\index{elt1})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  neq-chars-in-region-means-search-skips \\ \index{neq-chars-in-region-means-searc!h-skips}
\=\+(\=\+({\rm{elt1}}\,({\it{str\/}}, {\it{i\/}})\index{elt1} $\not=$ {\rm{elt1}}\,({\it{pat\/}}, {\it{j\/}})\index{elt1}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{strlen\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{strlen\/}} $\not<$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{patlen\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{patlen\/}} $\not<$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not<$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{strlen\/}} $\not<$ {\it{k\/}}) \\ 
$\wedge$$\;\;\;\;$(({\rm{search}}\,({\it{pat\/}}, {\it{str\/}}, {\it{patlen\/}}, {\it{strlen\/}}, {\it{k\/}})\index{search} $-\;1$) $\not<$ ({\it{i\/}} $-$ {\it{j\/}})))\- \\ 
$\rightarrow$$\;\;\;\;$(({\it{i\/}} $-$ {\it{j\/}}) $<$ ({\rm{search}}\,({\it{pat\/}}, {\it{str\/}}, {\it{patlen\/}}, {\it{strlen\/}}, {\it{k\/}})\index{search} $-\;1$))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  delta1-doesnt-go-beyond-end-of-match \\ \index{delta1-doesnt-go-beyond-end-of-!match}
\=\+(\=\+{\rm{match}}\,({\it{pat\/}}, {\tt{1}}, {\it{patlen\/}}, {\it{str\/}}, {\it{k\/}}, {\it{strlen\/}})\index{match} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{strlen\/}} $\not<$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{patlen\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{strlen\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ ({\it{k\/}} $+$ {\it{patlen\/}})))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(({\it{i\/}} $+$ {\rm{delta1}}\,({\it{pat\/}}, {\rm{elt1}}\,({\it{str\/}}, {\it{i\/}})\index{elt1}, {\it{patlen\/}})\index{delta1}) $<$ ({\it{k\/}} $+$ {\it{patlen\/}})) \\ 
$=$$\;\;\;\;$(({\it{i\/}} $<$ {\it{k\/}}) $\vee$ ({\it{i\/}} $=$ {\it{k\/}}) $\vee$ ({\it{k\/}} $<$ {\it{i\/}})))\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable match-implies-eq-chars.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  delta1-doesnt-go-beyond-search \\ \index{delta1-doesnt-go-beyond-search}
\=\+(\=\+({\rm{elt1}}\,({\it{str\/}}, {\it{i\/}})\index{elt1} $\not=$ {\rm{elt1}}\,({\it{pat\/}}, {\it{j\/}})\index{elt1}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{strlen\/}} $\not<$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{patlen\/}} $\not<$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{patlen\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{strlen\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$(({\it{i\/}} $-$ {\it{j\/}}) $<$ {\rm{search}}\,({\it{pat\/}}, {\it{str\/}}, {\it{patlen\/}}, {\it{strlen\/}}, {\it{k\/}})\index{search}) \\ 
$\wedge$$\;\;\;\;$({\it{strlen\/}} $\not<$ {\it{k\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not<$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $\not=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\it{i\/}} $+$ {\rm{delta1}}\,({\it{pat\/}}, {\rm{elt1}}\,({\it{str\/}}, {\it{i\/}})\index{elt1}, {\it{patlen\/}})\index{delta1}) \\ 
$<$$\;\;\;\;$({\it{patlen\/}} $+$ {\rm{search}}\,({\it{pat\/}}, {\it{str\/}}, {\it{patlen\/}}, {\it{strlen\/}}, {\it{k\/}})\index{search}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  outer-invrt1 \\ \index{outer-invrt1}
\=\+({\rm{zneqp}}\,({\sc{c\$2}}\index{c\$2}, {\rm{elt1}}\,({\sc{pat\$0}}\index{pat\$0}, {\sc{j\$2}}\index{j\$2})\index{elt1})\index{zneqp} $\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<$ {\sc{patlen\$0}}\index{patlen\$0}) \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\sc{i\$3}}\index{i\$3} \\ 
$<$$\;\;\;\;$(\=\+{\sc{patlen\$0}}\index{patlen\$0} \\ 
$+$$\;\;\;\;${\rm{search}}\,(\=\+{\sc{pat\$0}}\index{pat\$0}, \\ 
{\sc{str\$0}}\index{str\$0}, \\ 
{\sc{patlen\$0}}\index{patlen\$0}, \\ 
{\sc{strlen\$0}}\index{strlen\$0}, \\ 
{\tt{'}}{\tt{1}})\-\index{search})\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+({\it{c\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$(({\it{c\/}} $\not=$ {\tt{'}}{\tt{0}}) $\wedge$ ({\sc{asize\&}}\index{asize\&} $\not<$ {\it{c\/}})))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{elt1}}\,({\sc{blk-delta1\$3}}\index{blk-delta1\$3}, {\it{c\/}})\index{elt1} \\ 
$=$$\;\;\;\;${\rm{delta1}}\,({\sc{pat\$0}}\index{pat\$0}, {\it{c\/}}, {\sc{patlen\$0}}\index{patlen\$0})\index{delta1})\-)\-)\-)\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{lex}}\,(\=\+{\rm{cons}}\,(\=\+({\tt{'}}{\tt{1}} $+$ ({\sc{strlen\$0}}\index{strlen\$0} $+$ {\sc{patlen\$0}}\index{patlen\$0})) $-$ {\sc{i\$3}}\index{i\$3}, \\ 
{\rm{cons}}\,($1\;+$ {\sc{patlen\$0}}\index{patlen\$0}, {\tt{'}}{\tt{nil}}))\-, \\ 
{\rm{cons}}\,(\=\+({\tt{'}}{\tt{1}} $+$ ({\sc{strlen\$0}}\index{strlen\$0} $+$ {\sc{patlen\$0}}\index{patlen\$0})) $-$ ({\sc{nexti\$1}}\index{nexti\$1} $-\;1$), \\ 
{\rm{cons}}\,({\sc{j\$1}}\index{j\$1}, {\tt{'}}{\tt{nil}}))\-)\-\index{lex})\-\-
\end{tabbing}

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

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

\addvspace{18pt}

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

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

\begin{tabbing}{\sc Theorem}:  first-match-is-search \\ \index{first-match-is-search}
\=\+(\=\+{\rm{match}}\,({\it{pat\/}}, {\tt{1}}, {\it{patlen\/}}, {\it{str\/}}, {\it{i\/}}, {\it{strlen\/}})\index{match} \\ 
$\wedge$$\;\;\;\;$({\it{strlen\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{strlen\/}} $\not<$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not<$ {\it{k\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{search}}\,({\it{pat\/}}, {\it{str\/}}, {\it{patlen\/}}, {\it{strlen\/}}, {\it{k\/}})\index{search} $\not<$ {\it{i\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$(({\it{i\/}} $=$ {\rm{search}}\,({\it{pat\/}}, {\it{str\/}}, {\it{patlen\/}}, {\it{strlen\/}}, {\it{k\/}})\index{search}) $=$ {\bf{t}})\-
\end{tabbing}

\begin{tabbing}{\sc Axiom}:  assignment2 \\ \index{assignment2}
\=\+({\sc{i\$3}}\index{i\$3} $=$ {\sc{i\$2}}\index{i\$2}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{j\$3}}\index{j\$3} $=$ {\sc{j\$2}}\index{j\$2}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{c\$3}}\index{c\$3} $=$ {\sc{c\$2}}\index{c\$2}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{nexti\$3}}\index{nexti\$3} $=$ {\sc{nexti\$2}}\index{nexti\$2}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{x\$3}}\index{x\$3} $=$ {\sc{i\$2}}\index{i\$2}) \\ 
$\wedge$$\;\;\;\;$({\sc{blk-delta1\$3}}\index{blk-delta1\$3} $=$ {\sc{blk-delta1\$2}}\index{blk-delta1\$2}))\-)\-)\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  output \\ \index{output}
\=\+({\rm{zeqp}}\,({\sc{j\$2}}\index{j\$2}, {\tt{'}}{\tt{1}})\index{zeqp} $\wedge$ (($\neg$ {\rm{zneqp}}\,({\sc{c\$2}}\index{c\$2}, {\rm{elt1}}\,({\sc{pat\$0}}\index{pat\$0}, {\sc{j\$2}}\index{j\$2})\index{elt1})\index{zneqp}) $\wedge$ {\sc{path-hyps}}\index{path-hyps})) \\ 
$\rightarrow$$\;\;\;\;$({\sc{x\$3}}\index{x\$3} $=$ {\rm{search}}\,({\sc{pat\$0}}\index{pat\$0}, {\sc{str\$0}}\index{str\$0}, {\sc{patlen\$0}}\index{patlen\$0}, {\sc{strlen\$0}}\index{strlen\$0}, {\tt{'}}{\tt{1}})\index{search})\-
\end{tabbing}

\begin{verbatim}#| (COMMENT INNER-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-F1)
\end{verbatim}\begin{tabbing}{\sc Axiom}:  logical-if-f1 \\ \index{logical-if-f1}
{\bf{t}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  input-cond-of-zdifference \\ \index{input-cond-of-zdifference}
\=\+(($\neg$ {\rm{zeqp}}\,({\sc{j\$2}}\index{j\$2}, {\tt{'}}{\tt{1}})\index{zeqp}) $\wedge$ (($\neg$ {\rm{zneqp}}\,({\sc{c\$2}}\index{c\$2}, {\rm{elt1}}\,({\sc{pat\$0}}\index{pat\$0}, {\sc{j\$2}}\index{j\$2})\index{elt1})\index{zneqp}) $\wedge$ {\sc{path-hyps}}\index{path-hyps})) \\ 
$\rightarrow$$\;\;\;\;${\rm{expressible-znumberp}}\,({\rm{zdifference}}\,({\sc{j\$2}}\index{j\$2}, {\tt{'}}{\tt{1}})\index{zdifference})\index{expressible-znumberp}\-
\end{tabbing}

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

\end{verbatim}\begin{tabbing}{\sc Axiom}:  assignment2 \\ \index{assignment2}
\=\+({\sc{i\$3}}\index{i\$3} $=$ {\sc{i\$2}}\index{i\$2}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{j\$3}}\index{j\$3} $=$ {\rm{zdifference}}\,({\sc{j\$2}}\index{j\$2}, {\tt{'}}{\tt{1}})\index{zdifference}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{c\$3}}\index{c\$3} $=$ {\sc{c\$2}}\index{c\$2}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{nexti\$3}}\index{nexti\$3} $=$ {\sc{nexti\$2}}\index{nexti\$2}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{x\$3}}\index{x\$3} $=$ {\sc{x\$2}}\index{x\$2}) \\ 
$\wedge$$\;\;\;\;$({\sc{blk-delta1\$3}}\index{blk-delta1\$3} $=$ {\sc{blk-delta1\$2}}\index{blk-delta1\$2}))\-)\-)\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  input-cond-of-zdifference1 \\ \index{input-cond-of-zdifference1}
\=\+(($\neg$ {\rm{zeqp}}\,({\sc{j\$2}}\index{j\$2}, {\tt{'}}{\tt{1}})\index{zeqp}) $\wedge$ (($\neg$ {\rm{zneqp}}\,({\sc{c\$2}}\index{c\$2}, {\rm{elt1}}\,({\sc{pat\$0}}\index{pat\$0}, {\sc{j\$2}}\index{j\$2})\index{elt1})\index{zneqp}) $\wedge$ {\sc{path-hyps}}\index{path-hyps})) \\ 
$\rightarrow$$\;\;\;\;${\rm{expressible-znumberp}}\,({\rm{zdifference}}\,({\sc{i\$3}}\index{i\$3}, {\tt{'}}{\tt{1}})\index{zdifference})\index{expressible-znumberp}\-
\end{tabbing}

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

\end{verbatim}\begin{tabbing}{\sc Axiom}:  assignment3 \\ \index{assignment3}
\=\+({\sc{i\$4}}\index{i\$4} $=$ {\rm{zdifference}}\,({\sc{i\$3}}\index{i\$3}, {\tt{'}}{\tt{1}})\index{zdifference}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{j\$4}}\index{j\$4} $=$ {\sc{j\$3}}\index{j\$3}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{c\$4}}\index{c\$4} $=$ {\sc{c\$3}}\index{c\$3}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{nexti\$4}}\index{nexti\$4} $=$ {\sc{nexti\$3}}\index{nexti\$3}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\sc{x\$4}}\index{x\$4} $=$ {\sc{x\$3}}\index{x\$3}) \\ 
$\wedge$$\;\;\;\;$({\sc{blk-delta1\$4}}\index{blk-delta1\$4} $=$ {\sc{blk-delta1\$3}}\index{blk-delta1\$3}))\-)\-)\-)\-\-
\end{tabbing}

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

%\item 
\begin{verbatim}


(PROVE-LEMMA INNER-INVRT1 NIL
 (IMPLIES
  (AND (NOT (ZEQP (J$2) '1))
       (AND (NOT (ZNEQP (C$2) (ELT1 (PAT$0) (J$2))))
            (PATH-HYPS)))
  (AND
   (AND
    (NOT (LESSP (NEXTI$4) (ADD1 (PATLEN$0))))
    (AND
     (LESSP (NEXTI$4)
            (ADD1 (PLUS (PATLEN$0)
                        (SEARCH (PAT$0)
                                (STR$0)
                                (PATLEN$0)
                                (STRLEN$0)
                                '1))))
     (AND
      (IMPLIES (AND (NUMBERP C)
                    (AND (NOT (EQUAL C '0))
                         (NOT (LESSP (ASIZE&) C))))
               (EQUAL (ELT1 (BLK-DELTA1$4) C)
                      (DELTA1 (PAT$0) C (PATLEN$0))))
      (AND
       (NUMBERP (I$4))
       (AND
        (NOT (EQUAL (I$4) '0))
        (AND
         (NUMBERP (J$4))
         (AND
          (NOT (EQUAL (J$4) '0))
          (AND
           (NUMBERP (NEXTI$4))
           (AND
            (NOT (LESSP (PATLEN$0) (J$4)))
            (AND
             (NOT (LESSP (STRLEN$0) (I$4)))
             (AND
              (EQUAL (NEXTI$4)
                     (PLUS (ADD1 (PATLEN$0))
                           (DIFFERENCE (I$4) (J$4))))
              (AND
               (NOT (LESSP (ADD1 (STRLEN$0)) (NEXTI$4)))
               (AND
                  (NOT (LESSP (I$4) (J$4)))
                  (AND (MATCH (PAT$0)
                              (ADD1 (J$4))
                              (PATLEN$0)
                              (STR$0)
                              (ADD1 (I$4))
                              (STRLEN$0))
                       (AND (NUMBERP (ELT1 (BLK-DELTA1$4)
                                           (ELT1 (STR$0) (I$4))))
                            (AND (NUMBERP (ELT1 (STR$0) (I$4)))
                                 (NUMBERP (ELT1 (PAT$0) (J$4)))))))))))))))))))
   (LEX (CONS (DIFFERENCE (PLUS '1
                                (PLUS (STRLEN$0) (PATLEN$0)))
                          (SUB1 (NEXTI$4)))
              (CONS (J$4) 'NIL))
        (CONS (DIFFERENCE (PLUS '1
                                (PLUS (STRLEN$0) (PATLEN$0)))
                          (SUB1 (NEXTI$1)))
              (CONS (J$1) 'NIL))))))
\end{verbatim}


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

\end{verbatim}
\noindent{\sc Event}:   Undo back through the event named `paths-from-inner-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.
        (DELTA1 A C MAXI)
           =
        (IF (ZEROP MAXI)
            0
            (IF (EQUAL C (ELT1 A MAXI))
                0
                (ADD1 (DELTA1 A C (SUB1 MAXI)))))
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Definition.
        (STRINGP A I SIZE)
           =
        (IF (ZEROP I)
            T
            (AND (NUMBERP (ELT1 A I))
                 (NOT (EQUAL (ELT1 A I) 0))
                 (NOT (LESSP SIZE (ELT1 A I)))
                 (STRINGP A (SUB1 I) SIZE)))
@END(VERBATIM)
@END(GROUP)

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

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Definition.
        (MATCH PAT J PATLEN STR I STRLEN)
           =
        (IF (LESSP PATLEN J)
            T
            (IF (LESSP STRLEN I)
                F
                (AND (EQUAL (ELT1 PAT J) (ELT1 STR I))
                     (MATCH PAT
                            (ADD1 J)
                            PATLEN STR
                            (ADD1 I)
                            STRLEN))))
        Hint:  ((LESSP (DIFFERENCE (ADD1 PATLEN) J))
                (LESSP (DIFFERENCE (ADD1 STRLEN) I)))
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Definition.
        (SEARCH PAT STR PATLEN STRLEN I)
           =
        (IF (LESSP STRLEN I)
            (ADD1 STRLEN)
            (IF (MATCH PAT 1 PATLEN STR I STRLEN)
                I
                (SEARCH PAT STR PATLEN STRLEN
                        (ADD1 I))))
        Hint:  Consider the well-founded relation LESSP
               and the measure (DIFFERENCE (ADD1 STRLEN) I)
@END(VERBATIM)
@END(GROUP)

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


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

Specification for routine SETUP

The input assertion:
        (AND (STRINGP (A STATE)
                      (MAXI STATE)
                      (ASIZE&))
             (NOT (EQUAL (MAXI STATE) 0))
             (NUMBERP (MAXI STATE))
             (LESSP (ADD1 (ASIZE&))
                    (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
             (LESSP (ADD1 (MAXI STATE))
                    (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))


The output assertion:
        (IMPLIES (AND (NUMBERP C)
                      (NOT (EQUAL C 0))
                      (NOT (LESSP (ASIZE&) C)))
                 (EQUAL (ELT1 (BLK-DELTA1 NEWSTATE) C)
                        (DELTA1 (A STATE) C (MAXI STATE))))
\end{verbatim}
\newpage
\begin{verbatim}

Specification for routine FSRCH

The input assertion:
        (AND (LESSP (ADD1 (ASIZE&))
                    (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
             (STRINGP (PAT STATE)
                      (PATLEN STATE)
                      (ASIZE&))
             (NUMBERP (PATLEN STATE))
             (LESSP 0 (PATLEN STATE))
             (STRINGP (STR STATE)
                      (STRLEN STATE)
                      (ASIZE&))
             (NUMBERP (STRLEN STATE))
             (LESSP 0 (STRLEN STATE))
             (LESSP (PLUS (PATLEN STATE) (STRLEN STATE))
                    (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))


The output assertion:
        (EQUAL (X NEWSTATE)
               (SEARCH (PAT STATE)
                       (STR STATE)
                       (PATLEN STATE)
                       (STRLEN STATE)
                       1))
\end{verbatim}
\newpage
\begin{verbatim}

      INTEGER DELTA1
      DIMENSION DELTA1(ASIZE&)
      COMMON /BLK/DELTA1
      END
      SUBROUTINE SETUP(A, MAXI)
      INTEGER DELTA1
      INTEGER A
      INTEGER MAXI
      INTEGER I
      INTEGER C
      DIMENSION DELTA1(ASIZE&)
      DIMENSION A(MAXI)
      COMMON /BLK/DELTA1
      DO 50 I = 1, ASIZE&
C     DOJUNK PASS1
      DELTA1(I) = MAXI
50    CONTINUE
      DO 100 I = 1, MAXI
C     DOJUNK PASS2
      C = A(I)
      DELTA1(C) = (MAXI - I)
100   CONTINUE
      RETURN
      END
      SUBROUTINE FSRCH(PAT, STR, PATLEN, STRLEN, X)
      INTEGER DELTA1
      INTEGER MAX0
      INTEGER PATLEN
      INTEGER STRLEN
      INTEGER PAT
      INTEGER STR
      INTEGER I
      INTEGER J
      INTEGER C
      INTEGER NEXTI
      INTEGER X
      DIMENSION DELTA1(ASIZE&)
      DIMENSION PAT(PATLEN)
      DIMENSION STR(STRLEN)
      COMMON /BLK/DELTA1
      CALL SETUP(PAT, PATLEN)
      I = PATLEN
200   CONTINUE
C     XXX INNER-TO-OUTER-HINTS
      CONTINUE
C     ASSERTION OUTER-INVRT
      IF ((I .GT. STRLEN)) GOTO 500
      J = PATLEN
      NEXTI = (1 + I)
300   CONTINUE
C     ASSERTION INNER-INVRT
      C = STR(I)
      IF ((C .NE. PAT(J))) GOTO 400
      IF ((J .EQ. 1)) GOTO 600
      J = (J - 1)
      I = (I - 1)
C     XXX INNER-TO-INNER-HINTS
      GOTO 300
400   I = MAX0((I + DELTA1(C)), NEXTI)
      GOTO 200
500   X = (STRLEN + 1)
      RETURN
600   CONTINUE
C     XXX INNER-TO-EXIT-HINTS
      X = I
      RETURN
      END


The XXX at USEFUL-LEMMAS.
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  STRINGP-IS-A-UNIV-QUANTIFIER (rewrite):
        (IMPLIES (AND (STRINGP A I (ASIZE&))
                      (NOT (EQUAL J 0))
                      (NUMBERP J)
                      (NOT (LESSP I J)))
                 (AND (NUMBERP (ELT1 A J))
                      (NOT (LESSP (ASIZE&) (ELT1 A J)))
                      (NOT (EQUAL (ELT1 A J) 0))))
@END(VERBATIM)
@END(GROUP)



The XXX at USEFUL-LEMMAS-ABOUT-SEARCHING.
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  SEARCH-NON-ZERO (rewrite):
        (IMPLIES (NOT (ZEROP I))
                 (LESSP 0
                        (SEARCH PAT STR PATLEN STRLEN I)))
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  MATCH-AT-PATLEN (rewrite):
        (IMPLIES (LESSP PATLEN J)
                 (MATCH PAT J PATLEN STR I STRLEN))
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  MATCH-AT-STRLEN (rewrite):
        (IMPLIES (LESSP STRLEN I)
                 (EQUAL (MATCH PAT J PATLEN STR I STRLEN)
                        (LESSP PATLEN J)))
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  MATCH-NEEDS-PATLEN-CHARS (rewrite):
        (IMPLIES (AND (NUMBERP PATLEN)
                      (NUMBERP STRLEN)
                      (NOT (LESSP PATLEN J))
                      (NOT (LESSP STRLEN I))
                      (LESSP (PLUS J STRLEN)
                             (PLUS I PATLEN)))
                 (NOT (MATCH PAT J PATLEN STR I STRLEN)))
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  SEARCH-BOUNDARY (rewrite):
        (IMPLIES
               (AND (NOT (ZEROP PATLEN))
                    (NUMBERP STRLEN)
                    (NOT (LESSP STRLEN I))
                    (LESSP (ADD1 STRLEN)
                           (PLUS PATLEN
                                 (SEARCH PAT STR PATLEN STRLEN I))))
               (EQUAL (SEARCH PAT STR PATLEN STRLEN I)
                      (ADD1 STRLEN)))
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  DELTA1-LESSEQP-PATLEN (rewrite):
        (NOT (LESSP PATLEN
                    (DELTA1 PAT CHAR PATLEN)))
@END(VERBATIM)
@END(GROUP)


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

Hints for routine SETUP

                              

The input clock:
        (LIST (PLUS 2 (ASIZE&) (MAXI (START))))

The DO junk named PASS1:
        ((TEST PASS1-INVRT))

The invariant and clock named PASS1-INVRT.

        (AND (NUMBERP (I STATE))
             (NOT (EQUAL (I STATE) 0))
             (NOT (LESSP (ADD1 (ASIZE&)) (I STATE)))
             (IMPLIES (AND (NUMBERP J)
                           (NOT (EQUAL J 0))
                           (LESSP J (I STATE)))
                      (EQUAL (ELT1 (BLK-DELTA1 STATE) J)
                             (MAXI (START)))))

        (LIST (DIFFERENCE (PLUS 2 (ASIZE&) (MAXI (START)))
                          (I STATE)))

The DO junk named PASS2:
        ((TEST PASS2-INVRT)
         (JUMP PASS2-TO-PASS2-HINT))

The invariant and clock named PASS2-INVRT.

        (AND (NUMBERP (I STATE))
             (NOT (EQUAL (I STATE) 0))
             (NOT (LESSP (ADD1 (MAXI (START)))
                         (I STATE)))
             (IMPLIES (AND (NOT (ZEROP J))
                           (NOT (LESSP (ASIZE&) J)))
                      (EQUAL (ELT1 (BLK-DELTA1 STATE) J)
                             (PLUS (DELTA1 (A (START))
                                           J
                                           (SUB1 (I STATE)))
                                   (DIFFERENCE (MAXI (START))
                                               (SUB1 (I STATE)))))))

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

The XXX named PASS2-TO-PASS2-HINT:
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  DELTA1-SKIP (rewrite):
        (IMPLIES (AND (NOT (EQUAL J (ELT1 PAT I)))
                      (NOT (ZEROP I)))
                 (EQUAL (DELTA1 PAT J I)
                        (ADD1 (DELTA1 PAT J (SUB1 I)))))
@END(VERBATIM)
@END(GROUP)


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

Hints for routine FSRCH

                              

The input clock:
        (LIST (PLUS 1
                    (STRLEN (START))
                    (PATLEN (START)))
              (ADD1 (PATLEN (START))))

The XXX named INNER-TO-OUTER-HINTS:
        Path encryption:
        ((INNER-INVRT T))
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  DELTA1-PLUS-J-LESSEQP-PATLEN (rewrite):
        (IMPLIES
              (AND (NUMBERP J)
                   (NOT (EQUAL J 0))
                   (NOT (LESSP PATLEN J)))
              (NOT (LESSP PATLEN
                          (PLUS J
                                (DELTA1 PAT (ELT1 PAT J) PATLEN)))))
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  DIFFERENCE-PLUS-ID (rewrite):
        (EQUAL (DIFFERENCE (PLUS K J) J)
               (FIX K))
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  MATCH-IMPLIES-EQ-CHARS (rewrite):
        (IMPLIES (AND (MATCH PAT J PATLEN STR K STRLEN)
                      (NUMBERP K)
                      (NUMBERP J)
                      (NUMBERP PATLEN)
                      (NUMBERP STRLEN)
                      (NOT (LESSP STRLEN K))
                      (NOT (LESSP PATLEN J))
                      (NOT (EQUAL K 0))
                      (NOT (EQUAL J 0))
                      (NUMBERP L)
                      (NOT (LESSP L K))
                      (NOT (LESSP (PLUS K PATLEN) (PLUS J L))))
                 (EQUAL (ELT1 STR L)
                        (ELT1 PAT (DIFFERENCE (PLUS J L) K))))
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  NEQ-CHARS-IN-REGION-MEANS-SEARCH-SKIPS (rewrite):
        (IMPLIES
            (AND (NOT (EQUAL (ELT1 STR I) (ELT1 PAT J)))
                 (NUMBERP I)
                 (NOT (EQUAL I 0))
                 (NUMBERP STRLEN)
                 (NOT (LESSP STRLEN I))
                 (NUMBERP J)
                 (NOT (EQUAL J 0))
                 (NUMBERP PATLEN)
                 (NOT (LESSP PATLEN J))
                 (NOT (LESSP I J))
                 (NUMBERP K)
                 (NOT (EQUAL K 0))
                 (NOT (LESSP STRLEN K))
                 (NOT (LESSP (SUB1 (SEARCH PAT STR PATLEN STRLEN K))
                             (DIFFERENCE I J))))
            (LESSP (DIFFERENCE I J)
                   (SUB1 (SEARCH PAT STR PATLEN STRLEN K))))
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  DELTA1-DOESNT-GO-BEYOND-END-OF-MATCH (rewrite):
        (IMPLIES
               (AND (MATCH PAT 1 PATLEN STR K STRLEN)
                    (NUMBERP I)
                    (NOT (LESSP STRLEN I))
                    (NUMBERP PATLEN)
                    (NUMBERP STRLEN)
                    (NUMBERP K)
                    (NOT (EQUAL K 0))
                    (LESSP I (PLUS K PATLEN)))
               (EQUAL (LESSP (PLUS I
                                   (DELTA1 PAT (ELT1 STR I) PATLEN))
                             (PLUS K PATLEN))
                      (OR (LESSP I K)
                          (EQUAL I K)
                          (LESSP K I))))
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Enable MATCH-IMPLIES-EQ-CHARS.
@END(VERBATIM)
@END(GROUP)

@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  DELTA1-DOESNT-GO-BEYOND-SEARCH (rewrite):
        (IMPLIES (AND (NOT (EQUAL (ELT1 STR I) (ELT1 PAT J)))
                      (NUMBERP I)
                      (NOT (LESSP STRLEN I))
                      (NUMBERP J)
                      (NOT (LESSP PATLEN J))
                      (NUMBERP PATLEN)
                      (NUMBERP STRLEN)
                      (LESSP (DIFFERENCE I J)
                             (SEARCH PAT STR PATLEN STRLEN K))
                      (NOT (LESSP STRLEN K))
                      (NOT (LESSP I J))
                      (NUMBERP K)
                      (NOT (EQUAL K 0)))
                 (LESSP (PLUS I
                              (DELTA1 PAT (ELT1 STR I) PATLEN))
                        (PLUS PATLEN
                              (SEARCH PAT STR PATLEN STRLEN K))))
@END(VERBATIM)
@END(GROUP)



The invariant and clock named OUTER-INVRT.

        (AND (NUMBERP (I STATE))
             (NOT (LESSP (I STATE) (PATLEN (START))))
             (LESSP (I STATE)
                    (PLUS (PATLEN (START))
                          (SEARCH (PAT (START))
                                  (STR (START))
                                  (PATLEN (START))
                                  (STRLEN (START))
                                  1)))
             (IMPLIES (AND (NUMBERP C)
                           (NOT (EQUAL C 0))
                           (NOT (LESSP (ASIZE&) C)))
                      (EQUAL (ELT1 (BLK-DELTA1 STATE) C)
                             (DELTA1 (PAT (START))
                                     C
                                     (PATLEN (START))))))

        (LIST (DIFFERENCE (PLUS 1
                                (STRLEN (START))
                                (PATLEN (START)))
                          (I STATE))
              (ADD1 (PATLEN (START))))

The invariant and clock named INNER-INVRT.

        (AND (NOT (LESSP (NEXTI STATE)
                         (ADD1 (PATLEN (START)))))
             (LESSP (NEXTI STATE)
                    (ADD1 (PLUS (PATLEN (START))
                                (SEARCH (PAT (START))
                                        (STR (START))
                                        (PATLEN (START))
                                        (STRLEN (START))
                                        1))))
             (IMPLIES (AND (NUMBERP C)
                           (NOT (EQUAL C 0))
                           (NOT (LESSP (ASIZE&) C)))
                      (EQUAL (ELT1 (BLK-DELTA1 STATE) C)
                             (DELTA1 (PAT (START))
                                     C
                                     (PATLEN (START)))))
             (NUMBERP (I STATE))
             (NOT (EQUAL (I STATE) 0))
             (NUMBERP (J STATE))
             (NOT (EQUAL (J STATE) 0))
             (NUMBERP (NEXTI STATE))
             (NOT (LESSP (PATLEN (START)) (J STATE)))
             (NOT (LESSP (STRLEN (START)) (I STATE)))
             (EQUAL (NEXTI STATE)
                    (PLUS (ADD1 (PATLEN (START)))
                          (DIFFERENCE (I STATE) (J STATE))))
             (NOT (LESSP (ADD1 (STRLEN (START)))
                         (NEXTI STATE)))
             (NOT (LESSP (I STATE) (J STATE)))
             (MATCH (PAT (START))
                    (ADD1 (J STATE))
                    (PATLEN (START))
                    (STR (START))
                    (ADD1 (I STATE))
                    (STRLEN (START)))
             (NUMBERP (ELT1 (BLK-DELTA1 STATE)
                            (ELT1 (STR (START)) (I STATE))))
             (NUMBERP (ELT1 (STR (START)) (I STATE)))
             (NUMBERP (ELT1 (PAT (START)) (J STATE))))

        (LIST (DIFFERENCE (PLUS 1
                                (STRLEN (START))
                                (PATLEN (START)))
                          (SUB1 (NEXTI STATE)))
              (J STATE))

The XXX named INNER-TO-INNER-HINTS:
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  OPEN-UP-DIFFERENCE (rewrite):
        (EQUAL (DIFFERENCE X 1) (SUB1 X))
@END(VERBATIM)
@END(GROUP)



The XXX named INNER-TO-EXIT-HINTS:
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  FIRST-MATCH-IS-SEARCH (rewrite):
        (IMPLIES (AND (MATCH PAT 1 PATLEN STR I STRLEN)
                      (NUMBERP STRLEN)
                      (NUMBERP I)
                      (NOT (LESSP STRLEN I))
                      (NUMBERP K)
                      (NOT (LESSP I K))
                      (NOT (EQUAL K 0))
                      (NOT (LESSP (SEARCH PAT STR PATLEN STRLEN K)
                                  I)))
                 (EQUAL (EQUAL I
                               (SEARCH PAT STR PATLEN STRLEN K))
                        T))
@END(VERBATIM)
@END(GROUP)

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