\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, J Strother Moore, and Mike Green.  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, J Strother Moore, and Mike Green 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, J Strother Moore, or Mike Green 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{"fortran"}} using the compiled version.

\addvspace{18pt}

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

\addvspace{18pt}
\begin{tabbing}{\sc Theorem}:  zplus-comm1 \\ \index{zplus-comm1}
{\rm{zplus}}\,({\it{x\/}}, {\it{y\/}})\index{zplus} $=$ {\rm{zplus}}\,({\it{y\/}}, {\it{x\/}})\index{zplus}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  zplus-comm2 \\ \index{zplus-comm2}
{\rm{zplus}}\,({\it{x\/}}, {\rm{zplus}}\,({\it{y\/}}, {\it{z\/}})\index{zplus})\index{zplus} $=$ {\rm{zplus}}\,({\it{y\/}}, {\rm{zplus}}\,({\it{x\/}}, {\it{z\/}})\index{zplus})\index{zplus}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  zplus-assoc \\ \index{zplus-assoc}
{\rm{zplus}}\,({\rm{zplus}}\,({\it{x\/}}, {\it{y\/}})\index{zplus}, {\it{z\/}})\index{zplus} $=$ {\rm{zplus}}\,({\it{x\/}}, {\rm{zplus}}\,({\it{y\/}}, {\it{z\/}})\index{zplus})\index{zplus}
\end{tabbing}

\noindent{\sc Event}:   Disable zplus.

\addvspace{18pt}

\noindent{\sc Event}:   Add the shell {\it{vehicle-state\/}}\index{vehicle-state}, with recognizer function symbol {\it{vehicle-statep\/}} and 3 accessors: {\it{w\/}}, with type restriction (none-of) and default value zero; {\it{y\/}}, with type restriction (none-of) and default value zero; {\it{v\/}}, with type restriction (none-of) and default value zero.

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{hd}$\;\;$
{\rm{hd}}\,({\it{x\/}})\index{hd} $=$ {\rm{car}}\,({\it{x\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{tl}$\;\;$
{\rm{tl}}\,({\it{x\/}})\index{tl} $=$ {\rm{cdr}}\,({\it{x\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{empty}$\;\;$
{\rm{empty}}\,({\it{x\/}})\index{empty} $=$ ($\neg$ {\rm{listp}}\,({\it{x\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  tl-rewrite \\ \index{tl-rewrite}
{\rm{tl}}\,({\it{x\/}})\index{tl} $=$ {\rm{cdr}}\,({\it{x\/}})
\end{tabbing}

\noindent{\sc Event}:   Disable tl.

\addvspace{18pt}
\begin{tabbing}{\sc Theorem}:  down-on-tl \\ \index{down-on-tl}
($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) $\rightarrow$ ({\rm{count}}\,({\rm{tl}}\,({\it{x\/}})\index{tl}) $<$ {\rm{count}}\,({\it{x\/}}))
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{random-delta-ws} \\  
\=\+{\rm{random-delta-ws}}\,({\it{lst\/}})\index{random-delta-ws} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{empty}}\,({\it{lst\/}})\index{empty}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }\=\+(\=\+({\rm{hd}}\,({\it{lst\/}})\index{hd} $=$ {\tt{-1}}) \\ 
$\vee$$\;\;\;\;$({\rm{hd}}\,({\it{lst\/}})\index{hd} $=$ {\tt{0}}) \\ 
$\vee$$\;\;\;\;$({\rm{hd}}\,({\it{lst\/}})\index{hd} $=$ {\tt{1}}))\- \\ 
$\wedge$$\;\;\;\;${\rm{random-delta-ws}}\,({\rm{tl}}\,({\it{lst\/}})\index{tl})\index{random-delta-ws}\-$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{controller} \\  
\=\+{\rm{controller}}\,({\it{sgn-y\/}}, {\it{sgn-old-y\/}})\index{controller} \\ 
$=$$\;\;\;\;${\rm{zplus}}\,({\rm{ztimes}}\,({\tt{-3}}, {\it{sgn-y\/}})\index{ztimes}, {\rm{ztimes}}\,({\tt{2}}, {\it{sgn-old-y\/}})\index{ztimes})\index{zplus}\-
\end{tabbing}

\noindent{\sc Event}:   Disable controller.

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{sgn} \\  
\=\+{\rm{sgn}}\,({\it{x\/}})\index{sgn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{negativep}}\,({\it{x\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{negative-guts}}\,({\it{x\/}}) $=$ {\tt{0}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\tt{-1}}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{x\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\tt{1}}$\;${\bf  endif}\-\-
\end{tabbing}

\noindent{\sc Event}:   Disable sgn.

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{next-state} \\  
\=\+{\rm{next-state}}\,({\it{delta-w\/}}, {\it{state\/}})\index{next-state} \\ 
$=$$\;\;\;\;${\rm{vehicle-state}}\,(\=\+{\rm{zplus}}\,({\rm{w}}\,({\it{state\/}})\index{w}, {\it{delta-w\/}})\index{zplus}, \\ 
{\rm{zplus}}\,({\rm{y}}\,({\it{state\/}})\index{y}, {\rm{zplus}}\,({\rm{v}}\,({\it{state\/}})\index{v}, {\rm{zplus}}\,({\rm{w}}\,({\it{state\/}})\index{w}, {\it{delta-w\/}})\index{zplus})\index{zplus})\index{zplus}, \\ 
{\rm{zplus}}\,(\=\+{\rm{v}}\,({\it{state\/}})\index{v}, \\ 
{\rm{controller}}\,(\=\+{\rm{sgn}}\,({\rm{zplus}}\,(\=\+{\rm{y}}\,({\it{state\/}})\index{y}, \\ 
{\rm{zplus}}\,(\=\+{\rm{v}}\,({\it{state\/}})\index{v}, \\ 
{\rm{zplus}}\,({\rm{w}}\,({\it{state\/}})\index{w}, {\it{delta-w\/}})\index{zplus})\-\index{zplus})\-\index{zplus})\index{sgn}, \\ 
{\rm{sgn}}\,({\rm{y}}\,({\it{state\/}})\index{y})\index{sgn})\-\index{controller})\-\index{zplus})\-\index{vehicle-state}\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{final-state-of-vehicle} \\  
\=\+{\rm{final-state-of-vehicle}}\,({\it{delta-ws\/}}, {\it{state\/}})\index{final-state-of-vehicle} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{empty}}\,({\it{delta-ws\/}})\index{empty}$\;\;${\bf then }{\it{state\/}} \\ 
{\bf else }{\rm{final-state-of-vehicle}}\,(\=\+{\rm{tl}}\,({\it{delta-ws\/}})\index{tl}, \\ 
{\rm{next-state}}\,({\rm{hd}}\,({\it{delta-ws\/}})\index{hd}, {\it{state\/}})\index{next-state})\-\index{final-state-of-vehicle}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{good-statep} \\  
\=\+{\rm{good-statep}}\,({\it{state\/}})\index{good-statep} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{y}}\,({\it{state\/}})\index{y} $=$ {\tt{0}} \\ 
{\bf then }\=\+({\rm{zplus}}\,({\rm{v}}\,({\it{state\/}})\index{v}, {\rm{w}}\,({\it{state\/}})\index{w})\index{zplus} $=$ {\tt{-1}}) \\ 
$\vee$$\;\;\;\;$({\rm{zplus}}\,({\rm{v}}\,({\it{state\/}})\index{v}, {\rm{w}}\,({\it{state\/}})\index{w})\index{zplus} $=$ {\tt{0}}) \\ 
$\vee$$\;\;\;\;$({\rm{zplus}}\,({\rm{v}}\,({\it{state\/}})\index{v}, {\rm{w}}\,({\it{state\/}})\index{w})\index{zplus} $=$ {\tt{1}})\- \\ 
{\bf elseif }{\rm{y}}\,({\it{state\/}})\index{y} $=$ {\tt{1}} \\ 
{\bf then }\=\+({\rm{zplus}}\,({\rm{v}}\,({\it{state\/}})\index{v}, {\rm{w}}\,({\it{state\/}})\index{w})\index{zplus} $=$ {\tt{-2}}) \\ 
$\vee$$\;\;\;\;$({\rm{zplus}}\,({\rm{v}}\,({\it{state\/}})\index{v}, {\rm{w}}\,({\it{state\/}})\index{w})\index{zplus} $=$ {\tt{-3}})\- \\ 
{\bf elseif }{\rm{y}}\,({\it{state\/}})\index{y} $=$ {\tt{2}} \\ 
{\bf then }\=\+({\rm{zplus}}\,({\rm{v}}\,({\it{state\/}})\index{v}, {\rm{w}}\,({\it{state\/}})\index{w})\index{zplus} $=$ {\tt{-1}}) \\ 
$\vee$$\;\;\;\;$({\rm{zplus}}\,({\rm{v}}\,({\it{state\/}})\index{v}, {\rm{w}}\,({\it{state\/}})\index{w})\index{zplus} $=$ {\tt{-2}})\- \\ 
{\bf elseif }{\rm{y}}\,({\it{state\/}})\index{y} $=$ {\tt{3}}$\;\;${\bf then }{\rm{zplus}}\,({\rm{v}}\,({\it{state\/}})\index{v}, {\rm{w}}\,({\it{state\/}})\index{w})\index{zplus} $=$ {\tt{-1}} \\ 
{\bf elseif }{\rm{y}}\,({\it{state\/}})\index{y} $=$ {\tt{-3}}$\;\;${\bf then }{\rm{zplus}}\,({\rm{v}}\,({\it{state\/}})\index{v}, {\rm{w}}\,({\it{state\/}})\index{w})\index{zplus} $=$ {\tt{1}} \\ 
{\bf elseif }{\rm{y}}\,({\it{state\/}})\index{y} $=$ {\tt{-2}} \\ 
{\bf then }\=\+({\rm{zplus}}\,({\rm{v}}\,({\it{state\/}})\index{v}, {\rm{w}}\,({\it{state\/}})\index{w})\index{zplus} $=$ {\tt{1}}) \\ 
$\vee$$\;\;\;\;$({\rm{zplus}}\,({\rm{v}}\,({\it{state\/}})\index{v}, {\rm{w}}\,({\it{state\/}})\index{w})\index{zplus} $=$ {\tt{2}})\- \\ 
{\bf elseif }{\rm{y}}\,({\it{state\/}})\index{y} $=$ {\tt{-1}} \\ 
{\bf then }\=\+({\rm{zplus}}\,({\rm{v}}\,({\it{state\/}})\index{v}, {\rm{w}}\,({\it{state\/}})\index{w})\index{zplus} $=$ {\tt{2}}) \\ 
$\vee$$\;\;\;\;$({\rm{zplus}}\,({\rm{v}}\,({\it{state\/}})\index{v}, {\rm{w}}\,({\it{state\/}})\index{w})\index{zplus} $=$ {\tt{3}})\- \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  next-good-state \\ \index{next-good-state}
\=\+({\rm{good-statep}}\,({\it{state\/}})\index{good-statep} $\wedge$ (({\it{r\/}} $=$ {\tt{-1}}) $\vee$ ({\it{r\/}} $=$ {\tt{0}}) $\vee$ ({\it{r\/}} $=$ {\tt{1}}))) \\ 
$\rightarrow$$\;\;\;\;${\rm{good-statep}}\,({\rm{next-state}}\,({\it{r\/}}, {\it{state\/}})\index{next-state})\index{good-statep}\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{zero-delta-ws} \\  
\=\+{\rm{zero-delta-ws}}\,({\it{lst\/}})\index{zero-delta-ws} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{empty}}\,({\it{lst\/}})\index{empty}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }({\rm{hd}}\,({\it{lst\/}})\index{hd} $=$ {\tt{0}}) $\wedge$ {\rm{zero-delta-ws}}\,({\rm{tl}}\,({\it{lst\/}})\index{tl})\index{zero-delta-ws}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{concat} \\  
\=\+{\rm{concat}}\,({\it{x\/}}, {\it{y\/}})\index{concat} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\it{y\/}} \\ 
{\bf else }{\rm{cons}}\,({\rm{hd}}\,({\it{x\/}})\index{hd}, {\rm{concat}}\,({\rm{tl}}\,({\it{x\/}})\index{tl}, {\it{y\/}})\index{concat})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{length} \\  
\=\+{\rm{length}}\,({\it{x\/}})\index{length} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }$1\;+$ {\rm{length}}\,({\rm{tl}}\,({\it{x\/}})\index{tl})\index{length}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  length-0 \\ \index{length-0}
({\rm{length}}\,({\it{x\/}})\index{length} $=$ {\tt{0}}) $=$ {\rm{empty}}\,({\it{x\/}})\index{empty}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  decompose-list-of-length-4 \\ \index{decompose-list-of-length-4}
\=\+{\rm{zero-delta-ws}}\,({\it{lst\/}})\index{zero-delta-ws} \\ 
$\rightarrow$$\;\;\;\;$(({\rm{length}}\,({\it{lst\/}})\index{length} $<$ {\tt{4}}) $=$ ({\it{lst\/}} $\not=$ {\rm{concat}}\,({\tt{'}}{\tt{(}}{\tt{0}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{0}}{\tt{)}}, {\rm{cddddr}}\,({\it{lst\/}}))\index{concat}))\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  drift-to-0-in-4 \\ \index{drift-to-0-in-4}
\=\+{\rm{good-statep}}\,({\it{state\/}})\index{good-statep} \\ 
$\rightarrow$$\;\;\;\;$({\rm{y}}\,({\rm{final-state-of-vehicle}}\,({\tt{'}}{\tt{(}}{\tt{0}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{0}}{\tt{)}}, {\it{state\/}})\index{final-state-of-vehicle})\index{y} $=$ {\tt{0}})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  cancel-wind-in-4 \\ \index{cancel-wind-in-4}
\=\+{\rm{good-statep}}\,({\it{state\/}})\index{good-statep} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{zplus}}\,(\=\+{\rm{v}}\,({\rm{final-state-of-vehicle}}\,({\tt{'}}{\tt{(}}{\tt{0}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{0}}{\tt{)}}, {\it{state\/}})\index{final-state-of-vehicle})\index{v}, \\ 
{\rm{w}}\,({\rm{final-state-of-vehicle}}\,({\tt{'}}{\tt{(}}{\tt{0}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{0}}{\tt{)}}, {\it{state\/}})\index{final-state-of-vehicle})\index{w})\-\index{zplus} \\ 
$=$$\;\;\;\;${\tt{0}})\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  once-0-always-0 \\ \index{once-0-always-0}
\=\+(\=\+{\rm{zero-delta-ws}}\,({\it{lst\/}})\index{zero-delta-ws} \\ 
$\wedge$$\;\;\;\;$({\rm{y}}\,({\it{state\/}})\index{y} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{zplus}}\,({\rm{w}}\,({\it{state\/}})\index{w}, {\rm{v}}\,({\it{state\/}})\index{v})\index{zplus} $=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{y}}\,({\rm{final-state-of-vehicle}}\,({\it{lst\/}}, {\it{state\/}})\index{final-state-of-vehicle})\index{y} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{zplus}}\,(\=\+{\rm{v}}\,({\rm{final-state-of-vehicle}}\,({\it{lst\/}}, {\it{state\/}})\index{final-state-of-vehicle})\index{v}, \\ 
{\rm{w}}\,({\rm{final-state-of-vehicle}}\,({\it{lst\/}}, {\it{state\/}})\index{final-state-of-vehicle})\index{w})\-\index{zplus} \\ 
$=$$\;\;\;\;${\tt{0}})\-)\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  final-state-of-vehicle-concat \\ \index{final-state-of-vehicle-concat}
\=\+{\rm{final-state-of-vehicle}}\,({\rm{concat}}\,({\it{a\/}}, {\it{b\/}})\index{concat}, {\it{state\/}})\index{final-state-of-vehicle} \\ 
$=$$\;\;\;\;${\rm{final-state-of-vehicle}}\,({\it{b\/}}, {\rm{final-state-of-vehicle}}\,({\it{a\/}}, {\it{state\/}})\index{final-state-of-vehicle})\index{final-state-of-vehicle}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  zero-delta-ws-concat \\ \index{zero-delta-ws-concat}
{\rm{zero-delta-ws}}\,({\rm{concat}}\,({\tt{'}}{\tt{(}}{\tt{0}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{0}}{\tt{)}}, {\it{v\/}})\index{concat})\index{zero-delta-ws} $=$ {\rm{zero-delta-ws}}\,({\it{v\/}})\index{zero-delta-ws}
\end{tabbing}

\noindent{\sc Event}:   Disable concat.

\addvspace{18pt}

\noindent{\sc Event}:   Disable next-state.

\addvspace{18pt}
\begin{tabbing}{\sc Theorem}:  good-statep-bounded-above \\ \index{good-statep-bounded-above}
{\rm{good-statep}}\,({\it{state\/}})\index{good-statep} $\rightarrow$ ($\neg$ {\rm{zlessp}}\,({\tt{3}}, {\rm{y}}\,({\it{state\/}})\index{y})\index{zlessp})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  good-statep-bounded-below \\ \index{good-statep-bounded-below}
{\rm{good-statep}}\,({\it{state\/}})\index{good-statep} $\rightarrow$ ($\neg$ {\rm{zlessp}}\,({\rm{y}}\,({\it{state\/}})\index{y}, {\tt{-3}})\index{zlessp})
\end{tabbing}

\noindent{\sc Event}:   Disable good-statep.

\addvspace{18pt}
\begin{tabbing}{\sc Theorem}:  zlessp-is-lessp \\ \index{zlessp-is-lessp}
(({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{y\/}} $\in\;${\bf{N}}${}$)) $\rightarrow$ ({\rm{zlessp}}\,({\it{x\/}}, {\it{y\/}})\index{zlessp} $=$ ({\it{x\/}} $<$ {\it{y\/}}))
\end{tabbing}

\noindent{\sc Event}:   Disable zlessp.

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{fsv} \\  
\=\+{\rm{fsv}}\,({\it{d\/}}, {\it{s\/}})\index{fsv} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{empty}}\,({\it{d\/}})\index{empty}$\;\;${\bf then }{\it{s\/}} \\ 
{\bf else }{\rm{fsv}}\,({\rm{tl}}\,({\it{d\/}})\index{tl}, {\rm{next-state}}\,({\rm{hd}}\,({\it{d\/}})\index{hd}, {\it{s\/}})\index{next-state})\index{fsv}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  all-good-states \\ \index{all-good-states}
\=\+({\rm{random-delta-ws}}\,({\it{lst\/}})\index{random-delta-ws} $\wedge$ {\rm{good-statep}}\,({\it{state\/}})\index{good-statep}) \\ 
$\rightarrow$$\;\;\;\;${\rm{good-statep}}\,({\rm{final-state-of-vehicle}}\,({\it{lst\/}}, {\it{state\/}})\index{final-state-of-vehicle})\index{good-statep}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  vehicle-stays-within-3-of-course \\ \index{vehicle-stays-within-3-of-course}
\=\+(\=\+{\rm{random-delta-ws}}\,({\it{lst\/}})\index{random-delta-ws} \\ 
$\wedge$$\;\;\;\;$({\it{state\/}} $=$ {\rm{final-state-of-vehicle}}\,({\it{lst\/}}, {\rm{vehicle-state}}\,({\tt{0}}, {\tt{0}}, {\tt{0}})\index{vehicle-state})\index{final-state-of-vehicle}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{zlesseqp}}\,({\tt{-3}}, {\rm{y}}\,({\it{state\/}})\index{y})\index{zlesseqp} $\wedge$ {\rm{zlesseqp}}\,({\rm{y}}\,({\it{state\/}})\index{y}, {\tt{3}})\index{zlesseqp})\-
\end{tabbing}

\noindent{\sc Event}:   Disable final-state-of-vehicle.

\addvspace{18pt}
\begin{tabbing}{\sc Theorem}:  zero-delta-ws-cddddr \\ \index{zero-delta-ws-cddddr}
{\rm{zero-delta-ws}}\,({\it{x\/}})\index{zero-delta-ws} $\rightarrow$ {\rm{zero-delta-ws}}\,({\rm{cddddr}}\,({\it{x\/}}))\index{zero-delta-ws}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  good-states-find-and-stay-at-0 \\ \index{good-states-find-and-stay-at-0}
\=\+({\rm{good-statep}}\,({\it{state\/}})\index{good-statep} $\wedge$ {\rm{zero-delta-ws}}\,({\it{lst2\/}})\index{zero-delta-ws} $\wedge$ ({\rm{length}}\,({\it{lst2\/}})\index{length} $\not<$ {\tt{4}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{y}}\,({\rm{final-state-of-vehicle}}\,({\it{lst2\/}}, {\it{state\/}})\index{final-state-of-vehicle})\index{y} $=$ {\tt{0}})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  vehicle-gets-on-course-in-steady-wind \\ \index{vehicle-gets-on-course-in-stead!y-wind}
\=\+(\=\+{\rm{random-delta-ws}}\,({\it{lst1\/}})\index{random-delta-ws} \\ 
$\wedge$$\;\;\;\;${\rm{zero-delta-ws}}\,({\it{lst2\/}})\index{zero-delta-ws} \\ 
$\wedge$$\;\;\;\;${\rm{zgreatereqp}}\,({\rm{length}}\,({\it{lst2\/}})\index{length}, {\tt{4}})\index{zgreatereqp} \\ 
$\wedge$$\;\;\;\;$({\it{state\/}} $=$ {\rm{final-state-of-vehicle}}\,(\=\+{\rm{concat}}\,({\it{lst1\/}}, {\it{lst2\/}})\index{concat}, \\ 
{\rm{vehicle-state}}\,({\tt{0}}, {\tt{0}}, {\tt{0}})\index{vehicle-state})\-\index{final-state-of-vehicle}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{y}}\,({\it{state\/}})\index{y} $=$ {\tt{0}})\-
\end{tabbing}

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