\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 J Strother Moore.  All Rights Reserved.

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

 NO WARRANTY

 J Strother Moore 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 J Strother Moore 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 initial {\bf nqthm} theory.

\addvspace{18pt}

\noindent{\sc Event}:   For efficiency, compile those definitions not yet compiled.

\addvspace{18pt}

\noindent{\sc Event}:   Add the shell {\it{zn\/}}\index{zn}, with recognizer function symbol {\it{znp\/}} and 2 accessors: {\it{pos\/}}, with type restriction (one-of numberp) and default value zero; {\it{neg\/}}, with type restriction (one-of numberp) and default value zero.

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{zlessp} \\  
{\rm{zlessp}}\,({\it{x\/}}, {\it{y\/}})\index{zlessp} $=$ (({\rm{pos}}\,({\it{x\/}})\index{pos} $+$ {\rm{neg}}\,({\it{y\/}})\index{neg}) $<$ ({\rm{neg}}\,({\it{x\/}})\index{neg} $+$ {\rm{pos}}\,({\it{y\/}})\index{pos}))
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{zlesseqp}$\;\;$
{\rm{zlesseqp}}\,({\it{x\/}}, {\it{y\/}})\index{zlesseqp} $=$ ($\neg$ {\rm{zlessp}}\,({\it{y\/}}, {\it{x\/}})\index{zlessp})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{zmax} \\  
\=\+{\rm{zmax}}\,({\it{x\/}}, {\it{y\/}})\index{zmax} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{zlessp}}\,({\it{x\/}}, {\it{y\/}})\index{zlessp}$\;\;${\bf then }{\it{y\/}} \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{zmin} \\  
\=\+{\rm{zmin}}\,({\it{x\/}}, {\it{y\/}})\index{zmin} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{zlessp}}\,({\it{x\/}}, {\it{y\/}})\index{zlessp}$\;\;${\bf then }{\it{x\/}} \\ 
{\bf else }{\it{y\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{zsub1}$\;\;$
{\rm{zsub1}}\,({\it{x\/}})\index{zsub1} $=$ {\rm{zn}}\,({\rm{pos}}\,({\it{x\/}})\index{pos}, $1\;+$ {\rm{neg}}\,({\it{x\/}})\index{neg})\index{zn}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{pzdifference} \\  
{\rm{pzdifference}}\,({\it{x\/}}, {\it{y\/}})\index{pzdifference} $=$ (({\rm{pos}}\,({\it{x\/}})\index{pos} $+$ {\rm{neg}}\,({\it{y\/}})\index{neg}) $-$ ({\rm{neg}}\,({\it{x\/}})\index{neg} $+$ {\rm{pos}}\,({\it{y\/}})\index{pos}))
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{m1} \\  
\=\+{\rm{m1}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{m1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{zlesseqp}}\,({\it{x\/}}, {\it{y\/}})\index{zlesseqp}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\tt{1}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{m2} \\  
{\rm{m2}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{m2} $=$ {\rm{pzdifference}}\,({\rm{zmax}}\,({\it{x\/}}, {\rm{zmax}}\,({\it{y\/}}, {\it{z\/}})\index{zmax})\index{zmax}, {\rm{zmin}}\,({\it{x\/}}, {\rm{zmin}}\,({\it{y\/}}, {\it{z\/}})\index{zmin})\index{zmin})\index{pzdifference}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{m3}$\;\;$
{\rm{m3}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{m3} $=$ {\rm{pzdifference}}\,({\it{x\/}}, {\rm{zmin}}\,({\it{x\/}}, {\rm{zmin}}\,({\it{y\/}}, {\it{z\/}})\index{zmin})\index{zmin})\index{pzdifference}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{tak0} \\  
\=\+{\rm{tak0}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{tak0} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{zlesseqp}}\,({\it{x\/}}, {\it{y\/}})\index{zlesseqp}$\;\;${\bf then }{\it{y\/}} \\ 
{\bf elseif }{\rm{zlesseqp}}\,({\it{y\/}}, {\it{z\/}})\index{zlesseqp}$\;\;${\bf then }{\it{z\/}} \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{m} \\  
{\rm{m}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{m} $=$ {\rm{cons}}\,({\rm{m1}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{m1}, {\rm{cons}}\,({\rm{m2}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{m2}, {\rm{cons}}\,({\rm{m3}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{m3}, {\bf{nil}})))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  tak0-satisfies-tak-equation \\ \index{tak0-satisfies-tak-equation}
\=\+{\rm{tak0}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{tak0} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{zlesseqp}}\,({\it{x\/}}, {\it{y\/}})\index{zlesseqp}$\;\;${\bf then }{\it{y\/}} \\ 
{\bf else }{\rm{tak0}}\,(\=\+{\rm{tak0}}\,({\rm{zsub1}}\,({\it{x\/}})\index{zsub1}, {\it{y\/}}, {\it{z\/}})\index{tak0}, \\ 
{\rm{tak0}}\,({\rm{zsub1}}\,({\it{y\/}})\index{zsub1}, {\it{z\/}}, {\it{x\/}})\index{tak0}, \\ 
{\rm{tak0}}\,({\rm{zsub1}}\,({\it{z\/}})\index{zsub1}, {\it{x\/}}, {\it{y\/}})\index{tak0})\-\index{tak0}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  m1-lesseqp-0 \\ \index{m1-lesseqp-0}
\=\+($\neg$ {\rm{zlesseqp}}\,({\it{x\/}}, {\it{y\/}})\index{zlesseqp}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{m1}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{m1} \\ 
$\not<$$\;\;\;\;${\rm{m1}}\,({\rm{tak0}}\,({\rm{zsub1}}\,({\it{x\/}})\index{zsub1}, {\it{y\/}}, {\it{z\/}})\index{tak0}, {\rm{tak0}}\,({\rm{zsub1}}\,({\it{y\/}})\index{zsub1}, {\it{z\/}}, {\it{x\/}})\index{tak0}, {\rm{tak0}}\,({\rm{zsub1}}\,({\it{z\/}})\index{zsub1}, {\it{x\/}}, {\it{y\/}})\index{tak0})\index{m1})\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  m1-lesseqp-1 \\ \index{m1-lesseqp-1}
($\neg$ {\rm{zlesseqp}}\,({\it{x\/}}, {\it{y\/}})\index{zlesseqp}) $\rightarrow$ ({\rm{m1}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{m1} $\not<$ {\rm{m1}}\,({\rm{zsub1}}\,({\it{x\/}})\index{zsub1}, {\it{y\/}}, {\it{z\/}})\index{m1})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  m1-lesseqp-2 \\ \index{m1-lesseqp-2}
($\neg$ {\rm{zlesseqp}}\,({\it{x\/}}, {\it{y\/}})\index{zlesseqp}) $\rightarrow$ ({\rm{m1}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{m1} $\not<$ {\rm{m1}}\,({\rm{zsub1}}\,({\it{y\/}})\index{zsub1}, {\it{z\/}}, {\it{x\/}})\index{m1})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  m1-lesseqp-3 \\ \index{m1-lesseqp-3}
($\neg$ {\rm{zlesseqp}}\,({\it{x\/}}, {\it{y\/}})\index{zlesseqp}) $\rightarrow$ ({\rm{m1}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{m1} $\not<$ {\rm{m1}}\,({\rm{zsub1}}\,({\it{z\/}})\index{zsub1}, {\it{x\/}}, {\it{y\/}})\index{m1})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  m2-lesseqp-0 \\ \index{m2-lesseqp-0}
\=\+($\neg$ {\rm{zlesseqp}}\,({\it{x\/}}, {\it{y\/}})\index{zlesseqp}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{m2}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{m2} \\ 
$\not<$$\;\;\;\;${\rm{m2}}\,({\rm{tak0}}\,({\rm{zsub1}}\,({\it{x\/}})\index{zsub1}, {\it{y\/}}, {\it{z\/}})\index{tak0}, {\rm{tak0}}\,({\rm{zsub1}}\,({\it{y\/}})\index{zsub1}, {\it{z\/}}, {\it{x\/}})\index{tak0}, {\rm{tak0}}\,({\rm{zsub1}}\,({\it{z\/}})\index{zsub1}, {\it{x\/}}, {\it{y\/}})\index{tak0})\index{m2})\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  m2-lesseqp-1 \\ \index{m2-lesseqp-1}
($\neg$ {\rm{zlesseqp}}\,({\it{x\/}}, {\it{y\/}})\index{zlesseqp}) $\rightarrow$ ({\rm{m2}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{m2} $\not<$ {\rm{m2}}\,({\rm{zsub1}}\,({\it{x\/}})\index{zsub1}, {\it{y\/}}, {\it{z\/}})\index{m2})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  m2-lesseqp-2 \\ \index{m2-lesseqp-2}
\=\+(($\neg$ {\rm{zlesseqp}}\,({\it{x\/}}, {\it{y\/}})\index{zlesseqp}) $\wedge$ ({\rm{m1}}\,({\rm{zsub1}}\,({\it{y\/}})\index{zsub1}, {\it{z\/}}, {\it{x\/}})\index{m1} $=$ {\rm{m1}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{m1})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{m2}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{m2} $\not<$ {\rm{m2}}\,({\rm{zsub1}}\,({\it{y\/}})\index{zsub1}, {\it{z\/}}, {\it{x\/}})\index{m2})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  m2-lesseqp-3 \\ \index{m2-lesseqp-3}
\=\+(($\neg$ {\rm{zlesseqp}}\,({\it{x\/}}, {\it{y\/}})\index{zlesseqp}) $\wedge$ ({\rm{m1}}\,({\rm{zsub1}}\,({\it{z\/}})\index{zsub1}, {\it{x\/}}, {\it{y\/}})\index{m1} $=$ {\rm{m1}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{m1})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{m2}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{m2} $\not<$ {\rm{m2}}\,({\rm{zsub1}}\,({\it{z\/}})\index{zsub1}, {\it{x\/}}, {\it{y\/}})\index{m2})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  m3-lessp-0 \\ \index{m3-lessp-0}
\=\+(\=\+($\neg$ {\rm{zlesseqp}}\,({\it{x\/}}, {\it{y\/}})\index{zlesseqp}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{m1}}\,({\rm{tak0}}\,({\rm{zsub1}}\,({\it{x\/}})\index{zsub1}, {\it{y\/}}, {\it{z\/}})\index{tak0}, {\rm{tak0}}\,({\rm{zsub1}}\,({\it{y\/}})\index{zsub1}, {\it{z\/}}, {\it{x\/}})\index{tak0}, {\rm{tak0}}\,({\rm{zsub1}}\,({\it{z\/}})\index{zsub1}, {\it{x\/}}, {\it{y\/}})\index{tak0})\index{m1} \\ 
$=$$\;\;\;\;${\rm{m1}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{m1})\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{m3}}\,({\rm{tak0}}\,({\rm{zsub1}}\,({\it{x\/}})\index{zsub1}, {\it{y\/}}, {\it{z\/}})\index{tak0}, {\rm{tak0}}\,({\rm{zsub1}}\,({\it{y\/}})\index{zsub1}, {\it{z\/}}, {\it{x\/}})\index{tak0}, {\rm{tak0}}\,({\rm{zsub1}}\,({\it{z\/}})\index{zsub1}, {\it{x\/}}, {\it{y\/}})\index{tak0})\index{m3} \\ 
$<$$\;\;\;\;${\rm{m3}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{m3})\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  m3-lessp-1 \\ \index{m3-lessp-1}
\=\+(($\neg$ {\rm{zlesseqp}}\,({\it{x\/}}, {\it{y\/}})\index{zlesseqp}) $\wedge$ ({\rm{m1}}\,({\rm{zsub1}}\,({\it{x\/}})\index{zsub1}, {\it{y\/}}, {\it{z\/}})\index{m1} $=$ {\rm{m1}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{m1})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{m3}}\,({\rm{zsub1}}\,({\it{x\/}})\index{zsub1}, {\it{y\/}}, {\it{z\/}})\index{m3} $<$ {\rm{m3}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{m3})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  m3-lessp-2 \\ \index{m3-lessp-2}
\=\+(($\neg$ {\rm{zlesseqp}}\,({\it{x\/}}, {\it{y\/}})\index{zlesseqp}) $\wedge$ ({\rm{m1}}\,({\rm{zsub1}}\,({\it{y\/}})\index{zsub1}, {\it{z\/}}, {\it{x\/}})\index{m1} $=$ {\rm{m1}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{m1})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{m3}}\,({\rm{zsub1}}\,({\it{y\/}})\index{zsub1}, {\it{z\/}}, {\it{x\/}})\index{m3} $<$ {\rm{m3}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{m3})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  m3-lessp-3 \\ \index{m3-lessp-3}
\=\+(($\neg$ {\rm{zlesseqp}}\,({\it{x\/}}, {\it{y\/}})\index{zlesseqp}) $\wedge$ ({\rm{m1}}\,({\rm{zsub1}}\,({\it{z\/}})\index{zsub1}, {\it{x\/}}, {\it{y\/}})\index{m1} $=$ {\rm{m1}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{m1})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{m2}}\,({\rm{zsub1}}\,({\it{z\/}})\index{zsub1}, {\it{x\/}}, {\it{y\/}})\index{m2} $<$ {\rm{m2}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{m2})\-
\end{tabbing}

\noindent{\sc Event}:   Disable zlessp.

\addvspace{18pt}

\noindent{\sc Event}:   Disable m1.

\addvspace{18pt}

\noindent{\sc Event}:   Disable m2.

\addvspace{18pt}

\noindent{\sc Event}:   Disable m3.

\addvspace{18pt}

\noindent{\sc Event}:   Disable tak0.

\addvspace{18pt}

\noindent{\sc Event}:   Disable zsub1.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{make-ordinal3} \\  
\=\+{\rm{make-ordinal3}}\,({\it{x\/}})\index{make-ordinal3} \\ 
$=$$\;\;\;\;${\rm{cons}}\,({\rm{cons}}\,($1\;+$ {\rm{car}}\,({\it{x\/}}), {\tt{0}}), {\rm{cons}}\,($1\;+$ {\rm{cadr}}\,({\it{x\/}}), {\rm{fix}}\,({\rm{caddr}}\,({\it{x\/}}))))\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  ordinalp-make-ordinal3 \\ \index{ordinalp-make-ordinal3}
{\rm{ordinalp}}\,({\rm{make-ordinal3}}\,({\it{x\/}})\index{make-ordinal3})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{lex3} \\  
{\rm{lex3}}\,({\it{x\/}}, {\it{y\/}})\index{lex3} $=$ {\rm{ord-lessp}}\,({\rm{make-ordinal3}}\,({\it{x\/}})\index{make-ordinal3}, {\rm{make-ordinal3}}\,({\it{y\/}})\index{make-ordinal3})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  m-goes-down-1 \\ \index{m-goes-down-1}
($\neg$ {\rm{zlesseqp}}\,({\it{x\/}}, {\it{y\/}})\index{zlesseqp}) $\rightarrow$ {\rm{lex3}}\,({\rm{m}}\,({\rm{zsub1}}\,({\it{x\/}})\index{zsub1}, {\it{y\/}}, {\it{z\/}})\index{m}, {\rm{m}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{m})\index{lex3}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  m-goes-down-2 \\ \index{m-goes-down-2}
($\neg$ {\rm{zlesseqp}}\,({\it{x\/}}, {\it{y\/}})\index{zlesseqp}) $\rightarrow$ {\rm{lex3}}\,({\rm{m}}\,({\rm{zsub1}}\,({\it{y\/}})\index{zsub1}, {\it{z\/}}, {\it{x\/}})\index{m}, {\rm{m}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{m})\index{lex3}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  m-goes-down-3 \\ \index{m-goes-down-3}
($\neg$ {\rm{zlesseqp}}\,({\it{x\/}}, {\it{y\/}})\index{zlesseqp}) $\rightarrow$ {\rm{lex3}}\,({\rm{m}}\,({\rm{zsub1}}\,({\it{z\/}})\index{zsub1}, {\it{x\/}}, {\it{y\/}})\index{m}, {\rm{m}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{m})\index{lex3}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  m-goes-down-0 \\ \index{m-goes-down-0}
\=\+($\neg$ {\rm{zlesseqp}}\,({\it{x\/}}, {\it{y\/}})\index{zlesseqp}) \\ 
$\rightarrow$$\;\;\;\;${\rm{lex3}}\,(\=\+{\rm{m}}\,({\rm{tak0}}\,({\rm{zsub1}}\,({\it{x\/}})\index{zsub1}, {\it{y\/}}, {\it{z\/}})\index{tak0}, {\rm{tak0}}\,({\rm{zsub1}}\,({\it{y\/}})\index{zsub1}, {\it{z\/}}, {\it{x\/}})\index{tak0}, {\rm{tak0}}\,({\rm{zsub1}}\,({\it{z\/}})\index{zsub1}, {\it{x\/}}, {\it{y\/}})\index{tak0})\index{m}, \\ 
{\rm{m}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{m})\-\index{lex3}\-
\end{tabbing}
%\end{list}
\printindex
\end{document}
