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

\begin{verbatim}#|

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

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

 NO WARRANTY

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

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

|#

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

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

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

char *
strncat(dst, src, n)
	char *dst;
	const char *src;
	register size_t n;
{
	if (n != 0) {
		register char *d = dst;
		register const char *s = src;

		while (*d != 0)
			d++;
		do {
			if ((*d = *s++) == 0)
				break;
			d++;
		} while (--n != 0);
		*d = 0;
	}
	return (dst);
}

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

0x25d0 <strncat>:       linkw fp,#0
0x25d4 <strncat+4>:     movel d2,sp@-
0x25d6 <strncat+6>:     movel fp@(8),d2
0x25da <strncat+10>:    movel fp@(16),d1
0x25de <strncat+14>:    beq 0x25fe <strncat+46>
0x25e0 <strncat+16>:    moveal d2,a0
0x25e2 <strncat+18>:    moveal fp@(12),a1
0x25e6 <strncat+22>:    tstb a0@
0x25e8 <strncat+24>:    beq 0x25f0 <strncat+32>
0x25ea <strncat+26>:    addqw #1,a0
0x25ec <strncat+28>:    tstb a0@
0x25ee <strncat+30>:    bne 0x25ea <strncat+26>
0x25f0 <strncat+32>:    moveb a1@+,d0
0x25f2 <strncat+34>:    moveb d0,a0@
0x25f4 <strncat+36>:    beq 0x25fc <strncat+44>
0x25f6 <strncat+38>:    addqw #1,a0
0x25f8 <strncat+40>:    subl #1,d1
0x25fa <strncat+42>:    bne 0x25f0 <strncat+32>
0x25fc <strncat+44>:    clrb a0@
0x25fe <strncat+46>:    movel d2,d0
0x2600 <strncat+48>:    movel fp@(-4),d2
0x2604 <strncat+52>:    unlk fp
0x2606 <strncat+54>:    rts

The machine code of the above program is:

<strncat>:     0x4e56  0x0000  0x2f02  0x242e  0x0008  0x222e  0x0010  0x671e
<strncat+16>:  0x2042  0x226e  0x000c  0x4a10  0x6706  0x5248  0x4a10  0x66fa
<strncat+32>:  0x1019  0x1080  0x6706  0x5248  0x5381  0x66f4  0x4210  0x2002
<strncat+48>:  0x242e  0xfffc  0x4e5e  0x4e75

'(78      86      0       0       47      2       36      46
  0       8       34      46      0       16      103     30
  32      66      34      110     0       12      74      16
  103     6       82      72      74      16      102     250
  16      25      16      128     103     6       82      72
  83      129     102     244     66      16      32      2
  36      46      255     252     78      94      78      117)
|#

; in the logic, the above program is defined by (strncat-code). 
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{strncat-code} \\  
\=\+{\sc{strncat-code}}\index{strncat-code} \\ 
$=$$\;\;\;\;${\tt{'}}{\tt{(}}\=\+{\tt{78}}{\tt{ }}{\tt{86}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{47}}{\tt{ }}{\tt{2}}{\tt{ }}{\tt{36}}{\tt{ }}{\tt{46}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{8}}{\tt{ }}{\tt{34}}{\tt{ }}{\tt{46}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{16}}{\tt{ }}{\tt{103}}{\tt{ }}{\tt{30}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{66}}{\tt{ }}{\tt{34}} \\ 
{\tt{110}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{12}}{\tt{ }}{\tt{74}}{\tt{ }}{\tt{16}}{\tt{ }}{\tt{103}}{\tt{ }}{\tt{6}}{\tt{ }}{\tt{82}}{\tt{ }}{\tt{72}}{\tt{ }}{\tt{74}}{\tt{ }}{\tt{16}}{\tt{ }}{\tt{102}}{\tt{ }}{\tt{250}}{\tt{ }}{\tt{16}}{\tt{ }}{\tt{25}}{\tt{ }}{\tt{16}} \\ 
{\tt{128}}{\tt{ }}{\tt{103}}{\tt{ }}{\tt{6}}{\tt{ }}{\tt{82}}{\tt{ }}{\tt{72}}{\tt{ }}{\tt{83}}{\tt{ }}{\tt{129}}{\tt{ }}{\tt{102}}{\tt{ }}{\tt{244}}{\tt{ }}{\tt{66}}{\tt{ }}{\tt{16}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{2}}{\tt{ }}{\tt{36}}{\tt{ }}{\tt{46}}{\tt{ }}{\tt{255}} \\ 
{\tt{252}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{94}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{117}}{\tt{)}}\-\-
\end{tabbing}

\begin{verbatim}; the computation time of the program.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{strncat-t0} \\  
\=\+{\rm{strncat-t0}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}})\index{strncat-t0} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $<$ {\it{n1\/}} \\ 
{\bf then }\=\+{\bf if }{\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\tt{0}}$\;\;${\bf then }{\tt{2}} \\ 
{\bf else }{\rm{splus}}\,({\tt{3}}, {\rm{strncat-t0}}\,($1\;+$ {\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}})\index{strncat-t0})\index{splus}$\;${\bf  endif}\- \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{strncat-t1} \\  
{\rm{strncat-t1}}\,({\it{n1\/}}, {\it{lst1\/}})\index{strncat-t1} $=$ {\rm{splus}}\,({\tt{10}}, {\rm{strncat-t0}}\,({\tt{1}}, {\it{n1\/}}, {\it{lst1\/}})\index{strncat-t0})\index{splus}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{strncat-t2} \\  
\=\+{\rm{strncat-t2}}\,({\it{j\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strncat-t2} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{get-nth}}\,({\it{j\/}}, {\it{lst2\/}})\index{get-nth} $=$ {\tt{0}}$\;\;${\bf then }{\tt{8}} \\ 
{\bf elseif }({\it{n\/}} $-\;1$) $=$ {\tt{0}}$\;\;${\bf then }{\tt{11}} \\ 
{\bf else }{\rm{splus}}\,({\tt{6}}, {\rm{strncat-t2}}\,($1\;+$ {\it{j\/}}, {\it{n\/}} $-\;1$, {\it{lst2\/}})\index{strncat-t2})\index{splus}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{strncat-t} \\  
\=\+{\rm{strncat-t}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strncat-t} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $=$ {\tt{0}}$\;\;${\bf then }{\tt{9}} \\ 
{\bf elseif }{\rm{get-nth}}\,({\tt{0}}, {\it{lst1\/}})\index{get-nth} $=$ {\tt{0}}$\;\;${\bf then }{\rm{splus}}\,({\tt{9}}, {\rm{strncat-t2}}\,({\tt{0}}, {\it{n\/}}, {\it{lst2\/}})\index{strncat-t2})\index{splus} \\ 
{\bf else }{\rm{splus}}\,({\rm{strncat-t1}}\,({\it{n1\/}}, {\it{lst1\/}})\index{strncat-t1}, {\rm{strncat-t2}}\,({\tt{0}}, {\it{n\/}}, {\it{lst2\/}})\index{strncat-t2})\index{splus}$\;${\bf  endif}\-\-
\end{tabbing}

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

\begin{tabbing}{\sc Definition}:\index{strncat-induct1} \\  
\=\+{\rm{strncat-induct1}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{lst1\/}}, {\it{j*\/}}, {\it{j\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strncat-induct1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{get-nth}}\,({\it{j\/}}, {\it{lst2\/}})\index{get-nth} $=$ {\tt{0}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }({\it{n\/}} $-\;1$) $=$ {\tt{0}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{strncat-induct1}}\,(\=\+{\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn}, \\ 
{\rm{add}}\,({\tt{32}}, {\it{i*\/}}, {\tt{1}})\index{add}, \\ 
$1\;+$ {\it{i\/}}, \\ 
{\rm{put-nth}}\,({\rm{get-nth}}\,({\it{j\/}}, {\it{lst2\/}})\index{get-nth}, {\it{i\/}}, {\it{lst1\/}})\index{put-nth}, \\ 
{\rm{add}}\,({\tt{32}}, {\it{j*\/}}, {\tt{1}})\index{add}, \\ 
$1\;+$ {\it{j\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{lst2\/}})\-\index{strncat-induct1}$\;${\bf  endif}\-\-
\end{tabbing}

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

\begin{verbatim}; an intermediate state s0.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{strncat-s0p} \\  
\=\+{\rm{strncat-s0p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strncat-s0p} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{evenp}}\,({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{evenp} \\ 
$\wedge$$\;\;\;\;${\rm{rom-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{28}}, {\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{56}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{28}}, {\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{strncat-code}}\index{strncat-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\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{n\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,({\tt{1}}, {\it{str2\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n\/}}, {\it{lst2\/}})\index{mem-lst} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{24}}, {\it{str1\/}}, {\it{n1\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{24}}, {\it{str2\/}}, {\it{n\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{str1\/}}, {\it{n1\/}}, {\it{str2\/}}, {\it{n\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{0}}, {\it{s\/}})\index{read-an}, {\rm{add}}\,({\tt{32}}, {\it{str1\/}}, {\it{i*\/}})\index{add})\index{equal*} \\ 
$\wedge$$\;\;\;\;$({\it{str1\/}} $=$ {\rm{read-dn}}\,({\tt{32}}, {\tt{2}}, {\it{s\/}})\index{read-dn}) \\ 
$\wedge$$\;\;\;\;$({\it{str2\/}} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{1}}, {\it{s\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $=$ {\rm{nat-to-uint}}\,({\rm{read-dn}}\,({\tt{32}}, {\tt{1}}, {\it{s\/}})\index{read-dn})\index{nat-to-uint}) \\ 
$\wedge$$\;\;\;\;$({\it{i*\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{nat-rangep}}\,({\it{i*\/}}, {\tt{32}})\index{nat-rangep} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $=$ {\rm{nat-to-uint}}\,({\it{i*\/}})\index{nat-to-uint}) \\ 
$\wedge$$\;\;\;\;$(($1\;+$ ({\rm{slen}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}})\index{slen} $+$ {\it{n\/}})) $<$ {\it{n1\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{n1\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\it{n1\/}}, {\tt{32}})\index{uint-rangep} \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not=$ {\tt{0}}))\-\-
\end{tabbing}

\begin{verbatim}; an intermediate state s1.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{strncat-s1p} \\  
\=\+{\rm{strncat-s1p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{j*\/}}, {\it{j\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}}, {\it{i\_\/}}, {\it{n\_\/}})\index{strncat-s1p} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{evenp}}\,({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{evenp} \\ 
$\wedge$$\;\;\;\;${\rm{rom-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{32}}, {\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{56}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{32}}, {\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{strncat-code}}\index{strncat-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\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{n\_\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,({\tt{1}}, {\it{str2\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n\_\/}}, {\it{lst2\/}})\index{mem-lst} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{24}}, {\it{str1\/}}, {\it{n1\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{24}}, {\it{str2\/}}, {\it{n\_\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{str1\/}}, {\it{n1\/}}, {\it{str2\/}}, {\it{n\_\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{0}}, {\it{s\/}})\index{read-an}, {\rm{add}}\,({\tt{32}}, {\it{str1\/}}, {\it{i*\/}})\index{add})\index{equal*} \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{1}}, {\it{s\/}})\index{read-an}, {\rm{add}}\,({\tt{32}}, {\it{str2\/}}, {\it{j*\/}})\index{add})\index{equal*} \\ 
$\wedge$$\;\;\;\;$({\it{str1\/}} $=$ {\rm{read-dn}}\,({\tt{32}}, {\tt{2}}, {\it{s\/}})\index{read-dn}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $=$ {\rm{nat-to-uint}}\,({\rm{read-dn}}\,({\tt{32}}, {\tt{1}}, {\it{s\/}})\index{read-dn})\index{nat-to-uint}) \\ 
$\wedge$$\;\;\;\;$(({\it{j\/}} $+$ {\it{n\/}}) $\leq$ {\it{n\_\/}}) \\ 
$\wedge$$\;\;\;\;$(($1\;+$ ({\it{i\_\/}} $+$ {\it{n\_\/}})) $<$ {\it{n1\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\leq$ ({\it{i\_\/}} $+$ {\it{j\/}})) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{i*\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{nat-rangep}}\,({\it{i*\/}}, {\tt{32}})\index{nat-rangep} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $=$ {\rm{nat-to-uint}}\,({\it{i*\/}})\index{nat-to-uint}) \\ 
$\wedge$$\;\;\;\;$({\it{j*\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{nat-rangep}}\,({\it{j*\/}}, {\tt{32}})\index{nat-rangep} \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $=$ {\rm{nat-to-uint}}\,({\it{j*\/}})\index{nat-to-uint}) \\ 
$\wedge$$\;\;\;\;$({\it{n1\/}} $<$ {\tt{4294967296}}) \\ 
$\wedge$$\;\;\;\;$({\it{n\_\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{n\_\/}} $<$ {\tt{4294967296}}))\-\-
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  strncat-s-sn-rfile \\ \index{strncat-s-sn-rfile}
\=\+(\=\+{\rm{strncat-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strncat-statep} \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $=$ {\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{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}:  strncat-s-sn-mem \\ \index{strncat-s-sn-mem}
\=\+(\=\+{\rm{strncat-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strncat-statep} \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{8}}, {\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 the initial state s to s0: s --> s0, when n =\= 0, lst1[0] =\= 0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strncat-s-s0 \\ \index{strncat-s-s0}
\=\+(\=\+{\rm{strncat-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strncat-statep} \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\tt{0}}, {\it{lst1\/}})\index{get-nth} $\not=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{strncat-s0p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{10}})\index{stepn}, {\tt{1}}, {\tt{1}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strncat-s0p} \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{10}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{10}})\index{stepn})\index{linked-a6} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{10}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub})\- \\ 
$\wedge$$\;\;\;\;$({\rm{rn-saved}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{10}})\index{stepn})\index{rn-saved} $=$ {\rm{read-dn}}\,({\tt{32}}, {\tt{2}}, {\it{s\/}})\index{read-dn}))\-\-
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  strncat-s-s0-mem \\ \index{strncat-s-s0-mem}
\=\+(\=\+{\rm{strncat-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strncat-statep} \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\tt{0}}, {\it{lst1\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{8}}, {\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{10}})\index{stepn})\index{mc-mem}, {\it{k\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-
\end{tabbing}

\begin{verbatim}; from initial state s to s1, when n =\= 0, lst1[0] = 0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strncat-s-s1 \\ \index{strncat-s-s1}
\=\+(\=\+{\rm{strncat-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strncat-statep} \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\tt{0}}, {\it{lst1\/}})\index{get-nth} $=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{strncat-s1p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn}, {\tt{0}}, {\tt{0}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\tt{0}}, {\tt{0}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}}, {\tt{0}}, {\it{n\/}})\index{strncat-s1p}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strncat-s-s1-else \\ \index{strncat-s-s1-else}
\=\+(\=\+{\rm{strncat-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strncat-statep} \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\tt{0}}, {\it{lst1\/}})\index{get-nth} $=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn})\index{linked-a6} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub})\- \\ 
$\wedge$$\;\;\;\;$({\rm{rn-saved}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn})\index{rn-saved} $=$ {\rm{read-rn}}\,({\tt{32}}, {\tt{2}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strncat-s-s1-rfile \\ \index{strncat-s-s1-rfile}
\=\+(\=\+{\rm{strncat-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strncat-statep} \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\tt{0}}, {\it{lst1\/}})\index{get-nth} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{d3-7a2-5p}}\,({\it{rn\/}})\index{d3-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}:  strncat-s-s1-mem \\ \index{strncat-s-s1-mem}
\=\+(\=\+{\rm{strncat-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strncat-statep} \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\tt{0}}, {\it{lst1\/}})\index{get-nth} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{8}}, {\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.
; base case:  s0 --> s1, when lst1[i] = 0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strncat-s0-s1-base \\ \index{strncat-s0-s1-base}
\=\+({\rm{strncat-s0p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strncat-s0p} $\wedge$ ({\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\tt{0}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{strncat-s1p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{2}})\index{stepn}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\tt{0}}, {\tt{0}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}}, {\it{i\/}}, {\it{n\/}})\index{strncat-s1p} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{2}})\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{2}})\index{stepn})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{2}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{rn-saved}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{2}})\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{2}})\index{stepn})\index{mc-mem}, {\it{k\/}})\index{read-mem} \\ 
$=$$\;\;\;\;${\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-)\-\-
\end{tabbing}	  
		   
\begin{tabbing}{\sc Theorem}:  strncat-s0-s1-rfile-base \\ \index{strncat-s0-s1-rfile-base}
\=\+(\=\+{\rm{strncat-s0p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strncat-s0p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{d3-7a2-5p}}\,({\it{rn\/}})\index{d3-7a2-5p})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{2}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-\-
\end{tabbing}

\begin{verbatim}; induction case: s0 --> s0, when lst1[i] =\= 0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strncat-s0-s0 \\ \index{strncat-s0-s0}
\=\+({\rm{strncat-s0p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strncat-s0p} $\wedge$ ({\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $\not=$ {\tt{0}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{strncat-s0p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{3}})\index{stepn}, {\rm{add}}\,({\tt{32}}, {\it{i*\/}}, {\tt{1}})\index{add}, $1\;+$ {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strncat-s0p} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{3}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\- \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{3}})\index{stepn})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{3}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{rn-saved}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{3}})\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{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}:  strncat-s0-s0-rfile \\ \index{strncat-s0-s0-rfile}
\=\+(\=\+{\rm{strncat-s0p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strncat-s0p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{d3-7a2-5p}}\,({\it{rn\/}})\index{d3-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}; put together. s0 --> s1.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strncat-s0p-info \\ \index{strncat-s0p-info}
{\rm{strncat-s0p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strncat-s0p} $\rightarrow$ (({\it{i\/}} $<$ {\it{n1\/}}) $=$ {\bf{t}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strncat-s0-s1 \\ \index{strncat-s0-s1}
\=\+{\rm{strncat-s0p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strncat-s0p} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{strncat-s1p}}\,(\=\+{\rm{stepn}}\,({\it{s\/}}, {\rm{strncat-t0}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}})\index{strncat-t0})\index{stepn}, \\ 
{\rm{strlen*}}\,({\it{i*\/}}, {\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}})\index{strlen*}, \\ 
{\rm{strlen}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}})\index{strlen}, \\ 
{\it{str1\/}}, \\ 
{\it{n1\/}}, \\ 
{\it{lst1\/}}, \\ 
{\tt{0}}, \\ 
{\tt{0}}, \\ 
{\it{str2\/}}, \\ 
{\it{n\/}}, \\ 
{\it{lst2\/}}, \\ 
{\rm{strlen}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}})\index{strlen}, \\ 
{\it{n\/}})\-\index{strncat-s1p} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{strncat-t0}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}})\index{strncat-t0})\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\/}}, {\rm{strncat-t0}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}})\index{strncat-t0})\index{stepn})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{strncat-t0}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}})\index{strncat-t0})\index{stepn})\index{linked-rts-addr} \\ 
$=$$\;\;\;\;${\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr})\- \\ 
$\wedge$$\;\;\;\;$({\rm{rn-saved}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{strncat-t0}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}})\index{strncat-t0})\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\/}}, {\rm{strncat-t0}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}})\index{strncat-t0})\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}


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

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  strncat-s0-s1-rfile \\ \index{strncat-s0-s1-rfile}
\=\+({\rm{strncat-s0p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strncat-s0p} $\wedge$ {\rm{d3-7a2-5p}}\,({\it{rn\/}})\index{d3-7a2-5p}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{strncat-t0}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}})\index{strncat-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: s --> s1.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strncat-s-s1-1 \\ \index{strncat-s-s1-1}
\=\+(\=\+{\rm{strncat-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strncat-statep} \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\tt{0}}, {\it{lst1\/}})\index{get-nth} $\not=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{strncat-s1p}}\,(\=\+{\rm{stepn}}\,({\it{s\/}}, {\rm{strncat-t1}}\,({\it{n1\/}}, {\it{lst1\/}})\index{strncat-t1})\index{stepn}, \\ 
{\rm{strlen*}}\,({\tt{1}}, {\tt{1}}, {\it{n1\/}}, {\it{lst1\/}})\index{strlen*}, \\ 
{\rm{strlen}}\,({\tt{1}}, {\it{n1\/}}, {\it{lst1\/}})\index{strlen}, \\ 
{\it{str1\/}}, \\ 
{\it{n1\/}}, \\ 
{\it{lst1\/}}, \\ 
{\tt{0}}, \\ 
{\tt{0}}, \\ 
{\it{str2\/}}, \\ 
{\it{n\/}}, \\ 
{\it{lst2\/}}, \\ 
{\rm{strlen}}\,({\tt{1}}, {\it{n1\/}}, {\it{lst1\/}})\index{strlen}, \\ 
{\it{n\/}})\-\index{strncat-s1p}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strncat-s-s1-else-1 \\ \index{strncat-s-s1-else-1}
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strncat-t1}}\,({\it{n1\/}}, {\it{lst1\/}})\index{strncat-t1})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strncat-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strncat-statep} \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\tt{0}}, {\it{lst1\/}})\index{get-nth} $\not=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{linked-rts-addr}}\,({\it{s1\/}})\index{linked-rts-addr} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\it{s1\/}})\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{s1\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub})\- \\ 
$\wedge$$\;\;\;\;$({\rm{rn-saved}}\,({\it{s1\/}})\index{rn-saved} $=$ {\rm{read-rn}}\,({\tt{32}}, {\tt{2}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn}))\-\-$\;${\bf  endlet}\-
\end{tabbing}
     
\begin{tabbing}{\sc Theorem}:  strncat-s-s1-rfile-1 \\ \index{strncat-s-s1-rfile-1}
\=\+(\=\+{\rm{strncat-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strncat-statep} \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\tt{0}}, {\it{lst1\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{d3-7a2-5p}}\,({\it{rn\/}})\index{d3-7a2-5p})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{strncat-t1}}\,({\it{n1\/}}, {\it{lst1\/}})\index{strncat-t1})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strncat-s-s1-mem-1 \\ \index{strncat-s-s1-mem-1}
\=\+(\=\+{\rm{strncat-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strncat-statep} \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\tt{0}}, {\it{lst1\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{8}}, {\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\/}}, {\rm{strncat-t1}}\,({\it{n1\/}}, {\it{lst1\/}})\index{strncat-t1})\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 s1 to exit: s1 --> sn.  By induction.
; base case 1: s1 --> sn, when lst2[j] = 0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strncat-s1-sn-base1 \\ \index{strncat-s1-sn-base1}
\=\+(\=\+{\rm{strncat-s1p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{j*\/}}, {\it{j\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}}, {\it{i\_\/}}, {\it{n\_\/}})\index{strncat-s1p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\it{lst2\/}})\index{get-nth} $=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{mc-pc} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-dn}}\,({\tt{32}}, {\tt{0}}, {\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{read-dn} $=$ {\it{str1\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,({\tt{1}}, {\it{str1\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{mc-mem}, {\it{n1\/}}, {\rm{put-nth}}\,({\tt{0}}, {\it{i\/}}, {\it{lst1\/}})\index{put-nth})\index{mem-lst} \\ 
$\wedge$$\;\;\;\;$({\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{mc-rfile})\index{read-rn} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{add}}\,({\tt{32}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}, {\tt{8}})\index{add})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strncat-s0-sn-rfile-base1 \\ \index{strncat-s0-sn-rfile-base1}
\=\+(\=\+{\rm{strncat-s1p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{j*\/}}, {\it{j\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}}, {\it{i\_\/}}, {\it{n\_\/}})\index{strncat-s1p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\it{lst2\/}})\index{get-nth} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{oplen\/}} $\leq$ {\tt{32}}) \\ 
$\wedge$$\;\;\;\;${\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{d3-7a2-5p}}\,({\it{rn\/}})\index{d3-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{head}}\,({\rm{rn-saved}}\,({\it{s\/}})\index{rn-saved}, {\it{oplen\/}})\index{head}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strncat-s1-sn-mem-base1 \\ \index{strncat-s1-sn-mem-base1}
\=\+(\=\+{\rm{strncat-s1p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{j*\/}}, {\it{j\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}}, {\it{i\_\/}}, {\it{n\_\/}})\index{strncat-s1p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\it{lst2\/}})\index{get-nth} $=$ {\tt{0}}) \\ 
$\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{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}; base case 2: s1 --> sn, when lst2[j] =\= 0, n-1 = 0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strncat-s1-sn-base2 \\ \index{strncat-s1-sn-base2}
\=\+(\=\+{\rm{strncat-s1p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{j*\/}}, {\it{j\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}}, {\it{i\_\/}}, {\it{n\_\/}})\index{strncat-s1p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\it{lst2\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$(({\it{n\/}} $-\;1$) $=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{11}})\index{stepn})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{11}})\index{stepn})\index{mc-pc} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-dn}}\,({\tt{32}}, {\tt{0}}, {\rm{stepn}}\,({\it{s\/}}, {\tt{11}})\index{stepn})\index{read-dn} $=$ {\it{str1\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,(\=\+{\tt{1}}, \\ 
{\it{str1\/}}, \\ 
{\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{11}})\index{stepn})\index{mc-mem}, \\ 
{\it{n1\/}}, \\ 
{\rm{put-nth}}\,({\tt{0}}, $1\;+$ {\it{i\/}}, {\rm{put-nth}}\,({\rm{get-nth}}\,({\it{j\/}}, {\it{lst2\/}})\index{get-nth}, {\it{i\/}}, {\it{lst1\/}})\index{put-nth})\index{put-nth})\-\index{mem-lst} \\ 
$\wedge$$\;\;\;\;$({\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{11}})\index{stepn})\index{mc-rfile})\index{read-rn} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{11}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{add}}\,({\tt{32}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}, {\tt{8}})\index{add})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strncat-s1-sn-rfile-base2 \\ \index{strncat-s1-sn-rfile-base2}
\=\+(\=\+{\rm{strncat-s1p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{j*\/}}, {\it{j\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}}, {\it{i\_\/}}, {\it{n\_\/}})\index{strncat-s1p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\it{lst2\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$(({\it{n\/}} $-\;1$) $=$ {\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{11}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{d3-7a2-5p}}\,({\it{rn\/}})\index{d3-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{head}}\,({\rm{rn-saved}}\,({\it{s\/}})\index{rn-saved}, {\it{oplen\/}})\index{head}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strncat-s1-sn-mem-base2 \\ \index{strncat-s1-sn-mem-base2}
\=\+(\=\+{\rm{strncat-s1p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{j*\/}}, {\it{j\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}}, {\it{i\_\/}}, {\it{n\_\/}})\index{strncat-s1p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\it{lst2\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$(({\it{n\/}} $-\;1$) $=$ {\tt{0}}) \\ 
$\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{11}})\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}; induction case: s1 --> s1, when lst2[j] =\= 0, n-1 =\= 0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strncat-s1-s1 \\ \index{strncat-s1-s1}
\=\+(\=\+{\rm{strncat-s1p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{j*\/}}, {\it{j\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}}, {\it{i\_\/}}, {\it{n\_\/}})\index{strncat-s1p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\it{lst2\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$(({\it{n\/}} $-\;1$) $\not=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{strncat-s1p}}\,(\=\+{\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn}, \\ 
{\rm{add}}\,({\tt{32}}, {\it{i*\/}}, {\tt{1}})\index{add}, \\ 
$1\;+$ {\it{i\/}}, \\ 
{\it{str1\/}}, \\ 
{\it{n1\/}}, \\ 
{\rm{put-nth}}\,({\rm{get-nth}}\,({\it{j\/}}, {\it{lst2\/}})\index{get-nth}, {\it{i\/}}, {\it{lst1\/}})\index{put-nth}, \\ 
{\rm{add}}\,({\tt{32}}, {\it{j*\/}}, {\tt{1}})\index{add}, \\ 
$1\;+$ {\it{j\/}}, \\ 
{\it{str2\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{lst2\/}}, \\ 
{\it{i\_\/}}, \\ 
{\it{n\_\/}})\-\index{strncat-s1p} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\- \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{rn-saved}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn})\index{rn-saved} $=$ {\rm{rn-saved}}\,({\it{s\/}})\index{rn-saved}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strncat-s1-s1-rfile \\ \index{strncat-s1-s1-rfile}
\=\+(\=\+{\rm{strncat-s1p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{j*\/}}, {\it{j\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}}, {\it{i\_\/}}, {\it{n\_\/}})\index{strncat-s1p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\it{lst2\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$(({\it{n\/}} $-\;1$) $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{d3-7a2-5p}}\,({\it{rn\/}})\index{d3-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}:  strncat-s1-s1-mem \\ \index{strncat-s1-s1-mem}
\=\+(\=\+{\rm{strncat-s1p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{j*\/}}, {\it{j\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}}, {\it{i\_\/}}, {\it{n\_\/}})\index{strncat-s1p} \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\it{lst2\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$(({\it{n\/}} $-\;1$) $\not=$ {\tt{0}}) \\ 
$\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{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}; put together.  s1 --> sn.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strncat-s1-sn \\ \index{strncat-s1-sn}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strncat-t2}}\,({\it{j\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strncat-t2})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{strncat-s1p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{j*\/}}, {\it{j\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}}, {\it{i\_\/}}, {\it{n\_\/}})\index{strncat-s1p} \\ 
$\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{str1\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,({\tt{1}}, {\it{str1\/}}, {\rm{mc-mem}}\,({\it{sn\/}})\index{mc-mem}, {\it{n1\/}}, {\rm{strcpy2}}\,({\it{i\/}}, {\it{lst1\/}}, {\it{j\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strcpy2})\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}:  strncat-s1-sn-rfile \\ \index{strncat-s1-sn-rfile}
\=\+(\=\+{\rm{strncat-s1p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{j*\/}}, {\it{j\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}}, {\it{i\_\/}}, {\it{n\_\/}})\index{strncat-s1p} \\ 
$\wedge$$\;\;\;\;$({\it{oplen\/}} $\leq$ {\tt{32}}) \\ 
$\wedge$$\;\;\;\;${\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{strncat-t2}}\,({\it{j\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strncat-t2})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{d3-7a2-5p}}\,({\it{rn\/}})\index{d3-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{head}}\,({\rm{rn-saved}}\,({\it{s\/}})\index{rn-saved}, {\it{oplen\/}})\index{head}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strncat-s1-sn-mem \\ \index{strncat-s1-sn-mem}
\=\+(\=\+{\rm{strncat-s1p}}\,({\it{s\/}}, {\it{i*\/}}, {\it{i\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{j*\/}}, {\it{j\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}}, {\it{i\_\/}}, {\it{n\_\/}})\index{strncat-s1p} \\ 
$\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\/}}, {\rm{strncat-t2}}\,({\it{j\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strncat-t2})\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}; the correctness of strncat.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strncat-correctness \\ \index{strncat-correctness}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strncat-t}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strncat-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{strncat-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strncat-statep} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{sn\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{sn\/}})\index{mc-pc} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{sn\/}})\index{read-an} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-an}}\,({\tt{32}}, {\tt{7}}, {\it{sn\/}})\index{read-an} $=$ {\rm{add}}\,({\tt{32}}, {\rm{read-an}}\,({\tt{32}}, {\tt{7}}, {\it{s\/}})\index{read-an}, {\tt{4}})\index{add}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p} $\wedge$ ({\it{oplen\/}} $\leq$ {\tt{32}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{sn\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{8}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{24}})\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})\-)\- \\ 
$\wedge$$\;\;\;\;$({\rm{read-dn}}\,({\tt{32}}, {\tt{0}}, {\it{sn\/}})\index{read-dn} $=$ {\it{str1\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,({\tt{1}}, {\it{str1\/}}, {\rm{mc-mem}}\,({\it{sn\/}})\index{mc-mem}, {\it{n1\/}}, {\rm{strncat}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strncat})\index{mem-lst})\-\-$\;${\bf  endlet}\-
\end{tabbing}


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

\addvspace{18pt}

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