\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 Robert S. Boyer and 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

 Robert S. Boyer and J Strother Moore PROVIDE 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 Robert S. Boyer or 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}
\begin{tabbing}{\sc Definition}:\index{logicalp}$\;\;$
{\rm{logicalp}}\,({\it{x\/}})\index{logicalp} $=$ (({\it{x\/}} $=$ {\sc{true}}) $\vee$ ({\it{x\/}} $=$ {\sc{false}}))
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{expt} \\  
\=\+{\rm{expt}}\,({\it{i\/}}, {\it{j\/}})\index{expt} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{j\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\it{i\/}} $*$ {\rm{expt}}\,({\it{i\/}}, {\it{j\/}} $-\;1$)\index{expt}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{znumberp}$\;\;$
{\rm{znumberp}}\,({\it{x\/}})\index{znumberp} $=$ ({\rm{negativep}}\,({\it{x\/}}) $\vee$ ({\it{x\/}} $\in\;${\bf{N}}${}$))
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{zzero}$\;\;$
{\sc{zzero}}\index{zzero} $=$ {\sc{zero}}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{zplus} \\  
\=\+{\rm{zplus}}\,({\it{x\/}}, {\it{y\/}})\index{zplus} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{negativep}}\,({\it{x\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{negativep}}\,({\it{y\/}})$\;\;${\bf then }$-$ ({\rm{negative-guts}}\,({\it{x\/}}) $+$ {\rm{negative-guts}}\,({\it{y\/}})) \\ 
{\bf elseif }{\it{y\/}} $<$ {\rm{negative-guts}}\,({\it{x\/}})$\;\;${\bf then }$-$ ({\rm{negative-guts}}\,({\it{x\/}}) $-$ {\it{y\/}}) \\ 
{\bf else }{\it{y\/}} $-$ {\rm{negative-guts}}\,({\it{x\/}})$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{negativep}}\,({\it{y\/}}) \\ 
{\bf then }\=\+{\bf if }{\it{x\/}} $<$ {\rm{negative-guts}}\,({\it{y\/}})$\;\;${\bf then }$-$ ({\rm{negative-guts}}\,({\it{y\/}}) $-$ {\it{x\/}}) \\ 
{\bf else }{\it{x\/}} $-$ {\rm{negative-guts}}\,({\it{y\/}})$\;${\bf  endif}\- \\ 
{\bf else }{\it{x\/}} $+$ {\it{y\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{zdifference} \\  
\=\+{\rm{zdifference}}\,({\it{x\/}}, {\it{y\/}})\index{zdifference} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{negativep}}\,({\it{x\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{negativep}}\,({\it{y\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{negative-guts}}\,({\it{y\/}}) $<$ {\rm{negative-guts}}\,({\it{x\/}}) \\ 
{\bf then }$-$ ({\rm{negative-guts}}\,({\it{x\/}}) $-$ {\rm{negative-guts}}\,({\it{y\/}})) \\ 
{\bf else }{\rm{negative-guts}}\,({\it{y\/}}) $-$ {\rm{negative-guts}}\,({\it{x\/}})$\;${\bf  endif}\- \\ 
{\bf else }$-$ ({\rm{negative-guts}}\,({\it{x\/}}) $+$ {\it{y\/}})$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{negativep}}\,({\it{y\/}})$\;\;${\bf then }{\it{x\/}} $+$ {\rm{negative-guts}}\,({\it{y\/}}) \\ 
{\bf elseif }{\it{x\/}} $<$ {\it{y\/}}$\;\;${\bf then }$-$ ({\it{y\/}} $-$ {\it{x\/}}) \\ 
{\bf else }{\it{x\/}} $-$ {\it{y\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{ztimes} \\  
\=\+{\rm{ztimes}}\,({\it{x\/}}, {\it{y\/}})\index{ztimes} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{negativep}}\,({\it{x\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{negativep}}\,({\it{y\/}})$\;\;${\bf then }{\rm{negative-guts}}\,({\it{x\/}}) $*$ {\rm{negative-guts}}\,({\it{y\/}}) \\ 
{\bf else }$-$ ({\rm{negative-guts}}\,({\it{x\/}}) $*$ {\it{y\/}})$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{negativep}}\,({\it{y\/}})$\;\;${\bf then }$-$ ({\it{x\/}} $*$ {\rm{negative-guts}}\,({\it{y\/}})) \\ 
{\bf else }{\it{x\/}} $*$ {\it{y\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{zquotient} \\  
\=\+{\rm{zquotient}}\,({\it{x\/}}, {\it{y\/}})\index{zquotient} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{negativep}}\,({\it{x\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{negativep}}\,({\it{y\/}})$\;\;${\bf then }{\rm{negative-guts}}\,({\it{x\/}}) $\div$ {\rm{negative-guts}}\,({\it{y\/}}) \\ 
{\bf else }$-$ ({\rm{negative-guts}}\,({\it{x\/}}) $\div$ {\it{y\/}})$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{negativep}}\,({\it{y\/}})$\;\;${\bf then }$-$ ({\it{x\/}} $\div$ {\rm{negative-guts}}\,({\it{y\/}})) \\ 
{\bf else }{\it{x\/}} $\div$ {\it{y\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{zexptz} \\  
\=\+{\rm{zexptz}}\,({\it{i\/}}, {\it{j\/}})\index{zexptz} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{j\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\rm{ztimes}}\,({\it{i\/}}, {\rm{zexptz}}\,({\it{i\/}}, {\it{j\/}} $-\;1$)\index{zexptz})\index{ztimes}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{znormalize} \\  
\=\+{\rm{znormalize}}\,({\it{x\/}})\index{znormalize} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{negativep}}\,({\it{x\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{negative-guts}}\,({\it{x\/}}) $=$ {\tt{0}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\- \\ 
{\bf else }{\rm{fix}}\,({\it{x\/}})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{zeqp}$\;\;$
{\rm{zeqp}}\,({\it{x\/}}, {\it{y\/}})\index{zeqp} $=$ ({\rm{znormalize}}\,({\it{x\/}})\index{znormalize} $=$ {\rm{znormalize}}\,({\it{y\/}})\index{znormalize})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{zneqp}$\;\;$
{\rm{zneqp}}\,({\it{x\/}}, {\it{y\/}})\index{zneqp} $=$ ($\neg$ {\rm{zeqp}}\,({\it{x\/}}, {\it{y\/}})\index{zeqp})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{zlessp} \\  
\=\+{\rm{zlessp}}\,({\it{x\/}}, {\it{y\/}})\index{zlessp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{negativep}}\,({\it{x\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{negativep}}\,({\it{y\/}})$\;\;${\bf then }{\rm{negative-guts}}\,({\it{y\/}}) $<$ {\rm{negative-guts}}\,({\it{x\/}}) \\ 
{\bf else }$\neg$ (({\rm{negative-guts}}\,({\it{x\/}}) $=$ {\tt{0}}) $\wedge$ ({\it{y\/}} $\simeq {\tt{0}}$))$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{negativep}}\,({\it{y\/}})$\;\;${\bf then }{\bf{f}} \\ 
{\bf else }{\it{x\/}} $<$ {\it{y\/}}$\;${\bf  endif}\-\-
\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{zgreaterp}$\;\;$
{\rm{zgreaterp}}\,({\it{x\/}}, {\it{y\/}})\index{zgreaterp} $=$ {\rm{zlessp}}\,({\it{y\/}}, {\it{x\/}})\index{zlessp}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{zgreatereqp}$\;\;$
{\rm{zgreatereqp}}\,({\it{x\/}}, {\it{y\/}})\index{zgreatereqp} $=$ ($\neg$ {\rm{zlessp}}\,({\it{x\/}}, {\it{y\/}})\index{zlessp})
\end{tabbing}
\begin{tabbing}{\sc Conservative Axiom}:  integer-size \\ \index{integer-size}
\=\+({\sc{least-inexpressible-positive-integer}}\index{least-inexpressible-positive-inte!ger} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{negativep}}\,({\sc{greatest-inexpressible-negative-integer}}\index{greatest-inexpressible-negative!-integer}) \\ 
$\wedge$$\;\;\;\;$({\tt{200}} $<$ {\rm{negative-guts}}\,({\sc{greatest-inexpressible-negative-integer}}\index{greatest-inexpressible-negative!-integer})) \\ 
$\wedge$$\;\;\;\;$({\tt{200}} $<$ {\sc{least-inexpressible-positive-integer}}\index{least-inexpressible-positive-inte!ger})\-
\end{tabbing}\noindent Simultaneously, we introduce the new function symbols {\it greatest-inexpressible-negative-integer\/} and {\it least-inexpressible-positive-integer\/}.
\begin{tabbing}{\sc Definition}:\index{expressible-znumberp} \\  
\=\+{\rm{expressible-znumberp}}\,({\it{x\/}})\index{expressible-znumberp} \\ 
$=$$\;\;\;\;$(\=\+{\rm{zlessp}}\,({\sc{greatest-inexpressible-negative-integer}}\index{greatest-inexpressible-negative!-integer}, {\it{x\/}})\index{zlessp} \\ 
$\wedge$$\;\;\;\;${\rm{zlessp}}\,({\it{x\/}}, {\sc{least-inexpressible-positive-integer}}\index{least-inexpressible-positive-inte!ger})\index{zlessp})\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{iabs} \\  
\=\+{\rm{iabs}}\,({\it{i\/}})\index{iabs} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{negativep}}\,({\it{i\/}})$\;\;${\bf then }{\rm{negative-guts}}\,({\it{i\/}}) \\ 
{\bf else }{\rm{fix}}\,({\it{i\/}})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{mod}$\;\;$
{\rm{mod}}\,({\it{x\/}}, {\it{y\/}})\index{mod} $=$ {\rm{zdifference}}\,({\it{x\/}}, {\rm{ztimes}}\,({\it{y\/}}, {\rm{zquotient}}\,({\it{x\/}}, {\it{y\/}})\index{zquotient})\index{ztimes})\index{zdifference}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{max0} \\  
\=\+{\rm{max0}}\,({\it{i\/}}, {\it{j\/}})\index{max0} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{zlessp}}\,({\it{i\/}}, {\it{j\/}})\index{zlessp}$\;\;${\bf then }{\it{j\/}} \\ 
{\bf else }{\it{i\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{min0} \\  
\=\+{\rm{min0}}\,({\it{i\/}}, {\it{j\/}})\index{min0} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{zlessp}}\,({\it{i\/}}, {\it{j\/}})\index{zlessp}$\;\;${\bf then }{\it{i\/}} \\ 
{\bf else }{\it{j\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{isign} \\  
\=\+{\rm{isign}}\,({\it{i\/}}, {\it{j\/}})\index{isign} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{negativep}}\,({\it{j\/}})$\;\;${\bf then }{\rm{ztimes}}\,({\tt{-1}}, {\rm{iabs}}\,({\it{i\/}})\index{iabs})\index{ztimes} \\ 
{\bf else }{\rm{iabs}}\,({\it{i\/}})\index{iabs}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{idim}$\;\;$
{\rm{idim}}\,({\it{i\/}}, {\it{j\/}})\index{idim} $=$ {\rm{zdifference}}\,({\it{i\/}}, {\rm{min0}}\,({\it{i\/}}, {\it{j\/}})\index{min0})\index{zdifference}
\end{tabbing}

\begin{verbatim};;; In the old FORTRAN xxx we used UNDEF for all occurrences of the
;;; substring FORTRAN-UNDEF below.  However, in the quantifier version
;;; of the logic, UNDEF is a function name set up in the bootstrap.
;;; To avoid conflict we have changed the name here.  However, it is
;;; possible that vcs mention UNDEF -- not just the function DEFINEDP
;;; which is still around here.  If so, the vcg will have be to be
;;; changed should we decide to support it.

\end{verbatim}
\noindent{\sc Event}:   Add the shell {\it{fortran-undef\/}}\index{fortran-undef}, with recognizer function symbol {\it{fortran-undefined\/}} and 1 accessor: {\it{fortran-undef-guts\/}}, with type restriction (none-of) and default value zero.

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{definedp}$\;\;$
{\rm{definedp}}\,({\it{x\/}})\index{definedp} $=$ ($\neg$ {\rm{fortran-undefined}}\,({\it{x\/}})\index{fortran-undefined})
\end{tabbing}

\noindent{\sc Event}:   Introduce the function symbol {\it elt1\index{elt1}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it elt2\index{elt2}\/} of 3 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it elt3\index{elt3}\/} of 4 arguments.

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{lex} \\  
\=\+{\rm{lex}}\,({\it{l1\/}}, {\it{l2\/}})\index{lex} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{l1\/}} $\simeq\;${{\bf{nil}}}${}$) $\vee$ ({\it{l2\/}} $\simeq\;${{\bf{nil}}}${}$)$\;\;${\bf then }{\bf{f}} \\ 
{\bf else }\=\+({\rm{car}}\,({\it{l1\/}}) $<$ {\rm{car}}\,({\it{l2\/}})) \\ 
$\vee$$\;\;\;\;$(({\rm{car}}\,({\it{l1\/}}) $=$ {\rm{car}}\,({\it{l2\/}})) $\wedge$ {\rm{lex}}\,({\rm{cdr}}\,({\it{l1\/}}), {\rm{cdr}}\,({\it{l2\/}}))\index{lex})\-$\;${\bf  endif}\-\-
\end{tabbing}

\noindent{\sc Event}:   Introduce the function symbol {\it rnumberp\index{rnumberp}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it dnumberp\index{dnumberp}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it cnumberp\index{cnumberp}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it rzero\index{rzero}\/} of 0 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it dzero\index{dzero}\/} of 0 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it czero\index{czero}\/} of 0 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it expressible-rnumberp\index{expressible-rnumberp}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it expressible-dnumberp\index{expressible-dnumberp}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it expressible-cnumberp\index{expressible-cnumberp}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it rplus\index{rplus}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it rtimes\index{rtimes}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it rdifference\index{rdifference}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it rquotient\index{rquotient}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it rlessp\index{rlessp}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it rlesseqp\index{rlesseqp}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it reqp\index{reqp}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it rneqp\index{rneqp}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it rgreatereqp\index{rgreatereqp}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it rgreaterp\index{rgreaterp}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it dplus\index{dplus}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it dtimes\index{dtimes}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it ddifference\index{ddifference}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it dquotient\index{dquotient}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it dlessp\index{dlessp}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it dlesseqp\index{dlesseqp}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it deqp\index{deqp}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it dneqp\index{dneqp}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it dgreatereqp\index{dgreatereqp}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it dgreaterp\index{dgreaterp}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it cplus\index{cplus}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it ctimes\index{ctimes}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it cdifference\index{cdifference}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it cquotient\index{cquotient}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it ceqp\index{ceqp}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it cneqp\index{cneqp}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it rexptz\index{rexptz}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it dexptz\index{dexptz}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it cexptz\index{cexptz}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it rexptr\index{rexptr}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it rexptd\index{rexptd}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it dexptr\index{dexptr}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it dexptd\index{dexptd}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it abs\index{abs}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it dabs\index{dabs}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it aint\index{aint}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it int\index{int}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it idint\index{idint}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it amod\index{amod}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it amax0\index{amax0}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it amax1\index{amax1}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it max1\index{max1}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it dmax1\index{dmax1}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it amin0\index{amin0}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it amin1\index{amin1}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it min1\index{min1}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it dmin1\index{dmin1}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it float\index{float}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it ifix\index{ifix}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it sign\index{sign}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it dsign\index{dsign}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it dim\index{dim}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it sngl\index{sngl}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it real\index{real}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it aimag\index{aimag}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it dble\index{dble}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it cmplx\index{cmplx}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it conjg\index{conjg}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it exp\index{exp}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it dexp\index{dexp}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it cexp\index{cexp}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it alog\index{alog}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it dlog\index{dlog}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it clog\index{clog}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it alog10\index{alog10}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it dlog10\index{dlog10}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it sin\index{sin}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it dsin\index{dsin}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it csin\index{csin}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it cos\index{cos}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it dcos\index{dcos}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it ccos\index{ccos}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it tanh\index{tanh}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it sqrt\index{sqrt}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it dsqrt\index{dsqrt}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it csqrt\index{csqrt}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it atan\index{atan}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it datan\index{datan}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it atan2\index{atan2}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it datan2\index{datan2}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it dmod\index{dmod}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it cabs\index{cabs}\/} of one argument.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{almost-equal1} \\  
\=\+{\rm{almost-equal1}}\,({\it{a1\/}}, {\it{a2\/}}, {\it{u\/}}, {\it{v\/}}, {\it{i\/}}, {\it{e\/}})\index{almost-equal1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{v\/}} $\simeq {\tt{0}}$) $\vee$ ({\it{v\/}} $<$ {\it{u\/}})$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }\=\+\=\+{\bf if }{\it{v\/}} $=$ {\it{i\/}}$\;\;${\bf then }{\rm{elt1}}\,({\it{a2\/}}, {\it{v\/}})\index{elt1} $=$ {\it{e\/}} \\ 
{\bf else }{\rm{elt1}}\,({\it{a2\/}}, {\it{v\/}})\index{elt1} $=$ {\rm{elt1}}\,({\it{a1\/}}, {\it{v\/}})\index{elt1}$\;${\bf  endif}\- \\ 
$\wedge$$\;\;\;\;${\rm{almost-equal1}}\,({\it{a1\/}}, {\it{a2\/}}, {\it{u\/}}, {\it{v\/}} $-\;1$, {\it{i\/}}, {\it{e\/}})\index{almost-equal1}\-$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  plus-0 \\ \index{plus-0}
({\it{x\/}} $+$ {\tt{0}}) $=$ {\rm{fix}}\,({\it{x\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  plus-non-numberp \\ \index{plus-non-numberp}
({\it{y\/}} $\not\in\;${\bf{N}}${}$) $\rightarrow$ (({\it{x\/}} $+$ {\it{y\/}}) $=$ {\rm{fix}}\,({\it{x\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  plus-add1 \\ \index{plus-add1}
\=\+({\it{x\/}} $+$ ($1\;+$ {\it{y\/}})) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{y\/}} $\in\;${\bf{N}}${}$$\;\;${\bf then }$1\;+$ ({\it{x\/}} $+$ {\it{y\/}}) \\ 
{\bf else }$1\;+$ {\it{x\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  commutativity2-of-plus \\ \index{commutativity2-of-plus}
({\it{x\/}} $+$ ({\it{y\/}} $+$ {\it{z\/}})) $=$ ({\it{y\/}} $+$ ({\it{x\/}} $+$ {\it{z\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  commutativity-of-plus \\ \index{commutativity-of-plus}
({\it{x\/}} $+$ {\it{y\/}}) $=$ ({\it{y\/}} $+$ {\it{x\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  associativity-of-plus \\ \index{associativity-of-plus}
(({\it{x\/}} $+$ {\it{y\/}}) $+$ {\it{z\/}}) $=$ ({\it{x\/}} $+$ ({\it{y\/}} $+$ {\it{z\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  times-0 \\ \index{times-0}
({\it{x\/}} $*$ {\tt{0}}) $=$ {\tt{0}}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  times-non-numberp \\ \index{times-non-numberp}
({\it{y\/}} $\not\in\;${\bf{N}}${}$) $\rightarrow$ (({\it{x\/}} $*$ {\it{y\/}}) $=$ {\tt{0}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  distributivity-of-times-over-plus \\ \index{distributivity-of-times-over-pl!us}
({\it{x\/}} $*$ ({\it{y\/}} $+$ {\it{z\/}})) $=$ (({\it{x\/}} $*$ {\it{y\/}}) $+$ ({\it{x\/}} $*$ {\it{z\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  times-add1 \\ \index{times-add1}
\=\+({\it{x\/}} $*$ ($1\;+$ {\it{y\/}})) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{y\/}} $\in\;${\bf{N}}${}$$\;\;${\bf then }{\it{x\/}} $+$ ({\it{x\/}} $*$ {\it{y\/}}) \\ 
{\bf else }{\rm{fix}}\,({\it{x\/}})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  commutativity2-of-times \\ \index{commutativity2-of-times}
({\it{x\/}} $*$ ({\it{y\/}} $*$ {\it{z\/}})) $=$ ({\it{y\/}} $*$ ({\it{x\/}} $*$ {\it{z\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  commutativity-of-times \\ \index{commutativity-of-times}
({\it{x\/}} $*$ {\it{y\/}}) $=$ ({\it{y\/}} $*$ {\it{x\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  associativity-of-times \\ \index{associativity-of-times}
(({\it{x\/}} $*$ {\it{y\/}}) $*$ {\it{z\/}}) $=$ ({\it{x\/}} $*$ ({\it{y\/}} $*$ {\it{z\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  equal-times-0 \\ \index{equal-times-0}
(({\it{x\/}} $*$ {\it{y\/}}) $=$ {\tt{0}}) $=$ (({\it{x\/}} $\simeq {\tt{0}}$) $\vee$ ({\it{y\/}} $\simeq {\tt{0}}$))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  equal-lessp \\ \index{equal-lessp}
\=\+(({\it{x\/}} $<$ {\it{y\/}}) $=$ {\it{z\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $<$ {\it{y\/}}$\;\;${\bf then }{\bf{t}} $=$ {\it{z\/}} \\ 
{\bf else }{\bf{f}} $=$ {\it{z\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  almost-equal1-in-range \\ \index{almost-equal1-in-range}
\=\+(\=\+({\rm{elt1}}\,({\it{a2\/}}, {\it{j\/}})\index{elt1} $\not=$ {\it{w\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{w\/}} $=$ \=\+{\bf if }{\it{j\/}} $=$ {\it{i\/}}$\;\;${\bf then }{\it{e\/}} \\ 
{\bf else }{\rm{elt1}}\,({\it{a1\/}}, {\it{j\/}})\index{elt1}$\;${\bf  endif}\-) \\ 
$\wedge$$\;\;\;\;$({\it{u\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\not<$ {\it{u\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{v\/}} $\not<$ {\it{j\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{almost-equal1}}\,({\it{a1\/}}, {\it{a2\/}}, {\it{u\/}}, {\it{v\/}}, {\it{i\/}}, {\it{e\/}})\index{almost-equal1})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  almost-equal1-in-range-opened-up \\ \index{almost-equal1-in-range-opened-up}
\=\+(\=\+({\rm{elt1}}\,({\it{a2\/}}, {\it{j\/}})\index{elt1} $\not=$ {\it{w\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{w\/}} $=$ \=\+{\bf if }{\it{j\/}} $=$ {\it{i\/}}$\;\;${\bf then }{\it{e\/}} \\ 
{\bf else }{\rm{elt1}}\,({\it{a1\/}}, {\it{j\/}})\index{elt1}$\;${\bf  endif}\-) \\ 
$\wedge$$\;\;\;\;$({\it{u\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{u\/}} $\leq$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\leq$ {\it{v\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{v\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{v\/}} $\not<$ {\it{u\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{v\/}} $\not=$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{elt1}}\,({\it{a2\/}}, {\it{v\/}})\index{elt1} $=$ {\rm{elt1}}\,({\it{a1\/}}, {\it{v\/}})\index{elt1}))\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{almost-equal1}}\,({\it{a1\/}}, {\it{a2\/}}, {\it{u\/}}, {\it{v\/}} $-\;1$, {\it{i\/}}, {\it{e\/}})\index{almost-equal1})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  almost-equal1-contracts \\ \index{almost-equal1-contracts}
\=\+({\rm{almost-equal1}}\,({\it{a1\/}}, {\it{a2\/}}, {\it{u\/}}, {\it{v\/}}, {\it{i\/}}, {\it{e\/}})\index{almost-equal1} $\wedge$ ({\it{u\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{x\/}} $\not<$ {\it{u\/}}) $\wedge$ ({\it{v\/}} $\not<$ {\it{y\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{almost-equal1}}\,({\it{a1\/}}, {\it{a2\/}}, {\it{x\/}}, {\it{y\/}}, {\it{i\/}}, {\it{e\/}})\index{almost-equal1}\-
\end{tabbing}


\noindent{\sc Event}:   Make the library {\tt{"fortran"}} and compile it.

\addvspace{18pt}

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