\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}; some general theorems.  They are used to establish properties of string
; functions.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  ilessp-lessp \\ \index{ilessp-lessp}
(({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{y\/}} $\in\;${\bf{N}}${}$)) $\rightarrow$ ({\rm{ilessp}}\,({\it{x\/}}, {\it{y\/}})\index{ilessp} $=$ ({\it{x\/}} $<$ {\it{y\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  idifference-numberp \\ \index{idifference-numberp}
({\rm{idifference}}\,({\it{x\/}}, {\it{y\/}})\index{idifference} $\in\;${\bf{N}}${}$) $=$ ($\neg$ {\rm{ilessp}}\,({\it{x\/}}, {\it{y\/}})\index{ilessp})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  idifference-equal-0 \\ \index{idifference-equal-0}
({\rm{idifference}}\,({\it{x\/}}, {\it{y\/}})\index{idifference} $=$ {\tt{0}}) $=$ ({\rm{fix-int}}\,({\it{x\/}})\index{fix-int} $=$ {\rm{fix-int}}\,({\it{y\/}})\index{fix-int})
\end{tabbing}


\noindent{\sc Event}:   Enable get-nth-0.

\addvspace{18pt}

\noindent{\sc Event}:   Enable put-nth-0.

\addvspace{18pt}

\begin{verbatim}; the upper bound of strlen.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strlen-ub \\ \index{strlen-ub}
{\rm{stringp}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{stringp} $\rightarrow$ ({\rm{strlen}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{strlen} $<$ {\it{n\/}})
\end{tabbing}

\begin{verbatim}; the lower bound of strlen.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strlen-lb \\ \index{strlen-lb}
{\rm{strlen}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{strlen} $\not<$ {\it{i\/}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strlen-01 \\ \index{strlen-01}
\=\+({\rm{strlen}}\,({\it{i\/}}, {\tt{0}}, {\it{lst\/}})\index{strlen} $=$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{strlen}}\,({\it{i\/}}, {\tt{1}}, {\it{lst\/}})\index{strlen} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{i\/}} $<$ {\tt{1}}) $\wedge$ ({\rm{get-nth}}\,({\tt{0}}, {\it{lst\/}})\index{get-nth} $\not=$ {\tt{0}})$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\it{i\/}}$\;${\bf  endif}\-)\- \\ 
$\wedge$$\;\;\;\;$({\rm{strlen}}\,({\tt{1}}, {\it{n\/}}, {\it{lst\/}})\index{strlen} $\not=$ {\tt{0}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strlen-ii \\ \index{strlen-ii}
{\rm{strlen}}\,({\it{i\/}}, {\it{i\/}}, {\it{lst\/}})\index{strlen} $=$ {\it{i\/}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strlen-ii1 \\ \index{strlen-ii1}
\=\+{\rm{strlen}}\,({\it{i\/}}, $1\;+$ {\it{i\/}}, {\it{lst\/}})\index{strlen} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth} $=$ {\tt{0}}$\;\;${\bf then }{\it{i\/}} \\ 
{\bf else }$1\;+$ {\it{i\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; some properties of strlen.
; lst[j] =\= 0, if i <= j < strlen(lst).
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strlen-non0p \\ \index{strlen-non0p}
(({\it{i\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $<$ {\rm{strlen}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{strlen})) $\rightarrow$ ({\rm{get-nth}}\,({\it{j\/}}, {\it{lst\/}})\index{get-nth} $\not=$ {\tt{0}})
\end{tabbing}

\begin{verbatim}; lst[strlen] == 0!
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strlen-0p \\ \index{strlen-0p}
{\rm{stringp}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{stringp} $\rightarrow$ ({\rm{get-nth}}\,({\rm{strlen}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{strlen}, {\it{lst\/}})\index{get-nth} $=$ {\tt{0}})
\end{tabbing}

\begin{verbatim}; some properties of strcpy.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strcpy-get-1 \\ \index{strcpy-get-1}
({\it{j\/}} $<$ {\it{i\/}}) $\rightarrow$ ({\rm{get-nth}}\,({\it{j\/}}, {\rm{strcpy}}\,({\it{i\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcpy})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{j\/}}, {\it{lst1\/}})\index{get-nth})
\end{tabbing}

\begin{verbatim}; strlen(strcpy(lst1, lst2)) == strlen(lst2).
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strcpy-strlen \\ \index{strcpy-strlen}
{\rm{strlen}}\,({\it{i\/}}, {\it{n2\/}}, {\rm{strcpy}}\,({\it{i\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcpy})\index{strlen} $=$ {\rm{strlen}}\,({\it{i\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strlen}
\end{tabbing}

\begin{verbatim};  if i <= j <= strlen(lst2), lst1[j] == lst2[j].
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strcpy-cpy \\ \index{strcpy-cpy}
\=\+({\rm{stringp}}\,({\it{i\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{stringp} $\wedge$ ({\it{i\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $\leq$ {\rm{strlen}}\,({\it{i\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strlen})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\rm{strcpy}}\,({\it{i\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcpy})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{j\/}}, {\it{lst2\/}})\index{get-nth})\-
\end{tabbing}

\begin{verbatim};  if lst2 is a string, then lst1' is also a string.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strcpy-stringp \\ \index{strcpy-stringp}
{\rm{stringp}}\,({\it{i\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{stringp} $\rightarrow$ {\rm{stringp}}\,({\it{i\/}}, {\it{n2\/}}, {\rm{strcpy}}\,({\it{i\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcpy})\index{stringp}
\end{tabbing}

\begin{verbatim}; some properties of strcmp.
; (strcmp lst lst) == 0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strcmp-id \\ \index{strcmp-id}
{\rm{strcmp}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{lst\/}})\index{strcmp} $=$ {\tt{0}}
\end{tabbing}

\begin{verbatim}; (strcmp lst1 lst2) < 0 ==> (strcmp lst2 lst1) >= 0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strcmp-antisym \\ \index{strcmp-antisym}
{\rm{negativep}}\,({\rm{strcmp}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strcmp}) $=$ ({\tt{0}} $<$ {\rm{strcmp}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst2\/}}, {\it{lst1\/}})\index{strcmp})
\end{tabbing}

\begin{verbatim}; the transitivity of strcmp.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strcmp-trans-1 \\ \index{strcmp-trans-1}
\=\+(\=\+{\rm{lst-of-chrp}}\,({\it{lst1\/}})\index{lst-of-chrp} \\ 
$\wedge$$\;\;\;\;${\rm{lst-of-chrp}}\,({\it{lst2\/}})\index{lst-of-chrp} \\ 
$\wedge$$\;\;\;\;${\rm{lst-of-chrp}}\,({\it{lst3\/}})\index{lst-of-chrp} \\ 
$\wedge$$\;\;\;\;$({\rm{strcmp}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strcmp} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{strcmp}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst2\/}}, {\it{lst3\/}})\index{strcmp} $\in\;${\bf{N}}${}$))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{strcmp}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst1\/}}, {\it{lst3\/}})\index{strcmp} $\in\;${\bf{N}}${}$)\-
\end{tabbing}

\begin{verbatim}; (strcpy lst1 lst2) == lst2.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strcmp-strcpy \\ \index{strcmp-strcpy}
{\rm{strcmp}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst2\/}}, {\rm{strcpy}}\,({\it{i\/}}, {\it{lst1\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strcpy})\index{strcmp} $=$ {\tt{0}}
\end{tabbing}

\begin{verbatim}; if (strcmp lst1 lst2) == 0, all i <= j < (strlen lst1) lst1[j] == lst2[j].
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strcmp-thm1 \\ \index{strcmp-thm1}
\=\+(\=\+{\rm{lst-of-chrp}}\,({\it{lst1\/}})\index{lst-of-chrp} \\ 
$\wedge$$\;\;\;\;${\rm{lst-of-chrp}}\,({\it{lst2\/}})\index{lst-of-chrp} \\ 
$\wedge$$\;\;\;\;$({\rm{strcmp}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strcmp} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\leq$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ {\rm{strlen}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst1\/}})\index{strlen}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{j\/}}, {\it{lst2\/}})\index{get-nth})\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{strcmp-sk} \\  
\=\+{\rm{strcmp-sk}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strcmp-sk} \\ 
$\leftrightarrow$$\;\;\;\;$$\exists\;${\it{j\/}}$\;$(\=\+$\forall\;${\it{i\/}}$\;$(({\it{i\/}} $<$ {\it{j\/}}) $\rightarrow$ ({\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{i\/}}, {\it{lst2\/}})\index{get-nth}))\index{forall} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{strcmp}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strcmp} \\ 
$=$$\;\;\;\;${\rm{idifference}}\,({\rm{get-nth}}\,({\it{j\/}}, {\it{lst1\/}})\index{get-nth}, {\rm{get-nth}}\,({\it{j\/}}, {\it{lst2\/}})\index{get-nth})\index{idifference})\-)\-\index{exists}\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{strcmp-j} \\  
\=\+{\rm{strcmp-j}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strcmp-j} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $<$ {\it{n1\/}} \\ 
{\bf then }\=\+{\bf if }{\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{i\/}}, {\it{lst2\/}})\index{get-nth} \\ 
{\bf then }\=\+{\bf if }{\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\sc{null}}\index{null}$\;\;${\bf then }{\rm{fix}}\,({\it{i\/}}) \\ 
{\bf else }{\rm{strcmp-j}}\,($1\;+$ {\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strcmp-j}$\;${\bf  endif}\- \\ 
{\bf else }{\rm{fix}}\,({\it{i\/}})$\;${\bf  endif}\- \\ 
{\bf else }{\rm{fix}}\,({\it{i\/}})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strcmp-j-1 \\ \index{strcmp-j-1}
\=\+(({\it{i\/}} $<$ {\rm{strcmp-j}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strcmp-j}) $\wedge$ ({\it{i1\/}} $\leq$ {\it{i\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{i\/}}, {\it{lst2\/}})\index{get-nth})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strcmp-j-2 \\ \index{strcmp-j-2}
\=\+({\rm{strcmp}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strcmp} $\not=$ {\tt{0}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{strcmp}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strcmp} \\ 
$=$$\;\;\;\;${\rm{idifference}}\,(\=\+{\rm{get-nth}}\,({\rm{strcmp-j}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strcmp-j}, {\it{lst1\/}})\index{get-nth}, \\ 
{\rm{get-nth}}\,({\rm{strcmp-j}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strcmp-j}, {\it{lst2\/}})\index{get-nth})\-\index{idifference})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strcmp-thm2 \\ \index{strcmp-thm2}
({\rm{strcmp}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strcmp} $\not=$ {\tt{0}}) $\rightarrow$ {\rm{strcmp-sk}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strcmp-sk}
\end{tabbing}


\noindent{\sc Event}:   Disable strcmp-j-1.

\addvspace{18pt}

\noindent{\sc Event}:   Disable strcmp-j-2.

\addvspace{18pt}

\begin{verbatim}; some properties of strcat.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strcpy1-get-1 \\ \index{strcpy1-get-1}
({\it{j\/}} $<$ {\it{i1\/}}) $\rightarrow$ ({\rm{get-nth}}\,({\it{j\/}}, {\rm{strcpy1}}\,({\it{i1\/}}, {\it{lst1\/}}, {\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcpy1})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{j\/}}, {\it{lst1\/}})\index{get-nth})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{strlen1} \\  
\=\+{\rm{strlen1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{strlen1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $<$ {\it{n\/}} \\ 
{\bf then }\=\+{\bf if }{\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth} $=$ {\sc{null}}\index{null}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }$1\;+$ {\rm{strlen1}}\,($1\;+$ {\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{strlen1}$\;${\bf  endif}\- \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strlen1-strlen \\ \index{strlen1-strlen}
{\rm{strlen1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{strlen1} $=$ ({\rm{strlen}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{strlen} $-$ {\it{i\/}})
\end{tabbing}


\noindent{\sc Event}:   Disable strlen1-strlen.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  strcpy1-get-2 \\ \index{strcpy1-get-2}
\=\+(({\it{i1\/}} $+$ {\rm{strlen1}}\,({\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strlen1}) $<$ {\it{j\/}}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\rm{strcpy1}}\,({\it{i1\/}}, {\it{lst1\/}}, {\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcpy1})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{j\/}}, {\it{lst1\/}})\index{get-nth})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  get-nth-plus-0 \\ \index{get-nth-plus-0}
({\it{j\/}} $\not\in\;${\bf{N}}${}$) $\rightarrow$ ({\rm{get-nth}}\,({\it{i\/}} $+$ {\it{j\/}}, {\it{lst\/}})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  plus-sub1-add1 \\ \index{plus-sub1-add1}
(({\it{x\/}} $+$ ($1\;+$ {\it{y\/}})) $-\;1$) $=$ ({\it{x\/}} $+$ {\it{y\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strcpy1-get-3 \\ \index{strcpy1-get-3}
\=\+(({\it{i1\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $<$ ({\it{i1\/}} $+$ {\rm{strlen1}}\,({\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strlen1}))) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{get-nth}}\,({\it{j\/}}, {\rm{strcpy1}}\,({\it{i1\/}}, {\it{lst1\/}}, {\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcpy1})\index{get-nth} \\ 
$=$$\;\;\;\;${\rm{get-nth}}\,({\it{i2\/}} $+$ ({\it{j\/}} $-$ {\it{i1\/}}), {\it{lst2\/}})\index{get-nth})\-\-
\end{tabbing}

\begin{verbatim}; all 0 <= j < (strlen lst1) lst1'[j] == lst1[j].
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strcat-get-1 \\ \index{strcat-get-1}
\=\+({\it{j\/}} $<$ {\rm{strlen}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}})\index{strlen}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\rm{strcat}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcat})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{j\/}}, {\it{lst1\/}})\index{get-nth})\-
\end{tabbing}

\begin{verbatim}; all (strlen lst1) <= j < (strlen lst1)+(strlen lst2) lst1'[j] == lst2[j].
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strcat-get-2 \\ \index{strcat-get-2}
\=\+(\=\+{\rm{stringp}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}})\index{stringp} \\ 
$\wedge$$\;\;\;\;$({\rm{strlen}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}})\index{strlen} $\leq$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ ({\rm{strlen}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}})\index{strlen} $+$ {\rm{strlen}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}})\index{strlen})))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{get-nth}}\,({\it{j\/}}, {\rm{strcat}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcat})\index{get-nth} \\ 
$=$$\;\;\;\;${\rm{get-nth}}\,({\it{j\/}} $-$ {\rm{strlen}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}})\index{strlen}, {\it{lst2\/}})\index{get-nth})\-\-
\end{tabbing}

\begin{verbatim}; some properties about strchr.
; lst[strchr] == ch,  if strchr returns non-f.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strchr-thm1 \\ \index{strchr-thm1}
{\rm{strchr}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr} $\rightarrow$ ({\rm{get-nth}}\,({\rm{strchr}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr}, {\it{lst\/}})\index{get-nth} $=$ {\it{ch\/}})
\end{tabbing}

\begin{verbatim}; all i <= j < strchr, lst[j] =\= ch.  i.e. strchr is the first one.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strchr-thm2 \\ \index{strchr-thm2}
(({\it{i\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $<$ {\rm{strchr}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr})) $\rightarrow$ ({\rm{get-nth}}\,({\it{j\/}}, {\it{lst\/}})\index{get-nth} $\not=$ {\it{ch\/}})
\end{tabbing}
                   
\begin{verbatim}; all i <= j < strlen, lst[j] =\= ch, if strchr returns f.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strchr-thm3 \\ \index{strchr-thm3}
\=\+(($\neg$ {\rm{strchr}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr}) $\wedge$ ({\it{i\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $<$ {\rm{strlen}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{strlen})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\it{lst\/}})\index{get-nth} $\not=$ {\it{ch\/}})\-
\end{tabbing}

\begin{verbatim}; ch is not equal to the null character, if strchr returns f.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strchr-thm4 \\ \index{strchr-thm4}
({\rm{stringp}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{stringp} $\wedge$ ($\neg$ {\rm{strchr}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr})) $\rightarrow$ ({\it{ch\/}} $\not=$ {\tt{0}})
\end{tabbing}

\begin{verbatim}; strcpy and strchr.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strcpy-strchr \\ \index{strcpy-strchr}
{\rm{strchr}}\,({\it{i\/}}, {\it{n\/}}, {\rm{strcpy}}\,({\it{i\/}}, {\it{lst1\/}}, {\it{n\/}}, {\it{lst2\/}})\index{strcpy}, {\it{ch\/}})\index{strchr} $=$ {\rm{strchr}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst2\/}}, {\it{ch\/}})\index{strchr}
\end{tabbing}

\begin{verbatim}; some properties about memset.
; lemmas about memset1.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  memset1-get-1 \\ \index{memset1-get-1}
({\it{j\/}} $<$ {\it{i\/}}) $\rightarrow$ ({\rm{get-nth}}\,({\it{j\/}}, {\rm{memset1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{memset1})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{j\/}}, {\it{lst\/}})\index{get-nth})
\end{tabbing}

\begin{verbatim}; all i <= j < i+n, lst'[j] == ch.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  memset1-thm1 \\ \index{memset1-thm1}
\=\+(({\it{i\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $<$ ({\it{i\/}} $+$ {\it{n\/}}))) \\ 
$\rightarrow$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\rm{memset1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{memset1})\index{get-nth} $=$ {\it{ch\/}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  memset1-thm2 \\ \index{memset1-thm2}
\=\+((({\it{i\/}} $+$ {\it{n\/}}) $\leq$ {\it{j\/}}) $\wedge$ ({\it{n\/}} $\not\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\rm{memset1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{memset1})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{j\/}}, {\it{lst\/}})\index{get-nth})\-
\end{tabbing}

\begin{verbatim}; all i <= j < n, lst'[j] == ch.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  memset-thm1 \\ \index{memset-thm1}
(({\it{i\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $<$ {\it{n\/}})) $\rightarrow$ ({\rm{get-nth}}\,({\it{j\/}}, {\rm{memset}}\,({\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{memset})\index{get-nth} $=$ {\it{ch\/}})
\end{tabbing}

\begin{verbatim}; all j >= n, lst'[j] == lst[j].
\end{verbatim}\begin{tabbing}{\sc Theorem}:  memset-thm2 \\ \index{memset-thm2}
\=\+(({\it{n\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{n\/}} $\in\;${\bf{N}}${}$)) \\ 
$\rightarrow$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\rm{memset}}\,({\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{memset})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{j\/}}, {\it{lst\/}})\index{get-nth})\-
\end{tabbing}

\begin{verbatim}; some properties about memchr.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  memchr1-thm1 \\ \index{memchr1-thm1}
{\rm{memchr1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{memchr1} $\rightarrow$ ({\rm{get-nth}}\,({\rm{memchr1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{memchr1}, {\it{lst\/}})\index{get-nth} $=$ {\it{ch\/}})
\end{tabbing}

\begin{verbatim}; lst[memchr] == ch,  if memchr returns non-f.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  memchr-thm1 \\ \index{memchr-thm1}
{\rm{memchr}}\,({\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{memchr} $\rightarrow$ ({\rm{get-nth}}\,({\rm{memchr}}\,({\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{memchr}, {\it{lst\/}})\index{get-nth} $=$ {\it{ch\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  memchr1-thm2 \\ \index{memchr1-thm2}
(({\it{i\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $<$ {\rm{memchr1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{memchr1})) $\rightarrow$ ({\rm{get-nth}}\,({\it{j\/}}, {\it{lst\/}})\index{get-nth} $\not=$ {\it{ch\/}})
\end{tabbing}

\begin{verbatim}; all j < memchr, lst[j] =\= ch.  i.e. memchr is the first one.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  memchr-thm2 \\ \index{memchr-thm2}
({\it{j\/}} $<$ {\rm{memchr}}\,({\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{memchr}) $\rightarrow$ ({\rm{get-nth}}\,({\it{j\/}}, {\it{lst\/}})\index{get-nth} $\not=$ {\it{ch\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  memchr1-thm3 \\ \index{memchr1-thm3}
\=\+(($\neg$ {\rm{memchr1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{memchr1}) $\wedge$ ({\it{i\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $<$ ({\it{i\/}} $+$ {\it{n\/}}))) \\ 
$\rightarrow$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\it{lst\/}})\index{get-nth} $\not=$ {\it{ch\/}})\-
\end{tabbing}

\begin{verbatim}; all j < n, lst[j] =\= ch, if memchr returns f.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  memchr-thm3 \\ \index{memchr-thm3}
(($\neg$ {\rm{memchr}}\,({\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{memchr}) $\wedge$ ({\it{j\/}} $<$ {\it{n\/}})) $\rightarrow$ ({\rm{get-nth}}\,({\it{j\/}}, {\it{lst\/}})\index{get-nth} $\not=$ {\it{ch\/}})
\end{tabbing}

\begin{verbatim}; some properties about strrchr.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strrchr-la1 \\ \index{strrchr-la1}
({\it{j\/}} $\in\;${\bf{N}}${}$) $\rightarrow$ {\rm{strrchr}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}}, {\it{j\/}})\index{strrchr}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strrchr-strchr-la \\ \index{strrchr-strchr-la}
($\neg$ {\rm{strchr}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr}) $\rightarrow$ ({\rm{strrchr}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}}, {\it{j\/}})\index{strrchr} $=$ {\it{j\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strrchr-la2 \\ \index{strrchr-la2}
{\rm{strchr}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr} $\rightarrow$ ({\rm{get-nth}}\,({\rm{strrchr}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}}, {\it{j\/}})\index{strrchr}, {\it{lst\/}})\index{get-nth} $=$ {\it{ch\/}})
\end{tabbing}

\begin{verbatim}; strrchr finds ch in the string.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strrchr-thm1 \\ \index{strrchr-thm1}
{\rm{strrchr}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}}, {\bf{f}})\index{strrchr} $\rightarrow$ ({\rm{get-nth}}\,({\rm{strrchr}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}}, {\bf{f}})\index{strrchr}, {\it{lst\/}})\index{get-nth} $=$ {\it{ch\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strchr-get \\ \index{strchr-get}
(({\it{i\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $<$ {\rm{strlen}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{strlen})) $\rightarrow$ {\rm{strchr}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\rm{get-nth}}\,({\it{j\/}}, {\it{lst\/}})\index{get-nth})\index{strchr}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strrchr-la3 \\ \index{strrchr-la3}
\=\+(\=\+{\rm{strchr}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr} \\ 
$\wedge$$\;\;\;\;$({\rm{strrchr}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}}, {\it{k\/}})\index{strrchr} $<$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ {\rm{strlen}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{strlen}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\it{lst\/}})\index{get-nth} $\not=$ {\it{ch\/}})\-
\end{tabbing}

\begin{verbatim}; strrchr returns the last one.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strrchr-thm2 \\ \index{strrchr-thm2}
\=\+(\=\+{\rm{strrchr}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}}, {\bf{f}})\index{strrchr} \\ 
$\wedge$$\;\;\;\;$({\rm{strrchr}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}}, {\bf{f}})\index{strrchr} $<$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ {\rm{strlen}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{strlen}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\it{lst\/}})\index{get-nth} $\not=$ {\it{ch\/}})\-
\end{tabbing}

\begin{verbatim}; no means none.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strrchr-thm3 \\ \index{strrchr-thm3}
\=\+(($\neg$ {\rm{strrchr}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}}, {\it{k\/}})\index{strrchr}) $\wedge$ ({\it{i\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $<$ {\rm{strlen}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{strlen})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\it{lst\/}})\index{get-nth} $\not=$ {\it{ch\/}})\-
\end{tabbing}

\begin{verbatim}; ch is not equal to the null character, if strrchr returns f.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strrchr-thm4 \\ \index{strrchr-thm4}
({\rm{stringp}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{stringp} $\wedge$ ($\neg$ {\rm{strrchr}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}}, {\it{k\/}})\index{strrchr})) $\rightarrow$ ({\it{ch\/}} $\not=$ {\tt{0}})
\end{tabbing}

\begin{verbatim}; some properties about memcmp.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  memcmp1-id \\ \index{memcmp1-id}
{\rm{memcmp1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{lst\/}})\index{memcmp1} $=$ {\tt{0}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  memcmp-id \\ \index{memcmp-id}
{\rm{memcmp}}\,({\it{n\/}}, {\it{lst\/}}, {\it{lst\/}})\index{memcmp} $=$ {\tt{0}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  memcmp1-thm1 \\ \index{memcmp1-thm1}
\=\+(\=\+{\rm{lst-of-chrp}}\,({\it{lst1\/}})\index{lst-of-chrp} \\ 
$\wedge$$\;\;\;\;${\rm{lst-of-chrp}}\,({\it{lst2\/}})\index{lst-of-chrp} \\ 
$\wedge$$\;\;\;\;$({\rm{memcmp1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{memcmp1} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\leq$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ ({\it{i\/}} $+$ {\it{n\/}})))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{j\/}}, {\it{lst2\/}})\index{get-nth})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  memcmp-thm1 \\ \index{memcmp-thm1}
\=\+(\=\+{\rm{lst-of-chrp}}\,({\it{lst1\/}})\index{lst-of-chrp} \\ 
$\wedge$$\;\;\;\;${\rm{lst-of-chrp}}\,({\it{lst2\/}})\index{lst-of-chrp} \\ 
$\wedge$$\;\;\;\;$({\rm{memcmp}}\,({\it{n\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{memcmp} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ {\it{n\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{j\/}}, {\it{lst2\/}})\index{get-nth})\-
\end{tabbing}
             
\begin{tabbing}{\sc Definition}:\index{memcmp-sk} \\  
\=\+{\rm{memcmp-sk}}\,({\it{n\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{memcmp-sk} \\ 
$\leftrightarrow$$\;\;\;\;$$\exists\;${\it{j\/}}$\;$(\=\+$\forall\;${\it{i\/}}$\;$(({\it{i\/}} $<$ {\it{j\/}}) $\rightarrow$ ({\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{i\/}}, {\it{lst2\/}})\index{get-nth}))\index{forall} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{memcmp}}\,({\it{n\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{memcmp} \\ 
$=$$\;\;\;\;${\rm{idifference}}\,({\rm{get-nth}}\,({\it{j\/}}, {\it{lst1\/}})\index{get-nth}, {\rm{get-nth}}\,({\it{j\/}}, {\it{lst2\/}})\index{get-nth})\index{idifference})\-)\-\index{exists}\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{memcmp-j} \\  
\=\+{\rm{memcmp-j}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{memcmp-j} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{i\/}}, {\it{lst2\/}})\index{get-nth} \\ 
{\bf then }\=\+{\bf if }({\it{n\/}} $-\;1$) $=$ {\tt{0}}$\;\;${\bf then }{\rm{fix}}\,({\it{i\/}}) \\ 
{\bf else }{\rm{memcmp-j}}\,($1\;+$ {\it{i\/}}, {\it{n\/}} $-\;1$, {\it{lst1\/}}, {\it{lst2\/}})\index{memcmp-j}$\;${\bf  endif}\- \\ 
{\bf else }{\rm{fix}}\,({\it{i\/}})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  memcmp-j-1 \\ \index{memcmp-j-1}
\=\+(({\it{i\/}} $<$ {\rm{memcmp-j}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{memcmp-j}) $\wedge$ ({\it{i1\/}} $\leq$ {\it{i\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{i\/}}, {\it{lst2\/}})\index{get-nth})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  memcmp-j-2 \\ \index{memcmp-j-2}
\=\+({\rm{memcmp1}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{memcmp1} $\not=$ {\tt{0}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{memcmp1}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{memcmp1} \\ 
$=$$\;\;\;\;${\rm{idifference}}\,(\=\+{\rm{get-nth}}\,({\rm{memcmp-j}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{memcmp-j}, {\it{lst1\/}})\index{get-nth}, \\ 
{\rm{get-nth}}\,({\rm{memcmp-j}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{memcmp-j}, {\it{lst2\/}})\index{get-nth})\-\index{idifference})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  memcmp-thm2 \\ \index{memcmp-thm2}
({\rm{memcmp}}\,({\it{n\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{memcmp} $\not=$ {\tt{0}}) $\rightarrow$ {\rm{memcmp-sk}}\,({\it{n\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{memcmp-sk}
\end{tabbing}


\noindent{\sc Event}:   Disable memcmp-j-1.

\addvspace{18pt}

\noindent{\sc Event}:   Disable memcmp-j-2.

\addvspace{18pt}

\begin{verbatim}; some properties about strncat.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strcpy2-get-1 \\ \index{strcpy2-get-1}
({\it{j\/}} $<$ {\it{i1\/}}) $\rightarrow$ ({\rm{get-nth}}\,({\it{j\/}}, {\rm{strcpy2}}\,({\it{i1\/}}, {\it{lst1\/}}, {\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcpy2})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{j\/}}, {\it{lst1\/}})\index{get-nth})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strlen1-ii \\ \index{strlen1-ii}
{\rm{strlen1}}\,({\it{i\/}}, {\it{i\/}}, {\it{lst\/}})\index{strlen1} $=$ {\tt{0}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strcpy2-get-2 \\ \index{strcpy2-get-2}
\=\+(({\it{i1\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $<$ ({\it{i1\/}} $+$ {\rm{strlen1}}\,({\it{i2\/}}, {\it{i2\/}} $+$ {\it{n2\/}}, {\it{lst2\/}})\index{strlen1}))) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{get-nth}}\,({\it{j\/}}, {\rm{strcpy2}}\,({\it{i1\/}}, {\it{lst1\/}}, {\it{i2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcpy2})\index{get-nth} \\ 
$=$$\;\;\;\;${\rm{get-nth}}\,(({\it{i2\/}} $+$ {\it{j\/}}) $-$ {\it{i1\/}}, {\it{lst2\/}})\index{get-nth})\-\-
\end{tabbing}

\begin{verbatim}; all j < (strlen lst1), lst'[j] == lst1[j].
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strncat-get-1 \\ \index{strncat-get-1}
\=\+({\it{j\/}} $<$ {\rm{strlen}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}})\index{strlen}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\rm{strncat}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strncat})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{j\/}}, {\it{lst1\/}})\index{get-nth})\-
\end{tabbing}

\begin{verbatim}; all (strlen lst1) <= j < (strlen lst1)+(strlen lst2), 
; lst'[j] == lst2[j-(strlen lst1)].
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strncat-get-2 \\ \index{strncat-get-2}
\=\+(\=\+{\rm{stringp}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}})\index{stringp} \\ 
$\wedge$$\;\;\;\;$({\rm{strlen}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}})\index{strlen} $\leq$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ ({\rm{strlen}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}})\index{strlen} $+$ {\rm{strlen}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}})\index{strlen})))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{get-nth}}\,({\it{j\/}}, {\rm{strncat}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strncat})\index{get-nth} \\ 
$=$$\;\;\;\;${\rm{get-nth}}\,({\it{j\/}} $-$ {\rm{strlen}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}})\index{strlen}, {\it{lst2\/}})\index{get-nth})\-\-
\end{tabbing}

\begin{verbatim}; some properties about strncpy.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  zero-list1-la \\ \index{zero-list1-la}
({\it{j\/}} $<$ {\it{i\/}}) $\rightarrow$ ({\rm{get-nth}}\,({\it{j\/}}, {\rm{zero-list1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{zero-list1})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{j\/}}, {\it{lst\/}})\index{get-nth})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  zero-list1-get \\ \index{zero-list1-get}
\=\+(({\it{i\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $<$ (({\it{i\/}} $+$ {\it{n\/}}) $-\;1$))) \\ 
$\rightarrow$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\rm{zero-list1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{zero-list1})\index{get-nth} $=$ {\tt{0}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  zero-list-get \\ \index{zero-list-get}
\=\+(({\it{i\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $<$ ({\it{i\/}} $+$ {\it{n\/}}))) \\ 
$\rightarrow$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\rm{zero-list}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{zero-list})\index{get-nth} $=$ {\tt{0}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strncpy1-get \\ \index{strncpy1-get}
({\it{j\/}} $<$ {\it{i\/}}) $\rightarrow$ ({\rm{get-nth}}\,({\it{j\/}}, {\rm{strncpy1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strncpy1})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{j\/}}, {\it{lst1\/}})\index{get-nth})
\end{tabbing}


\noindent{\sc Event}:   Disable zero-list.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  strncpy1-strlen \\ \index{strncpy1-strlen}
{\rm{strlen}}\,({\it{i\/}}, {\it{i\/}} $+$ {\it{n\/}}, {\rm{strncpy1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strncpy1})\index{strlen} $=$ {\rm{strlen}}\,({\it{i\/}}, {\it{i\/}} $+$ {\it{n\/}}, {\it{lst2\/}})\index{strlen}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strcpy-0 \\ \index{strcpy-0}
{\rm{strncpy}}\,({\tt{0}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strncpy} $=$ {\it{lst1\/}}
\end{tabbing}

\begin{verbatim}; the length of (strncpy lst1 lst2) equals the length of lst2.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strncpy-strlen \\ \index{strncpy-strlen}
\=\+{\rm{strlen}}\,({\tt{0}}, {\it{n\/}}, {\rm{strncpy}}\,({\it{n\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strncpy})\index{strlen} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{strlen}}\,({\tt{0}}, {\it{n\/}}, {\it{lst1\/}})\index{strlen} \\ 
{\bf else }{\rm{strlen}}\,({\tt{0}}, {\it{n\/}}, {\it{lst2\/}})\index{strlen}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strncpy1-cpy \\ \index{strncpy1-cpy}
\=\+(({\it{i\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $<$ {\rm{strlen}}\,({\it{i\/}}, {\it{i\/}} $+$ {\it{n\/}}, {\it{lst2\/}})\index{strlen})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\rm{strncpy1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strncpy1})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{j\/}}, {\it{lst2\/}})\index{get-nth})\-
\end{tabbing}

\begin{verbatim}; all j < (strlen lst2), lst'[j] == lst2[j].
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strncpy-cpy \\ \index{strncpy-cpy}
\=\+({\it{j\/}} $<$ {\rm{strlen}}\,({\tt{0}}, {\it{n\/}}, {\it{lst2\/}})\index{strlen}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\rm{strncpy}}\,({\it{n\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strncpy})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{j\/}}, {\it{lst2\/}})\index{get-nth})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strncpy1-0s \\ \index{strncpy1-0s}
\=\+(({\rm{strlen}}\,({\it{i\/}}, {\it{i\/}} $+$ {\it{n\/}}, {\it{lst2\/}})\index{strlen} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $<$ ({\it{i\/}} $+$ {\it{n\/}}))) \\ 
$\rightarrow$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\rm{strncpy1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strncpy1})\index{get-nth} $=$ {\tt{0}})\-
\end{tabbing}

\begin{verbatim}; all (strlen lst2) <= j < n, lst'[j] == 0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strncpy-0s \\ \index{strncpy-0s}
\=\+(({\rm{strlen}}\,({\tt{0}}, {\it{n\/}}, {\it{lst2\/}})\index{strlen} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $<$ {\it{n\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\rm{strncpy}}\,({\it{n\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strncpy})\index{get-nth} $=$ {\tt{0}})\-
\end{tabbing}

\begin{verbatim}; some properties about strncmp.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strncmp1-id \\ \index{strncmp1-id}
{\rm{strncmp1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{lst\/}})\index{strncmp1} $=$ {\tt{0}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strncmp-id \\ \index{strncmp-id}
{\rm{strncmp}}\,({\it{n\/}}, {\it{lst\/}}, {\it{lst\/}})\index{strncmp} $=$ {\tt{0}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strncmp1-thm1 \\ \index{strncmp1-thm1}
\=\+(\=\+{\rm{lst-of-chrp}}\,({\it{lst1\/}})\index{lst-of-chrp} \\ 
$\wedge$$\;\;\;\;${\rm{lst-of-chrp}}\,({\it{lst2\/}})\index{lst-of-chrp} \\ 
$\wedge$$\;\;\;\;$({\rm{strncmp1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strncmp1} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\leq$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ {\rm{strlen}}\,({\it{i\/}}, {\it{i\/}} $+$ {\it{n\/}}, {\it{lst1\/}})\index{strlen}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{j\/}}, {\it{lst2\/}})\index{get-nth})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strncmp-thm1 \\ \index{strncmp-thm1}
\=\+(\=\+{\rm{lst-of-chrp}}\,({\it{lst1\/}})\index{lst-of-chrp} \\ 
$\wedge$$\;\;\;\;${\rm{lst-of-chrp}}\,({\it{lst2\/}})\index{lst-of-chrp} \\ 
$\wedge$$\;\;\;\;$({\rm{strncmp}}\,({\it{n\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strncmp} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ {\rm{strlen}}\,({\tt{0}}, {\it{n\/}}, {\it{lst1\/}})\index{strlen}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{j\/}}, {\it{lst2\/}})\index{get-nth})\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{strncmp-j} \\  
\=\+{\rm{strncmp-j}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strncmp-j} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{i\/}}, {\it{lst2\/}})\index{get-nth} \\ 
{\bf then }\=\+{\bf if }{\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\tt{0}}$\;\;${\bf then }{\rm{fix}}\,({\it{i\/}}) \\ 
{\bf elseif }({\it{n\/}} $-\;1$) $=$ {\tt{0}}$\;\;${\bf then }{\rm{fix}}\,({\it{i\/}}) \\ 
{\bf else }{\rm{strncmp-j}}\,($1\;+$ {\it{i\/}}, {\it{n\/}} $-\;1$, {\it{lst1\/}}, {\it{lst2\/}})\index{strncmp-j}$\;${\bf  endif}\- \\ 
{\bf else }{\rm{fix}}\,({\it{i\/}})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{strncmp-sk} \\  
\=\+{\rm{strncmp-sk}}\,({\it{n\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strncmp-sk} \\ 
$\leftrightarrow$$\;\;\;\;$$\exists\;${\it{j\/}}$\;$(\=\+$\forall\;${\it{i\/}}$\;$(({\it{i\/}} $<$ {\it{j\/}}) $\rightarrow$ ({\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{i\/}}, {\it{lst2\/}})\index{get-nth}))\index{forall} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{strncmp}}\,({\it{n\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strncmp} \\ 
$=$$\;\;\;\;${\rm{idifference}}\,({\rm{get-nth}}\,({\it{j\/}}, {\it{lst1\/}})\index{get-nth}, {\rm{get-nth}}\,({\it{j\/}}, {\it{lst2\/}})\index{get-nth})\index{idifference})\-)\-\index{exists}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strncmp-j-1 \\ \index{strncmp-j-1}
\=\+(({\it{i\/}} $<$ {\rm{strncmp-j}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strncmp-j}) $\wedge$ ({\it{i1\/}} $\leq$ {\it{i\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{i\/}}, {\it{lst2\/}})\index{get-nth})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strncmp-j-2 \\ \index{strncmp-j-2}
\=\+({\rm{strncmp1}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strncmp1} $\not=$ {\tt{0}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{strncmp1}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strncmp1} \\ 
$=$$\;\;\;\;${\rm{idifference}}\,(\=\+{\rm{get-nth}}\,({\rm{strncmp-j}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strncmp-j}, {\it{lst1\/}})\index{get-nth}, \\ 
{\rm{get-nth}}\,({\rm{strncmp-j}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strncmp-j}, {\it{lst2\/}})\index{get-nth})\-\index{idifference})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strncmp-thm2 \\ \index{strncmp-thm2}
({\rm{strncmp}}\,({\it{n\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strncmp} $\not=$ {\tt{0}}) $\rightarrow$ {\rm{strncmp-sk}}\,({\it{n\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strncmp-sk}
\end{tabbing}


\noindent{\sc Event}:   Disable strncmp-j-1.

\addvspace{18pt}

\noindent{\sc Event}:   Disable strncmp-j-2.

\addvspace{18pt}

\begin{verbatim}; some properties about strpbrk.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strpbrk-thm1 \\ \index{strpbrk-thm1}
\=\+{\bf let }\=\+{\it{j\/}}{\bf $\;$ be$\;\;$}{\rm{strpbrk}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk}\- \\ 
{\bf in} \\ 
{\it{j\/}} $\rightarrow$ {\rm{strchr1}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{j\/}}, {\it{lst1\/}})\index{get-nth})\index{strchr1}$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strpbrk-thm2 \\ \index{strpbrk-thm2}
\=\+(({\it{i1\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $<$ {\rm{strpbrk}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk})) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{strchr1}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{j\/}}, {\it{lst1\/}})\index{get-nth})\index{strchr1})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strpbrk-thm3 \\ \index{strpbrk-thm3}
\=\+(\=\+($\neg$ {\rm{strpbrk}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strpbrk}) \\ 
$\wedge$$\;\;\;\;$({\it{i1\/}} $\leq$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ {\rm{strlen}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}})\index{strlen}))\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{strchr1}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{j\/}}, {\it{lst1\/}})\index{get-nth})\index{strchr1})\-
\end{tabbing}

\begin{verbatim}; strchr1, which is used to specify several string functions, is a variant 
; of strchr.  strchr1 does not have the `thm4' of strchr.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strchr1-thm1 \\ \index{strchr1-thm1}
{\rm{strchr1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr1} $\rightarrow$ ({\rm{get-nth}}\,({\rm{strchr1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr1}, {\it{lst\/}})\index{get-nth} $=$ {\it{ch\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strchr1-thm2 \\ \index{strchr1-thm2}
(({\it{i\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $<$ {\rm{strchr1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr1})) $\rightarrow$ ({\rm{get-nth}}\,({\it{j\/}}, {\it{lst\/}})\index{get-nth} $\not=$ {\it{ch\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strchr1-thm3 \\ \index{strchr1-thm3}
\=\+(($\neg$ {\rm{strchr1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr1}) $\wedge$ ({\it{i\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $<$ {\rm{strlen}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{strlen})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{get-nth}}\,({\it{j\/}}, {\it{lst\/}})\index{get-nth} $\not=$ {\it{ch\/}})\-
\end{tabbing}

\begin{verbatim}; some properties of strcspn.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strcspn-thm1 \\ \index{strcspn-thm1}
\=\+{\bf let }\=\+{\it{j\/}}{\bf $\;$ be$\;\;$}{\rm{strcspn}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcspn}\- \\ 
{\bf in} \\ 
{\it{j\/}} $\rightarrow$ {\rm{strchr}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{j\/}}, {\it{lst1\/}})\index{get-nth})\index{strchr}$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strcspn-thm2 \\ \index{strcspn-thm2}
\=\+(({\it{i1\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $<$ {\rm{strcspn}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcspn})) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{strchr}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{j\/}}, {\it{lst1\/}})\index{get-nth})\index{strchr})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strcspn-thm3 \\ \index{strcspn-thm3}
\=\+(\=\+($\neg$ {\rm{strcspn}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcspn}) \\ 
$\wedge$$\;\;\;\;$({\it{i1\/}} $\leq$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ {\rm{strlen}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}})\index{strlen}))\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{strchr}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{j\/}}, {\it{lst1\/}})\index{get-nth})\index{strchr})\-
\end{tabbing}

\begin{verbatim}; some properties of strspn.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strspn-thm1 \\ \index{strspn-thm1}
\=\+{\bf let }\=\+{\it{j\/}}{\bf $\;$ be$\;\;$}{\rm{strspn}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strspn}\- \\ 
{\bf in} \\ 
{\it{j\/}} $\rightarrow$ ($\neg$ {\rm{strchr1}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{j\/}}, {\it{lst1\/}})\index{get-nth})\index{strchr1})$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strspn-thm2 \\ \index{strspn-thm2}
\=\+(({\it{i1\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $<$ {\rm{strspn}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strspn})) \\ 
$\rightarrow$$\;\;\;\;${\rm{strchr1}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{j\/}}, {\it{lst1\/}})\index{get-nth})\index{strchr1}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strspn-thm3 \\ \index{strspn-thm3}
\=\+(\=\+($\neg$ {\rm{strspn}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strspn}) \\ 
$\wedge$$\;\;\;\;$({\it{i1\/}} $\leq$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ {\rm{strlen}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}})\index{strlen}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{strchr1}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}}, {\rm{get-nth}}\,({\it{j\/}}, {\it{lst1\/}})\index{get-nth})\index{strchr1}\-
\end{tabbing}

\begin{verbatim}; a generalized defn for strncmp.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{strncmp2} \\  
\=\+{\rm{strncmp2}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst1\/}}, {\it{j\/}}, {\it{lst2\/}})\index{strncmp2} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{j\/}}, {\it{lst2\/}})\index{get-nth} \\ 
{\bf then }\=\+{\bf if }{\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\tt{0}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\rm{strncmp2}}\,($1\;+$ {\it{i\/}}, {\it{n\/}} $-\;1$, {\it{lst1\/}}, $1\;+$ {\it{j\/}}, {\it{lst2\/}})\index{strncmp2}$\;${\bf  endif}\- \\ 
{\bf else }{\rm{idifference}}\,({\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth}, {\rm{get-nth}}\,({\it{j\/}}, {\it{lst2\/}})\index{get-nth})\index{idifference}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strncmp2-non-numberp \\ \index{strncmp2-non-numberp}
({\it{i\/}} $\not\in\;${\bf{N}}${}$) $\rightarrow$ ({\rm{strncmp2}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst1\/}}, {\it{j\/}}, {\it{lst2\/}})\index{strncmp2} $=$ {\rm{strncmp2}}\,({\tt{0}}, {\it{n\/}}, {\it{lst1\/}}, {\it{j\/}}, {\it{lst2\/}})\index{strncmp2})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strncmp2-0 \\ \index{strncmp2-0}
{\rm{strncmp2}}\,({\it{i\/}}, {\tt{0}}, {\it{lst1\/}}, {\it{j\/}}, {\it{lst2\/}})\index{strncmp2} $=$ {\tt{0}}
\end{tabbing}
                 
\begin{tabbing}{\sc Theorem}:  strncmp1-strncmp2 \\ \index{strncmp1-strncmp2}
({\it{n\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ ({\rm{strncmp1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strncmp1} $=$ {\rm{strncmp2}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst1\/}}, {\it{i\/}}, {\it{lst2\/}})\index{strncmp2})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strncmp-strncmp2 \\ \index{strncmp-strncmp2}
{\rm{strncmp}}\,({\it{n\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strncmp} $=$ {\rm{strncmp2}}\,({\tt{0}}, {\it{n\/}}, {\it{lst1\/}}, {\tt{0}}, {\it{lst2\/}})\index{strncmp2}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strncmp2-mcdr-1 \\ \index{strncmp2-mcdr-1}
{\rm{strncmp2}}\,({\it{i1\/}}, {\it{n\/}}, {\rm{mcdr}}\,({\it{j\/}}, {\it{lst1\/}})\index{mcdr}, {\it{i2\/}}, {\it{lst2\/}})\index{strncmp2} $=$ {\rm{strncmp2}}\,({\it{i1\/}} $+$ {\it{j\/}}, {\it{n\/}}, {\it{lst1\/}}, {\it{i2\/}}, {\it{lst2\/}})\index{strncmp2}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strncmp2-mcdr-2 \\ \index{strncmp2-mcdr-2}
{\rm{strncmp2}}\,({\it{i1\/}}, {\it{n\/}}, {\it{lst1\/}}, {\it{i2\/}}, {\rm{mcdr}}\,({\it{j\/}}, {\it{lst2\/}})\index{mcdr})\index{strncmp2} $=$ {\rm{strncmp2}}\,({\it{i1\/}}, {\it{n\/}}, {\it{lst1\/}}, {\it{i2\/}} $+$ {\it{j\/}}, {\it{lst2\/}})\index{strncmp2}
\end{tabbing}

\begin{verbatim}; a lemma of strlen and mcdr.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strlen-cdr \\ \index{strlen-cdr}
({\it{i\/}} $\in\;${\bf{N}}${}$) $\rightarrow$ ({\rm{strlen}}\,({\it{i\/}}, {\it{n\/}} $-\;1$, {\rm{mcdr}}\,({\tt{1}}, {\it{lst\/}})\index{mcdr})\index{strlen} $=$ ({\rm{strlen}}\,($1\;+$ {\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{strlen} $-\;1$))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strlen-mcdr \\ \index{strlen-mcdr}
\=\+({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\rightarrow$$\;\;\;\;$({\rm{strlen}}\,({\it{i\/}}, {\it{n\/}}, {\rm{mcdr}}\,({\it{k\/}}, {\it{lst\/}})\index{mcdr})\index{strlen} $=$ ({\rm{strlen}}\,({\it{i\/}} $+$ {\it{k\/}}, {\it{k\/}} $+$ {\it{n\/}}, {\it{lst\/}})\index{strlen} $-$ {\it{k\/}}))\-
\end{tabbing}

\begin{verbatim}; some properties of strstr.
; a lemma for strstr-thm1.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strstr1-thm1 \\ \index{strstr1-thm1}
\=\+{\bf let }\=\+{\it{j\/}}{\bf $\;$ be$\;\;$}{\rm{strstr1}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr1}\- \\ 
{\bf in} \\ 
\=\+(({\it{j\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{n\/}} $=$ ($1\;+$ {\it{len\/}}))) \\ 
$\rightarrow$$\;\;\;\;$({\rm{strncmp2}}\,({\it{j\/}}, {\it{n\/}}, {\it{lst1\/}}, {\tt{0}}, {\it{lst2\/}})\index{strncmp2} $=$ {\tt{0}})\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim}; all 0 <= i < (strlen lst2), lst1[j+i] == lst2[i], if strstr == j =\= 0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strstr-thm1 \\ \index{strstr-thm1}
\=\+{\bf let }\=\+{\it{j\/}}{\bf $\;$ be$\;\;$}{\rm{strstr}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr}\- \\ 
{\bf in} \\ 
({\it{j\/}} $\in\;${\bf{N}}${}$) $\rightarrow$ ({\rm{strncmp}}\,({\rm{strlen}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}})\index{strlen}, {\rm{mcdr}}\,({\it{j\/}}, {\it{lst1\/}})\index{mcdr}, {\it{lst2\/}})\index{strncmp} $=$ {\tt{0}})$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim}; a few lemmas about strchr1.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strchr1-nth \\ \index{strchr1-nth}
\=\+(({\it{i\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $<$ {\rm{strlen}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{strlen})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{strchr1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\rm{get-nth}}\,({\it{j\/}}, {\it{lst\/}})\index{get-nth})\index{strchr1} $\in\;${\bf{N}}${}$)\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strlen-strchr1-nth \\ \index{strlen-strchr1-nth}
\=\+(({\it{i\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $<$ {\rm{strlen}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{strlen})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{strlen}}\,($1\;+$ {\rm{strchr1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\rm{get-nth}}\,({\it{j\/}}, {\it{lst\/}})\index{get-nth})\index{strchr1}, {\it{n\/}}, {\it{lst\/}})\index{strlen} \\ 
$=$$\;\;\;\;${\rm{strlen}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{strlen})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strlen-strchr1 \\ \index{strlen-strchr1}
({\rm{strchr1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\tt{0}})\index{strchr1} $\in\;${\bf{N}}${}$) $\rightarrow$ ({\rm{strchr1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\tt{0}})\index{strchr1} $\not<$ {\rm{strlen}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{strlen})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strchr1-ch0 \\ \index{strchr1-ch0}
$\neg$ {\rm{strchr1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\tt{0}})\index{strchr1}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strchr1-nth-first \\ \index{strchr1-nth-first}
\=\+(({\rm{strchr1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\rm{get-nth}}\,({\it{j\/}}, {\it{lst\/}})\index{get-nth})\index{strchr1} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{i\/}} $\leq$ {\it{j\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\it{j\/}} $\not<$ {\rm{strchr1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\rm{get-nth}}\,({\it{j\/}}, {\it{lst\/}})\index{get-nth})\index{strchr1})\-
\end{tabbing}

\begin{verbatim}; a lemma for strstr-thm2.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strstr1-thm2 \\ \index{strstr1-thm2}
\=\+(\=\+{\rm{lst-of-chrp}}\,({\it{lst1\/}})\index{lst-of-chrp} \\ 
$\wedge$$\;\;\;\;${\rm{lst-of-chrp}}\,({\it{lst2\/}})\index{lst-of-chrp} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\leq$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ {\rm{strstr1}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr1}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $=$ ($1\;+$ {\it{len\/}})))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{strncmp2}}\,({\it{j\/}}, {\it{n\/}}, {\it{lst1\/}}, {\tt{0}}, {\it{lst2\/}})\index{strncmp2} $\not=$ {\tt{0}})\-
\end{tabbing}

\begin{verbatim}; all j < (strstr lst1 lst2), (strncmp (mcdr j lst1) lst2) =\= 0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strstr-thm2 \\ \index{strstr-thm2}
\=\+(\=\+{\rm{lst-of-chrp}}\,({\it{lst1\/}})\index{lst-of-chrp} \\ 
$\wedge$$\;\;\;\;${\rm{lst-of-chrp}}\,({\it{lst2\/}})\index{lst-of-chrp} \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ {\rm{strstr}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr}) \\ 
$\wedge$$\;\;\;\;$({\it{n2\/}} $\not\simeq {\tt{0}}$))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{strncmp}}\,({\rm{strlen}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}})\index{strlen}, {\rm{mcdr}}\,({\it{j\/}}, {\it{lst1\/}})\index{mcdr}, {\it{lst2\/}})\index{strncmp} $\not=$ {\tt{0}})\-
\end{tabbing}

\begin{verbatim}; a lemma for strstr-thm3.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strstr1-thm3 \\ \index{strstr1-thm3}
\=\+(\=\+{\rm{lst-of-chrp}}\,({\it{lst1\/}})\index{lst-of-chrp} \\ 
$\wedge$$\;\;\;\;${\rm{lst-of-chrp}}\,({\it{lst2\/}})\index{lst-of-chrp} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{strstr1}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}}, {\it{len\/}})\index{strstr1}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\leq$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ {\rm{strlen}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}})\index{strlen}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $=$ ($1\;+$ {\it{len\/}})))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{strncmp2}}\,({\it{j\/}}, {\it{n\/}}, {\it{lst1\/}}, {\tt{0}}, {\it{lst2\/}})\index{strncmp2} $\not=$ {\tt{0}})\-
\end{tabbing}

\begin{verbatim}; all j < (strlen lst1), (strncmp (mcdr j lst1) lst2) =\= 0. 
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strstr-thm3 \\ \index{strstr-thm3}
\=\+(\=\+{\rm{lst-of-chrp}}\,({\it{lst1\/}})\index{lst-of-chrp} \\ 
$\wedge$$\;\;\;\;${\rm{lst-of-chrp}}\,({\it{lst2\/}})\index{lst-of-chrp} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{strstr}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strstr}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ {\rm{strlen}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}})\index{strlen}) \\ 
$\wedge$$\;\;\;\;$({\it{n2\/}} $\not\simeq {\tt{0}}$))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{strncmp}}\,({\rm{strlen}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}})\index{strlen}, {\rm{mcdr}}\,({\it{j\/}}, {\it{lst1\/}})\index{mcdr}, {\it{lst2\/}})\index{strncmp} $\not=$ {\tt{0}})\-
\end{tabbing}

\begin{verbatim}; some properties of strtok.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strtok-thm1 \\ \index{strtok-thm1}
\=\+{\bf let }\=\+{\it{i\/}}{\bf $\;$ be$\;\;$}{\rm{strspn}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strspn}\- \\ 
{\bf in} \\ 
\=\+(({\rm{nat-to-uint}}\,({\it{s1\/}})\index{nat-to-uint} $\not=$ {\tt{0}}) $\wedge$ ({\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $=$ {\tt{0}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{strtok-tok}}\,({\it{s1\/}}, {\it{last\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-tok} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{strtok-last}}\,({\it{s1\/}}, {\it{last\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-last} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{strtok-lst}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-lst} $=$ {\it{lst1\/}}))\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strtok-thm2 \\ \index{strtok-thm2}
\=\+{\bf let }\=\+{\it{i\/}}{\bf $\;$ be$\;\;$}{\rm{strspn}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strspn}\- \\ 
{\bf in} \\ 
\=\+(\=\+({\rm{nat-to-uint}}\,({\it{s1\/}})\index{nat-to-uint} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\rm{strcspn}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcspn}, {\it{lst1\/}})\index{get-nth} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{stringp}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}})\index{stringp} \\ 
$\wedge$$\;\;\;\;$({\it{n1\/}} $\in\;${\bf{N}}${}$))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+{\rm{strtok-tok}}\,({\it{s1\/}}, {\it{last\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-tok} \\ 
$=$$\;\;\;\;${\rm{add}}\,({\tt{32}}, {\it{s1\/}}, {\rm{strspn*}}\,({\tt{0}}, {\tt{0}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strspn*})\index{add})\- \\ 
$\wedge$$\;\;\;\;$({\rm{strtok-last}}\,({\it{s1\/}}, {\it{last\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-last} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{strtok-lst}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-lst} $=$ {\it{lst1\/}}))\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strspn-strchr1 \\ \index{strspn-strchr1}
\=\+{\rm{strspn}}\,({\it{i1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strspn} \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{strchr1}}\,({\tt{0}}, {\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{strchr1})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strchr-strchr1 \\ \index{strchr-strchr1}
({\it{ch\/}} $\not=$ {\tt{0}}) $\rightarrow$ ({\rm{strchr}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr} $=$ {\rm{strchr1}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{ch\/}})\index{strchr1})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strspn-true \\ \index{strspn-true}
({\rm{stringp}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}})\index{stringp} $\wedge$ {\rm{stringp}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}})\index{stringp}) $\rightarrow$ {\rm{strspn}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strspn}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strtok-thm3 \\ \index{strtok-thm3}
\=\+{\bf let }\=\+{\it{i*\/}}{\bf $\;$ be$\;\;$}{\rm{strspn*}}\,({\tt{0}}, {\tt{0}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strspn*}, \\ 
{\it{i\/}}{\bf $\;$ be$\;\;$}{\rm{strspn}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strspn}\- \\ 
{\bf in} \\ 
\=\+(\=\+({\rm{nat-to-uint}}\,({\it{s1\/}})\index{nat-to-uint} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\rm{strcspn}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcspn}, {\it{lst1\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{stringp}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}})\index{stringp} \\ 
$\wedge$$\;\;\;\;${\rm{stringp}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}})\index{stringp} \\ 
$\wedge$$\;\;\;\;$({\it{n1\/}} $\in\;${\bf{N}}${}$))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+{\rm{strtok-tok}}\,({\it{s1\/}}, {\it{last\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-tok} \\ 
$=$$\;\;\;\;${\rm{add}}\,({\tt{32}}, {\it{s1\/}}, {\rm{strspn*}}\,({\tt{0}}, {\tt{0}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strspn*})\index{add})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{strtok-last}}\,({\it{s1\/}}, {\it{last\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-last} \\ 
$=$$\;\;\;\;${\rm{add}}\,(\=\+{\tt{32}}, \\ 
{\it{s1\/}}, \\ 
{\rm{add}}\,({\tt{32}}, {\rm{strcspn*}}\,({\it{i*\/}}, {\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcspn*}, {\tt{1}})\index{add})\-\index{add})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{get-nth}}\,(\=\+{\rm{strcspn}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcspn}, \\ 
{\rm{strtok-lst}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-lst})\-\index{get-nth} \\ 
$=$$\;\;\;\;${\tt{0}})\-)\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strtok-thm4 \\ \index{strtok-thm4}
\=\+({\rm{strtok-tok}}\,({\tt{0}}, {\tt{0}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-tok} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{strtok-last}}\,({\tt{0}}, {\tt{0}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-last} $=$ {\tt{0}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strtok-thm5 \\ \index{strtok-thm5}
\=\+{\bf let }\=\+{\it{i\/}}{\bf $\;$ be$\;\;$}{\rm{strspn}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strspn}\- \\ 
{\bf in} \\ 
\=\+(\=\+({\rm{nat-to-uint}}\,({\it{last\/}})\index{nat-to-uint} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\rm{strcspn}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcspn}, {\it{lst1\/}})\index{get-nth} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{stringp}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}})\index{stringp} \\ 
$\wedge$$\;\;\;\;$({\it{n1\/}} $\in\;${\bf{N}}${}$))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+{\rm{strtok-tok}}\,({\tt{0}}, {\it{last\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-tok} \\ 
$=$$\;\;\;\;${\rm{add}}\,({\tt{32}}, {\it{last\/}}, {\rm{strspn*}}\,({\tt{0}}, {\tt{0}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strspn*})\index{add})\- \\ 
$\wedge$$\;\;\;\;$({\rm{strtok-last}}\,({\tt{0}}, {\it{last\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-last} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{strtok-lst}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-lst} $=$ {\it{lst1\/}}))\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strtok-thm6 \\ \index{strtok-thm6}
\=\+{\bf let }\=\+{\it{i*\/}}{\bf $\;$ be$\;\;$}{\rm{strspn*}}\,({\tt{0}}, {\tt{0}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strspn*}, \\ 
{\it{i\/}}{\bf $\;$ be$\;\;$}{\rm{strspn}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strspn}\- \\ 
{\bf in} \\ 
\=\+(\=\+({\rm{nat-to-uint}}\,({\it{last\/}})\index{nat-to-uint} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\it{i\/}}, {\it{lst1\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{get-nth}}\,({\rm{strcspn}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcspn}, {\it{lst1\/}})\index{get-nth} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{stringp}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}})\index{stringp} \\ 
$\wedge$$\;\;\;\;${\rm{stringp}}\,({\tt{0}}, {\it{n2\/}}, {\it{lst2\/}})\index{stringp} \\ 
$\wedge$$\;\;\;\;$({\it{n1\/}} $\in\;${\bf{N}}${}$))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+{\rm{strtok-tok}}\,({\tt{0}}, {\it{last\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-tok} \\ 
$=$$\;\;\;\;${\rm{add}}\,({\tt{32}}, {\it{last\/}}, {\rm{strspn*}}\,({\tt{0}}, {\tt{0}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strspn*})\index{add})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{strtok-last}}\,({\tt{0}}, {\it{last\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-last} \\ 
$=$$\;\;\;\;${\rm{add}}\,(\=\+{\tt{32}}, \\ 
{\it{last\/}}, \\ 
{\rm{add}}\,({\tt{32}}, {\rm{strcspn*}}\,({\it{i*\/}}, {\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcspn*}, {\tt{1}})\index{add})\-\index{add})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{get-nth}}\,(\=\+{\rm{strcspn}}\,({\it{i\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcspn}, \\ 
{\rm{strtok-lst}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strtok-lst})\-\index{get-nth} \\ 
$=$$\;\;\;\;${\tt{0}})\-)\-\-$\;${\bf  endlet}\-
\end{tabbing}


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

\addvspace{18pt}

\begin{verbatim}; some properties of memmove.
; memmove is equivalent to lstmov.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  mmov1-lst-cpy \\ \index{mmov1-lst-cpy}
{\rm{mmov1-lst}}\,({\it{i\/}}, {\it{lst1\/}}, {\it{lst2\/}}, {\it{n\/}})\index{mmov1-lst} $=$ {\rm{lstcpy}}\,({\it{i\/}}, {\it{lst1\/}}, {\it{i\/}}, {\it{lst2\/}}, {\it{n\/}})\index{lstcpy}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mmovn-mmov1-lst \\ \index{mmovn-mmov1-lst}
{\rm{mmovn-lst}}\,({\it{h\/}}, {\it{lst1\/}}, {\it{lst2\/}}, {\it{i\/}}, {\it{n\/}})\index{mmovn-lst} $=$ {\rm{mmov1-lst}}\,({\it{i\/}}, {\it{lst1\/}}, {\it{lst2\/}}, {\it{h\/}} $*$ {\it{n\/}})\index{mmov1-lst}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lstcpy-nonnumberp \\ \index{lstcpy-nonnumberp}
\=\+({\it{i1\/}} $\not\in\;${\bf{N}}${}$) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{lstcpy}}\,({\it{i1\/}}, {\it{lst1\/}}, {\it{i2\/}}, {\it{lst2\/}}, {\it{n\/}})\index{lstcpy} $=$ {\rm{lstcpy}}\,({\tt{0}}, {\it{lst1\/}}, {\it{i2\/}}, {\it{lst2\/}}, {\it{n\/}})\index{lstcpy}) \\ 
$\wedge$$\;\;\;\;$({\rm{lstcpy}}\,({\it{i2\/}}, {\it{lst1\/}}, {\it{i1\/}}, {\it{lst2\/}}, {\it{n\/}})\index{lstcpy} $=$ {\rm{lstcpy}}\,({\it{i2\/}}, {\it{lst1\/}}, {\tt{0}}, {\it{lst2\/}}, {\it{n\/}})\index{lstcpy}))\-\-
\end{tabbing}
             
\begin{tabbing}{\sc Theorem}:  lstcpy-lstcpy-0 \\ \index{lstcpy-lstcpy-0}
\=\+{\rm{lstcpy}}\,({\it{h1\/}}, {\rm{lstcpy}}\,({\tt{0}}, {\it{lst1\/}}, {\tt{0}}, {\it{lst2\/}}, {\it{h1\/}})\index{lstcpy}, {\it{h1\/}}, {\it{lst2\/}}, {\it{h2\/}})\index{lstcpy} \\ 
$=$$\;\;\;\;${\rm{lstcpy}}\,({\tt{0}}, {\it{lst1\/}}, {\tt{0}}, {\it{lst2\/}}, {\it{h1\/}} $+$ {\it{h2\/}})\index{lstcpy}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mmov1-lst1-cpy \\ \index{mmov1-lst1-cpy}
\=\+({\it{n\/}} $\leq$ {\it{i\/}}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{mmov1-lst1}}\,({\it{i\/}}, {\it{lst1\/}}, {\it{lst2\/}}, {\it{n\/}})\index{mmov1-lst1} $=$ {\rm{lstcpy}}\,({\it{i\/}} $-$ {\it{n\/}}, {\it{lst1\/}}, {\it{i\/}} $-$ {\it{n\/}}, {\it{lst2\/}}, {\it{n\/}})\index{lstcpy})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lstcpy-lstcpy-1 \\ \index{lstcpy-lstcpy-1}
\=\+(({\it{j1\/}} $=$ ({\it{h1\/}} $+$ {\it{i1\/}})) $\wedge$ ({\it{j2\/}} $=$ ({\it{h1\/}} $+$ {\it{i2\/}}))) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{lstcpy}}\,({\it{i1\/}}, {\rm{lstcpy}}\,({\it{j1\/}}, {\it{lst1\/}}, {\it{j2\/}}, {\it{lst2\/}}, {\it{h2\/}})\index{lstcpy}, {\it{i2\/}}, {\it{lst2\/}}, {\it{h1\/}})\index{lstcpy} \\ 
$=$$\;\;\;\;${\rm{lstcpy}}\,({\it{i1\/}}, {\it{lst1\/}}, {\it{i2\/}}, {\it{lst2\/}}, {\it{h1\/}} $+$ {\it{h2\/}})\index{lstcpy})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  times-lessp-dual \\ \index{times-lessp-dual}
({\it{x\/}} $<$ {\it{y\/}}) $\rightarrow$ (({\it{x\/}} $<$ ({\it{y\/}} $*$ {\it{z\/}})) $=$ ({\it{z\/}} $\not\simeq {\tt{0}}$))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mmovn-lst1-mmov1-lst \\ \index{mmovn-lst1-mmov1-lst}
\=\+(({\it{h\/}} $*$ {\it{n\/}}) $\leq$ {\it{i\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{mmovn-lst1}}\,({\it{h\/}}, {\it{lst1\/}}, {\it{lst2\/}}, {\it{i\/}}, {\it{n\/}})\index{mmovn-lst1} \\ 
$=$$\;\;\;\;${\rm{mmov1-lst}}\,({\it{i\/}} $-$ ({\it{h\/}} $*$ {\it{n\/}}), {\it{lst1\/}}, {\it{lst2\/}}, {\it{h\/}} $*$ {\it{n\/}})\index{mmov1-lst})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-shrink-fast-1 \\ \index{quotient-shrink-fast-1}
({\it{x\/}} $<$ ({\it{y\/}} $*$ ({\it{x\/}} $\div$ {\it{y\/}}))) $=$ {\bf{f}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  memmove-mmov1-lst \\ \index{memmove-mmov1-lst}
\=\+{\rm{memmove}}\,({\it{str1\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{memmove} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\it{lst1\/}} \\ 
{\bf elseif }{\rm{nat-to-uint}}\,({\it{str1\/}})\index{nat-to-uint} $=$ {\rm{nat-to-uint}}\,({\it{str2\/}})\index{nat-to-uint}$\;\;${\bf then }{\it{lst2\/}} \\ 
{\bf else }{\rm{mmov1-lst}}\,({\tt{0}}, {\it{lst1\/}}, {\it{lst2\/}}, {\it{n\/}})\index{mmov1-lst}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; for k < i, lstcpy(lst1,lst2)[k] == lst1[k].
\end{verbatim}\begin{tabbing}{\sc Theorem}:  lstcpy-get-1 \\ \index{lstcpy-get-1}
({\it{k\/}} $<$ {\it{i\/}}) $\rightarrow$ ({\rm{get-nth}}\,({\it{k\/}}, {\rm{lstcpy}}\,({\it{i\/}}, {\it{lst1\/}}, {\it{j\/}}, {\it{lst2\/}}, {\it{n\/}})\index{lstcpy})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{k\/}}, {\it{lst1\/}})\index{get-nth})
\end{tabbing}

\begin{verbatim}; for i <= i1 < i+n, lstcpy(lst1,lst2)[i1] == lst2[i1].
\end{verbatim}\begin{tabbing}{\sc Theorem}:  lstcpy-get-2 \\ \index{lstcpy-get-2}
\=\+(({\it{i\/}} $\leq$ {\it{i1\/}}) $\wedge$ ({\it{i1\/}} $<$ ({\it{i\/}} $+$ {\it{n\/}}))) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{get-nth}}\,({\it{i1\/}}, {\rm{lstcpy}}\,({\it{i\/}}, {\it{lst1\/}}, {\it{j\/}}, {\it{lst2\/}}, {\it{n\/}})\index{lstcpy})\index{get-nth} \\ 
$=$$\;\;\;\;${\rm{get-nth}}\,(({\it{j\/}} $+$ {\it{i1\/}}) $-$ {\it{i\/}}, {\it{lst2\/}})\index{get-nth})\-\-
\end{tabbing}

\begin{verbatim}; for 0 <= i < n, mmov1-lst(lst1,lst2)[i] == lst2[i].
\end{verbatim}\begin{tabbing}{\sc Theorem}:  mmov1-lst-thm1 \\ \index{mmov1-lst-thm1}
({\it{i1\/}} $<$ {\it{n\/}}) $\rightarrow$ ({\rm{get-nth}}\,({\it{i1\/}}, {\rm{mmov1-lst}}\,({\tt{0}}, {\it{lst1\/}}, {\it{lst2\/}}, {\it{n\/}})\index{mmov1-lst})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{i1\/}}, {\it{lst2\/}})\index{get-nth})
\end{tabbing}

\begin{verbatim}; for 0 <= i < n, memmove(lst1,lst2,n)[i] == lst2[i].
\end{verbatim}\begin{tabbing}{\sc Theorem}:  memmove-thm1 \\ \index{memmove-thm1}
\=\+({\it{i\/}} $<$ {\it{n\/}}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{get-nth}}\,({\it{i\/}}, {\rm{memmove}}\,({\it{str1\/}}, {\it{str2\/}}, {\it{n\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{memmove})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{i\/}}, {\it{lst2\/}})\index{get-nth})\-
\end{tabbing}


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