\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{"mc20-2"}} using the compiled version.

\addvspace{18pt}
\begin{verbatim};          Proof of the Correctness of the STRPBRK 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 strpbrk function in the Berkeley string library.

char *
strpbrk(s1, s2)
	register const char *s1, *s2;
{
	register const char *scanp;
	register int c, sc;

	while ((c = *s1++) != 0) {
		for (scanp = s2; (sc = *scanp++) != 0;)
			if (sc == c)
				return ((char *)(s1 - 1));
	}
	return (NULL);
}

Remark. Should the local variables c and sc have type register char?

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

0x2688 <strpbrk>:       linkw fp,#0
0x268c <strpbrk+4>:     moveml d2-d3,sp@-
0x2690 <strpbrk+8>:     moveal fp@(8),a1
0x2694 <strpbrk+12>:    movel fp@(12),d3
0x2698 <strpbrk+16>:    bra 0x26b0 <strpbrk+40>
0x269a <strpbrk+18>:    moveal d3,a0
0x269c <strpbrk+20>:    movel a1,d1
0x269e <strpbrk+22>:    subl #1,d1
0x26a0 <strpbrk+24>:    bra 0x26aa <strpbrk+34>
0x26a2 <strpbrk+26>:    cmpl d0,d2
0x26a4 <strpbrk+28>:    bne 0x26aa <strpbrk+34>
0x26a6 <strpbrk+30>:    movel d1,d0
0x26a8 <strpbrk+32>:    bra 0x26b8 <strpbrk+48>
0x26aa <strpbrk+34>:    moveb a0@+,d0
0x26ac <strpbrk+36>:    extbl d0
0x26ae <strpbrk+38>:    bne 0x26a2 <strpbrk+26>
0x26b0 <strpbrk+40>:    moveb a1@+,d2
0x26b2 <strpbrk+42>:    extbl d2
0x26b4 <strpbrk+44>:    bne 0x269a <strpbrk+18>
0x26b6 <strpbrk+46>:    clrl d0
0x26b8 <strpbrk+48>:    moveml fp@(-8),d2-d3
0x26be <strpbrk+54>:    unlk fp
0x26c0 <strpbrk+56>:    rts

The machine code of the above program is:

<strpbrk>:     0x4e56  0x0000  0x48e7  0x3000  0x226e  0x0008  0x262e  0x000c
<strpbrk+16>:  0x6016  0x2043  0x2209  0x5381  0x6008  0xb480  0x6604  0x2001
<strpbrk+32>:  0x600e  0x1018  0x49c0  0x66f2  0x1419  0x49c2  0x66e4  0x4280
<strpbrk+48>:  0x4cee  0x000c  0xfff8  0x4e5e  0x4e75

'(78      86      0       0       72      231     48      0
  34      110     0       8       38      46      0       12
  96      22      32      67      34      9       83      129
  96      8       180     128     102     4       32      1
  96      14      16      24      73      192     102     242
  20      25      73      194     102     228     66      128
  76      238     0       12      255     248     78      94
  78      117)
|#

; in the logic, the above program is defined by (strpbrk-code).
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{strpbrk-code} \\  
\=\+{\sc{strpbrk-code}}\index{strpbrk-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{0}}{\tt{ }}{\tt{34}}{\tt{ }}{\tt{110}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{8}}{\tt{ }}{\tt{38}}{\tt{ }}{\tt{46}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{12}}{\tt{ }}{\tt{96}}{\tt{ }}{\tt{22}}{\tt{ }}{\tt{32}} \\ 
{\tt{67}}{\tt{ }}{\tt{34}}{\tt{ }}{\tt{9}}{\tt{ }}{\tt{83}}{\tt{ }}{\tt{129}}{\tt{ }}{\tt{96}}{\tt{ }}{\tt{8}}{\tt{ }}{\tt{180}}{\tt{ }}{\tt{128}}{\tt{ }}{\tt{102}}{\tt{ }}{\tt{4}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{1}}{\tt{ }}{\tt{96}}{\tt{ }}{\tt{14}}{\tt{ }}{\tt{16}}{\tt{ }}{\tt{24}} \\ 
{\tt{73}}{\tt{ }}{\tt{192}}{\tt{ }}{\tt{102}}{\tt{ }}{\tt{242}}{\tt{ }}{\tt{20}}{\tt{ }}{\tt{25}}{\tt{ }}{\tt{73}}{\tt{ }}{\tt{194}}{\tt{ }}{\tt{102}}{\tt{ }}{\tt{228}}{\tt{ }}{\tt{66}}{\tt{ }}{\tt{128}}{\tt{ }}{\tt{76}}{\tt{ }}{\tt{238}}{\tt{ }}{\tt{0}} \\ 
{\tt{12}}{\tt{ }}{\tt{255}}{\tt{ }}{\tt{248}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{94}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{117}}{\tt{)}}\-\-
\end{tabbing}

\begin{verbatim}; the computation time of the program.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{strpbrk-t0} \\  
\=\+{\rm{strpbrk-t0}}\,({\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strpbrk-t0} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i2\/}} $<$ {\it{n2\/}} \\ 
{\bf then }\=\+{\bf if }{\rm{get-nth}}\,({\it{i2\/}}, {\it{lst2\/}})\index{get-nth} $=$ {\tt{0}}$\;\;${\bf then }{\tt{3}} \\ 
{\bf elseif }{\rm{get-nth}}\,({\it{i2\/}}, {\it{lst2\/}})\index{get-nth} $=$ {\it{ch\/}}$\;\;${\bf then }{\tt{10}} \\ 
{\bf else }{\rm{splus}}\,({\tt{5}}, {\rm{strpbrk-t0}}\,($1\;+$ {\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strpbrk-t0})\index{splus}$\;${\bf  endif}\- \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{strpbrk-t1} \\  
{\rm{strpbrk-t1}}\,({\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strpbrk-t1} $=$ {\rm{splus}}\,({\tt{7}}, {\rm{strpbrk-t0}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strpbrk-t0})\index{splus}
\end{tabbing}

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

\begin{tabbing}{\sc Definition}:\index{strpbrk-t} \\  
{\rm{strpbrk-t}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk-t} $=$ {\rm{splus}}\,({\tt{5}}, {\rm{strpbrk-t2}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk-t2})\index{splus}
\end{tabbing}

\begin{verbatim}; two induction hints.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{strpbrk-induct0} \\  
\=\+{\rm{strpbrk-induct0}}\,({\it{s\/}}, {\it{i2*\/}}, {\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strpbrk-induct0} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i2\/}} $<$ {\it{n2\/}} \\ 
{\bf then }\=\+{\bf if }{\rm{get-nth}}\,({\it{i2\/}}, {\it{lst2\/}})\index{get-nth} $=$ {\tt{0}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{get-nth}}\,({\it{i2\/}}, {\it{lst2\/}})\index{get-nth} $=$ {\it{ch\/}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{strpbrk-induct0}}\,(\=\+{\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\index{stepn}, \\ 
{\rm{add}}\,({\tt{32}}, {\it{i2*\/}}, {\tt{1}})\index{add}, \\ 
$1\;+$ {\it{i2\/}}, \\ 
{\it{n2\/}}, \\ 
{\it{lst2\/}}, \\ 
{\it{ch\/}})\-\index{strpbrk-induct0}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{strpbrk-induct1} \\  
\=\+{\rm{strpbrk-induct1}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk-induct1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i1\/}} $<$ {\it{n1\/}} \\ 
{\bf then }\=\+{\bf if }\=\+({\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\tt{0}}) \\ 
$\vee$$\;\;\;\;${\rm{strchr1}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth})\index{strchr1}\-$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{strpbrk-induct1}}\,(\=\+{\rm{stepn}}\,(\=\+{\it{s\/}}, \\ 
{\rm{strpbrk-t1}}\,(\=\+{\it{n2\/}}, \\ 
{\it{lst2\/}}, \\ 
{\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth})\-\index{strpbrk-t1})\-\index{stepn}, \\ 
{\rm{add}}\,({\tt{32}}, {\it{i1*\/}}, {\tt{1}})\index{add}, \\ 
$1\;+$ {\it{i1\/}}, \\ 
{\it{n1\/}}, \\ 
{\it{lst1\/}}, \\ 
{\it{n2\/}}, \\ 
{\it{lst2\/}})\-\index{strpbrk-induct1}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; the preconditions of the initial state.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{strpbrk-statep} \\  
\=\+{\rm{strpbrk-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk-statep} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{evenp}}\,({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{evenp} \\ 
$\wedge$$\;\;\;\;${\rm{rom-addrp}}\,({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{58}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{strpbrk-code}}\index{strpbrk-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{12}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{24}})\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{12}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{24}}, {\it{str1\/}}, {\it{n1\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{sub}}\,({\tt{32}}, {\tt{12}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{24}}, {\it{str2\/}}, {\it{n2\/}})\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$$\;\;\;\;$({\it{n1\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{n2\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\it{n1\/}}, {\tt{32}})\index{uint-rangep} \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\it{n2\/}}, {\tt{32}})\index{uint-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})\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{strpbrk-s0p} \\  
\=\+{\rm{strpbrk-s0p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk-s0p} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{evenp}}\,({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{evenp} \\ 
$\wedge$$\;\;\;\;${\rm{rom-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{40}}, {\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{58}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{40}}, {\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{strpbrk-code}}\index{strpbrk-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{8}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{24}})\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{8}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{24}}, {\it{str1\/}}, {\it{n1\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{sub}}\,({\tt{32}}, {\tt{8}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{24}}, {\it{str2\/}}, {\it{n2\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{1}}, {\it{s\/}})\index{read-an}, {\rm{add}}\,({\tt{32}}, {\it{str1\/}}, {\it{i1*\/}})\index{add})\index{equal*} \\ 
$\wedge$$\;\;\;\;$({\it{str2\/}} $=$ {\rm{read-dn}}\,({\tt{32}}, {\tt{3}}, {\it{s\/}})\index{read-dn}) \\ 
$\wedge$$\;\;\;\;$({\it{i1*\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{nat-rangep}}\,({\it{i1*\/}}, {\tt{32}})\index{nat-rangep} \\ 
$\wedge$$\;\;\;\;$({\it{i1\/}} $=$ {\rm{nat-to-uint}}\,({\it{i1*\/}})\index{nat-to-uint}) \\ 
$\wedge$$\;\;\;\;$({\rm{slen}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}})\index{slen} $<$ {\it{n1\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{slen}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}})\index{slen} $<$ {\it{n2\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{n1\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{n2\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\it{n1\/}}, {\tt{32}})\index{uint-rangep} \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\it{n2\/}}, {\tt{32}})\index{uint-rangep})\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{strpbrk-s1p} \\  
\=\+{\rm{strpbrk-s1p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{i2*\/}}, {\it{i2\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strpbrk-s1p} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{evenp}}\,({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{evenp} \\ 
$\wedge$$\;\;\;\;${\rm{rom-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{34}}, {\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{58}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{34}}, {\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{strpbrk-code}}\index{strpbrk-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{8}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{24}})\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{8}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{24}}, {\it{str1\/}}, {\it{n1\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{sub}}\,({\tt{32}}, {\tt{8}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{24}}, {\it{str2\/}}, {\it{n2\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{1}}, {\it{s\/}})\index{read-an}, {\rm{add}}\,({\tt{32}}, {\it{str1\/}}, {\it{i1*\/}})\index{add})\index{equal*} \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{0}}, {\it{s\/}})\index{read-an}, {\rm{add}}\,({\tt{32}}, {\it{str2\/}}, {\it{i2*\/}})\index{add})\index{equal*} \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-dn}}\,({\tt{32}}, {\tt{1}}, {\it{s\/}})\index{read-dn}, {\rm{sub}}\,({\tt{32}}, {\tt{1}}, {\rm{read-an}}\,({\tt{32}}, {\tt{1}}, {\it{s\/}})\index{read-an})\index{sub})\index{equal*} \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-dn}}\,({\tt{32}}, {\tt{2}}, {\it{s\/}})\index{read-dn}, {\rm{ext}}\,({\tt{8}}, {\rm{read-dn}}\,({\tt{8}}, {\tt{2}}, {\it{s\/}})\index{read-dn}, {\tt{32}})\index{ext})\index{equal*} \\ 
$\wedge$$\;\;\;\;$({\it{str2\/}} $=$ {\rm{read-dn}}\,({\tt{32}}, {\tt{3}}, {\it{s\/}})\index{read-dn}) \\ 
$\wedge$$\;\;\;\;$({\it{ch\/}} $=$ {\rm{uread-dn}}\,({\tt{8}}, {\tt{2}}, {\it{s\/}})\index{uread-dn}) \\ 
$\wedge$$\;\;\;\;$({\rm{slen}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}})\index{slen} $<$ {\it{n1\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{slen}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}})\index{slen} $<$ {\it{n2\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{slen}}\,({\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{slen} $<$ {\it{n2\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i1*\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{nat-rangep}}\,({\it{i1*\/}}, {\tt{32}})\index{nat-rangep} \\ 
$\wedge$$\;\;\;\;$({\it{i1\/}} $=$ {\rm{nat-to-uint}}\,({\it{i1*\/}})\index{nat-to-uint}) \\ 
$\wedge$$\;\;\;\;$({\it{i2*\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{nat-rangep}}\,({\it{i2*\/}}, {\tt{32}})\index{nat-rangep} \\ 
$\wedge$$\;\;\;\;$({\it{i2\/}} $=$ {\rm{nat-to-uint}}\,({\it{i2*\/}})\index{nat-to-uint}) \\ 
$\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}; from the initial state s to s0: s --> s0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strpbrk-s-s0 \\ \index{strpbrk-s-s0}
\=\+{\rm{strpbrk-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk-statep} \\ 
$\rightarrow$$\;\;\;\;${\rm{strpbrk-s0p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\index{stepn}, {\tt{0}}, {\tt{0}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk-s0p}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strpbrk-s-s0-else \\ \index{strpbrk-s-s0-else}
\=\+{\rm{strpbrk-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk-statep} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\index{stepn})\index{linked-a6} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\index{stepn})\index{read-an} $=$ {\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{5}})\index{stepn}, {\tt{4}}, {\tt{8}}, {\tt{2}})\index{movem-saved} \\ 
$=$$\;\;\;\;${\rm{readm-rn}}\,({\tt{32}}, {\tt{'}}{\tt{(}}{\tt{2}}{\tt{ }}{\tt{3}}{\tt{)}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{readm-rn})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strpbrk-s-s0-rfile \\ \index{strpbrk-s-s0-rfile}
\=\+({\rm{strpbrk-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk-statep} $\wedge$ {\rm{d4-7a2-5p}}\,({\it{rn\/}})\index{d4-7a2-5p}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\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}:  strpbrk-s-s0-mem \\ \index{strpbrk-s-s0-mem}
\=\+(\=\+{\rm{strpbrk-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk-statep} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{12}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{24}})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\index{stepn})\index{mc-mem}, {\it{k\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-
\end{tabbing}

\begin{verbatim}; from s0 to exit.
; base case.  s0 --> sn, when lst1[i1] = 0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strpbrk-s0-sn-base1 \\ \index{strpbrk-s0-sn-base1}
\=\+(\=\+{\rm{strpbrk-s0p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk-s0p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i1\/}}, {\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-an}}\,({\tt{32}}, {\tt{6}}, {\rm{stepn}}\,({\it{s\/}}, {\tt{7}})\index{stepn})\index{read-an} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-an}}\,({\tt{32}}, {\tt{7}}, {\rm{stepn}}\,({\it{s\/}}, {\tt{7}})\index{stepn})\index{read-an} $=$ {\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}:  strpbrk-s0-sn-rfile-base1 \\ \index{strpbrk-s0-sn-rfile-base1}
\=\+(\=\+{\rm{strpbrk-s0p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk-s0p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\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{7}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{d4-7a2-5p}}\,({\it{rn\/}})\index{d4-7a2-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{)}}, {\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{8}}, {\tt{2}})\index{movem-saved})\index{get-vlst}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{verbatim}; induction case. s0 --> s0, when lst1[i1] =\= 0.
; from s0 to s1: s0 --> s1, when lst1[i1] =\= 0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strpbrk-s0-s1 \\ \index{strpbrk-s0-s1}
\=\+(\=\+{\rm{strpbrk-s0p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk-s0p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth} $\not=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{strpbrk-s1p}}\,(\=\+{\rm{stepn}}\,({\it{s\/}}, {\tt{7}})\index{stepn}, \\ 
{\rm{add}}\,({\tt{32}}, {\it{i1*\/}}, {\tt{1}})\index{add}, \\ 
$1\;+$ {\it{i1\/}}, \\ 
{\it{str1\/}}, \\ 
{\it{n1\/}}, \\ 
{\it{lst1\/}}, \\ 
{\tt{0}}, \\ 
{\tt{0}}, \\ 
{\it{str2\/}}, \\ 
{\it{n2\/}}, \\ 
{\it{lst2\/}}, \\ 
{\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth})\-\index{strpbrk-s1p}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strpbrk-s0-s1-else \\ \index{strpbrk-s0-s1-else}
\=\+(\=\+{\rm{strpbrk-s0p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk-s0p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth} $\not=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\rm{stepn}}\,({\it{s\/}}, {\tt{7}})\index{stepn})\index{read-an} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{7}})\index{stepn})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{7}})\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{7}})\index{stepn}, {\tt{4}}, {\tt{8}}, {\tt{2}})\index{movem-saved} $=$ {\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{8}}, {\tt{2}})\index{movem-saved}) \\ 
$\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}:  strpbrk-s0-s1-rfile \\ \index{strpbrk-s0-s1-rfile}
\=\+(\=\+{\rm{strpbrk-s0p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk-s0p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{d4-7a2-5p}}\,({\it{rn\/}})\index{d4-7a2-5p})\- \\ 
$\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} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-\-
\end{tabbing}

\begin{verbatim}; from s1 to s0: 
; base case. s1 --> s0, when lst2[i2] = 0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strpbrk-s1-s0-base \\ \index{strpbrk-s1-s0-base}
\=\+(\=\+{\rm{strpbrk-s1p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{i2*\/}}, {\it{i2\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strpbrk-s1p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i2\/}}, {\it{lst2\/}})\index{get-nth} $=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{strpbrk-s0p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{3}})\index{stepn}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk-s0p} \\ 
$\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-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{3}})\index{stepn})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\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{movem-saved}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{3}})\index{stepn}, {\tt{4}}, {\tt{8}}, {\tt{2}})\index{movem-saved} $=$ {\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{8}}, {\tt{2}})\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}:  strpbrk-s1-s0-rfile-base \\ \index{strpbrk-s1-s0-rfile-base}
\=\+(\=\+{\rm{strpbrk-s1p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{i2*\/}}, {\it{i2\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strpbrk-s1p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i2\/}}, {\it{lst2\/}})\index{get-nth} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{d4-7a2-5p}}\,({\it{rn\/}})\index{d4-7a2-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}; induction case. s1 --> s1, when lst2[i2] =\= 0 and lst2[i2] =\= ch.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strpbrk-s1-s1 \\ \index{strpbrk-s1-s1}
\=\+(\=\+{\rm{strpbrk-s1p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{i2*\/}}, {\it{i2\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strpbrk-s1p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i2\/}}, {\it{lst2\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i2\/}}, {\it{lst2\/}})\index{get-nth} $\not=$ {\it{ch\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{strpbrk-s1p}}\,(\=\+{\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\index{stepn}, \\ 
{\it{i1*\/}}, \\ 
{\it{i1\/}}, \\ 
{\it{str1\/}}, \\ 
{\it{n1\/}}, \\ 
{\it{lst1\/}}, \\ 
{\rm{add}}\,({\tt{32}}, {\it{i2*\/}}, {\tt{1}})\index{add}, \\ 
$1\;+$ {\it{i2\/}}, \\ 
{\it{str2\/}}, \\ 
{\it{n2\/}}, \\ 
{\it{lst2\/}}, \\ 
{\it{ch\/}})\-\index{strpbrk-s1p} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\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{5}})\index{stepn})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\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{5}})\index{stepn}, {\tt{4}}, {\tt{8}}, {\tt{2}})\index{movem-saved} $=$ {\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{8}}, {\tt{2}})\index{movem-saved}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\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}:  strpbrk-s1-s1-rfile \\ \index{strpbrk-s1-s1-rfile}
\=\+(\=\+{\rm{strpbrk-s1p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{i2*\/}}, {\it{i2\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strpbrk-s1p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i2\/}}, {\it{lst2\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i2\/}}, {\it{lst2\/}})\index{get-nth} $\not=$ {\it{ch\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{d4-7a2-5p}}\,({\it{rn\/}})\index{d4-7a2-5p})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\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.  s1 --> s0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strpbrk-s1p-info \\ \index{strpbrk-s1p-info}
\=\+{\rm{strpbrk-s1p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{i2*\/}}, {\it{i2\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strpbrk-s1p} \\ 
$\rightarrow$$\;\;\;\;$(({\it{i2\/}} $<$ {\it{n2\/}}) $=$ {\bf{t}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strpbrk-s1-s0 \\ \index{strpbrk-s1-s0}
\=\+{\bf let }\=\+{\it{s0\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strpbrk-t0}}\,({\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strpbrk-t0})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strpbrk-s1p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{i2*\/}}, {\it{i2\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strpbrk-s1p} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{strchr1}}\,({\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strchr1}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{strpbrk-s0p}}\,({\it{s0\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk-s0p} \\ 
$\wedge$$\;\;\;\;$({\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s0\/}})\index{read-an} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\it{s0\/}})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\it{s0\/}})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{movem-saved}}\,({\it{s0\/}}, {\tt{4}}, {\tt{8}}, {\tt{2}})\index{movem-saved} $=$ {\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{8}}, {\tt{2}})\index{movem-saved}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s0\/}})\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}:  strpbrk-s1-s0-rfile \\ \index{strpbrk-s1-s0-rfile}
\=\+(\=\+{\rm{strpbrk-s1p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{i2*\/}}, {\it{i2\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strpbrk-s1p} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{strchr1}}\,({\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strchr1}) \\ 
$\wedge$$\;\;\;\;${\rm{d4-7a2-5p}}\,({\it{rn\/}})\index{d4-7a2-5p})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{strpbrk-t0}}\,({\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strpbrk-t0})\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 s1 to exit:
; base case. s1 --> sn, when lst2[i2] =\= 0 and lst2[i2] = ch.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strpbrk-s1-sn-base \\ \index{strpbrk-s1-sn-base}
\=\+(\=\+{\rm{strpbrk-s1p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{i2*\/}}, {\it{i2\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strpbrk-s1p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i2\/}}, {\it{lst2\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i2\/}}, {\it{lst2\/}})\index{get-nth} $=$ {\it{ch\/}}))\- \\ 
$\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{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-dn}}\,({\tt{32}}, {\tt{0}}, {\rm{stepn}}\,({\it{s\/}}, {\tt{10}})\index{stepn})\index{read-dn} $=$ {\rm{add}}\,({\tt{32}}, {\it{str1\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{1}}, {\it{i1*\/}})\index{sub})\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{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\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{6}}, {\it{s\/}})\index{read-an}, {\tt{8}})\index{add})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{10}})\index{stepn})\index{mc-mem}, {\it{k\/}})\index{read-mem} \\ 
$=$$\;\;\;\;${\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strpbrk-s1-sn-rfile-base \\ \index{strpbrk-s1-sn-rfile-base}
\=\+(\=\+{\rm{strpbrk-s1p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{i2*\/}}, {\it{i2\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strpbrk-s1p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i2\/}}, {\it{lst2\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i2\/}}, {\it{lst2\/}})\index{get-nth} $=$ {\it{ch\/}}) \\ 
$\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} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{d4-7a2-5p}}\,({\it{rn\/}})\index{d4-7a2-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{)}}, {\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{8}}, {\tt{2}})\index{movem-saved})\index{get-vlst}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{verbatim}; put together.  s1 --> sn.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strpbrk-s1-sn \\ \index{strpbrk-s1-sn}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strpbrk-t0}}\,({\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strpbrk-t0})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strpbrk-s1p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{i2*\/}}, {\it{i2\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strpbrk-s1p} \\ 
$\wedge$$\;\;\;\;${\rm{strchr1}}\,({\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strchr1})\- \\ 
$\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\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{1}}, {\it{i1*\/}})\index{sub})\index{add}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{sn\/}})\index{read-an} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-an}}\,({\tt{32}}, {\tt{7}}, {\it{sn\/}})\index{read-an} $=$ {\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}:  strpbrk-s1-sn-rfile \\ \index{strpbrk-s1-sn-rfile}
\=\+(\=\+{\rm{strpbrk-s1p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{i2*\/}}, {\it{i2\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strpbrk-s1p} \\ 
$\wedge$$\;\;\;\;${\rm{strchr1}}\,({\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strchr1} \\ 
$\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\/}}, {\rm{strpbrk-t0}}\,({\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strpbrk-t0})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{d4-7a2-5p}}\,({\it{rn\/}})\index{d4-7a2-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{)}}, {\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{8}}, {\tt{2}})\index{movem-saved})\index{get-vlst}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{verbatim}; base case 2. from s0 --> sn.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strpbrk-s0-sn-base2 \\ \index{strpbrk-s0-sn-base2}
\=\+{\bf let }\=\+{\it{ch\/}}{\bf $\;$ be$\;\;$}{\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth}, \\ 
{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strpbrk-t1}}\,({\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth})\index{strpbrk-t1})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strpbrk-s0p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk-s0p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{strchr1}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strchr1})\- \\ 
$\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{i1*\/}})\index{add}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{sn\/}})\index{read-an} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-an}}\,({\tt{32}}, {\tt{7}}, {\it{sn\/}})\index{read-an} $=$ {\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}:  strpbrk-s0-sn-rfile-base2 \\ \index{strpbrk-s0-sn-rfile-base2}
\=\+{\bf let }\=\+{\it{ch\/}}{\bf $\;$ be$\;\;$}{\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strpbrk-s0p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk-s0p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{strchr1}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strchr1} \\ 
$\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\/}}, {\rm{strpbrk-t1}}\,({\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strpbrk-t1})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{d4-7a2-5p}}\,({\it{rn\/}})\index{d4-7a2-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{)}}, \\ 
{\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{8}}, {\tt{2}})\index{movem-saved})\-\index{get-vlst}$\;${\bf  endif}\-)\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim}; induction case.  from s0 --> s0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strpbrk-s0-s0 \\ \index{strpbrk-s0-s0}
\=\+{\bf let }\=\+{\it{ch\/}}{\bf $\;$ be$\;\;$}{\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth}, \\ 
{\it{s0\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strpbrk-t1}}\,({\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth})\index{strpbrk-t1})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strpbrk-s0p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk-s0p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{strchr1}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strchr1}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{strpbrk-s0p}}\,(\=\+{\it{s0\/}}, \\ 
{\rm{add}}\,({\tt{32}}, {\it{i1*\/}}, {\tt{1}})\index{add}, \\ 
$1\;+$ {\it{i1\/}}, \\ 
{\it{str1\/}}, \\ 
{\it{n1\/}}, \\ 
{\it{lst1\/}}, \\ 
{\it{str2\/}}, \\ 
{\it{n2\/}}, \\ 
{\it{lst2\/}})\-\index{strpbrk-s0p} \\ 
$\wedge$$\;\;\;\;$({\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s0\/}})\index{read-an} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\it{s0\/}})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\it{s0\/}})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{movem-saved}}\,({\it{s0\/}}, {\tt{4}}, {\tt{8}}, {\tt{2}})\index{movem-saved} $=$ {\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{8}}, {\tt{2}})\index{movem-saved}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s0\/}})\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}:  strpbrk-s0-s0-rfile \\ \index{strpbrk-s0-s0-rfile}
\=\+{\bf let }\=\+{\it{ch\/}}{\bf $\;$ be$\;\;$}{\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strpbrk-s0p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk-s0p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{strchr1}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strchr1}) \\ 
$\wedge$$\;\;\;\;${\rm{d4-7a2-5p}}\,({\it{rn\/}})\index{d4-7a2-5p})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{strpbrk-t1}}\,({\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strpbrk-t1})\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})\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim}; put together.  s0 --> sn.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strpbrk-s0p-info \\ \index{strpbrk-s0p-info}
{\rm{strpbrk-s0p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk-s0p} $\rightarrow$ (({\it{i1\/}} $<$ {\it{n1\/}}) $=$ {\bf{t}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strpbrk-s0-sn \\ \index{strpbrk-s0-sn}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strpbrk-t2}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk-t2})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{strpbrk-s0p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk-s0p} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{sn\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{sn\/}})\index{mc-pc} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-dn}}\,({\tt{32}}, {\tt{0}}, {\it{sn\/}})\index{read-dn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{strpbrk}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk} \\ 
{\bf then }{\rm{add}}\,(\=\+{\tt{32}}, \\ 
{\it{str1\/}}, \\ 
{\rm{strpbrk*}}\,({\it{i1*\/}}, {\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk*})\-\index{add} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-)\- \\ 
$\wedge$$\;\;\;\;$({\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{sn\/}})\index{read-an} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-an}}\,({\tt{32}}, {\tt{7}}, {\it{sn\/}})\index{read-an} $=$ {\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}:  strpbrk-s0-sn-rfile \\ \index{strpbrk-s0-sn-rfile}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strpbrk-t2}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk-t2})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strpbrk-s0p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk-s0p} \\ 
$\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-7a2-5p}}\,({\it{rn\/}})\index{d4-7a2-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{)}}, \\ 
{\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{8}}, {\tt{2}})\index{movem-saved})\-\index{get-vlst}$\;${\bf  endif}\-)\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim}; the correctness of strpbrk.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strpbrk-correctness \\ \index{strpbrk-correctness}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strpbrk-t}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{strpbrk-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk-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-an}}\,({\tt{32}}, {\tt{6}}, {\it{sn\/}})\index{read-an} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-an}}\,({\tt{32}}, {\tt{7}}, {\it{sn\/}})\index{read-an} $=$ {\rm{add}}\,({\tt{32}}, {\rm{read-an}}\,({\tt{32}}, {\tt{7}}, {\it{s\/}})\index{read-an}, {\tt{4}})\index{add}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p} $\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{12}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{24}})\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{strpbrk}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk} \\ 
{\bf then }{\rm{add}}\,(\=\+{\tt{32}}, \\ 
{\it{str1\/}}, \\ 
{\rm{strpbrk*}}\,({\tt{0}}, {\tt{0}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk*})\-\index{add} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-)\-)\-\-$\;${\bf  endlet}\-
\end{tabbing}


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

\addvspace{18pt}

\begin{verbatim}; strpbrk* --> strpbrk.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strpbrk*-strpbrk \\ \index{strpbrk*-strpbrk}
\=\+(\=\+{\rm{strpbrk}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk} \\ 
$\wedge$$\;\;\;\;$({\it{i1\/}} $=$ {\rm{nat-to-uint}}\,({\it{i1*\/}})\index{nat-to-uint}) \\ 
$\wedge$$\;\;\;\;${\rm{nat-rangep}}\,({\it{i1*\/}}, {\tt{32}})\index{nat-rangep} \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\it{n1\/}}, {\tt{32}})\index{uint-rangep})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{nat-to-uint}}\,({\rm{strpbrk*}}\,({\it{i1*\/}}, {\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk*})\index{nat-to-uint} \\ 
$=$$\;\;\;\;${\rm{strpbrk}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strpbrk-non-zerop-la \\ \index{strpbrk-non-zerop-la}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strpbrk-t}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strpbrk-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk-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$$\;\;\;\;${\rm{strpbrk}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk})\- \\ 
$\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}:  strpbrk-non-zerop \\ \index{strpbrk-non-zerop}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strpbrk-t}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strpbrk-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk-statep} \\ 
$\wedge$$\;\;\;\;${\rm{strpbrk}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk})\- \\ 
$\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 strpbrk*.

\addvspace{18pt}

\begin{verbatim}; some properties of strrchr.
; see file cstring.events.

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