\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.

|#

;          Proof of the Correctness of the STRTOK Function
\end{verbatim}
\noindent{\sc Event}:   Start with the library {\tt{"mc20-2"}} using the compiled version.

\addvspace{18pt}
\begin{verbatim}#|
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 strtok function in the Berkeley string library.

char *
strtok(s, delim)
        register char *s;
        register const char *delim;
{
        register const char *spanp;
        register int c, sc;
        char *tok;
        static char *last;


        if (s == NULL && (s = last) == NULL)
                return (NULL);

        /*
         * Skip (span) leading delimiters (s += strspn(s, delim), sort of).
         */
cont:
        c = *s++;
        for (spanp = delim; (sc = *spanp++) != 0;) {
                if (c == sc)
                        goto cont;
        }

        if (c == 0) {           /* no non-delimiter characters */
                last = NULL;
                return (NULL);
        }
        tok = s - 1;

        /*
         * Scan token (scan for delimiters: s += strcspn(s, delim), sort of).
         * Note that delim must have one NUL; we stop if we see that, too.
         */
        for (;;) {
                c = *s++;
                spanp = delim;
                do {
                        if ((sc = *spanp++) == c) {
                                if (c == 0)
                                        s = NULL;
                                else
                                        s[-1] = 0;
                                last = s;
                                return (tok);
                        }
                } while (sc != 0);
        }
        /* NOTREACHED */
}

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

0x2768 <strtok>:        linkw fp,#0
0x276c <strtok+4>:      moveml d2-d3,sp@-
0x2770 <strtok+8>:      moveal fp@(8),a1
0x2774 <strtok+12>:     movel fp@(12),d3
0x2778 <strtok+16>:     tstl a1
0x277a <strtok+18>:     bne 0x278a <strtok+34>
0x277c <strtok+20>:     moveal @#0x20098 <edata>,a1
0x2782 <strtok+26>:     tstl a1
0x2784 <strtok+28>:     bne 0x278a <strtok+34>
0x2786 <strtok+30>:     clrl d0
0x2788 <strtok+32>:     bra 0x27d8 <strtok+112>
0x278a <strtok+34>:     moveb a1@+,d1
0x278c <strtok+36>:     extbl d1
0x278e <strtok+38>:     moveal d3,a0
0x2790 <strtok+40>:     bra 0x2796 <strtok+46>
0x2792 <strtok+42>:     cmpl d1,d0
0x2794 <strtok+44>:     beq 0x278a <strtok+34>
0x2796 <strtok+46>:     moveb a0@+,d0
0x2798 <strtok+48>:     extbl d0
0x279a <strtok+50>:     bne 0x2792 <strtok+42>
0x279c <strtok+52>:     tstl d1
0x279e <strtok+54>:     bne 0x27aa <strtok+66>
0x27a0 <strtok+56>:     clrl @#0x20098 <edata>
0x27a6 <strtok+62>:     clrl d0
0x27a8 <strtok+64>:     bra 0x27d8 <strtok+112>
0x27aa <strtok+66>:     movel a1,d2
0x27ac <strtok+68>:     subl #1,d2
0x27ae <strtok+70>:     moveb a1@+,d1
0x27b0 <strtok+72>:     extbl d1
0x27b2 <strtok+74>:     moveal d3,a0
0x27b4 <strtok+76>:     moveb a0@+,d0
0x27b6 <strtok+78>:     extbl d0
0x27b8 <strtok+80>:     cmpl d0,d1
0x27ba <strtok+82>:     bne 0x27d2 <strtok+106>
0x27bc <strtok+84>:     tstl d1
0x27be <strtok+86>:     bne 0x27c4 <strtok+92>
0x27c0 <strtok+88>:     subal a1,a1
0x27c2 <strtok+90>:     bra 0x27c8 <strtok+96>
0x27c4 <strtok+92>:     clrb a1@(-1)
0x27c8 <strtok+96>:     movel a1,@#0x20098 <edata>
0x27ce <strtok+102>:    movel d2,d0
0x27d0 <strtok+104>:    bra 0x27d8 <strtok+112>
0x27d2 <strtok+106>:    tstl d0
0x27d4 <strtok+108>:    bne 0x27b4 <strtok+76>
0x27d6 <strtok+110>:    bra 0x27ae <strtok+70>
0x27d8 <strtok+112>:    moveml fp@(-8),d2-d3
0x27de <strtok+118>:    unlk fp
0x27e0 <strtok+120>:    rts

The machine code of the above program is:

<strtok>:      0x4e56  0x0000  0x48e7  0x3000  0x226e  0x0008  0x262e  0x000c
<strtok+16>:   0x4a89  0x660e  0x2279  0x0002  0x0098  0x4a89  0x6604  0x4280
<strtok+32>:   0x604e  0x1219  0x49c1  0x2043  0x6004  0xb081  0x67f4  0x1018
<strtok+48>:   0x49c0  0x66f6  0x4a81  0x660a  0x42b9  0x0002  0x0098  0x4280
<strtok+64>:   0x602e  0x2409  0x5382  0x1219  0x49c1  0x2043  0x1018  0x49c0
<strtok+80>:   0xb280  0x6616  0x4a81  0x6604  0x93c9  0x6004  0x4229  0xffff
<strtok+96>:   0x23c9  0x0002  0x0098  0x2002  0x6006  0x4a80  0x66de  0x60d6
<strtok+112>:  0x4cee  0x000c  0xfff8  0x4e5e  0x4e75

'(78      86      0       0       72      231     48      0
  34      110     0       8       38      46      0       12
  74      137     102     14      34      121     0       2
  0       152     74      137     102     4       66      128
  96      78      18      25      73      193     32      67
  96      4       176     129     103     244     16      24
  73      192     102     246     74      129     102     10
  66      185     0       2       0       152     66      128
  96      46      36      9       83      130     18      25
  73      193     32      67      16      24      73      192
  178     128     102     22      74      129     102     4
  147     201     96      4       66      41      255     255
  35      201     0       2       0       152     32      2
  96      6       74      128     102     222     96      214
  76      238     0       12      255     248     78      94
  78      117)
|#

;  in the logic, the above program is defined by (strtok-code).
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{strtok-code} \\  
\=\+{\sc{strtok-code}}\index{strtok-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{74}}{\tt{ }}{\tt{137}} \\ 
{\tt{102}}{\tt{ }}{\tt{14}}{\tt{ }}{\tt{34}}{\tt{ }}{\tt{121}}{\tt{ }}{\tt{-1}}{\tt{ }}{\tt{-1}}{\tt{ }}{\tt{-1}}{\tt{ }}{\tt{-1}}{\tt{ }}{\tt{74}}{\tt{ }}{\tt{137}}{\tt{ }}{\tt{102}}{\tt{ }}{\tt{4}}{\tt{ }}{\tt{66}}{\tt{ }}{\tt{128}}{\tt{ }}{\tt{96}}{\tt{ }}{\tt{78}} \\ 
{\tt{18}}{\tt{ }}{\tt{25}}{\tt{ }}{\tt{73}}{\tt{ }}{\tt{193}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{67}}{\tt{ }}{\tt{96}}{\tt{ }}{\tt{4}}{\tt{ }}{\tt{176}}{\tt{ }}{\tt{129}}{\tt{ }}{\tt{103}}{\tt{ }}{\tt{244}}{\tt{ }}{\tt{16}}{\tt{ }}{\tt{24}}{\tt{ }}{\tt{73}}{\tt{ }}{\tt{192}} \\ 
{\tt{102}}{\tt{ }}{\tt{246}}{\tt{ }}{\tt{74}}{\tt{ }}{\tt{129}}{\tt{ }}{\tt{102}}{\tt{ }}{\tt{10}}{\tt{ }}{\tt{66}}{\tt{ }}{\tt{185}}{\tt{ }}{\tt{-1}}{\tt{ }}{\tt{-1}}{\tt{ }}{\tt{-1}}{\tt{ }}{\tt{-1}}{\tt{ }}{\tt{66}}{\tt{ }}{\tt{128}}{\tt{ }}{\tt{96}} \\ 
{\tt{46}}{\tt{ }}{\tt{36}}{\tt{ }}{\tt{9}}{\tt{ }}{\tt{83}}{\tt{ }}{\tt{130}}{\tt{ }}{\tt{18}}{\tt{ }}{\tt{25}}{\tt{ }}{\tt{73}}{\tt{ }}{\tt{193}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{67}}{\tt{ }}{\tt{16}}{\tt{ }}{\tt{24}}{\tt{ }}{\tt{73}}{\tt{ }}{\tt{192}}{\tt{ }}{\tt{178}} \\ 
{\tt{128}}{\tt{ }}{\tt{102}}{\tt{ }}{\tt{22}}{\tt{ }}{\tt{74}}{\tt{ }}{\tt{129}}{\tt{ }}{\tt{102}}{\tt{ }}{\tt{4}}{\tt{ }}{\tt{147}}{\tt{ }}{\tt{201}}{\tt{ }}{\tt{96}}{\tt{ }}{\tt{4}}{\tt{ }}{\tt{66}}{\tt{ }}{\tt{41}}{\tt{ }}{\tt{255}}{\tt{ }}{\tt{255}} \\ 
{\tt{35}}{\tt{ }}{\tt{201}}{\tt{ }}{\tt{-1}}{\tt{ }}{\tt{-1}}{\tt{ }}{\tt{-1}}{\tt{ }}{\tt{-1}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{2}}{\tt{ }}{\tt{96}}{\tt{ }}{\tt{6}}{\tt{ }}{\tt{74}}{\tt{ }}{\tt{128}}{\tt{ }}{\tt{102}}{\tt{ }}{\tt{222}}{\tt{ }}{\tt{96}}{\tt{ }}{\tt{214}} \\ 
{\tt{76}}{\tt{ }}{\tt{238}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{12}}{\tt{ }}{\tt{255}}{\tt{ }}{\tt{248}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{94}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{117}}{\tt{)}}\-\-
\end{tabbing}

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

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

\begin{verbatim}; the computation time of the program.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{strtok-t0} \\  
\=\+{\rm{strtok-t0}}\,({\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strtok-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{5}} \\ 
{\bf else }{\rm{splus}}\,({\tt{5}}, {\rm{strtok-t0}}\,($1\;+$ {\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strtok-t0})\index{splus}$\;${\bf  endif}\- \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

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

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

\begin{tabbing}{\sc Definition}:\index{strtok-t3} \\  
\=\+{\rm{strtok-t3}}\,({\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strtok-t3} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i2\/}} $<$ {\it{n2\/}} \\ 
{\bf then }\=\+{\bf if }{\it{ch\/}} $=$ {\rm{get-nth}}\,({\it{i2\/}}, {\it{lst2\/}})\index{get-nth} \\ 
{\bf then }\=\+{\bf if }{\it{ch\/}} $=$ {\tt{0}}$\;\;${\bf then }{\tt{14}} \\ 
{\bf else }{\tt{13}}$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{get-nth}}\,({\it{i2\/}}, {\it{lst2\/}})\index{get-nth} $=$ {\tt{0}}$\;\;${\bf then }{\tt{7}} \\ 
{\bf else }{\rm{splus}}\,({\tt{6}}, {\rm{strtok-t3}}\,($1\;+$ {\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strtok-t3})\index{splus}$\;${\bf  endif}\- \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{strtok-t4} \\  
{\rm{strtok-t4}}\,({\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strtok-t4} $=$ {\rm{splus}}\,({\tt{3}}, {\rm{strtok-t3}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strtok-t3})\index{splus}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{strtok-t5} \\  
\=\+{\rm{strtok-t5}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-t5} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i1\/}} $<$ {\it{n1\/}} \\ 
{\bf then }\=\+{\bf if }{\rm{strchr}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth})\index{strchr} \\ 
{\bf then }{\rm{strtok-t4}}\,({\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth})\index{strtok-t4} \\ 
{\bf else }{\rm{splus}}\,(\=\+{\rm{strtok-t4}}\,({\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth})\index{strtok-t4}, \\ 
{\rm{strtok-t5}}\,($1\;+$ {\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-t5})\-\index{splus}$\;${\bf  endif}\- \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{strtok-t6} \\  
\=\+{\rm{strtok-t6}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-t6} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\tt{0}}$\;\;${\bf then }{\tt{8}} \\ 
{\bf else }{\rm{splus}}\,({\tt{4}}, {\rm{strtok-t5}}\,($1\;+$ {\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-t5})\index{splus}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{strtok-t} \\  
\=\+{\rm{strtok-t}}\,({\it{str1\/}}, {\it{last\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-t} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{nat-to-uint}}\,({\it{str1\/}})\index{nat-to-uint} $=$ {\tt{0}} \\ 
{\bf then }\=\+{\bf if }{\rm{nat-to-uint}}\,({\it{last\/}})\index{nat-to-uint} $=$ {\tt{0}}$\;\;${\bf then }{\tt{14}} \\ 
{\bf else }{\rm{splus}}\,(\=\+{\tt{9}}, \\ 
{\rm{splus}}\,(\=\+{\rm{strtok-t2}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-t2}, \\ 
{\rm{strtok-t6}}\,(\=\+{\rm{strspn}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strspn}, \\ 
{\it{n1\/}}, \\ 
{\it{lst1\/}}, \\ 
{\it{n2\/}}, \\ 
{\it{lst2\/}})\-\index{strtok-t6})\-\index{splus})\-\index{splus}$\;${\bf  endif}\- \\ 
{\bf else }{\rm{splus}}\,(\=\+{\tt{6}}, \\ 
{\rm{splus}}\,(\=\+{\rm{strtok-t2}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-t2}, \\ 
{\rm{strtok-t6}}\,(\=\+{\rm{strspn}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strspn}, \\ 
{\it{n1\/}}, \\ 
{\it{lst1\/}}, \\ 
{\it{n2\/}}, \\ 
{\it{lst2\/}})\-\index{strtok-t6})\-\index{splus})\-\index{splus}$\;${\bf  endif}\-\-
\end{tabbing}
    
\begin{verbatim}; two induction hints.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{strtok-induct0} \\  
\=\+{\rm{strtok-induct0}}\,({\it{s\/}}, {\it{i2*\/}}, {\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strtok-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{strtok-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{strtok-induct0}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{strtok-induct1} \\  
\=\+{\rm{strtok-induct1}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-induct1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i1\/}} $<$ {\it{n1\/}} \\ 
{\bf then }\=\+{\bf if }{\rm{strchr1}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth})\index{strchr1} \\ 
{\bf then }{\rm{strtok-induct1}}\,(\=\+{\rm{stepn}}\,({\it{s\/}}, {\rm{strtok-t1}}\,({\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth})\index{strtok-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{strtok-induct1} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{strtok-induct2} \\  
\=\+{\rm{strtok-induct2}}\,({\it{s\/}}, {\it{i2*\/}}, {\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strtok-induct2} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i2\/}} $<$ {\it{n2\/}} \\ 
{\bf then }\=\+{\bf if }{\it{ch\/}} $=$ {\rm{get-nth}}\,({\it{i2\/}}, {\it{lst2\/}})\index{get-nth}$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{get-nth}}\,({\it{i2\/}}, {\it{lst2\/}})\index{get-nth} $=$ {\tt{0}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{strtok-induct2}}\,(\=\+{\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn}, \\ 
{\rm{add}}\,({\tt{32}}, {\it{i2*\/}}, {\tt{1}})\index{add}, \\ 
$1\;+$ {\it{i2\/}}, \\ 
{\it{n2\/}}, \\ 
{\it{lst2\/}}, \\ 
{\it{ch\/}})\-\index{strtok-induct2}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{strtok-induct3} \\  
\=\+{\rm{strtok-induct3}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-induct3} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i1\/}} $<$ {\it{n1\/}} \\ 
{\bf then }\=\+{\bf if }{\rm{strchr}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth})\index{strchr}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{strtok-induct3}}\,(\=\+{\rm{stepn}}\,(\=\+{\it{s\/}}, \\ 
{\rm{strtok-t4}}\,(\=\+{\it{n2\/}}, \\ 
{\it{lst2\/}}, \\ 
{\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth})\-\index{strtok-t4})\-\index{stepn}, \\ 
{\rm{add}}\,({\tt{32}}, {\it{i1*\/}}, {\tt{1}})\index{add}, \\ 
$1\;+$ {\it{i1\/}}, \\ 
{\it{n1\/}}, \\ 
{\it{lst1\/}}, \\ 
{\it{n2\/}}, \\ 
{\it{lst2\/}})\-\index{strtok-induct3}$\;${\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{strtok-statep} \\  
\=\+{\rm{strtok-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-statep} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{strtok-loadp}}\,({\it{s\/}})\index{strtok-loadp} \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc} $=$ {\sc{strtok-addr}}\index{strtok-addr}) \\ 
$\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{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{str2\/}}, {\it{n2\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{12}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{24}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\sc{strtok-last-addr}}\index{strtok-last-addr}, {\tt{4}}, {\rm{sub}}\,({\tt{32}}, {\tt{12}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{24}})\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$$\;\;\;\;$\=\+{\bf if }{\rm{nat-to-uint}}\,({\it{str1\/}})\index{nat-to-uint} $=$ {\tt{0}} \\ 
{\bf then }\=\+{\bf let }\=\+{\it{last\/}}{\bf $\;$ be$\;\;$}{\rm{read-mem}}\,({\sc{strtok-last-addr}}\index{strtok-last-addr}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{read-mem}\- \\ 
{\bf in} \\ 
\=\+{\bf if }{\rm{nat-to-uint}}\,({\it{last\/}})\index{nat-to-uint} $=$ {\tt{0}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }\=\+{\rm{ram-addrp}}\,({\it{last\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n1\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,(\=\+{\tt{1}}, \\ 
{\it{last\/}}, \\ 
{\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, \\ 
{\it{n1\/}}, \\ 
{\it{lst1\/}})\-\index{mem-lst} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,(\=\+{\it{last\/}}, \\ 
{\it{n1\/}}, \\ 
{\rm{sub}}\,({\tt{32}}, {\tt{12}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, \\ 
{\tt{24}})\-\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,(\=\+{\it{last\/}}, \\ 
{\it{n1\/}}, \\ 
{\sc{strtok-last-addr}}\index{strtok-last-addr}, \\ 
{\tt{4}})\-\index{disjoint}\-$\;${\bf  endif}\-$\;${\bf  endlet}\- \\ 
{\bf else }\=\+{\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{disjoint}}\,({\it{str1\/}}, {\it{n1\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{12}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{24}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{str1\/}}, {\it{n1\/}}, {\sc{strtok-last-addr}}\index{strtok-last-addr}, {\tt{4}})\index{disjoint}\-$\;${\bf  endif}\- \\ 
$\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$$\;\;\;\;${\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}; intermediate states.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{strtok-s0p} \\  
\=\+{\rm{strtok-s0p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-s0p} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{strtok-loadp}}\,({\it{s\/}})\index{strtok-loadp} \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc} $=$ {\rm{add}}\,({\tt{32}}, {\sc{strtok-addr}}\index{strtok-addr}, {\tt{34}})\index{add}) \\ 
$\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}}\,({\sc{strtok-last-addr}}\index{strtok-last-addr}, {\tt{4}}, {\rm{sub}}\,({\tt{32}}, {\tt{8}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{24}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{str1\/}}, {\it{n1\/}}, {\sc{strtok-last-addr}}\index{strtok-last-addr}, {\tt{4}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{str1\/}}, {\it{n1\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{8}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{24}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{str2\/}}, {\it{n2\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{8}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{24}})\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$$\;\;\;\;${\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{tabbing}{\sc Definition}:\index{strtok-s1p} \\  
\=\+{\rm{strtok-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{strtok-s1p} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{strtok-loadp}}\,({\it{s\/}})\index{strtok-loadp} \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc} $=$ {\rm{add}}\,({\tt{32}}, {\sc{strtok-addr}}\index{strtok-addr}, {\tt{46}})\index{add}) \\ 
$\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}}\,({\sc{strtok-last-addr}}\index{strtok-last-addr}, {\tt{4}}, {\rm{sub}}\,({\tt{32}}, {\tt{8}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{24}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{str1\/}}, {\it{n1\/}}, {\sc{strtok-last-addr}}\index{strtok-last-addr}, {\tt{4}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{str1\/}}, {\it{n1\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{8}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{24}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{str2\/}}, {\it{n2\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{8}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{24}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;$({\it{str2\/}} $=$ {\rm{read-dn}}\,({\tt{32}}, {\tt{3}}, {\it{s\/}})\index{read-dn}) \\ 
$\wedge$$\;\;\;\;$({\it{ch\/}} $=$ {\rm{uread-dn}}\,({\tt{8}}, {\tt{1}}, {\it{s\/}})\index{uread-dn}) \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-dn}}\,({\tt{32}}, {\tt{1}}, {\it{s\/}})\index{read-dn}, {\rm{ext}}\,({\tt{8}}, {\rm{read-dn}}\,({\tt{8}}, {\tt{1}}, {\it{s\/}})\index{read-dn}, {\tt{32}})\index{ext})\index{equal*} \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{1}}, {\it{s\/}})\index{read-an}, {\rm{add}}\,({\tt{32}}, {\it{str1\/}}, {\rm{add}}\,({\tt{32}}, {\it{i1*\/}}, {\tt{1}})\index{add})\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$$\;\;\;\;$({\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$$\;\;\;\;$({\rm{slen}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}})\index{slen} $<$ {\it{n2\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{slen}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}})\index{slen} $<$ {\it{n1\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{slen}}\,({\it{i2\/}}, {\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{tabbing}{\sc Definition}:\index{strtok-s2p} \\  
\=\+{\rm{strtok-s2p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strtok-s2p} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{strtok-loadp}}\,({\it{s\/}})\index{strtok-loadp} \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc} $=$ {\rm{add}}\,({\tt{32}}, {\sc{strtok-addr}}\index{strtok-addr}, {\tt{52}})\index{add}) \\ 
$\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}}\,({\sc{strtok-last-addr}}\index{strtok-last-addr}, {\tt{4}}, {\rm{sub}}\,({\tt{32}}, {\tt{8}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{24}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{str1\/}}, {\it{n1\/}}, {\sc{strtok-last-addr}}\index{strtok-last-addr}, {\tt{4}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{str1\/}}, {\it{n1\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{8}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{24}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-dn}}\,({\tt{32}}, {\tt{1}}, {\it{s\/}})\index{read-dn}, {\rm{ext}}\,({\tt{8}}, {\rm{read-dn}}\,({\tt{8}}, {\tt{1}}, {\it{s\/}})\index{read-dn}, {\tt{32}})\index{ext})\index{equal*} \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{1}}, {\it{s\/}})\index{read-an}, {\rm{add}}\,({\tt{32}}, {\it{str1\/}}, {\rm{add}}\,({\tt{32}}, {\it{i1*\/}}, {\tt{1}})\index{add})\index{add})\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{1}}, {\it{s\/}})\index{uread-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$$\;\;\;\;${\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{tabbing}{\sc Definition}:\index{strtok-s3p} \\  
\=\+{\rm{strtok-s3p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{tok\/}})\index{strtok-s3p} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{strtok-loadp}}\,({\it{s\/}})\index{strtok-loadp} \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc} $=$ {\rm{add}}\,({\tt{32}}, {\sc{strtok-addr}}\index{strtok-addr}, {\tt{70}})\index{add}) \\ 
$\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}}\,({\sc{strtok-last-addr}}\index{strtok-last-addr}, {\tt{4}}, {\rm{sub}}\,({\tt{32}}, {\tt{8}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{24}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{str1\/}}, {\it{n1\/}}, {\sc{strtok-last-addr}}\index{strtok-last-addr}, {\tt{4}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{str1\/}}, {\it{n1\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{8}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{24}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;$({\it{str2\/}} $=$ {\rm{read-dn}}\,({\tt{32}}, {\tt{3}}, {\it{s\/}})\index{read-dn}) \\ 
$\wedge$$\;\;\;\;$({\it{tok\/}} $=$ {\rm{read-dn}}\,({\tt{32}}, {\tt{2}}, {\it{s\/}})\index{read-dn}) \\ 
$\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{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$$\;\;\;\;${\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{tabbing}{\sc Definition}:\index{strtok-s4p} \\  
\=\+{\rm{strtok-s4p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{i2*\/}}, {\it{i2\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}}, {\it{tok\/}})\index{strtok-s4p} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{strtok-loadp}}\,({\it{s\/}})\index{strtok-loadp} \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc} $=$ {\rm{add}}\,({\tt{32}}, {\sc{strtok-addr}}\index{strtok-addr}, {\tt{76}})\index{add}) \\ 
$\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}}\,({\sc{strtok-last-addr}}\index{strtok-last-addr}, {\tt{4}}, {\rm{sub}}\,({\tt{32}}, {\tt{8}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{24}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{str1\/}}, {\it{n1\/}}, {\sc{strtok-last-addr}}\index{strtok-last-addr}, {\tt{4}})\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{str1\/}}, {\it{n1\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{1}}, {\it{s\/}})\index{read-an}, {\rm{add}}\,({\tt{32}}, {\it{str1\/}}, {\rm{add}}\,({\tt{32}}, {\it{i1*\/}}, {\tt{1}})\index{add})\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$$\;\;\;\;$({\it{str2\/}} $=$ {\rm{read-dn}}\,({\tt{32}}, {\tt{3}}, {\it{s\/}})\index{read-dn}) \\ 
$\wedge$$\;\;\;\;$({\it{ch\/}} $=$ {\rm{uread-dn}}\,({\tt{8}}, {\tt{1}}, {\it{s\/}})\index{uread-dn}) \\ 
$\wedge$$\;\;\;\;$({\it{tok\/}} $=$ {\rm{read-dn}}\,({\tt{32}}, {\tt{2}}, {\it{s\/}})\index{read-dn}) \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-dn}}\,({\tt{32}}, {\tt{1}}, {\it{s\/}})\index{read-dn}, {\rm{ext}}\,({\tt{8}}, {\rm{read-dn}}\,({\tt{8}}, {\tt{1}}, {\it{s\/}})\index{read-dn}, {\tt{32}})\index{ext})\index{equal*} \\ 
$\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$$\;\;\;\;$({\rm{slen}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}})\index{slen} $<$ {\it{n2\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{slen}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}})\index{slen} $<$ {\it{n1\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{slen}}\,({\it{i2\/}}, {\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}; from the initial state to exit.  s --> sn, when str1 == NULL & last == NULL.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strtok-s-sn \\ \index{strtok-s-sn}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\tt{14}})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strtok-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-statep} \\ 
$\wedge$$\;\;\;\;$({\rm{nat-to-uint}}\,({\it{str1\/}})\index{nat-to-uint} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{uread-mem}}\,({\sc{strtok-last-addr}}\index{strtok-last-addr}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{uread-mem} $=$ {\tt{0}}))\- \\ 
$\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-dn}}\,({\tt{32}}, {\tt{0}}, {\it{sn\/}})\index{read-dn} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\sc{strtok-last-addr}}\index{strtok-last-addr}, {\rm{mc-mem}}\,({\it{sn\/}})\index{mc-mem}, {\tt{4}})\index{read-mem} \\ 
$=$$\;\;\;\;${\rm{read-mem}}\,({\sc{strtok-last-addr}}\index{strtok-last-addr}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{read-mem})\- \\ 
$\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{7}}, {\it{s\/}})\index{read-an}, {\tt{4}})\index{add})\- \\ 
$\wedge$$\;\;\;\;$({\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{sn\/}})\index{mc-rfile})\index{read-rn} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}))\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strtok-s-sn-rfile \\ \index{strtok-s-sn-rfile}
\=\+(\=\+{\rm{strtok-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-statep} \\ 
$\wedge$$\;\;\;\;$({\rm{nat-to-uint}}\,({\it{str1\/}})\index{nat-to-uint} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{uread-mem}}\,({\sc{strtok-last-addr}}\index{strtok-last-addr}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{uread-mem} $=$ {\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{14}})\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}:  strtok-s-sn-mem \\ \index{strtok-s-sn-mem}
\=\+(\=\+{\rm{strtok-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-statep} \\ 
$\wedge$$\;\;\;\;$({\rm{nat-to-uint}}\,({\it{str1\/}})\index{nat-to-uint} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{uread-mem}}\,({\sc{strtok-last-addr}}\index{strtok-last-addr}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{uread-mem} $=$ {\tt{0}}) \\ 
$\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{14}})\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, when str1 =\= NULL.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strtok-s-s0-1 \\ \index{strtok-s-s0-1}
\=\+({\rm{strtok-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-statep} $\wedge$ ({\rm{nat-to-uint}}\,({\it{str1\/}})\index{nat-to-uint} $\not=$ {\tt{0}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{strtok-s0p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn}, {\tt{0}}, {\tt{0}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-s0p}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strtok-s-s0-else-1 \\ \index{strtok-s-s0-else-1}
\=\+{\bf let }\=\+{\it{s0\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strtok-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-statep} \\ 
$\wedge$$\;\;\;\;$({\rm{nat-to-uint}}\,({\it{str1\/}})\index{nat-to-uint} $\not=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{linked-rts-addr}}\,({\it{s0\/}})\index{linked-rts-addr} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\it{s0\/}})\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{s0\/}})\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{s0\/}}, {\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})\-)\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strtok-s-s0-rfile-1 \\ \index{strtok-s-s0-rfile-1}
\=\+(\=\+{\rm{strtok-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-statep} \\ 
$\wedge$$\;\;\;\;$({\rm{nat-to-uint}}\,({\it{str1\/}})\index{nat-to-uint} $\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{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{tabbing}{\sc Theorem}:  strtok-s-s0-mem-1 \\ \index{strtok-s-s0-mem-1}
\=\+(\=\+{\rm{strtok-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-statep} \\ 
$\wedge$$\;\;\;\;$({\rm{nat-to-uint}}\,({\it{str1\/}})\index{nat-to-uint} $\not=$ {\tt{0}}) \\ 
$\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{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{verbatim}; from s to s0.  s -> s0, when str1 == NULL and last =\= NULL.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strtok-s-s0-2 \\ \index{strtok-s-s0-2}
\=\+{\bf let }\=\+{\it{last\/}}{\bf $\;$ be$\;\;$}{\rm{read-mem}}\,({\sc{strtok-last-addr}}\index{strtok-last-addr}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{read-mem}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strtok-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-statep} \\ 
$\wedge$$\;\;\;\;$({\rm{nat-to-uint}}\,({\it{str1\/}})\index{nat-to-uint} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{nat-to-uint}}\,({\it{last\/}})\index{nat-to-uint} $\not=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{strtok-s0p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn}, {\tt{0}}, {\tt{0}}, {\it{last\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-s0p}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strtok-s-s0-else-2 \\ \index{strtok-s-s0-else-2}
\=\+{\bf let }\=\+{\it{s0\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn}, \\ 
{\it{last\/}}{\bf $\;$ be$\;\;$}{\rm{read-mem}}\,({\sc{strtok-last-addr}}\index{strtok-last-addr}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{read-mem}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strtok-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-statep} \\ 
$\wedge$$\;\;\;\;$({\rm{nat-to-uint}}\,({\it{str1\/}})\index{nat-to-uint} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{nat-to-uint}}\,({\it{last\/}})\index{nat-to-uint} $\not=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{linked-rts-addr}}\,({\it{s0\/}})\index{linked-rts-addr} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\it{s0\/}})\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{s0\/}})\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{s0\/}}, {\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})\-)\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strtok-s-s0-rfile-2 \\ \index{strtok-s-s0-rfile-2}
\=\+(\=\+{\rm{strtok-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-statep} \\ 
$\wedge$$\;\;\;\;$({\rm{nat-to-uint}}\,({\it{str1\/}})\index{nat-to-uint} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{uread-mem}}\,({\sc{strtok-last-addr}}\index{strtok-last-addr}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{uread-mem} $\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{9}})\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}:  strtok-s-s0-mem-2 \\ \index{strtok-s-s0-mem-2}
\=\+(\=\+{\rm{strtok-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-statep} \\ 
$\wedge$$\;\;\;\;$({\rm{nat-to-uint}}\,({\it{str1\/}})\index{nat-to-uint} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{uread-mem}}\,({\sc{strtok-last-addr}}\index{strtok-last-addr}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{uread-mem} $\not=$ {\tt{0}}) \\ 
$\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{9}})\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.
; s0 --> s1.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strtok-s0-s1 \\ \index{strtok-s0-s1}
\=\+{\rm{strtok-s0p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-s0p} \\ 
$\rightarrow$$\;\;\;\;${\rm{strtok-s1p}}\,(\=\+{\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn}, \\ 
{\it{i1*\/}}, \\ 
{\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{strtok-s1p}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strtok-s0-s1-else \\ \index{strtok-s0-s1-else}
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{strtok-s0p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-s0p} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\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{read-rn}}\,({\it{oplen\/}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s1\/}})\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}}\,({\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}) \\ 
$\wedge$$\;\;\;\;$({\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{tabbing}{\sc Theorem}:  strtok-s0-s1-rfile \\ \index{strtok-s0-s1-rfile}
\=\+({\rm{strtok-s0p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-s0p} $\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{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}; loop: s1 --> s1.
; base case: s1 --> s2, when lst2[i] == 0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strtok-s1-s2-base \\ \index{strtok-s1-s2-base}
\=\+(\=\+{\rm{strtok-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{strtok-s1p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i2\/}}, {\it{lst2\/}})\index{get-nth} $=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{strtok-s2p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{3}})\index{stepn}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strtok-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-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}) \\ 
$\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{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}:  strtok-s1-s2-rfile-base \\ \index{strtok-s1-s2-rfile-base}
\=\+(\=\+{\rm{strtok-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{strtok-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}; base case: s1 --> s0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strtok-s1-s0-base \\ \index{strtok-s1-s0-base}
\=\+(\=\+{\rm{strtok-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{strtok-s1p} \\ 
$\wedge$$\;\;\;\;$({\it{ch\/}} $=$ {\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth}) \\ 
$\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{strtok-s0p}}\,(\=\+{\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\index{stepn}, \\ 
{\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{strtok-s0p} \\ 
$\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{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}:  strtok-s1-s0-rfile-base \\ \index{strtok-s1-s0-rfile-base}
\=\+(\=\+{\rm{strtok-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{strtok-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$$\;\;\;\;${\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}; induction case: s1 --> s1.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strtok-s1-s1 \\ \index{strtok-s1-s1}
\=\+(\=\+{\rm{strtok-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{strtok-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{strtok-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{strtok-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{rn-saved}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\index{stepn})\index{rn-saved} $=$ {\rm{rn-saved}}\,({\it{s\/}})\index{rn-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}:  strtok-s1-s1-rfile \\ \index{strtok-s1-s1-rfile}
\=\+(\=\+{\rm{strtok-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{strtok-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, when (strchr1 i2 n2 lst2 ch).
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strtok-s1p-info \\ \index{strtok-s1p-info}
\=\+{\rm{strtok-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{strtok-s1p} \\ 
$\rightarrow$$\;\;\;\;$(({\it{i2\/}} $<$ {\it{n2\/}}) $=$ {\bf{t}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strtok-s1-s0 \\ \index{strtok-s1-s0}
\=\+{\bf let }\=\+{\it{s0\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strtok-t0}}\,({\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strtok-t0})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strtok-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{strtok-s1p} \\ 
$\wedge$$\;\;\;\;$({\it{ch\/}} $=$ {\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth}) \\ 
$\wedge$$\;\;\;\;${\rm{strchr1}}\,({\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strchr1})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{strtok-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{strtok-s0p} \\ 
$\wedge$$\;\;\;\;$({\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s0\/}})\index{mc-rfile})\index{read-rn} $=$ {\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}:  strtok-s1-s0-rfile \\ \index{strtok-s1-s0-rfile}
\=\+(\=\+{\rm{strtok-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{strtok-s1p} \\ 
$\wedge$$\;\;\;\;${\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{strtok-t0}}\,({\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strtok-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}; put together:  s1 --> s2, when (strchr1 i2 n2 lst2 ch).
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strtok-s1-s2 \\ \index{strtok-s1-s2}
\=\+{\bf let }\=\+{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strtok-t0}}\,({\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strtok-t0})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strtok-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{strtok-s1p} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{strchr1}}\,({\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strchr1}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{strtok-s2p}}\,({\it{s2\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strtok-s2p} \\ 
$\wedge$$\;\;\;\;$({\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s2\/}})\index{mc-rfile})\index{read-rn} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\it{s2\/}})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\it{s2\/}})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{movem-saved}}\,({\it{s2\/}}, {\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{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{tabbing}{\sc Theorem}:  strtok-s1-s2-rfile \\ \index{strtok-s1-s2-rfile}
\=\+(\=\+{\rm{strtok-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{strtok-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{strtok-t0}}\,({\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strtok-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}


\noindent{\sc Event}:   Disable strtok-s1p-info.

\addvspace{18pt}

\begin{verbatim}; from s0 to s2:  s0 --> s2.
; base case: s0 --> s2.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strtok-s0-s2-base \\ \index{strtok-s0-s2-base}
\=\+{\bf let }\=\+{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strtok-t1}}\,({\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth})\index{strtok-t1})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strtok-s0p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-s0p} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{strchr1}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth})\index{strchr1}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{strtok-s2p}}\,(\=\+{\it{s2\/}}, \\ 
{\it{i1*\/}}, \\ 
{\it{i1\/}}, \\ 
{\it{str1\/}}, \\ 
{\it{n1\/}}, \\ 
{\it{lst1\/}}, \\ 
{\it{str2\/}}, \\ 
{\it{n2\/}}, \\ 
{\it{lst2\/}}, \\ 
{\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth})\-\index{strtok-s2p} \\ 
$\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{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{movem-saved}}\,({\it{s2\/}}, {\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{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{tabbing}{\sc Theorem}:  strtok-s0-s2-rfile-base \\ \index{strtok-s0-s2-rfile-base}
\=\+{\bf let }\=\+{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strtok-t1}}\,({\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth})\index{strtok-t1})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strtok-s0p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-s0p} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{strchr1}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth})\index{strchr1}) \\ 
$\wedge$$\;\;\;\;${\rm{d4-7a2-5p}}\,({\it{rn\/}})\index{d4-7a2-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{verbatim}; induction case: s0 --> s0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strtok-s0-s0 \\ \index{strtok-s0-s0}
\=\+{\bf let }\=\+{\it{s0\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strtok-t1}}\,({\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth})\index{strtok-t1})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strtok-s0p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-s0p} \\ 
$\wedge$$\;\;\;\;${\rm{strchr1}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth})\index{strchr1})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{strtok-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{strtok-s0p} \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\it{s0\/}})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\it{s0\/}})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s0\/}})\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{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}:  strtok-s0-s0-rfile \\ \index{strtok-s0-s0-rfile}
\=\+{\bf let }\=\+{\it{s0\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strtok-t1}}\,({\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth})\index{strtok-t1})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strtok-s0p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-s0p} \\ 
$\wedge$$\;\;\;\;${\rm{strchr1}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth})\index{strchr1} \\ 
$\wedge$$\;\;\;\;${\rm{d4-7a2-5p}}\,({\it{rn\/}})\index{d4-7a2-5p})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s0\/}})\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 --> s2.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strtok-s0p-info \\ \index{strtok-s0p-info}
\=\+{\rm{strtok-s0p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-s0p} \\ 
$\rightarrow$$\;\;\;\;$(({\it{i1\/}} $\in\;${\bf{N}}${}$) $\wedge$ (({\it{i1\/}} $<$ {\it{n1\/}}) $=$ {\bf{t}}))\-
\end{tabbing}
  
\begin{tabbing}{\sc Theorem}:  strtok-s0-s2 \\ \index{strtok-s0-s2}
\=\+{\bf let }\=\+{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strtok-t2}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-t2})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{strtok-s0p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-s0p} \\ 
$\rightarrow$$\;\;\;\;${\rm{strtok-s2p}}\,(\=\+{\it{s2\/}}, \\ 
{\rm{strspn*}}\,({\it{i1*\/}}, {\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strspn*}, \\ 
{\rm{strspn}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strspn}, \\ 
{\it{str1\/}}, \\ 
{\it{n1\/}}, \\ 
{\it{lst1\/}}, \\ 
{\it{str2\/}}, \\ 
{\it{n2\/}}, \\ 
{\it{lst2\/}}, \\ 
{\rm{get-nth}}\,({\rm{strspn}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strspn}, {\it{lst1\/}})\index{get-nth})\-\index{strtok-s2p}\-$\;${\bf  endlet}\-
\end{tabbing}


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

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  strtok-s0-s2-else \\ \index{strtok-s0-s2-else}
\=\+{\bf let }\=\+{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strtok-t2}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-t2})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{strtok-s0p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-s0p} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\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{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{movem-saved}}\,({\it{s2\/}}, {\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{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{tabbing}{\sc Theorem}:  strtok-s0-s2-rfile \\ \index{strtok-s0-s2-rfile}
\=\+{\bf let }\=\+{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strtok-t2}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-t2})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+({\rm{strtok-s0p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-s0p} $\wedge$ {\rm{d4-7a2-5p}}\,({\it{rn\/}})\index{d4-7a2-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{verbatim}; from s2 to exit:  s2 --> sn.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strtok-s2-sn-1 \\ \index{strtok-s2-sn-1}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+({\rm{strtok-s2p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strtok-s2p} $\wedge$ ({\it{ch\/}} $=$ {\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} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-mem}}\,({\sc{strtok-last-addr}}\index{strtok-last-addr}, {\rm{mc-mem}}\,({\it{sn\/}})\index{mc-mem}, {\tt{4}})\index{read-mem} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,({\tt{1}}, {\it{str1\/}}, {\rm{mc-mem}}\,({\it{sn\/}})\index{mc-mem}, {\it{n1\/}}, {\it{lst1\/}})\index{mem-lst} \\ 
$\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}:  strtok-s2-sn-rfile-1 \\ \index{strtok-s2-sn-rfile-1}
\=\+(\=\+{\rm{strtok-s2p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strtok-s2p} \\ 
$\wedge$$\;\;\;\;$({\it{ch\/}} $=$ {\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-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{tabbing}{\sc Theorem}:  strtok-s2-sn-mem-1 \\ \index{strtok-s2-sn-mem-1}
\=\+(\=\+{\rm{strtok-s2p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strtok-s2p} \\ 
$\wedge$$\;\;\;\;$({\it{ch\/}} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\sc{strtok-last-addr}}\index{strtok-last-addr}, {\tt{4}})\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 s3:  s2 --> s3.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strtok-s2-s3 \\ \index{strtok-s2-s3}
\=\+(\=\+{\rm{strtok-s2p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strtok-s2p} \\ 
$\wedge$$\;\;\;\;$({\it{ch\/}} $=$ {\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth}) \\ 
$\wedge$$\;\;\;\;$({\it{ch\/}} $\not=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{strtok-s3p}}\,(\=\+{\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn}, \\ 
{\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\/}}, \\ 
{\rm{add}}\,({\tt{32}}, {\it{str1\/}}, {\it{i1*\/}})\index{add})\-\index{strtok-s3p}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strtok-s2-s3-else \\ \index{strtok-s2-s3-else}
\=\+{\bf let }\=\+{\it{s3\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+({\rm{strtok-s2p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strtok-s2p} $\wedge$ ({\it{ch\/}} $\not=$ {\tt{0}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\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{read-rn}}\,({\it{oplen\/}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s3\/}})\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}}\,({\it{s3\/}}, {\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{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{tabbing}{\sc Theorem}:  strtok-s2-s3-rfile \\ \index{strtok-s2-s3-rfile}
\=\+(\=\+{\rm{strtok-s2p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strtok-s2p} \\ 
$\wedge$$\;\;\;\;$({\it{ch\/}} $\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{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.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strtok-s3-s4 \\ \index{strtok-s3-s4}
\=\+{\rm{strtok-s3p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{tok\/}})\index{strtok-s3p} \\ 
$\rightarrow$$\;\;\;\;${\rm{strtok-s4p}}\,(\=\+{\rm{stepn}}\,({\it{s\/}}, {\tt{3}})\index{stepn}, \\ 
{\it{i1*\/}}, \\ 
{\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}, \\ 
{\it{tok\/}})\-\index{strtok-s4p}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strtok-s3-s4-else \\ \index{strtok-s3-s4-else}
\=\+{\bf let }\=\+{\it{s4\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\tt{3}})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{strtok-s3p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{tok\/}})\index{strtok-s3p} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\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{read-rn}}\,({\it{oplen\/}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s4\/}})\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}}\,({\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}) \\ 
$\wedge$$\;\;\;\;$({\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{tabbing}{\sc Theorem}:  strtok-s3-s4-rfile \\ \index{strtok-s3-s4-rfile}
\=\+({\rm{strtok-s3p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{tok\/}})\index{strtok-s3p} $\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}; from s4 to exit: s4 --> sn.
; case 1.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strtok-s4-sn-1 \\ \index{strtok-s4-sn-1}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\tt{13}})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strtok-s4p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{i2*\/}}, {\it{i2\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}}, {\it{tok\/}})\index{strtok-s4p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i2\/}}, {\it{lst2\/}})\index{get-nth} $=$ {\it{ch\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{ch\/}} $\not=$ {\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} $=$ {\it{tok\/}}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\sc{strtok-last-addr}}\index{strtok-last-addr}, {\rm{mc-mem}}\,({\it{sn\/}})\index{mc-mem}, {\tt{4}})\index{read-mem} \\ 
$=$$\;\;\;\;${\rm{add}}\,({\tt{32}}, {\it{str1\/}}, {\rm{add}}\,({\tt{32}}, {\it{i1*\/}}, {\tt{1}})\index{add})\index{add})\- \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,({\tt{1}}, {\it{str1\/}}, {\rm{mc-mem}}\,({\it{sn\/}})\index{mc-mem}, {\it{n1\/}}, {\rm{put-nth}}\,({\tt{0}}, {\it{i1\/}}, {\it{lst1\/}})\index{put-nth})\index{mem-lst} \\ 
$\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}:  strtok-s4-sn-rfile-1 \\ \index{strtok-s4-sn-rfile-1}
\=\+(\=\+{\rm{strtok-s4p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{i2*\/}}, {\it{i2\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}}, {\it{tok\/}})\index{strtok-s4p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i2\/}}, {\it{lst2\/}})\index{get-nth} $=$ {\it{ch\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{ch\/}} $\not=$ {\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{13}})\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{tabbing}{\sc Theorem}:  strtok-s4-sn-mem-1 \\ \index{strtok-s4-sn-mem-1}
\=\+(\=\+{\rm{strtok-s4p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{i2*\/}}, {\it{i2\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}}, {\it{tok\/}})\index{strtok-s4p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i2\/}}, {\it{lst2\/}})\index{get-nth} $=$ {\it{ch\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{ch\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\sc{strtok-last-addr}}\index{strtok-last-addr}, {\tt{4}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\it{str1\/}}, {\it{n1\/}})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{13}})\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}; case 2.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strtok-s4-sn-2 \\ \index{strtok-s4-sn-2}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\tt{14}})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strtok-s4p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{i2*\/}}, {\it{i2\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}}, {\it{tok\/}})\index{strtok-s4p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i2\/}}, {\it{lst2\/}})\index{get-nth} $=$ {\it{ch\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{ch\/}} $=$ {\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} $=$ {\it{tok\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-mem}}\,({\sc{strtok-last-addr}}\index{strtok-last-addr}, {\rm{mc-mem}}\,({\it{sn\/}})\index{mc-mem}, {\tt{4}})\index{read-mem} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,({\tt{1}}, {\it{str1\/}}, {\rm{mc-mem}}\,({\it{sn\/}})\index{mc-mem}, {\it{n1\/}}, {\it{lst1\/}})\index{mem-lst} \\ 
$\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}:  strtok-s4-sn-rfile-2 \\ \index{strtok-s4-sn-rfile-2}
\=\+(\=\+{\rm{strtok-s4p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{i2*\/}}, {\it{i2\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}}, {\it{tok\/}})\index{strtok-s4p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i2\/}}, {\it{lst2\/}})\index{get-nth} $=$ {\it{ch\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{ch\/}} $=$ {\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{14}})\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{tabbing}{\sc Theorem}:  strtok-s4-sn-mem-2 \\ \index{strtok-s4-sn-mem-2}
\=\+(\=\+{\rm{strtok-s4p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{i2*\/}}, {\it{i2\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}}, {\it{tok\/}})\index{strtok-s4p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i2\/}}, {\it{lst2\/}})\index{get-nth} $=$ {\it{ch\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{ch\/}} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\sc{strtok-last-addr}}\index{strtok-last-addr}, {\tt{4}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\it{str1\/}}, {\it{n1\/}})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{14}})\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 s4 to s3:  s4 --> s3.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strtok-s4-s3-base \\ \index{strtok-s4-s3-base}
\=\+{\bf let }\=\+{\it{s3\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\tt{7}})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strtok-s4p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{i2*\/}}, {\it{i2\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}}, {\it{tok\/}})\index{strtok-s4p} \\ 
$\wedge$$\;\;\;\;$({\it{ch\/}} $=$ {\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i2\/}}, {\it{lst2\/}})\index{get-nth} $\not=$ {\it{ch\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i2\/}}, {\it{lst2\/}})\index{get-nth} $=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{strtok-s3p}}\,(\=\+{\it{s3\/}}, \\ 
{\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\/}}, \\ 
{\it{tok\/}})\-\index{strtok-s3p} \\ 
$\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{read-rn}}\,({\it{oplen\/}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s3\/}})\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}}\,({\it{s3\/}}, {\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{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{tabbing}{\sc Theorem}:  strtok-s4-s3-rfile-base \\ \index{strtok-s4-s3-rfile-base}
\=\+(\=\+{\rm{strtok-s4p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{i2*\/}}, {\it{i2\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}}, {\it{tok\/}})\index{strtok-s4p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i2\/}}, {\it{lst2\/}})\index{get-nth} $\not=$ {\it{ch\/}}) \\ 
$\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{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 s4 to s4:  s4 --> s4.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strtok-s4-s4 \\ \index{strtok-s4-s4}
\=\+{\bf let }\=\+{\it{s4\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strtok-s4p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{i2*\/}}, {\it{i2\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}}, {\it{tok\/}})\index{strtok-s4p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i2\/}}, {\it{lst2\/}})\index{get-nth} $\not=$ {\it{ch\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i2\/}}, {\it{lst2\/}})\index{get-nth} $\not=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{strtok-s4p}}\,(\=\+{\it{s4\/}}, \\ 
{\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\/}}, \\ 
{\it{tok\/}})\-\index{strtok-s4p} \\ 
$\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{read-rn}}\,({\it{oplen\/}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s4\/}})\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}}\,({\it{s4\/}}, {\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{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{tabbing}{\sc Theorem}:  strtok-s4-s4-rfile \\ \index{strtok-s4-s4-rfile}
\=\+(\=\+{\rm{strtok-s4p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{i2*\/}}, {\it{i2\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}}, {\it{tok\/}})\index{strtok-s4p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i2\/}}, {\it{lst2\/}})\index{get-nth} $\not=$ {\it{ch\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i2\/}}, {\it{lst2\/}})\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{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: s4 --> sn.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strtok-s4-sn \\ \index{strtok-s4-sn}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strtok-t3}}\,({\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strtok-t3})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strtok-s4p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{i2*\/}}, {\it{i2\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}}, {\it{tok\/}})\index{strtok-s4p} \\ 
$\wedge$$\;\;\;\;${\rm{strchr}}\,({\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strchr})\- \\ 
$\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} $=$ {\it{tok\/}}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\sc{strtok-last-addr}}\index{strtok-last-addr}, {\rm{mc-mem}}\,({\it{sn\/}})\index{mc-mem}, {\tt{4}})\index{read-mem} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{ch\/}} $=$ {\tt{0}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\rm{add}}\,({\tt{32}}, {\it{str1\/}}, {\rm{add}}\,({\tt{32}}, {\it{i1*\/}}, {\tt{1}})\index{add})\index{add}$\;${\bf  endif}\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,({\tt{1}}, {\it{str1\/}}, {\rm{mc-mem}}\,({\it{sn\/}})\index{mc-mem}, {\it{n1\/}}, {\rm{strtok-lst0}}\,({\it{i1\/}}, {\it{lst1\/}}, {\it{ch\/}})\index{strtok-lst0})\index{mem-lst} \\ 
$\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}:  strtok-s4-sn-rfile \\ \index{strtok-s4-sn-rfile}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strtok-t3}}\,({\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strtok-t3})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strtok-s4p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{i2*\/}}, {\it{i2\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}}, {\it{tok\/}})\index{strtok-s4p} \\ 
$\wedge$$\;\;\;\;${\rm{strchr}}\,({\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strchr} \\ 
$\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{tabbing}{\sc Theorem}:  strtok-s4-sn-mem \\ \index{strtok-s4-sn-mem}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strtok-t3}}\,({\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strtok-t3})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strtok-s4p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{i2*\/}}, {\it{i2\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}}, {\it{tok\/}})\index{strtok-s4p} \\ 
$\wedge$$\;\;\;\;${\rm{strchr}}\,({\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strchr} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\sc{strtok-last-addr}}\index{strtok-last-addr}, {\tt{4}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\it{str1\/}}, {\it{n1\/}})\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: s4 --> s3.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strtok-s4p-info \\ \index{strtok-s4p-info}
\=\+{\rm{strtok-s4p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{i2*\/}}, {\it{i2\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}}, {\it{tok\/}})\index{strtok-s4p} \\ 
$\rightarrow$$\;\;\;\;$(({\it{i2\/}} $<$ {\it{n2\/}}) $=$ {\bf{t}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strtok-s4-s3 \\ \index{strtok-s4-s3}
\=\+{\bf let }\=\+{\it{s3\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strtok-t3}}\,({\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strtok-t3})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strtok-s4p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{i2*\/}}, {\it{i2\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}}, {\it{tok\/}})\index{strtok-s4p} \\ 
$\wedge$$\;\;\;\;$({\it{ch\/}} $=$ {\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{strchr}}\,({\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strchr}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{strtok-s3p}}\,(\=\+{\it{s3\/}}, \\ 
{\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\/}}, \\ 
{\it{tok\/}})\-\index{strtok-s3p} \\ 
$\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{read-rn}}\,({\it{oplen\/}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s3\/}})\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}}\,({\it{s3\/}}, {\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{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}       


\noindent{\sc Event}:   Disable strtok-s4p-info.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  strtok-s4-s3-rfile \\ \index{strtok-s4-s3-rfile}
\=\+{\bf let }\=\+{\it{s3\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strtok-t3}}\,({\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strtok-t3})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strtok-s4p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{i2*\/}}, {\it{i2\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}}, {\it{tok\/}})\index{strtok-s4p} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{strchr}}\,({\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strchr}) \\ 
$\wedge$$\;\;\;\;${\rm{d4-7a2-5p}}\,({\it{rn\/}})\index{d4-7a2-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{verbatim}; from s3 to exit:  s3 --> sn.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strtok-s3-sn-base \\ \index{strtok-s3-sn-base}
\=\+{\bf let }\=\+{\it{ch\/}}{\bf $\;$ be$\;\;$}{\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strtok-t4}}\,({\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strtok-t4})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strtok-s3p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{tok\/}})\index{strtok-s3p} \\ 
$\wedge$$\;\;\;\;${\rm{strchr}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strchr})\- \\ 
$\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} $=$ {\it{tok\/}}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\sc{strtok-last-addr}}\index{strtok-last-addr}, {\rm{mc-mem}}\,({\it{sn\/}})\index{mc-mem}, {\tt{4}})\index{read-mem} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{ch\/}} $=$ {\tt{0}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\rm{add}}\,({\tt{32}}, {\it{str1\/}}, {\rm{add}}\,({\tt{32}}, {\it{i1*\/}}, {\tt{1}})\index{add})\index{add}$\;${\bf  endif}\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,(\=\+{\tt{1}}, \\ 
{\it{str1\/}}, \\ 
{\rm{mc-mem}}\,({\it{sn\/}})\index{mc-mem}, \\ 
{\it{n1\/}}, \\ 
{\rm{strtok-lst0}}\,({\it{i1\/}}, {\it{lst1\/}}, {\it{ch\/}})\index{strtok-lst0})\-\index{mem-lst} \\ 
$\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}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strtok-s3-sn-rfile-base \\ \index{strtok-s3-sn-rfile-base}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strtok-t4}}\,({\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth})\index{strtok-t4})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strtok-s3p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{tok\/}})\index{strtok-s3p} \\ 
$\wedge$$\;\;\;\;${\rm{strchr}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth})\index{strchr} \\ 
$\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{tabbing}{\sc Theorem}:  strtok-s3-sn-mem-base \\ \index{strtok-s3-sn-mem-base}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strtok-t4}}\,({\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth})\index{strtok-t4})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strtok-s3p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{tok\/}})\index{strtok-s3p} \\ 
$\wedge$$\;\;\;\;${\rm{strchr}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth})\index{strchr} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\sc{strtok-last-addr}}\index{strtok-last-addr}, {\tt{4}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\it{str1\/}}, {\it{n1\/}})\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}; from s3 to s3:  s3 --> s3.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strtok-s3-s3 \\ \index{strtok-s3-s3}
\=\+{\bf let }\=\+{\it{s3\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strtok-t4}}\,({\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth})\index{strtok-t4})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strtok-s3p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{tok\/}})\index{strtok-s3p} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{strchr}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth})\index{strchr}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{strtok-s3p}}\,(\=\+{\it{s3\/}}, \\ 
{\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\/}}, \\ 
{\it{tok\/}})\-\index{strtok-s3p} \\ 
$\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{read-rn}}\,({\it{oplen\/}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s3\/}})\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}}\,({\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}) \\ 
$\wedge$$\;\;\;\;$({\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{tabbing}{\sc Theorem}:  strtok-s3-s3-rfile \\ \index{strtok-s3-s3-rfile}
\=\+{\bf let }\=\+{\it{s3\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strtok-t4}}\,({\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth})\index{strtok-t4})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strtok-s3p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{tok\/}})\index{strtok-s3p} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{strchr}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth})\index{strchr}) \\ 
$\wedge$$\;\;\;\;${\rm{d4-7a2-5p}}\,({\it{rn\/}})\index{d4-7a2-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{verbatim}; put together: s3 --> sn.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strtok-s3p-info \\ \index{strtok-s3p-info}
\=\+{\rm{strtok-s3p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{tok\/}})\index{strtok-s3p} \\ 
$\rightarrow$$\;\;\;\;$(({\it{i1\/}} $\in\;${\bf{N}}${}$) $\wedge$ (({\it{i1\/}} $<$ {\it{n1\/}}) $=$ {\bf{t}}))\-
\end{tabbing}
          
\begin{tabbing}{\sc Theorem}:  strtok-s3-sn \\ \index{strtok-s3-sn}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strtok-t5}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-t5})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{strtok-s3p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{tok\/}})\index{strtok-s3p} \\ 
$\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} $=$ {\it{tok\/}}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\sc{strtok-last-addr}}\index{strtok-last-addr}, {\rm{mc-mem}}\,({\it{sn\/}})\index{mc-mem}, {\tt{4}})\index{read-mem} \\ 
$=$$\;\;\;\;${\rm{strtok-last0}}\,({\it{str1\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-last0})\- \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,(\=\+{\tt{1}}, \\ 
{\it{str1\/}}, \\ 
{\rm{mc-mem}}\,({\it{sn\/}})\index{mc-mem}, \\ 
{\it{n1\/}}, \\ 
{\rm{strtok-lst1}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-lst1})\-\index{mem-lst} \\ 
$\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}:  strtok-s3-sn-rfile \\ \index{strtok-s3-sn-rfile}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strtok-t5}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-t5})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strtok-s3p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{tok\/}})\index{strtok-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{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{tabbing}{\sc Theorem}:  strtok-s3-sn-mem \\ \index{strtok-s3-sn-mem}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strtok-t5}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-t5})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strtok-s3p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{tok\/}})\index{strtok-s3p} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\sc{strtok-last-addr}}\index{strtok-last-addr}, {\tt{4}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\it{str1\/}}, {\it{n1\/}})\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 strtok-s3p-info.

\addvspace{18pt}

\begin{verbatim}; from s2 to exit:  s2 --> sn.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strtok-s2-sn \\ \index{strtok-s2-sn}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strtok-t6}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-t6})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strtok-s2p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strtok-s2p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i1\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\it{ch\/}}))\- \\ 
$\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 }{\it{ch\/}} $=$ {\tt{0}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\rm{add}}\,({\tt{32}}, {\it{str1\/}}, {\it{i1*\/}})\index{add}$\;${\bf  endif}\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\sc{strtok-last-addr}}\index{strtok-last-addr}, {\rm{mc-mem}}\,({\it{sn\/}})\index{mc-mem}, {\tt{4}})\index{read-mem} \\ 
$=$$\;\;\;\;${\rm{strtok-last1}}\,({\it{str1\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-last1})\- \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,(\=\+{\tt{1}}, \\ 
{\it{str1\/}}, \\ 
{\rm{mc-mem}}\,({\it{sn\/}})\index{mc-mem}, \\ 
{\it{n1\/}}, \\ 
{\rm{strtok-lst2}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-lst2})\-\index{mem-lst} \\ 
$\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}:  strtok-s2-sn-rfile \\ \index{strtok-s2-sn-rfile}
\=\+{\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{strtok-t6}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-t6})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strtok-s2p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strtok-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-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{tabbing}{\sc Theorem}:  strtok-s2-sn-mem \\ \index{strtok-s2-sn-mem}
\=\+{\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{strtok-t6}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-t6})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strtok-s2p}}\,({\it{s\/}}, {\it{i1*\/}}, {\it{i1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strtok-s2p} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\sc{strtok-last-addr}}\index{strtok-last-addr}, {\tt{4}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\it{str1\/}}, {\it{n1\/}})\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}; the correctness of strtok.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strtok-correctness \\ \index{strtok-correctness}
\=\+{\bf let }\=\+{\it{last\/}}{\bf $\;$ be$\;\;$}{\rm{read-mem}}\,({\sc{strtok-last-addr}}\index{strtok-last-addr}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{read-mem}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strtok-t}}\,({\it{str1\/}}, {\it{last\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{strtok-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-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-dn}}\,({\tt{32}}, {\tt{0}}, {\it{sn\/}})\index{read-dn} \\ 
$=$$\;\;\;\;${\rm{strtok-tok}}\,({\it{str1\/}}, {\it{last\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-tok})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\sc{strtok-last-addr}}\index{strtok-last-addr}, {\rm{mc-mem}}\,({\it{sn\/}})\index{mc-mem}, {\tt{4}})\index{read-mem} \\ 
$=$$\;\;\;\;${\rm{strtok-last}}\,({\it{str1\/}}, {\it{last\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-last})\- \\ 
$\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})\-)\-\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strtok-lst-1 \\ \index{strtok-lst-1}
\=\+{\bf let }\=\+{\it{last\/}}{\bf $\;$ be$\;\;$}{\rm{read-mem}}\,({\sc{strtok-last-addr}}\index{strtok-last-addr}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{read-mem}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strtok-t}}\,({\it{str1\/}}, {\it{last\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strtok-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-statep} \\ 
$\wedge$$\;\;\;\;$({\rm{nat-to-uint}}\,({\it{str1\/}})\index{nat-to-uint} $\not=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{mem-lst}}\,(\=\+{\tt{1}}, \\ 
{\it{str1\/}}, \\ 
{\rm{mc-mem}}\,({\it{sn\/}})\index{mc-mem}, \\ 
{\it{n1\/}}, \\ 
{\rm{strtok-lst}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-lst})\-\index{mem-lst}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strtok-lst-2 \\ \index{strtok-lst-2}
\=\+{\bf let }\=\+{\it{last\/}}{\bf $\;$ be$\;\;$}{\rm{read-mem}}\,({\sc{strtok-last-addr}}\index{strtok-last-addr}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{read-mem}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strtok-t}}\,({\it{str1\/}}, {\it{last\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strtok-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-statep} \\ 
$\wedge$$\;\;\;\;$({\rm{nat-to-uint}}\,({\it{str1\/}})\index{nat-to-uint} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{nat-to-uint}}\,({\it{last\/}})\index{nat-to-uint} $\not=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{mem-lst}}\,(\=\+{\tt{1}}, \\ 
{\it{last\/}}, \\ 
{\rm{mc-mem}}\,({\it{sn\/}})\index{mc-mem}, \\ 
{\it{n1\/}}, \\ 
{\rm{strtok-lst}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-lst})\-\index{mem-lst}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strtok-rfile \\ \index{strtok-rfile}
\=\+{\bf let }\=\+{\it{last\/}}{\bf $\;$ be$\;\;$}{\rm{read-mem}}\,({\sc{strtok-last-addr}}\index{strtok-last-addr}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{read-mem}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strtok-t}}\,({\it{str1\/}}, {\it{last\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strtok-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-statep} \\ 
$\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})\-\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strtok-mem \\ \index{strtok-mem}
\=\+{\bf let }\=\+{\it{last\/}}{\bf $\;$ be$\;\;$}{\rm{read-mem}}\,({\sc{strtok-last-addr}}\index{strtok-last-addr}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{read-mem}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strtok-t}}\,({\it{str1\/}}, {\it{last\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strtok-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-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} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\sc{strtok-last-addr}}\index{strtok-last-addr}, {\tt{4}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;$\=\+{\bf if }{\rm{nat-to-uint}}\,({\it{str1\/}})\index{nat-to-uint} $=$ {\tt{0}}$\;\;${\bf then }{\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\it{last\/}}, {\it{n1\/}})\index{disjoint} \\ 
{\bf else }{\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\it{str1\/}}, {\it{n1\/}})\index{disjoint}$\;${\bf  endif}\-)\- \\ 
$\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}\-$\;${\bf  endlet}\-
\end{tabbing}


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

\addvspace{18pt}

\begin{verbatim}; strspn* -> strspn, strcspn* --> strcspn.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strspn*-strspn \\ \index{strspn*-strspn}
\=\+(\=\+{\rm{strspn}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strspn} \\ 
$\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{strspn*}}\,({\it{i*\/}}, {\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strspn*})\index{nat-to-uint} \\ 
$=$$\;\;\;\;${\rm{strspn}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strspn})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strcspn*-strcspn \\ \index{strcspn*-strcspn}
\=\+(\=\+{\rm{strcspn}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcspn} \\ 
$\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{strcspn*}}\,({\it{i*\/}}, {\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcspn*})\index{nat-to-uint} \\ 
$=$$\;\;\;\;${\rm{strcspn}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcspn})\-\-
\end{tabbing}

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