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

\begin{verbatim}#|

 Copyright (C) 1994 by Yuan Yu.  All Rights Reserved.

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

 NO WARRANTY

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

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

|#

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

\addvspace{18pt}

\begin{verbatim};          Proof of the Correctness of the STRSTR Function
#|
This is part of our effort to verify the Berkeley string library.  The 
Berkeley string library is widely used as part of the Berkeley Unix OS.

This is the source code of strstr function in the Berkeley string library.

/* find pointer to first occurrence of find[] in s[] */
char *
strstr(s, find)
	register const char *s, *find;
{
	register char c, sc;
	register size_t len;

	if ((c = *find++) != 0) {
		len = strlen(find);
		do {
			do {
				if ((sc = *s++) == 0)
					return (NULL);
			} while (sc != c);
		} while (strncmp(s, find, len) != 0);
		s--;
	}
	return ((char *)s);
}

The MC68020 assembly code of the C function strstr on SUN-3 is given as 
follows.  This binary is generated by "gcc -O".

0x2718 <strstr>:        linkw fp,#0
0x271c <strstr+4>:      moveml d2-d3/a2-a3,sp@-
0x2720 <strstr+8>:      moveal fp@(8),a2
0x2724 <strstr+12>:     moveal fp@(12),a3
0x2728 <strstr+16>:     moveb a3@+,d2
0x272a <strstr+18>:     beq 0x275a <strstr+66>
0x272c <strstr+20>:     movel a3,sp@-
0x272e <strstr+22>:     jsr @#0x25b0 <strlen>
0x2734 <strstr+28>:     movel d0,d3
0x2736 <strstr+30>:     addqw #4,sp
0x2738 <strstr+32>:     moveb a2@+,d0
0x273a <strstr+34>:     bne 0x2740 <strstr+40>
0x273c <strstr+36>:     clrl d0
0x273e <strstr+38>:     bra 0x275c <strstr+68>
0x2740 <strstr+40>:     cmpb d0,d2
0x2742 <strstr+42>:     bne 0x2738 <strstr+32>
0x2744 <strstr+44>:     movel d3,sp@-
0x2746 <strstr+46>:     movel a3,sp@-
0x2748 <strstr+48>:     movel a2,sp@-
0x274a <strstr+50>:     jsr @#0x2608 <strncmp>
0x2750 <strstr+56>:     addaw #12,sp
0x2754 <strstr+60>:     tstl d0
0x2756 <strstr+62>:     bne 0x2738 <strstr+32>
0x2758 <strstr+64>:     subqw #1,a2
0x275a <strstr+66>:     movel a2,d0
0x275c <strstr+68>:     moveml fp@(-16),d2-d3/a2-a3
0x2762 <strstr+74>:     unlk fp
0x2764 <strstr+76>:     rts

The machine code of the above program is:

<strstr>:      0x4e56  0x0000  0x48e7  0x3030  0x246e  0x0008  0x266e  0x000c
<strstr+16>:   0x141b  0x672e  0x2f0b  0x4eb9  0x0000  0x25b0  0x2600  0x584f
<strstr+32>:   0x101a  0x6604  0x4280  0x601c  0xb400  0x66f4  0x2f03  0x2f0b
<strstr+48>:   0x2f0a  0x4eb9  0x0000  0x2608  0xdefc  0x000c  0x4a80  0x66e0
<strstr+64>:   0x534a  0x200a  0x4cee  0x0c0c  0xfff0  0x4e5e  0x4e75

'(78      86      0       0       72      231     48      48
  36      110     0       8       38      110     0       12
  20      27      103     46      47      11      78      185
  0       0       37      176     38      0       88      79
  16      26      102     4       66      128     96      28
  180     0       102     244     47      3       47      11
  47      10      78      185     0       0       38      8
  222     252     0       12      74      128     102     224
  83      74      32      10      76      238     12      12
  255     240     78      94      78      117)
|#

; in the logic, the above program is defined by (strstr-code).
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{strstr-code} \\  
\=\+{\sc{strstr-code}}\index{strstr-code} \\ 
$=$$\;\;\;\;${\tt{'}}{\tt{(}}\=\+{\tt{78}}{\tt{ }}{\tt{86}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{72}}{\tt{ }}{\tt{231}}{\tt{ }}{\tt{48}}{\tt{ }}{\tt{48}}{\tt{ }}{\tt{36}}{\tt{ }}{\tt{110}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{8}}{\tt{ }}{\tt{38}}{\tt{ }}{\tt{110}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{12}}{\tt{ }}{\tt{20}}{\tt{ }}{\tt{27}} \\ 
{\tt{103}}{\tt{ }}{\tt{46}}{\tt{ }}{\tt{47}}{\tt{ }}{\tt{11}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{185}}{\tt{ }}{\tt{-1}}{\tt{ }}{\tt{-1}}{\tt{ }}{\tt{-1}}{\tt{ }}{\tt{-1}}{\tt{ }}{\tt{38}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{88}}{\tt{ }}{\tt{79}}{\tt{ }}{\tt{16}}{\tt{ }}{\tt{26}}{\tt{ }}{\tt{102}} \\ 
{\tt{4}}{\tt{ }}{\tt{66}}{\tt{ }}{\tt{128}}{\tt{ }}{\tt{96}}{\tt{ }}{\tt{28}}{\tt{ }}{\tt{180}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{102}}{\tt{ }}{\tt{244}}{\tt{ }}{\tt{47}}{\tt{ }}{\tt{3}}{\tt{ }}{\tt{47}}{\tt{ }}{\tt{11}}{\tt{ }}{\tt{47}}{\tt{ }}{\tt{10}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{185}} \\ 
{\tt{-1}}{\tt{ }}{\tt{-1}}{\tt{ }}{\tt{-1}}{\tt{ }}{\tt{-1}}{\tt{ }}{\tt{222}}{\tt{ }}{\tt{252}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{12}}{\tt{ }}{\tt{74}}{\tt{ }}{\tt{128}}{\tt{ }}{\tt{102}}{\tt{ }}{\tt{224}}{\tt{ }}{\tt{83}}{\tt{ }}{\tt{74}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{10}} \\ 
{\tt{76}}{\tt{ }}{\tt{238}}{\tt{ }}{\tt{12}}{\tt{ }}{\tt{12}}{\tt{ }}{\tt{255}}{\tt{ }}{\tt{240}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{94}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{117}}{\tt{)}}\-\-
\end{tabbing}

\begin{tabbing}{\sc Conservative Axiom}:  strstr-load \\ \index{strstr-load}
\=\+{\rm{strstr-loadp}}\,({\it{s\/}})\index{strstr-loadp} \\ 
$=$$\;\;\;\;$(\=\+{\rm{evenp}}\,({\sc{strstr-addr}}\index{strstr-addr})\index{evenp} \\ 
$\wedge$$\;\;\;\;$({\sc{strstr-addr}}\index{strstr-addr} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{nat-rangep}}\,({\sc{strstr-addr}}\index{strstr-addr}, {\tt{32}})\index{nat-rangep} \\ 
$\wedge$$\;\;\;\;${\rm{rom-addrp}}\,({\sc{strstr-addr}}\index{strstr-addr}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{78}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\sc{strstr-addr}}\index{strstr-addr}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{strstr-code}}\index{strstr-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{strlen-loadp}}\,({\it{s\/}})\index{strlen-loadp} \\ 
$\wedge$$\;\;\;\;${\rm{strncmp-loadp}}\,({\it{s\/}})\index{strncmp-loadp} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{pc-read-mem}}\,({\rm{add}}\,({\tt{32}}, {\sc{strstr-addr}}\index{strstr-addr}, {\tt{24}})\index{add}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{pc-read-mem} \\ 
$=$$\;\;\;\;${\sc{strlen-addr}}\index{strlen-addr})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{pc-read-mem}}\,({\rm{add}}\,({\tt{32}}, {\sc{strstr-addr}}\index{strstr-addr}, {\tt{52}})\index{add}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{pc-read-mem} \\ 
$=$$\;\;\;\;${\sc{strncmp-addr}}\index{strncmp-addr})\-)\-\-
\end{tabbing}\noindent Simultaneously, we introduce the new function symbols {\it strstr-loadp\/} and {\it strstr-addr\/}.

\begin{tabbing}{\sc Theorem}:  stepn-strstr-loadp \\ \index{stepn-strstr-loadp}
{\rm{strstr-loadp}}\,({\rm{stepn}}\,({\it{s\/}}, {\it{n\/}})\index{stepn})\index{strstr-loadp} $=$ {\rm{strstr-loadp}}\,({\it{s\/}})\index{strstr-loadp}
\end{tabbing}

\begin{verbatim}; the computation time of the program.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{strstr-t0} \\  
{\rm{strstr-t0}}\,({\it{n2\/}}, {\it{lst2\/}})\index{strstr-t0} $=$ {\rm{splus}}\,({\tt{8}}, {\rm{splus}}\,({\rm{strlen-t}}\,({\it{n2\/}} $-\;1$, {\rm{cdr}}\,({\it{lst2\/}}))\index{strlen-t}, {\tt{2}})\index{splus})\index{splus}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{strstr-t1} \\  
\=\+{\rm{strstr-t1}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strstr-t1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $<$ {\it{n1\/}} \\ 
{\bf then }\=\+{\bf if }{\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\tt{0}}$\;\;${\bf then }{\tt{7}} \\ 
{\bf elseif }{\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth}$\;\;${\bf then }{\tt{8}} \\ 
{\bf else }{\rm{splus}}\,({\tt{4}}, {\rm{strstr-t1}}\,($1\;+$ {\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strstr-t1})\index{splus}$\;${\bf  endif}\- \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{strstr-t2} \\  
\=\+{\rm{strstr-t2}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-t2} \\ 
$=$$\;\;\;\;$\=\+{\bf let }\=\+{\it{j\/}}{\bf $\;$ be$\;\;$}{\rm{strchr1}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth})\index{strchr1}\- \\ 
{\bf in} \\ 
\=\+{\bf if }{\it{j\/}} $\in\;${\bf{N}}${}$ \\ 
{\bf then }\=\+{\bf if }{\rm{strncmp}}\,({\it{len\/}}, {\rm{mcdr}}\,($1\;+$ {\it{j\/}}, {\it{lst1\/}})\index{mcdr}, {\rm{mcdr}}\,({\tt{1}}, {\it{lst2\/}})\index{mcdr})\index{strncmp} $=$ {\tt{0}} \\ 
{\bf then }{\rm{splus}}\,(\=\+{\rm{strstr-t1}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strstr-t1}, \\ 
{\rm{splus}}\,(\=\+{\rm{strncmp-t}}\,(\=\+{\it{len\/}}, \\ 
{\rm{mcdr}}\,($1\;+$ {\it{j\/}}, {\it{lst1\/}})\index{mcdr}, \\ 
{\rm{mcdr}}\,({\tt{1}}, {\it{lst2\/}})\index{mcdr})\-\index{strncmp-t}, \\ 
{\tt{8}})\-\index{splus})\-\index{splus} \\ 
{\bf else }{\rm{splus}}\,(\=\+{\rm{strstr-t1}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strstr-t1}, \\ 
{\rm{splus}}\,(\=\+{\rm{strncmp-t}}\,(\=\+{\it{len\/}}, \\ 
{\rm{mcdr}}\,($1\;+$ {\it{j\/}}, {\it{lst1\/}})\index{mcdr}, \\ 
{\rm{mcdr}}\,({\tt{1}}, {\it{lst2\/}})\index{mcdr})\-\index{strncmp-t}, \\ 
{\tt{3}})\-\index{splus})\-\index{splus}$\;${\bf  endif}\- \\ 
{\bf else }{\rm{strstr-t1}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strstr-t1}$\;${\bf  endif}\-$\;${\bf  endlet}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{strstr-t3} \\  
\=\+{\rm{strstr-t3}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-t3} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $<$ {\it{n1\/}} \\ 
{\bf then }\=\+{\bf let }\=\+{\it{j\/}}{\bf $\;$ be$\;\;$}{\rm{strchr1}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth})\index{strchr1}\- \\ 
{\bf in} \\ 
\=\+{\bf if }{\it{j\/}} $\in\;${\bf{N}}${}$ \\ 
{\bf then }\=\+{\bf if }\=\+{\rm{strncmp}}\,({\it{len\/}}, {\rm{mcdr}}\,($1\;+$ {\it{j\/}}, {\it{lst1\/}})\index{mcdr}, {\rm{mcdr}}\,({\tt{1}}, {\it{lst2\/}})\index{mcdr})\index{strncmp} \\ 
$=$$\;\;\;\;${\tt{0}}\-$\;\;${\bf then }{\rm{strstr-t2}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-t2} \\ 
{\bf else }{\rm{splus}}\,(\=\+{\rm{strstr-t2}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-t2}, \\ 
{\rm{strstr-t3}}\,($1\;+$ {\it{j\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-t3})\-\index{splus}$\;${\bf  endif}\- \\ 
{\bf else }{\rm{strstr-t1}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strstr-t1}$\;${\bf  endif}\-$\;${\bf  endlet}\- \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{strstr-t} \\  
\=\+{\rm{strstr-t}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr-t} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth} $=$ {\tt{0}}$\;\;${\bf then }{\tt{10}} \\ 
{\bf else }{\rm{splus}}\,(\=\+{\rm{strstr-t0}}\,({\it{n2\/}}, {\it{lst2\/}})\index{strstr-t0}, \\ 
{\rm{strstr-t3}}\,(\=\+{\tt{0}}, \\ 
{\it{n1\/}}, \\ 
{\it{lst1\/}}, \\ 
{\it{lst2\/}}, \\ 
{\rm{strlen}}\,({\tt{0}}, {\it{n2\/}} $-\;1$, {\rm{mcdr}}\,({\tt{1}}, {\it{lst2\/}})\index{mcdr})\index{strlen})\-\index{strstr-t3})\-\index{splus}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; two induction hints.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{strstr-induct1} \\  
\=\+{\rm{strstr-induct1}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strstr-induct1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $<$ {\it{n1\/}} \\ 
{\bf then }\=\+{\bf if }{\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\tt{0}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{strstr-induct1}}\,(\=\+{\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn}, \\ 
{\rm{add}}\,({\tt{32}}, {\it{i*\/}}, {\tt{1}})\index{add}, \\ 
$1\;+$ {\it{i\/}}, \\ 
{\it{n1\/}}, \\ 
{\it{lst1\/}}, \\ 
{\it{lst2\/}})\-\index{strstr-induct1}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{strstr-induct2} \\  
\=\+{\rm{strstr-induct2}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-induct2} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $<$ {\it{n1\/}} \\ 
{\bf then }\=\+{\bf let }\=\+{\it{j*\/}}{\bf $\;$ be$\;\;$}{\rm{strchr1*}}\,({\it{i*\/}}, {\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth})\index{strchr1*}, \\ 
{\it{j\/}}{\bf $\;$ be$\;\;$}{\rm{strchr1}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth})\index{strchr1}\- \\ 
{\bf in} \\ 
\=\+{\bf if }{\it{j\/}} $\in\;${\bf{N}}${}$ \\ 
{\bf then }\=\+{\bf if }\=\+{\rm{strncmp}}\,({\it{len\/}}, {\rm{mcdr}}\,($1\;+$ {\it{j\/}}, {\it{lst1\/}})\index{mcdr}, {\rm{mcdr}}\,({\tt{1}}, {\it{lst2\/}})\index{mcdr})\index{strncmp} \\ 
$=$$\;\;\;\;${\tt{0}}\-$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{strstr-induct2}}\,(\=\+{\rm{stepn}}\,(\=\+{\it{s\/}}, \\ 
{\rm{strstr-t2}}\,(\=\+{\it{i\/}}, \\ 
{\it{n1\/}}, \\ 
{\it{lst1\/}}, \\ 
{\it{lst2\/}}, \\ 
{\it{len\/}})\-\index{strstr-t2})\-\index{stepn}, \\ 
{\rm{add}}\,({\tt{32}}, {\it{j*\/}}, {\tt{1}})\index{add}, \\ 
$1\;+$ {\it{j\/}}, \\ 
{\it{n1\/}}, \\ 
{\it{lst1\/}}, \\ 
{\it{lst2\/}}, \\ 
{\it{len\/}})\-\index{strstr-induct2}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-$\;${\bf  endlet}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}
  
\begin{verbatim}; the preconditions of the initial state.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{strstr-statep} \\  
\=\+{\rm{strstr-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr-statep} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{strstr-loadp}}\,({\it{s\/}})\index{strstr-loadp} \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc} $=$ {\sc{strstr-addr}}\index{strstr-addr}) \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{48}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{60}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\it{str1\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n1\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,({\tt{1}}, {\it{str1\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n1\/}}, {\it{lst1\/}})\index{mem-lst} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\it{str2\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n2\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,({\tt{1}}, {\it{str2\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n2\/}}, {\it{lst2\/}})\index{mem-lst} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{str1\/}}, {\it{n1\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{48}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{60}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{str2\/}}, {\it{n2\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{48}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{60}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;$({\it{str1\/}} $=$ {\rm{read-mem}}\,({\rm{add}}\,({\tt{32}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\tt{4}})\index{add}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{read-mem}) \\ 
$\wedge$$\;\;\;\;$({\it{str2\/}} $=$ {\rm{read-mem}}\,({\rm{add}}\,({\tt{32}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\tt{8}})\index{add}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{read-mem}) \\ 
$\wedge$$\;\;\;\;$({\rm{slen}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}})\index{slen} $<$ {\it{n1\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{slen}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}})\index{slen} $<$ {\it{n2\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{nat-to-uint}}\,({\it{str1\/}})\index{nat-to-uint} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{n1\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\rm{nat-to-uint}}\,({\it{str1\/}})\index{nat-to-uint} $+$ {\it{n1\/}}, {\tt{32}})\index{uint-rangep} \\ 
$\wedge$$\;\;\;\;$({\it{n2\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\it{n2\/}}, {\tt{32}})\index{uint-rangep})\-\-
\end{tabbing}

\begin{verbatim}; the intermediate state right before the call to strlen.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{strstr-s0p} \\  
\=\+{\rm{strstr-s0p}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr-s0p} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{strstr-loadp}}\,({\it{s\/}})\index{strstr-loadp} \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc} $=$ {\sc{strlen-addr}}\index{strlen-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr} $=$ {\rm{add}}\,({\tt{32}}, {\sc{strstr-addr}}\index{strstr-addr}, {\tt{28}})\index{add}) \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{44}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{60}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\it{str1\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n1\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,({\tt{1}}, {\it{str1\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n1\/}}, {\it{lst1\/}})\index{mem-lst} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\it{str2\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n2\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,({\tt{1}}, {\it{str2\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n2\/}}, {\it{lst2\/}})\index{mem-lst} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{str1\/}}, {\it{n1\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{44}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{60}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{str2\/}}, {\it{n2\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{44}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{60}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;$({\it{str1\/}} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{2}}, {\it{s\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;$({\rm{nat-to-uint}}\,({\rm{read-dn}}\,({\tt{8}}, {\tt{2}}, {\it{s\/}})\index{read-dn})\index{nat-to-uint} $=$ {\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth}) \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{3}}, {\it{s\/}})\index{read-an}, {\rm{add}}\,({\tt{32}}, {\it{str2\/}}, {\tt{1}})\index{add})\index{equal*} \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\rm{sub}}\,({\tt{32}}, {\tt{24}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub})\index{equal*} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-an}}\,({\tt{32}}, {\tt{3}}, {\it{s\/}})\index{read-an} \\ 
$=$$\;\;\;\;${\rm{read-mem}}\,({\rm{add}}\,({\tt{32}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\tt{4}})\index{add}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{read-mem})\- \\ 
$\wedge$$\;\;\;\;$({\rm{slen}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}})\index{slen} $<$ {\it{n1\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{slen}}\,({\tt{1}}, {\it{n2\/}}, {\it{lst2\/}})\index{slen} $<$ {\it{n2\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{n1\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\it{n1\/}}, {\tt{32}})\index{uint-rangep} \\ 
$\wedge$$\;\;\;\;$({\it{n2\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\it{n2\/}}, {\tt{32}})\index{uint-rangep})\-\-
\end{tabbing}

\begin{verbatim}; the intermediate state returned from the call to strlen.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{strstr-s1p} \\  
\=\+{\rm{strstr-s1p}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s1p} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{strstr-loadp}}\,({\it{s\/}})\index{strstr-loadp} \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc} $=$ {\rm{add}}\,({\tt{32}}, {\sc{strstr-addr}}\index{strstr-addr}, {\tt{28}})\index{add}) \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{44}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{60}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\it{str1\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n1\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,({\tt{1}}, {\it{str1\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n1\/}}, {\it{lst1\/}})\index{mem-lst} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\it{str2\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n2\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,({\tt{1}}, {\it{str2\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n2\/}}, {\it{lst2\/}})\index{mem-lst} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{str1\/}}, {\it{n1\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{44}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{60}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{str2\/}}, {\it{n2\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{44}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{60}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;$({\it{str1\/}} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{2}}, {\it{s\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;$({\rm{nat-to-uint}}\,({\rm{read-dn}}\,({\tt{8}}, {\tt{2}}, {\it{s\/}})\index{read-dn})\index{nat-to-uint} $=$ {\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth}) \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{3}}, {\it{s\/}})\index{read-an}, {\rm{add}}\,({\tt{32}}, {\it{str2\/}}, {\tt{1}})\index{add})\index{equal*} \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\rm{sub}}\,({\tt{32}}, {\tt{20}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub})\index{equal*} \\ 
$\wedge$$\;\;\;\;$({\it{len\/}} $=$ {\rm{uread-dn}}\,({\tt{32}}, {\tt{0}}, {\it{s\/}})\index{uread-dn}) \\ 
$\wedge$$\;\;\;\;$({\rm{slen}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}})\index{slen} $<$ {\it{n1\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{slen}}\,({\tt{1}}, {\it{n2\/}}, {\it{lst2\/}})\index{slen} $<$ {\it{n2\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{n1\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\it{n1\/}}, {\tt{32}})\index{uint-rangep} \\ 
$\wedge$$\;\;\;\;$({\it{n2\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\it{n2\/}}, {\tt{32}})\index{uint-rangep})\-\-
\end{tabbing}

\begin{verbatim}; the intermediate state right before the outer loop.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{strstr-s2p} \\  
\=\+{\rm{strstr-s2p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s2p} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{strstr-loadp}}\,({\it{s\/}})\index{strstr-loadp} \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc} $=$ {\rm{add}}\,({\tt{32}}, {\sc{strstr-addr}}\index{strstr-addr}, {\tt{32}})\index{add}) \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{44}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{60}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\it{str1\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n1\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,({\tt{1}}, {\it{str1\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n1\/}}, {\it{lst1\/}})\index{mem-lst} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\it{str2\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n2\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,({\tt{1}}, {\it{str2\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n2\/}}, {\it{lst2\/}})\index{mem-lst} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{str1\/}}, {\it{n1\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{44}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{60}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{str2\/}}, {\it{n2\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{44}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{60}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;$({\rm{uread-dn}}\,({\tt{8}}, {\tt{2}}, {\it{s\/}})\index{uread-dn} $=$ {\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth}) \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{2}}, {\it{s\/}})\index{read-an}, {\rm{add}}\,({\tt{32}}, {\it{str1\/}}, {\it{i*\/}})\index{add})\index{equal*} \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{3}}, {\it{s\/}})\index{read-an}, {\rm{add}}\,({\tt{32}}, {\it{str2\/}}, {\tt{1}})\index{add})\index{equal*} \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\rm{sub}}\,({\tt{32}}, {\tt{16}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub})\index{equal*} \\ 
$\wedge$$\;\;\;\;$({\it{len\/}} $=$ {\rm{uread-dn}}\,({\tt{32}}, {\tt{3}}, {\it{s\/}})\index{uread-dn}) \\ 
$\wedge$$\;\;\;\;$({\rm{slen}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}})\index{slen} $<$ {\it{n1\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{slen}}\,({\tt{1}}, {\it{n2\/}}, {\it{lst2\/}})\index{slen} $<$ {\it{n2\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i*\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{nat-rangep}}\,({\it{i*\/}}, {\tt{32}})\index{nat-rangep} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $=$ {\rm{nat-to-uint}}\,({\it{i*\/}})\index{nat-to-uint}) \\ 
$\wedge$$\;\;\;\;$({\it{n1\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\it{n1\/}}, {\tt{32}})\index{uint-rangep} \\ 
$\wedge$$\;\;\;\;$({\it{n2\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\it{n2\/}}, {\tt{32}})\index{uint-rangep})\-\-
\end{tabbing}

\begin{verbatim}; the intermediate state right before the call to strncmp.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{strstr-s3p} \\  
\=\+{\rm{strstr-s3p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s3p} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{strstr-loadp}}\,({\it{s\/}})\index{strstr-loadp} \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc} $=$ {\sc{strncmp-addr}}\index{strncmp-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr} $=$ {\rm{add}}\,({\tt{32}}, {\sc{strstr-addr}}\index{strstr-addr}, {\tt{56}})\index{add}) \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{44}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{60}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\it{str1\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n1\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,({\tt{1}}, {\it{str1\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n1\/}}, {\it{lst1\/}})\index{mem-lst} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\it{str2\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n2\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,({\tt{1}}, {\it{str2\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n2\/}}, {\it{lst2\/}})\index{mem-lst} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{sub}}\,({\tt{32}}, {\tt{44}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{60}}, {\it{str1\/}}, {\it{n1\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{sub}}\,({\tt{32}}, {\tt{44}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{60}}, {\it{str2\/}}, {\it{n2\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;$({\rm{uread-dn}}\,({\tt{8}}, {\tt{2}}, {\it{s\/}})\index{uread-dn} $=$ {\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth}) \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{2}}, {\it{s\/}})\index{read-an}, {\rm{add}}\,({\tt{32}}, {\it{str1\/}}, {\it{i*\/}})\index{add})\index{equal*} \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{3}}, {\it{s\/}})\index{read-an}, {\rm{add}}\,({\tt{32}}, {\it{str2\/}}, {\tt{1}})\index{add})\index{equal*} \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\rm{sub}}\,({\tt{32}}, {\tt{32}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub})\index{equal*} \\ 
$\wedge$$\;\;\;\;$({\it{len\/}} $=$ {\rm{uread-dn}}\,({\tt{32}}, {\tt{3}}, {\it{s\/}})\index{uread-dn}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-an}}\,({\tt{32}}, {\tt{2}}, {\it{s\/}})\index{read-an} \\ 
$=$$\;\;\;\;${\rm{read-mem}}\,({\rm{add}}\,({\tt{32}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\tt{4}})\index{add}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{read-mem})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-an}}\,({\tt{32}}, {\tt{3}}, {\it{s\/}})\index{read-an} \\ 
$=$$\;\;\;\;${\rm{read-mem}}\,({\rm{add}}\,({\tt{32}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\tt{8}})\index{add}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{read-mem})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-dn}}\,({\tt{32}}, {\tt{3}}, {\it{s\/}})\index{read-dn} \\ 
$=$$\;\;\;\;${\rm{read-mem}}\,({\rm{add}}\,({\tt{32}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\tt{12}})\index{add}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{read-mem})\- \\ 
$\wedge$$\;\;\;\;$({\rm{slen}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}})\index{slen} $<$ {\it{n1\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{slen}}\,({\tt{1}}, {\it{n2\/}}, {\it{lst2\/}})\index{slen} $<$ {\it{n2\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i*\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{nat-rangep}}\,({\it{i*\/}}, {\tt{32}})\index{nat-rangep} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $=$ {\rm{nat-to-uint}}\,({\it{i*\/}})\index{nat-to-uint}) \\ 
$\wedge$$\;\;\;\;$({\it{n1\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\it{n1\/}}, {\tt{32}})\index{uint-rangep} \\ 
$\wedge$$\;\;\;\;$({\it{n2\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\it{n2\/}}, {\tt{32}})\index{uint-rangep})\-\-
\end{tabbing}

\begin{verbatim}; the intermediate state right after the call to strncmp.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{strstr-s4p} \\  
\=\+{\rm{strstr-s4p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s4p} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{strstr-loadp}}\,({\it{s\/}})\index{strstr-loadp} \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc} $=$ {\rm{add}}\,({\tt{32}}, {\sc{strstr-addr}}\index{strstr-addr}, {\tt{56}})\index{add}) \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{44}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{60}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\it{str1\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n1\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,({\tt{1}}, {\it{str1\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n1\/}}, {\it{lst1\/}})\index{mem-lst} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\it{str2\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n2\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,({\tt{1}}, {\it{str2\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n2\/}}, {\it{lst2\/}})\index{mem-lst} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{str1\/}}, {\it{n1\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{44}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{60}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{str2\/}}, {\it{n2\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{44}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{60}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{iread-dn}}\,({\tt{32}}, {\tt{0}}, {\it{s\/}})\index{iread-dn} \\ 
$=$$\;\;\;\;${\rm{strncmp}}\,({\it{len\/}}, {\rm{mcdr}}\,({\it{i\/}}, {\it{lst1\/}})\index{mcdr}, {\rm{mcdr}}\,({\tt{1}}, {\it{lst2\/}})\index{mcdr})\index{strncmp})\- \\ 
$\wedge$$\;\;\;\;$({\rm{uread-dn}}\,({\tt{8}}, {\tt{2}}, {\it{s\/}})\index{uread-dn} $=$ {\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth}) \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{2}}, {\it{s\/}})\index{read-an}, {\rm{add}}\,({\tt{32}}, {\it{str1\/}}, {\it{i*\/}})\index{add})\index{equal*} \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{3}}, {\it{s\/}})\index{read-an}, {\rm{add}}\,({\tt{32}}, {\it{str2\/}}, {\tt{1}})\index{add})\index{equal*} \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\rm{sub}}\,({\tt{32}}, {\tt{28}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub})\index{equal*} \\ 
$\wedge$$\;\;\;\;$({\it{len\/}} $=$ {\rm{uread-dn}}\,({\tt{32}}, {\tt{3}}, {\it{s\/}})\index{uread-dn}) \\ 
$\wedge$$\;\;\;\;$({\rm{slen}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}})\index{slen} $<$ {\it{n1\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{slen}}\,({\tt{1}}, {\it{n2\/}}, {\it{lst2\/}})\index{slen} $<$ {\it{n2\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i*\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{nat-rangep}}\,({\it{i*\/}}, {\tt{32}})\index{nat-rangep} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $=$ {\rm{nat-to-uint}}\,({\it{i*\/}})\index{nat-to-uint}) \\ 
$\wedge$$\;\;\;\;$({\it{n1\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\it{n1\/}}, {\tt{32}})\index{uint-rangep} \\ 
$\wedge$$\;\;\;\;$({\it{n2\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\it{n2\/}}, {\tt{32}})\index{uint-rangep})\-\-
\end{tabbing}

\begin{verbatim}; from the initial state to exit:  s --> sn, when lst2[0] == 0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strstr-s-sn \\ \index{strstr-s-sn}
\=\+({\rm{strstr-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr-statep} $\wedge$ ({\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth} $=$ {\tt{0}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{10}})\index{stepn})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{10}})\index{stepn})\index{mc-pc} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-dn}}\,({\tt{32}}, {\tt{0}}, {\rm{stepn}}\,({\it{s\/}}, {\tt{10}})\index{stepn})\index{read-dn} $=$ {\it{str1\/}}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{10}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{add}}\,({\tt{32}}, {\rm{read-an}}\,({\tt{32}}, {\tt{7}}, {\it{s\/}})\index{read-an}, {\tt{4}})\index{add})\- \\ 
$\wedge$$\;\;\;\;$({\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{10}})\index{stepn})\index{mc-rfile})\index{read-rn} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-s-sn-rfile \\ \index{strstr-s-sn-rfile}
\=\+(\=\+{\rm{strstr-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr-statep} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{oplen\/}} $\leq$ {\tt{32}}) \\ 
$\wedge$$\;\;\;\;${\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{10}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-s-sn-mem \\ \index{strstr-s-sn-mem}
\=\+(\=\+{\rm{strstr-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr-statep} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{48}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{60}})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{10}})\index{stepn})\index{mc-mem}, {\it{k\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-
\end{tabbing}

\begin{verbatim}; from the initial state to s0.  s --> s0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strstr-s-s0 \\ \index{strstr-s-s0}
\=\+({\rm{strstr-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr-statep} $\wedge$ ({\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth} $\not=$ {\tt{0}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{strstr-s0p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr-s0p}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-s-s0-else \\ \index{strstr-s-s0-else}
\=\+({\rm{strstr-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr-statep} $\wedge$ ({\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth} $\not=$ {\tt{0}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{linked-a6} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{movem-saved}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved} \\ 
$=$$\;\;\;\;${\rm{readm-rn}}\,({\tt{32}}, {\tt{'}}{\tt{(}}{\tt{2}}{\tt{ }}{\tt{3}}{\tt{ }}{\tt{10}}{\tt{ }}{\tt{11}}{\tt{)}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{readm-rn})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-s-s0-rfile \\ \index{strstr-s-s0-rfile}
\=\+(\=\+{\rm{strstr-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr-statep} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{d4-7a4-5p}}\,({\it{rn\/}})\index{d4-7a4-5p})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-s-s0-mem \\ \index{strstr-s-s0-mem}
\=\+(\=\+{\rm{strstr-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr-statep} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{48}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{60}})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{mc-mem}, {\it{k\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-
\end{tabbing}

\begin{verbatim}; from s0 to s1:  s0 --> s1.  by strlen.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strstr-s0p-strlen-statep \\ \index{strstr-s0p-strlen-statep}
\=\+{\rm{strstr-s0p}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr-s0p} \\ 
$\rightarrow$$\;\;\;\;${\rm{strlen-statep}}\,({\it{s\/}}, {\rm{add}}\,({\tt{32}}, {\it{str2\/}}, {\tt{1}})\index{add}, {\it{n2\/}} $-\;1$, {\rm{mcdr}}\,({\tt{1}}, {\it{lst2\/}})\index{mcdr})\index{strlen-statep}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-s0-s1 \\ \index{strstr-s0-s1}
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strlen-t}}\,({\it{n2\/}} $-\;1$, {\rm{mcdr}}\,({\tt{1}}, {\it{lst2\/}})\index{mcdr})\index{strlen-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{strstr-s0p}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr-s0p} \\ 
$\rightarrow$$\;\;\;\;${\rm{strstr-s1p}}\,(\=\+{\it{s1\/}}, \\ 
{\it{str1\/}}, \\ 
{\it{n1\/}}, \\ 
{\it{lst1\/}}, \\ 
{\it{str2\/}}, \\ 
{\it{n2\/}}, \\ 
{\it{lst2\/}}, \\ 
{\rm{strlen}}\,({\tt{0}}, {\it{n2\/}} $-\;1$, {\rm{mcdr}}\,({\tt{1}}, {\it{lst2\/}})\index{mcdr})\index{strlen})\-\index{strstr-s1p}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-s0-s1-else \\ \index{strstr-s0-s1-else}
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strlen-t}}\,({\it{n2\/}} $-\;1$, {\rm{cdr}}\,({\it{lst2\/}}))\index{strlen-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{strstr-s0p}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr-s0p} \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s1\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\- \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\it{s1\/}})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\it{s1\/}})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$({\rm{movem-saved}}\,({\it{s1\/}}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved} $=$ {\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved}))\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-s0-s1-rfile \\ \index{strstr-s0-s1-rfile}
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strlen-t}}\,({\it{n2\/}} $-\;1$, {\rm{cdr}}\,({\it{lst2\/}}))\index{strlen-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+({\rm{strstr-s0p}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr-s0p} $\wedge$ {\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s1\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-s0-s1-mem \\ \index{strstr-s0-s1-mem}
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strlen-t}}\,({\it{n2\/}} $-\;1$, {\rm{cdr}}\,({\it{lst2\/}}))\index{strlen-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strstr-s0p}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr-s0p} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{44}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{60}})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s1\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim}; from s1 to s2:  s1 --> s2.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strstr-s1-s2 \\ \index{strstr-s1-s2}
\=\+{\rm{strstr-s1p}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s1p} \\ 
$\rightarrow$$\;\;\;\;${\rm{strstr-s2p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{2}})\index{stepn}, {\tt{0}}, {\tt{0}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s2p}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-s1-s2-else \\ \index{strstr-s1-s2-else}
\=\+{\rm{strstr-s1p}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s1p} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{2}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{2}})\index{stepn})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{2}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\- \\ 
$\wedge$$\;\;\;\;$({\rm{movem-saved}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{2}})\index{stepn}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved} $=$ {\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{2}})\index{stepn})\index{mc-mem}, {\it{k\/}})\index{read-mem} \\ 
$=$$\;\;\;\;${\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-s1-s2-rfile \\ \index{strstr-s1-s2-rfile}
\=\+({\rm{strstr-s1p}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s1p} $\wedge$ {\rm{d4-7a4-5p}}\,({\it{rn\/}})\index{d4-7a4-5p}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{2}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-\-
\end{tabbing}

\begin{verbatim}; from s2 to exit:  s2 --> sn, when lst1[i] == 0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strstr-s2-sn-base \\ \index{strstr-s2-sn-base}
\=\+(\=\+{\rm{strstr-s2p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s2p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{7}})\index{stepn})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{7}})\index{stepn})\index{mc-pc} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-dn}}\,({\tt{32}}, {\tt{0}}, {\rm{stepn}}\,({\it{s\/}}, {\tt{7}})\index{stepn})\index{read-dn} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{7}})\index{stepn})\index{mc-rfile})\index{read-rn} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{7}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{add}}\,({\tt{32}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}, {\tt{8}})\index{add})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{7}})\index{stepn})\index{mc-mem}, {\it{k\/}})\index{read-mem} \\ 
$=$$\;\;\;\;${\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-s2-sn-base-rfile \\ \index{strstr-s2-sn-base-rfile}
\=\+(\=\+{\rm{strstr-s2p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s2p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p} \\ 
$\wedge$$\;\;\;\;$({\it{oplen\/}} $\leq$ {\tt{32}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{7}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{d4-7a4-5p}}\,({\it{rn\/}})\index{d4-7a4-5p}$\;\;${\bf then }{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn} \\ 
{\bf else }{\rm{get-vlst}}\,(\=\+{\it{oplen\/}}, \\ 
{\tt{0}}, \\ 
{\it{rn\/}}, \\ 
{\tt{'}}{\tt{(}}{\tt{2}}{\tt{ }}{\tt{3}}{\tt{ }}{\tt{10}}{\tt{ }}{\tt{11}}{\tt{)}}, \\ 
{\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved})\-\index{get-vlst}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{verbatim}; from s2 to s3:  s2 --> s3, when lst1[i] =\= 0 and lst1[i] == lst2[0].
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strstr-s2-s3-base \\ \index{strstr-s2-s3-base}
\=\+(\=\+{\rm{strstr-s2p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s2p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{strstr-s3p}}\,(\=\+{\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn}, \\ 
{\rm{add}}\,({\tt{32}}, {\it{i*\/}}, {\tt{1}})\index{add}, \\ 
$1\;+$ {\it{i\/}}, \\ 
{\it{str1\/}}, \\ 
{\it{n1\/}}, \\ 
{\it{lst1\/}}, \\ 
{\it{str2\/}}, \\ 
{\it{n2\/}}, \\ 
{\it{lst2\/}}, \\ 
{\it{len\/}})\-\index{strstr-s3p} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\- \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{movem-saved}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved} $=$ {\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-s2-s3-base-rfile \\ \index{strstr-s2-s3-base-rfile}
\=\+(\=\+{\rm{strstr-s2p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s2p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth}) \\ 
$\wedge$$\;\;\;\;${\rm{d4-7a4-5p}}\,({\it{rn\/}})\index{d4-7a4-5p})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-s2-s3-base-mem \\ \index{strstr-s2-s3-base-mem}
\=\+(\=\+{\rm{strstr-s2p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s2p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth}) \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{44}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{60}})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{mc-mem}, {\it{k\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-
\end{tabbing}

\begin{verbatim}; from s2 to s2:  s2 --> s2.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strstr-s2-s2 \\ \index{strstr-s2-s2}
\=\+(\=\+{\rm{strstr-s2p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s2p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $\not=$ {\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{strstr-s2p}}\,(\=\+{\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn}, \\ 
{\rm{add}}\,({\tt{32}}, {\it{i*\/}}, {\tt{1}})\index{add}, \\ 
$1\;+$ {\it{i\/}}, \\ 
{\it{str1\/}}, \\ 
{\it{n1\/}}, \\ 
{\it{lst1\/}}, \\ 
{\it{str2\/}}, \\ 
{\it{n2\/}}, \\ 
{\it{lst2\/}}, \\ 
{\it{len\/}})\-\index{strstr-s2p} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\- \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn})\index{rts-addr} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{movem-saved}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved} $=$ {\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn})\index{mc-mem}, {\it{k\/}})\index{read-mem} \\ 
$=$$\;\;\;\;${\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-s2-s2-rfile \\ \index{strstr-s2-s2-rfile}
\=\+(\=\+{\rm{strstr-s2p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s2p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $\not=$ {\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth}) \\ 
$\wedge$$\;\;\;\;${\rm{d4-7a4-5p}}\,({\it{rn\/}})\index{d4-7a4-5p})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-\-
\end{tabbing}

\begin{verbatim}; from s3 to s4:  s3 --> s4. The call to strncmp.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strstr-s3p-strncmp-statep \\ \index{strstr-s3p-strncmp-statep}
\=\+{\rm{strstr-s3p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s3p} \\ 
$\rightarrow$$\;\;\;\;${\rm{strncmp-statep}}\,(\=\+{\it{s\/}}, \\ 
{\rm{add}}\,({\tt{32}}, {\it{str1\/}}, {\it{i*\/}})\index{add}, \\ 
{\it{n1\/}} $-$ {\it{i\/}}, \\ 
{\rm{mcdr}}\,({\it{i\/}}, {\it{lst1\/}})\index{mcdr}, \\ 
{\rm{add}}\,({\tt{32}}, {\it{str2\/}}, {\tt{1}})\index{add}, \\ 
{\it{n2\/}} $-\;1$, \\ 
{\rm{mcdr}}\,({\tt{1}}, {\it{lst2\/}})\index{mcdr}, \\ 
{\it{len\/}})\-\index{strncmp-statep}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-s3-s4 \\ \index{strstr-s3-s4}
\=\+{\bf let }\=\+{\it{s4\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strncmp-t}}\,({\it{len\/}}, {\rm{mcdr}}\,({\it{i\/}}, {\it{lst1\/}})\index{mcdr}, {\rm{mcdr}}\,({\tt{1}}, {\it{lst2\/}})\index{mcdr})\index{strncmp-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{strstr-s3p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s3p} \\ 
$\rightarrow$$\;\;\;\;${\rm{strstr-s4p}}\,({\it{s4\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s4p}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-s3-s4-else \\ \index{strstr-s3-s4-else}
\=\+{\bf let }\=\+{\it{s4\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strncmp-t}}\,({\it{len\/}}, {\rm{mcdr}}\,({\it{i\/}}, {\it{lst1\/}})\index{mcdr}, {\rm{mcdr}}\,({\tt{1}}, {\it{lst2\/}})\index{mcdr})\index{strncmp-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{strstr-s3p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s3p} \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s4\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\- \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\it{s4\/}})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\it{s4\/}})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$({\rm{movem-saved}}\,({\it{s4\/}}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved} $=$ {\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved}))\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-s3-s4-rfile \\ \index{strstr-s3-s4-rfile}
\=\+{\bf let }\=\+{\it{s4\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strncmp-t}}\,({\it{len\/}}, {\rm{mcdr}}\,({\it{i\/}}, {\it{lst1\/}})\index{mcdr}, {\rm{mcdr}}\,({\tt{1}}, {\it{lst2\/}})\index{mcdr})\index{strncmp-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strstr-s3p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s3p} \\ 
$\wedge$$\;\;\;\;${\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p} \\ 
$\wedge$$\;\;\;\;$({\it{oplen\/}} $\leq$ {\tt{32}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s4\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-s3-s4-mem \\ \index{strstr-s3-s4-mem}
\=\+{\bf let }\=\+{\it{s4\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strncmp-t}}\,({\it{len\/}}, {\rm{mcdr}}\,({\it{i\/}}, {\it{lst1\/}})\index{mcdr}, {\rm{mcdr}}\,({\tt{1}}, {\it{lst2\/}})\index{mcdr})\index{strncmp-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strstr-s3p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s3p} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{44}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{60}})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s4\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim}; from s4 to exit:  s4 --> sn, when strncmp == 0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strstr-s4-sn \\ \index{strstr-s4-sn}
\=\+(\=\+{\rm{strstr-s4p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s4p} \\ 
$\wedge$$\;\;\;\;$({\rm{strncmp}}\,({\it{len\/}}, {\rm{mcdr}}\,({\it{i\/}}, {\it{lst1\/}})\index{mcdr}, {\rm{mcdr}}\,({\tt{1}}, {\it{lst2\/}})\index{mcdr})\index{strncmp} $=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{mc-pc} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-dn}}\,({\tt{32}}, {\tt{0}}, {\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{read-dn} $=$ {\rm{add}}\,({\tt{32}}, {\it{str1\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{1}}, {\it{i*\/}})\index{sub})\index{add}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{mc-rfile})\index{read-rn} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{add}}\,({\tt{32}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}, {\tt{8}})\index{add})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{mc-mem}, {\it{k\/}})\index{read-mem} \\ 
$=$$\;\;\;\;${\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-s4-sn-rfile \\ \index{strstr-s4-sn-rfile}
\=\+(\=\+{\rm{strstr-s4p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s4p} \\ 
$\wedge$$\;\;\;\;$({\rm{strncmp}}\,({\it{len\/}}, {\rm{mcdr}}\,({\it{i\/}}, {\it{lst1\/}})\index{mcdr}, {\rm{mcdr}}\,({\tt{1}}, {\it{lst2\/}})\index{mcdr})\index{strncmp} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p} \\ 
$\wedge$$\;\;\;\;$({\it{oplen\/}} $\leq$ {\tt{32}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{d4-7a4-5p}}\,({\it{rn\/}})\index{d4-7a4-5p}$\;\;${\bf then }{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn} \\ 
{\bf else }{\rm{get-vlst}}\,(\=\+{\it{oplen\/}}, \\ 
{\tt{0}}, \\ 
{\it{rn\/}}, \\ 
{\tt{'}}{\tt{(}}{\tt{2}}{\tt{ }}{\tt{3}}{\tt{ }}{\tt{10}}{\tt{ }}{\tt{11}}{\tt{)}}, \\ 
{\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved})\-\index{get-vlst}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{verbatim}; from s4 to s2: s4 --> s2, when strncmp =\= 0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strstr-s4-s2 \\ \index{strstr-s4-s2}
\=\+(\=\+{\rm{strstr-s4p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s4p} \\ 
$\wedge$$\;\;\;\;$({\rm{strncmp}}\,({\it{len\/}}, {\rm{mcdr}}\,({\it{i\/}}, {\it{lst1\/}})\index{mcdr}, {\rm{mcdr}}\,({\tt{1}}, {\it{lst2\/}})\index{mcdr})\index{strncmp} $\not=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{strstr-s2p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{3}})\index{stepn}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s2p} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{3}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\- \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{3}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{3}})\index{stepn})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$({\rm{movem-saved}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{3}})\index{stepn}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved} $=$ {\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{3}})\index{stepn})\index{mc-mem}, {\it{k\/}})\index{read-mem} \\ 
$=$$\;\;\;\;${\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-s4-s2-rfile \\ \index{strstr-s4-s2-rfile}
\=\+(\=\+{\rm{strstr-s4p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s4p} \\ 
$\wedge$$\;\;\;\;$({\rm{strncmp}}\,({\it{len\/}}, {\rm{mcdr}}\,({\it{i\/}}, {\it{lst1\/}})\index{mcdr}, {\rm{mcdr}}\,({\tt{1}}, {\it{lst2\/}})\index{mcdr})\index{strncmp} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{d4-7a4-5p}}\,({\it{rn\/}})\index{d4-7a4-5p})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{3}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-\-
\end{tabbing}

\begin{verbatim}; put together: s2 --> s3.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strstr-s2p-info \\ \index{strstr-s2p-info}
\=\+{\rm{strstr-s2p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s2p} \\ 
$\rightarrow$$\;\;\;\;$(({\it{i\/}} $\in\;${\bf{N}}${}$) $\wedge$ (({\it{i\/}} $<$ {\it{n1\/}}) $=$ {\bf{t}}))\-
\end{tabbing}
		   
\begin{tabbing}{\sc Theorem}:  strstr-s2-s3 \\ \index{strstr-s2-s3}
\=\+(\=\+{\rm{strstr-s2p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s2p} \\ 
$\wedge$$\;\;\;\;$({\rm{strchr1}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth})\index{strchr1} $\in\;${\bf{N}}${}$))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{strstr-s3p}}\,(\=\+{\rm{stepn}}\,({\it{s\/}}, {\rm{strstr-t1}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strstr-t1})\index{stepn}, \\ 
{\rm{add}}\,({\tt{32}}, {\rm{strchr1*}}\,({\it{i*\/}}, {\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth})\index{strchr1*}, {\tt{1}})\index{add}, \\ 
$1\;+$ {\rm{strchr1}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth})\index{strchr1}, \\ 
{\it{str1\/}}, \\ 
{\it{n1\/}}, \\ 
{\it{lst1\/}}, \\ 
{\it{str2\/}}, \\ 
{\it{n2\/}}, \\ 
{\it{lst2\/}}, \\ 
{\it{len\/}})\-\index{strstr-s3p}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-s2-s3-else \\ \index{strstr-s2-s3-else}
\=\+{\bf let }\=\+{\it{s3\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strstr-t1}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strstr-t1})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strstr-s2p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s2p} \\ 
$\wedge$$\;\;\;\;$({\rm{strchr1}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth})\index{strchr1} $\in\;${\bf{N}}${}$))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s3\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\- \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\it{s3\/}})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\it{s3\/}})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$({\rm{movem-saved}}\,({\it{s3\/}}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved} $=$ {\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved}))\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-s2-s3-rfile \\ \index{strstr-s2-s3-rfile}
\=\+{\bf let }\=\+{\it{s3\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strstr-t1}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strstr-t1})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strstr-s2p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s2p} \\ 
$\wedge$$\;\;\;\;$({\rm{strchr1}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth})\index{strchr1} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{d4-7a4-5p}}\,({\it{rn\/}})\index{d4-7a4-5p})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s3\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-s2-s3-mem \\ \index{strstr-s2-s3-mem}
\=\+{\bf let }\=\+{\it{s3\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strstr-t1}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strstr-t1})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strstr-s2p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s2p} \\ 
$\wedge$$\;\;\;\;$({\rm{strchr1}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth})\index{strchr1} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{44}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{60}})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s3\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-$\;${\bf  endlet}\-
\end{tabbing}
		      
\begin{verbatim}; put together: s2 --> exit.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strstr-s2-sn \\ \index{strstr-s2-sn}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strstr-t1}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strstr-t1})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strstr-s2p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s2p} \\ 
$\wedge$$\;\;\;\;$({\rm{strchr1}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth})\index{strchr1} $\not\in\;${\bf{N}}${}$))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{sn\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{sn\/}})\index{mc-pc} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-dn}}\,({\tt{32}}, {\tt{0}}, {\it{sn\/}})\index{read-dn} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{sn\/}})\index{mc-rfile})\index{read-rn} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\it{sn\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{add}}\,({\tt{32}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}, {\tt{8}})\index{add})\- \\ 
$\wedge$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{sn\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem}))\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-s2-sn-rfile \\ \index{strstr-s2-sn-rfile}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strstr-t1}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strstr-t1})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strstr-s2p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s2p} \\ 
$\wedge$$\;\;\;\;$({\rm{strchr1}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth})\index{strchr1} $\not\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p} \\ 
$\wedge$$\;\;\;\;$({\it{oplen\/}} $\leq$ {\tt{32}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{sn\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{d4-7a4-5p}}\,({\it{rn\/}})\index{d4-7a4-5p}$\;\;${\bf then }{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn} \\ 
{\bf else }{\rm{get-vlst}}\,(\=\+{\it{oplen\/}}, \\ 
{\tt{0}}, \\ 
{\it{rn\/}}, \\ 
{\tt{'}}{\tt{(}}{\tt{2}}{\tt{ }}{\tt{3}}{\tt{ }}{\tt{10}}{\tt{ }}{\tt{11}}{\tt{)}}, \\ 
{\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved})\-\index{get-vlst}$\;${\bf  endif}\-)\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim}; put together: s --> s1.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strstr-s-s2 \\ \index{strstr-s-s2}
\=\+{\bf let }\=\+{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strstr-t0}}\,({\it{n2\/}}, {\it{lst2\/}})\index{strstr-t0})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strstr-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr-statep} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth} $\not=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{strstr-s2p}}\,(\=\+{\it{s2\/}}, \\ 
{\tt{0}}, \\ 
{\tt{0}}, \\ 
{\it{str1\/}}, \\ 
{\it{n1\/}}, \\ 
{\it{lst1\/}}, \\ 
{\it{str2\/}}, \\ 
{\it{n2\/}}, \\ 
{\it{lst2\/}}, \\ 
{\rm{strlen}}\,({\tt{0}}, {\it{n2\/}} $-\;1$, {\rm{mcdr}}\,({\tt{1}}, {\it{lst2\/}})\index{mcdr})\index{strlen})\-\index{strstr-s2p}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-s-s2-else \\ \index{strstr-s-s2-else}
\=\+{\bf let }\=\+{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strstr-t0}}\,({\it{n2\/}}, {\it{lst2\/}})\index{strstr-t0})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strstr-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr-statep} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth} $\not=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{linked-rts-addr}}\,({\it{s2\/}})\index{linked-rts-addr} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\it{s2\/}})\index{linked-a6} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s2\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{movem-saved}}\,({\it{s2\/}}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved} \\ 
$=$$\;\;\;\;${\rm{readm-rn}}\,({\tt{32}}, {\tt{'}}{\tt{(}}{\tt{2}}{\tt{ }}{\tt{3}}{\tt{ }}{\tt{10}}{\tt{ }}{\tt{11}}{\tt{)}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{readm-rn})\-)\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-s-s2-rfile \\ \index{strstr-s-s2-rfile}
\=\+{\bf let }\=\+{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strstr-t0}}\,({\it{n2\/}}, {\it{lst2\/}})\index{strstr-t0})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strstr-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr-statep} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{d4-7a4-5p}}\,({\it{rn\/}})\index{d4-7a4-5p})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s2\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-s-s2-mem \\ \index{strstr-s-s2-mem}
\=\+{\bf let }\=\+{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strstr-t0}}\,({\it{n2\/}}, {\it{lst2\/}})\index{strstr-t0})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strstr-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr-statep} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{48}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{60}})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s2\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-$\;${\bf  endlet}\-
\end{tabbing}     

\begin{verbatim}; put together: s2 --> s2.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strstr-s2-s2-1 \\ \index{strstr-s2-s2-1}
\=\+{\bf let }\=\+{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strstr-t2}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-t2})\index{stepn}, \\ 
{\it{j*\/}}{\bf $\;$ be$\;\;$}{\rm{strchr1*}}\,({\it{i*\/}}, {\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth})\index{strchr1*}, \\ 
{\it{j\/}}{\bf $\;$ be$\;\;$}{\rm{strchr1}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth})\index{strchr1}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strstr-s2p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s2p} \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{strncmp}}\,({\it{len\/}}, {\rm{mcdr}}\,($1\;+$ {\it{j\/}}, {\it{lst1\/}})\index{mcdr}, {\rm{mcdr}}\,({\tt{1}}, {\it{lst2\/}})\index{mcdr})\index{strncmp} $\not=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{strstr-s2p}}\,(\=\+{\it{s2\/}}, \\ 
{\rm{add}}\,({\tt{32}}, {\it{j*\/}}, {\tt{1}})\index{add}, \\ 
$1\;+$ {\it{j\/}}, \\ 
{\it{str1\/}}, \\ 
{\it{n1\/}}, \\ 
{\it{lst1\/}}, \\ 
{\it{str2\/}}, \\ 
{\it{n2\/}}, \\ 
{\it{lst2\/}}, \\ 
{\it{len\/}})\-\index{strstr-s2p} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s2\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\- \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\it{s2\/}})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\it{s2\/}})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$({\rm{movem-saved}}\,({\it{s2\/}}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved} $=$ {\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved}))\-\-$\;${\bf  endlet}\-
\end{tabbing}   

\begin{tabbing}{\sc Theorem}:  strstr-s2-s2-rfile-1 \\ \index{strstr-s2-s2-rfile-1}
\=\+{\bf let }\=\+{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strstr-t2}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-t2})\index{stepn}, \\ 
{\it{j\/}}{\bf $\;$ be$\;\;$}{\rm{strchr1}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth})\index{strchr1}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strstr-s2p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s2p} \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{strncmp}}\,({\it{len\/}}, {\rm{mcdr}}\,($1\;+$ {\it{j\/}}, {\it{lst1\/}})\index{mcdr}, {\rm{mcdr}}\,({\tt{1}}, {\it{lst2\/}})\index{mcdr})\index{strncmp} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{oplen\/}} $\leq$ {\tt{32}}) \\ 
$\wedge$$\;\;\;\;${\rm{d4-7a4-5p}}\,({\it{rn\/}})\index{d4-7a4-5p})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s2\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-s2-s2-mem-1 \\ \index{strstr-s2-s2-mem-1}
\=\+{\bf let }\=\+{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strstr-t2}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-t2})\index{stepn}, \\ 
{\it{j\/}}{\bf $\;$ be$\;\;$}{\rm{strchr1}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth})\index{strchr1}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strstr-s2p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s2p} \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{strncmp}}\,({\it{len\/}}, {\rm{mcdr}}\,($1\;+$ {\it{j\/}}, {\it{lst1\/}})\index{mcdr}, {\rm{mcdr}}\,({\tt{1}}, {\it{lst2\/}})\index{mcdr})\index{strncmp} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{44}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{60}})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s2\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim}; put together: s2 --> sn.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strstr-s2-sn-base-1 \\ \index{strstr-s2-sn-base-1}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strstr-t2}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-t2})\index{stepn}, \\ 
{\it{j*\/}}{\bf $\;$ be$\;\;$}{\rm{strchr1*}}\,({\it{i*\/}}, {\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth})\index{strchr1*}, \\ 
{\it{j\/}}{\bf $\;$ be$\;\;$}{\rm{strchr1}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth})\index{strchr1}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strstr-s2p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s2p} \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{strncmp}}\,({\it{len\/}}, {\rm{mcdr}}\,($1\;+$ {\it{j\/}}, {\it{lst1\/}})\index{mcdr}, {\rm{mcdr}}\,({\tt{1}}, {\it{lst2\/}})\index{mcdr})\index{strncmp} $=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{sn\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{sn\/}})\index{mc-pc} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-dn}}\,({\tt{32}}, {\tt{0}}, {\it{sn\/}})\index{read-dn} $=$ {\rm{add}}\,({\tt{32}}, {\it{str1\/}}, {\it{j*\/}})\index{add}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{sn\/}})\index{mc-rfile})\index{read-rn} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\it{sn\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{add}}\,({\tt{32}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}, {\tt{8}})\index{add})\-)\-\-$\;${\bf  endlet}\-
\end{tabbing}   

\begin{tabbing}{\sc Theorem}:  strstr-s2-sn-base-rfile-1 \\ \index{strstr-s2-sn-base-rfile-1}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strstr-t2}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-t2})\index{stepn}, \\ 
{\it{j\/}}{\bf $\;$ be$\;\;$}{\rm{strchr1}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth})\index{strchr1}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strstr-s2p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s2p} \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{strncmp}}\,({\it{len\/}}, {\rm{mcdr}}\,($1\;+$ {\it{j\/}}, {\it{lst1\/}})\index{mcdr}, {\rm{mcdr}}\,({\tt{1}}, {\it{lst2\/}})\index{mcdr})\index{strncmp} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{oplen\/}} $\leq$ {\tt{32}}) \\ 
$\wedge$$\;\;\;\;${\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{sn\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{d4-7a4-5p}}\,({\it{rn\/}})\index{d4-7a4-5p}$\;\;${\bf then }{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn} \\ 
{\bf else }{\rm{get-vlst}}\,(\=\+{\it{oplen\/}}, \\ 
{\tt{0}}, \\ 
{\it{rn\/}}, \\ 
{\tt{'}}{\tt{(}}{\tt{2}}{\tt{ }}{\tt{3}}{\tt{ }}{\tt{10}}{\tt{ }}{\tt{11}}{\tt{)}}, \\ 
{\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved})\-\index{get-vlst}$\;${\bf  endif}\-)\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-s2-sn-base-mem-1 \\ \index{strstr-s2-sn-base-mem-1}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strstr-t2}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-t2})\index{stepn}, \\ 
{\it{j\/}}{\bf $\;$ be$\;\;$}{\rm{strchr1}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\rm{get-nth}}\,({\tt{0}}, {\it{lst2\/}})\index{get-nth})\index{strchr1}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strstr-s2p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s2p} \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{strncmp}}\,({\it{len\/}}, {\rm{mcdr}}\,($1\;+$ {\it{j\/}}, {\it{lst1\/}})\index{mcdr}, {\rm{mcdr}}\,({\tt{1}}, {\it{lst2\/}})\index{mcdr})\index{strncmp} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{44}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{60}})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{sn\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim}; put together: s2 --> sn.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strstr-s2-sn-2 \\ \index{strstr-s2-sn-2}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strstr-t3}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-t3})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{strstr-s2p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s2p} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{sn\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{sn\/}})\index{mc-pc} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-dn}}\,({\tt{32}}, {\tt{0}}, {\it{sn\/}})\index{read-dn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{strstr1}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr1} \\ 
{\bf then }{\rm{add}}\,(\=\+{\tt{32}}, \\ 
{\it{str1\/}}, \\ 
{\rm{strstr1*}}\,({\it{i*\/}}, {\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr1*})\-\index{add} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-)\- \\ 
$\wedge$$\;\;\;\;$({\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{sn\/}})\index{mc-rfile})\index{read-rn} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\it{sn\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{add}}\,({\tt{32}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}, {\tt{8}})\index{add})\-)\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-s2-sn-rfile-2 \\ \index{strstr-s2-sn-rfile-2}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strstr-t3}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-t3})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strstr-s2p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s2p} \\ 
$\wedge$$\;\;\;\;${\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p} \\ 
$\wedge$$\;\;\;\;$({\it{oplen\/}} $\leq$ {\tt{32}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{sn\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{d4-7a4-5p}}\,({\it{rn\/}})\index{d4-7a4-5p}$\;\;${\bf then }{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn} \\ 
{\bf else }{\rm{get-vlst}}\,(\=\+{\it{oplen\/}}, \\ 
{\tt{0}}, \\ 
{\it{rn\/}}, \\ 
{\tt{'}}{\tt{(}}{\tt{2}}{\tt{ }}{\tt{3}}{\tt{ }}{\tt{10}}{\tt{ }}{\tt{11}}{\tt{)}}, \\ 
{\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved})\-\index{get-vlst}$\;${\bf  endif}\-)\-\-$\;${\bf  endlet}\-
\end{tabbing}     

\begin{tabbing}{\sc Theorem}:  strstr-s2-sn-mem-2 \\ \index{strstr-s2-sn-mem-2}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strstr-t3}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-t3})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strstr-s2p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr-s2p} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{44}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{60}})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{sn\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-$\;${\bf  endlet}\-
\end{tabbing}


\noindent{\sc Event}:   Disable strstr-s2p-info.

\addvspace{18pt}

\begin{verbatim}; the correctness of strstr.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strstr-statep-info \\ \index{strstr-statep-info}
\=\+{\rm{strstr-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr-statep} \\ 
$\rightarrow$$\;\;\;\;$(({\it{str1\/}} $\in\;${\bf{N}}${}$) $\wedge$ {\rm{nat-rangep}}\,({\it{str1\/}}, {\tt{32}})\index{nat-rangep})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-correctness \\ \index{strstr-correctness}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strstr-t}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{strstr-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr-statep} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{sn\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{sn\/}})\index{mc-pc} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{sn\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\it{sn\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{add}}\,({\tt{32}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\tt{4}})\index{add})\- \\ 
$\wedge$$\;\;\;\;$(\=\+({\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p} $\wedge$ ({\it{oplen\/}} $\leq$ {\tt{32}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{sn\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{48}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{60}})\index{disjoint} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{sn\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem} \\ 
$=$$\;\;\;\;${\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-dn}}\,({\tt{32}}, {\tt{0}}, {\it{sn\/}})\index{read-dn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{strstr}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr} \\ 
{\bf then }{\rm{add}}\,({\tt{32}}, {\it{str1\/}}, {\rm{strstr*}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr*})\index{add} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-)\-)\-\-$\;${\bf  endlet}\-
\end{tabbing}


\noindent{\sc Event}:   Disable strstr-statep-info.

\addvspace{18pt}

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

\addvspace{18pt}

\begin{verbatim}; strstr* --> strstr.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strchr1*-strchr1 \\ \index{strchr1*-strchr1}
\=\+(\=\+{\rm{strchr1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr1} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $=$ {\rm{nat-to-uint}}\,({\it{i*\/}})\index{nat-to-uint}) \\ 
$\wedge$$\;\;\;\;${\rm{nat-rangep}}\,({\it{i*\/}}, {\tt{32}})\index{nat-rangep} \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\it{n\/}}, {\tt{32}})\index{uint-rangep})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{nat-to-uint}}\,({\rm{strchr1*}}\,({\it{i*\/}}, {\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr1*})\index{nat-to-uint} $=$ {\rm{strchr1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr1})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr*-strstr \\ \index{strstr*-strstr}
\=\+(\=\+{\rm{strstr1}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr1} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $=$ {\rm{nat-to-uint}}\,({\it{i*\/}})\index{nat-to-uint}) \\ 
$\wedge$$\;\;\;\;${\rm{nat-rangep}}\,({\it{i*\/}}, {\tt{32}})\index{nat-rangep} \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\it{n1\/}}, {\tt{32}})\index{uint-rangep})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{nat-to-uint}}\,({\rm{strstr1*}}\,({\it{i*\/}}, {\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr1*})\index{nat-to-uint} \\ 
$=$$\;\;\;\;${\rm{strstr1}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr1})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-non-zerop-la \\ \index{strstr-non-zerop-la}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strstr-t}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strstr-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr-statep} \\ 
$\wedge$$\;\;\;\;${\rm{nat-rangep}}\,({\it{str1\/}}, {\tt{32}})\index{nat-rangep} \\ 
$\wedge$$\;\;\;\;$({\rm{nat-to-uint}}\,({\it{str1\/}})\index{nat-to-uint} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\rm{nat-to-uint}}\,({\it{str1\/}})\index{nat-to-uint} $+$ {\it{n1\/}}, {\tt{32}})\index{uint-rangep} \\ 
$\wedge$$\;\;\;\;$({\it{str1\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{strstr}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{nat-to-uint}}\,({\rm{read-dn}}\,({\tt{32}}, {\tt{0}}, {\it{sn\/}})\index{read-dn})\index{nat-to-uint} $\not=$ {\tt{0}})\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strstr-non-zerop \\ \index{strstr-non-zerop}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strstr-t}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strstr-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr-statep} \\ 
$\wedge$$\;\;\;\;${\rm{strstr}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{nat-to-uint}}\,({\rm{read-dn}}\,({\tt{32}}, {\tt{0}}, {\it{sn\/}})\index{read-dn})\index{nat-to-uint} $\not=$ {\tt{0}})\-$\;${\bf  endlet}\-
\end{tabbing}


\noindent{\sc Event}:   Disable strstr*.

\addvspace{18pt}

\begin{verbatim}; some properties of strstr.
; see the file cstring.events.
\end{verbatim}
%\end{list}
\printindex
\end{document}
