\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 STRCHR 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 strchr function in the Berkeley string library.

char *
strchr(p, ch)
        register char *p, ch;
{
        for (;; ++p) {
                if (*p == ch)
                        return(p);
                if (!*p)
                        return((char *)NULL);
        }
        /* NOTREACHED */
}

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

0x2500 <strchr>:        linkw fp,#0
0x2504 <strchr+4>:      moveal fp@(8),a0
0x2508 <strchr+8>:      moveb fp@(15),d0
0x250c <strchr+12>:     cmpb a0@,d0
0x250e <strchr+14>:     bne 0x2514 <strchr+20>
0x2510 <strchr+16>:     movel a0,d0
0x2512 <strchr+18>:     bra 0x2520 <strchr+32>
0x2514 <strchr+20>:     tstb a0@
0x2516 <strchr+22>:     bne 0x251c <strchr+28>
0x2518 <strchr+24>:     clrl d0
0x251a <strchr+26>:     bra 0x2520 <strchr+32>
0x251c <strchr+28>:     addqw #1,a0
0x251e <strchr+30>:     bra 0x250c <strchr+12>
0x2520 <strchr+32>:     unlk fp
0x2522 <strchr+34>:     rts

The machine code of the above program is:

<strchr>:      0x4e56  0x0000  0x206e  0x0008  0x102e  0x000f  0xb010  0x6604
<strchr+16>:   0x2008  0x600c  0x4a10  0x6604  0x4280  0x6004  0x5248  0x60ec
<strchr+32>:   0x4e5e  0x4e75

'(78      86      0       0       32      110     0       8
  16      46      0       15      176     16      102     4
  32      8       96      12      74      16      102     4
  66      128     96      4       82      72      96      236
  78      94      78      117)
|#

; in the logic, the above program is defined by (strchr-code).
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{strchr-code} \\  
\=\+{\sc{strchr-code}}\index{strchr-code} \\ 
$=$$\;\;\;\;${\tt{'}}{\tt{(}}\=\+{\tt{78}}{\tt{ }}{\tt{86}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{110}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{8}}{\tt{ }}{\tt{16}}{\tt{ }}{\tt{46}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{15}}{\tt{ }}{\tt{176}}{\tt{ }}{\tt{16}}{\tt{ }}{\tt{102}}{\tt{ }}{\tt{4}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{8}}{\tt{ }}{\tt{96}} \\ 
{\tt{12}}{\tt{ }}{\tt{74}}{\tt{ }}{\tt{16}}{\tt{ }}{\tt{102}}{\tt{ }}{\tt{4}}{\tt{ }}{\tt{66}}{\tt{ }}{\tt{128}}{\tt{ }}{\tt{96}}{\tt{ }}{\tt{4}}{\tt{ }}{\tt{82}}{\tt{ }}{\tt{72}}{\tt{ }}{\tt{96}}{\tt{ }}{\tt{236}}{\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{strchr1-t} \\  
\=\+{\rm{strchr1-t}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr1-t} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $<$ {\it{n\/}} \\ 
{\bf then }\=\+{\bf if }{\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth} $=$ {\it{ch\/}}$\;\;${\bf then }{\tt{6}} \\ 
{\bf elseif }{\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth} $=$ {\tt{0}}$\;\;${\bf then }{\tt{8}} \\ 
{\bf else }{\rm{splus}}\,({\tt{6}}, {\rm{strchr1-t}}\,($1\;+$ {\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr1-t})\index{splus}$\;${\bf  endif}\- \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{strchr-t} \\  
{\rm{strchr-t}}\,({\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr-t} $=$ {\rm{splus}}\,({\tt{3}}, {\rm{strchr1-t}}\,({\tt{0}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr1-t})\index{splus}
\end{tabbing}

\begin{verbatim}; an induction hint.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{strchr-induct} \\  
\=\+{\rm{strchr-induct}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr-induct} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $<$ {\it{n\/}} \\ 
{\bf then }\=\+{\bf if }{\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth} $=$ {\it{ch\/}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth} $=$ {\tt{0}}$\;\;${\bf then }{\tt{8}} \\ 
{\bf else }{\rm{strchr-induct}}\,(\=\+{\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn}, \\ 
{\rm{add}}\,({\tt{32}}, {\it{i*\/}}, {\tt{1}})\index{add}, \\ 
$1\;+$ {\it{i\/}}, \\ 
{\it{n\/}}, \\ 
{\it{lst\/}}, \\ 
{\it{ch\/}})\-\index{strchr-induct}$\;${\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{strchr-statep} \\  
\=\+{\rm{strchr-statep}}\,({\it{s\/}}, {\it{str\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr-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{38}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{strchr-code}}\index{strchr-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{16}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\it{str\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,({\tt{1}}, {\it{str\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n\/}}, {\it{lst\/}})\index{mem-lst} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{16}}, {\it{str\/}}, {\it{n\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;$({\it{str\/}} $=$ {\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{ch\/}} $=$ {\rm{uread-mem}}\,({\rm{add}}\,({\tt{32}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\tt{11}})\index{add}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{1}})\index{uread-mem}) \\ 
$\wedge$$\;\;\;\;$({\rm{slen}}\,({\tt{0}}, {\it{n\/}}, {\it{lst\/}})\index{slen} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{nat-to-uint}}\,({\it{str\/}})\index{nat-to-uint} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\rm{nat-to-uint}}\,({\it{str\/}})\index{nat-to-uint} $+$ {\it{n\/}}, {\tt{32}})\index{uint-rangep})\-\-
\end{tabbing}
       
\begin{verbatim}; an intermediate state.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{strchr-s0p} \\  
\=\+{\rm{strchr-s0p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr-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{12}}, {\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{38}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{12}}, {\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{strchr-code}}\index{strchr-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{16}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\it{str\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,({\tt{1}}, {\it{str\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n\/}}, {\it{lst\/}})\index{mem-lst} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}, {\tt{16}}, {\it{str\/}}, {\it{n\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{0}}, {\it{s\/}})\index{read-an}, {\rm{add}}\,({\tt{32}}, {\it{str\/}}, {\it{i*\/}})\index{add})\index{equal*} \\ 
$\wedge$$\;\;\;\;$({\it{ch\/}} $=$ {\rm{nat-to-uint}}\,({\rm{read-dn}}\,({\tt{8}}, {\tt{0}}, {\it{s\/}})\index{read-dn})\index{nat-to-uint}) \\ 
$\wedge$$\;\;\;\;$({\rm{slen}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{slen} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{n\/}}) \\ 
$\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{n\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\it{n\/}}, {\tt{32}})\index{uint-rangep})\-\-
\end{tabbing}

\begin{verbatim}; from the initial state s to s0: s --> s0;
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strchr-s-s0 \\ \index{strchr-s-s0}
{\rm{strchr-statep}}\,({\it{s\/}}, {\it{str\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr-statep} $\rightarrow$ {\rm{strchr-s0p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{3}})\index{stepn}, {\tt{0}}, {\tt{0}}, {\it{str\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr-s0p}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strchr-s-s0-else \\ \index{strchr-s-s0-else}
\=\+{\rm{strchr-statep}}\,({\it{s\/}}, {\it{str\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr-statep} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{3}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{3}})\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{3}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strchr-s-s0-rfile \\ \index{strchr-s-s0-rfile}
\=\+({\rm{strchr-statep}}\,({\it{s\/}}, {\it{str\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr-statep} $\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{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{tabbing}{\sc Theorem}:  strchr-s-s0-mem \\ \index{strchr-s-s0-mem}
\=\+({\rm{strchr-statep}}\,({\it{s\/}}, {\it{str\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr-statep} $\wedge$ {\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{16}})\index{disjoint}) \\ 
$\rightarrow$$\;\;\;\;$({\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{verbatim}; from s0 to exit: s0 --> sn.
; base case 1. s0 --> sn, when lst[i] = ch.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strchr-s0-sn-base1 \\ \index{strchr-s0-sn-base1}
\=\+({\rm{strchr-s0p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr-s0p} $\wedge$ ({\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth} $=$ {\it{ch\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\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{6}})\index{stepn})\index{read-dn} $=$ {\rm{add}}\,({\tt{32}}, {\it{str\/}}, {\it{i*\/}})\index{add}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\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{6}})\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{6}})\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}:  strchr-s0-sn-rfile-base1 \\ \index{strchr-s0-sn-rfile-base1}
\=\+(\=\+{\rm{strchr-s0p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr-s0p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth} $=$ {\it{ch\/}}) \\ 
$\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{6}})\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}; base case 2: s0 --> sn, when lst[i] =\= ch and lst[i] = 0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strchr-s0-sn-base2 \\ \index{strchr-s0-sn-base2}
\=\+(\=\+{\rm{strchr-s0p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr-s0p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth} $\not=$ {\it{ch\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth} $=$ {\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} $=$ {\tt{0}}) \\ 
$\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}:  strchr-s0-sn-rfile-base2 \\ \index{strchr-s0-sn-rfile-base2}
\=\+(\=\+{\rm{strchr-s0p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr-s0p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth} $\not=$ {\it{ch\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth} $=$ {\tt{0}}) \\ 
$\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{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{verbatim}; induction case: s0 --> s0, when lst[i] =\= ch and lst[i] =\= 0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strchr-s0-s0 \\ \index{strchr-s0-s0}
\=\+(\=\+{\rm{strchr-s0p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr-s0p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth} $\not=$ {\it{ch\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth} $\not=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{strchr-s0p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn}, {\rm{add}}\,({\tt{32}}, {\it{i*\/}}, {\tt{1}})\index{add}, $1\;+$ {\it{i\/}}, {\it{str\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr-s0p} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\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{6}})\index{stepn})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\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}:  strchr-s0-s0-rfile \\ \index{strchr-s0-s0-rfile}
\=\+(\=\+{\rm{strchr-s0p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr-s0p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth} $\not=$ {\it{ch\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\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{6}})\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. s0 --> exit.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strchr-s0p-info \\ \index{strchr-s0p-info}
{\rm{strchr-s0p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr-s0p} $\rightarrow$ (({\it{i\/}} $<$ {\it{n\/}}) $=$ {\bf{t}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strchr-s0-sn \\ \index{strchr-s0-sn}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strchr1-t}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr1-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{strchr-s0p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr-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{strchr}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr} \\ 
{\bf then }{\rm{add}}\,({\tt{32}}, {\it{str\/}}, {\rm{strchr*}}\,({\it{i*\/}}, {\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr*})\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})\- \\ 
$\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}:  strchr-s0-sn-rfile \\ \index{strchr-s0-sn-rfile}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strchr1-t}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr1-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+({\rm{strchr-s0p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr-s0p} $\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} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-\-$\;${\bf  endlet}\-
\end{tabbing}


\noindent{\sc Event}:   Disable strchr-s0p-info.

\addvspace{18pt}

\begin{verbatim}; the correctness of strchr.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strchr-correctness \\ \index{strchr-correctness}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strchr-t}}\,({\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{strchr-statep}}\,({\it{s\/}}, {\it{str\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr-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} \\ 
$\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{4}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{16}})\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{strchr}}\,({\tt{0}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr} \\ 
{\bf then }{\rm{add}}\,({\tt{32}}, {\it{str\/}}, {\rm{strchr*}}\,({\tt{0}}, {\tt{0}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr*})\index{add} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-)\-)\-\-$\;${\bf  endlet}\-
\end{tabbing}


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

\addvspace{18pt}

\begin{verbatim}; strchr* --> strchr.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strchr*-strchr \\ \index{strchr*-strchr}
\=\+(\=\+{\rm{strchr}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr} \\ 
$\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{strchr*}}\,({\it{i*\/}}, {\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr*})\index{nat-to-uint} $=$ {\rm{strchr}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strchr-non-zerop-la \\ \index{strchr-non-zerop-la}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strchr-t}}\,({\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strchr-statep}}\,({\it{s\/}}, {\it{str\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr-statep} \\ 
$\wedge$$\;\;\;\;${\rm{nat-rangep}}\,({\it{str\/}}, {\tt{32}})\index{nat-rangep} \\ 
$\wedge$$\;\;\;\;$({\rm{nat-to-uint}}\,({\it{str\/}})\index{nat-to-uint} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\rm{nat-to-uint}}\,({\it{str\/}})\index{nat-to-uint} $+$ {\it{n\/}}, {\tt{32}})\index{uint-rangep} \\ 
$\wedge$$\;\;\;\;${\rm{strchr}}\,({\tt{0}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr})\- \\ 
$\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}:  strchr-non-zerop \\ \index{strchr-non-zerop}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strchr-t}}\,({\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+({\rm{strchr-statep}}\,({\it{s\/}}, {\it{str\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr-statep} $\wedge$ {\rm{strchr}}\,({\tt{0}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr}) \\ 
$\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 strchr*.

\addvspace{18pt}

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


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