\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 Computational Logic, Inc.  All Rights Reserved.

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

 NO WARRANTY

 Computational Logic, Inc. 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 Computational Logic, Inc. 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.
|#

;; Matt Kaufmann

;; See CLI Internal Note 216 for explanation.  I thank Stan Letovsky
;; for suggesting this example and for taking the lead in formalizing
;; the problem for the Boyer-Moore theorem prover.

\end{verbatim}
\noindent{\sc Event}:   Start with the initial {\bf nqthm} theory.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  append-associativity \\ \index{append-associativity}
{\rm{append}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}), {\it{z\/}}) $=$ {\rm{append}}\,({\it{x\/}}, {\rm{append}}\,({\it{y\/}}, {\it{z\/}}))
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{length} \\  
\=\+{\rm{length}}\,({\it{lst\/}})\index{length} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{lst\/}})$\;\;${\bf then }$1\;+$ {\rm{length}}\,({\rm{cdr}}\,({\it{lst\/}}))\index{length} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}


\noindent{\sc Event}:   Add the shell {\it{make-op\/}}\index{make-op}, with recognizer function symbol {\it{op?\/}} and 2 accessors: {\it{op-type\/}}, with type restriction (none-of) and default value zero; {\it{tid\/}}, with type restriction (one-of numberp) and default value zero.

\addvspace{18pt}


\noindent{\sc Event}:   Add the shell {\it{make-obj\/}}\index{make-obj}, with recognizer function symbol {\it{obj?\/}} and 2 accessors: {\it{lock-tid\/}}, with type restriction (one-of numberp falsep) and default value zero; {\it{waiters\/}}, with type restriction (none-of) and default value zero.

\addvspace{18pt}

\begin{verbatim};; oops -- another basic lemma needed
\end{verbatim}\begin{tabbing}{\sc Theorem}:  length-append \\ \index{length-append}
{\rm{length}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}))\index{length} $=$ ({\rm{length}}\,({\it{x\/}})\index{length} $+$ {\rm{length}}\,({\it{y\/}})\index{length})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{server} \\  
\=\+{\rm{server}}\,({\it{tranq\/}}, {\it{x\/}})\index{server} \\ 
$=$$\;\;\;\;$\=\+{\bf let }\=\+{\it{current\/}}{\bf $\;$ be$\;\;$}{\rm{car}}\,({\it{tranq\/}})\- \\ 
{\bf in} \\ 
\=\+{\bf if }{\it{tranq\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }\=\+({\rm{op-type}}\,({\it{current\/}})\index{op-type} $=$ {\tt{'}}{\tt{write}}) \\ 
$\wedge$$\;\;\;\;$({\rm{tid}}\,({\it{current\/}})\index{tid} $=$ {\rm{lock-tid}}\,({\it{x\/}})\index{lock-tid})\- \\ 
{\bf then }{\rm{cons}}\,(\=\+{\it{current\/}}, \\ 
{\rm{server}}\,({\rm{append}}\,({\rm{waiters}}\,({\it{x\/}})\index{waiters}, {\rm{cdr}}\,({\it{tranq\/}})), {\rm{make-obj}}\,({\bf{f}}, {\bf{nil}})\index{make-obj})\index{server})\- \\ 
{\bf elseif }{\rm{falsep}}\,({\rm{lock-tid}}\,({\it{x\/}})\index{lock-tid}) \\ 
{\bf then }\=\+{\bf if }{\rm{op-type}}\,({\it{current\/}})\index{op-type} $=$ {\tt{'}}{\tt{read}} \\ 
{\bf then }{\rm{cons}}\,(\=\+{\it{current\/}}, \\ 
{\rm{server}}\,(\=\+{\rm{cdr}}\,({\it{tranq\/}}), \\ 
{\rm{make-obj}}\,({\rm{tid}}\,({\it{current\/}})\index{tid}, {\rm{waiters}}\,({\it{x\/}})\index{waiters})\index{make-obj})\-\index{server})\- \\ 
{\bf else }{\rm{cons}}\,({\it{current\/}}, {\rm{server}}\,({\rm{cdr}}\,({\it{tranq\/}}), {\it{x\/}})\index{server})$\;${\bf  endif}\- \\ 
{\bf else }{\rm{server}}\,(\=\+{\rm{cdr}}\,({\it{tranq\/}}), \\ 
{\rm{make-obj}}\,(\=\+{\rm{lock-tid}}\,({\it{x\/}})\index{lock-tid}, \\ 
{\rm{append}}\,({\rm{waiters}}\,({\it{x\/}})\index{waiters}, {\rm{list}}\,({\it{current\/}})))\-\index{make-obj})\-\index{server}$\;${\bf  endif}\-$\;${\bf  endlet}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{find-write} \\  
\=\+{\rm{find-write}}\,({\it{tid\/}}, {\it{tranq\/}})\index{find-write} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{tranq\/}}) \\ 
{\bf then }\=\+(\=\+{\rm{op?}}\,({\rm{car}}\,({\it{tranq\/}}))\index{op?} \\ 
$\wedge$$\;\;\;\;$({\rm{op-type}}\,({\rm{car}}\,({\it{tranq\/}}))\index{op-type} $=$ {\tt{'}}{\tt{write}}) \\ 
$\wedge$$\;\;\;\;$({\it{tid\/}} $=$ {\rm{tid}}\,({\rm{car}}\,({\it{tranq\/}}))\index{tid}))\- \\ 
$\vee$$\;\;\;\;${\rm{find-write}}\,({\it{tid\/}}, {\rm{cdr}}\,({\it{tranq\/}}))\index{find-write}\- \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}#|
I was trying to prove a lemma (later not needed) which generated
the following goal:

(IMPLIES (AND (LISTP TRANQ)
              (OP? (CAR TRANQ))
              (EQUAL TID (TID (CAR TRANQ))))
         (IMPLIES (FIND-WRITE TID TRANQ)
                  (EQUAL (GOOD-TRANQ (REMOVE-WRITE TID TRANQ))
                         (GOOD-TRANQ TRANQ))))

Inspection of this goal lead me to realize that when removing
or finding a WRITE operation, one needs to check not only the
TID but also that the operation is really a WRITE!  I then fixed
the definition of REMOVE-WRITE (as indicated below), and later
realized I needed to make a similar change to the definition of
FIND-WRITE (see above).
|#

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{remove-write} \\  
\=\+{\rm{remove-write}}\,({\it{tid\/}}, {\it{tranq\/}})\index{remove-write} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{tranq\/}}) \\ 
{\bf then }\=\+{\bf if }\=\+{\rm{op?}}\,({\rm{car}}\,({\it{tranq\/}}))\index{op?} \\ 
$\wedge$$\;\;\;\;$({\rm{op-type}}\,({\rm{car}}\,({\it{tranq\/}}))\index{op-type} $=$ {\tt{'}}{\tt{write}}) \\ 
$\wedge$$\;\;\;\;$({\it{tid\/}} $=$ {\rm{tid}}\,({\rm{car}}\,({\it{tranq\/}}))\index{tid})\-$\;\;${\bf then }{\rm{cdr}}\,({\it{tranq\/}}) \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\it{tranq\/}}), {\rm{remove-write}}\,({\it{tid\/}}, {\rm{cdr}}\,({\it{tranq\/}}))\index{remove-write})$\;${\bf  endif}\- \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  good-tranq-helper \\ \index{good-tranq-helper}
{\rm{length}}\,({\it{tranq\/}})\index{length} $\not<$ {\rm{length}}\,({\rm{remove-write}}\,({\it{tid\/}}, {\it{tranq\/}})\index{remove-write})\index{length}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{good-tranq} \\  
\=\+{\rm{good-tranq}}\,({\it{tranq\/}})\index{good-tranq} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{tranq\/}}) \\ 
{\bf then }\=\+{\rm{op?}}\,({\rm{car}}\,({\it{tranq\/}}))\index{op?} \\ 
$\wedge$$\;\;\;\;$\=\+{\bf if }{\rm{op-type}}\,({\rm{car}}\,({\it{tranq\/}}))\index{op-type} $=$ {\tt{'}}{\tt{read}} \\ 
{\bf then }\=\+{\rm{find-write}}\,({\rm{tid}}\,({\rm{car}}\,({\it{tranq\/}}))\index{tid}, {\rm{cdr}}\,({\it{tranq\/}}))\index{find-write} \\ 
$\wedge$$\;\;\;\;${\rm{good-tranq}}\,({\rm{remove-write}}\,(\=\+{\rm{tid}}\,({\rm{car}}\,({\it{tranq\/}}))\index{tid}, \\ 
{\rm{cdr}}\,({\it{tranq\/}}))\-\index{remove-write})\index{good-tranq}\- \\ 
{\bf else }{\rm{good-tranq}}\,({\rm{cdr}}\,({\it{tranq\/}}))\index{good-tranq}$\;${\bf  endif}\-\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{good-trace} \\  
\=\+{\rm{good-trace}}\,({\it{trace\/}}, {\it{tid\/}})\index{good-trace} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{trace\/}}) \\ 
{\bf then }\=\+{\rm{op?}}\,({\rm{car}}\,({\it{trace\/}}))\index{op?} \\ 
$\wedge$$\;\;\;\;$\=\+{\bf if }{\it{tid\/}} \\ 
{\bf then }\=\+{\bf case on }{\rm{op-type}}\,({\rm{car}}\,({\it{trace\/}}))\index{op-type}: \\ 
{\bf case = }{\it{read\/}} \\ 
{\bf then }{\bf{f}} \\ 
{\bf case = }{\it{write\/}} \\ 
{\bf $\;\;$then }\=\+({\rm{tid}}\,({\rm{car}}\,({\it{trace\/}}))\index{tid} $=$ {\it{tid\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{good-trace}}\,({\rm{cdr}}\,({\it{trace\/}}), {\bf{f}})\index{good-trace}\- \\ 
{\bf otherwise }{\rm{good-trace}}\,({\rm{cdr}}\,({\it{trace\/}}), {\it{tid\/}})\index{good-trace}$\;${\bf  endcase}\- \\ 
{\bf else }\=\+{\bf case on }{\rm{op-type}}\,({\rm{car}}\,({\it{trace\/}}))\index{op-type}: \\ 
{\bf case = }{\it{read\/}} \\ 
{\bf then }{\rm{good-trace}}\,({\rm{cdr}}\,({\it{trace\/}}), {\rm{tid}}\,({\rm{car}}\,({\it{trace\/}}))\index{tid})\index{good-trace} \\ 
{\bf otherwise }{\rm{good-trace}}\,({\rm{cdr}}\,({\it{trace\/}}), {\bf{f}})\index{good-trace}$\;${\bf  endcase}\-$\;${\bf  endif}\-\- \\ 
{\bf elseif }{\it{tid\/}}$\;\;${\bf then }{\bf{f}} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};; *** The simplification in the case below where tid is F is perhaps
;; the key to the whole proof.  Once I made this change, the only
;; remaining fix was the one in the definition shown above, and that
;; was easy to locate by inspection of the output of the main lemma,
;; SERVER-SAFETY-MAIN-LEMMA.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{good-tranq-tid} \\  
\=\+{\rm{good-tranq-tid}}\,({\it{x\/}}, {\it{y\/}}, {\it{tid\/}})\index{good-tranq-tid} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{tid\/}} \\ 
{\bf then }{\rm{find-write}}\,({\it{tid\/}}, {\it{y\/}})\index{find-write} $\wedge$ {\rm{good-tranq}}\,({\rm{append}}\,({\it{x\/}}, {\rm{remove-write}}\,({\it{tid\/}}, {\it{y\/}})\index{remove-write}))\index{good-tranq} \\ 
{\bf else }({\it{x\/}} $=$ {\bf{nil}}) $\wedge$ {\rm{good-tranq}}\,({\it{y\/}})\index{good-tranq}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  server-safety-main-lemma \\ \index{server-safety-main-lemma}
\=\+({\rm{obj?}}\,({\it{x\/}})\index{obj?} $\wedge$ {\rm{good-tranq-tid}}\,({\rm{waiters}}\,({\it{x\/}})\index{waiters}, {\it{tranq\/}}, {\rm{lock-tid}}\,({\it{x\/}})\index{lock-tid})\index{good-tranq-tid}) \\ 
$\rightarrow$$\;\;\;\;${\rm{good-trace}}\,({\rm{server}}\,({\it{tranq\/}}, {\it{x\/}})\index{server}, {\rm{lock-tid}}\,({\it{x\/}})\index{lock-tid})\index{good-trace}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  server-safety \\ \index{server-safety}
{\rm{good-tranq}}\,({\it{tranq\/}})\index{good-tranq} $\rightarrow$ {\rm{good-trace}}\,({\rm{server}}\,({\it{tranq\/}}, {\rm{make-obj}}\,({\bf{f}}, {\bf{nil}})\index{make-obj})\index{server}, {\bf{f}})\index{good-trace}
\end{tabbing}


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