\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[]




\noindent{\sc Event}:   Start with the library {\tt{"naturals"}}.

\addvspace{18pt}

\begin{verbatim};;; Several Useful Theorems

\end{verbatim}\begin{tabbing}{\sc Theorem}:  equal-iff \\ \index{equal-iff}
\=\+(({\rm{truep}}\,({\it{a\/}}) $\vee$ {\rm{falsep}}\,({\it{a\/}})) $\wedge$ ({\rm{truep}}\,({\it{b\/}}) $\vee$ {\rm{falsep}}\,({\it{b\/}}))) \\ 
$\rightarrow$$\;\;\;\;$(({\it{a\/}} $=$ {\it{b\/}}) $=$ ({\it{a\/}} $\leftrightarrow$ {\it{b\/}}))\-
\end{tabbing}


\noindent{\sc Event}:   Disable equal-iff.

\addvspace{18pt}

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

\begin{tabbing}{\sc Definition}:\index{nth} \\  
\=\+{\rm{nth}}\,({\it{list\/}}, {\it{n\/}})\index{nth} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{car}}\,({\it{list\/}}) \\ 
{\bf else }{\rm{nth}}\,({\rm{cdr}}\,({\it{list\/}}), {\it{n\/}} $-\;1$)\index{nth}$\;${\bf  endif}\-\-
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  nth-member \\ \index{nth-member}
({\it{n\/}} $<$ {\rm{length}}\,({\it{list\/}})\index{length}) $\rightarrow$ ({\rm{nth}}\,({\it{list\/}}, {\it{n\/}})\index{nth} $\in$ {\it{list\/}})
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  listp-not-zero-length \\ \index{listp-not-zero-length}
({\rm{length}}\,({\it{list\/}})\index{length} $=$ {\tt{0}}) $=$ ($\neg$ {\rm{listp}}\,({\it{list\/}}))
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  position-zero \\ \index{position-zero}
({\it{e\/}} $\not\in$ {\it{prg\/}}) $\rightarrow$ ({\rm{position}}\,({\it{prg\/}}, {\it{e\/}})\index{position} $=$ {\rm{length}}\,({\it{prg\/}})\index{length})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  position-lessp \\ \index{position-lessp}
({\it{e\/}} $\in$ {\it{prg\/}}) $\rightarrow$ ({\rm{position}}\,({\it{prg\/}}, {\it{e\/}})\index{position} $<$ {\rm{length}}\,({\it{prg\/}})\index{length})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  nth-position \\ \index{nth-position}
\=\+{\rm{nth}}\,({\it{prg\/}}, {\rm{position}}\,({\it{prg\/}}, {\it{e\/}})\index{position})\index{nth} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{e\/}} $\in$ {\it{prg\/}}$\;\;${\bf then }{\it{e\/}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  position-nth \\ \index{position-nth}
(({\it{e\/}} $\in$ {\it{list\/}}) $\wedge$ ({\rm{nth}}\,({\it{list\/}}, {\it{n\/}})\index{nth} $\not=$ {\it{e\/}})) $\rightarrow$ (({\rm{position}}\,({\it{list\/}}, {\it{e\/}})\index{position} $=$ {\it{n\/}}) $=$ {\bf{f}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-append \\ \index{member-append}
({\it{e\/}} $\in$ {\rm{append}}\,({\it{j\/}}, {\it{k\/}})) $=$ (({\it{e\/}} $\in$ {\it{j\/}}) $\vee$ ({\it{e\/}} $\in$ {\it{k\/}}))
\end{tabbing}


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


\begin{verbatim};;; The Witness function for the Computation


\end{verbatim}\begin{tabbing}{\sc Definition}:\index{mchoose}$\;\;$
{\rm{mchoose}}\,({\it{prg\/}}, {\it{i\/}})\index{mchoose} $=$ {\rm{nth}}\,({\it{prg\/}}, {\it{i\/}} ${}${\bf{mod}}${}$ {\rm{length}}\,({\it{prg\/}})\index{length})\index{nth}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{mnext} \\  
\=\+{\rm{mnext}}\,({\it{prg\/}}, {\it{e\/}}, {\it{i\/}})\index{mnext} \\ 
$=$$\;\;\;\;$({\it{i\/}} $+$ \=\+{\bf if }{\rm{position}}\,({\it{prg\/}}, {\it{e\/}})\index{position} $<$ ({\it{i\/}} ${}${\bf{mod}}${}$ {\rm{length}}\,({\it{prg\/}})\index{length}) \\ 
{\bf then }\=\+{\rm{position}}\,({\it{prg\/}}, {\it{e\/}})\index{position} \\ 
$+$$\;\;\;\;$({\rm{length}}\,({\it{prg\/}})\index{length} $-$ ({\it{i\/}} ${}${\bf{mod}}${}$ {\rm{length}}\,({\it{prg\/}})\index{length}))\- \\ 
{\bf else }{\rm{position}}\,({\it{prg\/}}, {\it{e\/}})\index{position} $-$ ({\it{i\/}} ${}${\bf{mod}}${}$ {\rm{length}}\,({\it{prg\/}})\index{length})$\;${\bf  endif}\-)\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mnext-fixes \\ \index{mnext-fixes}
(({\it{e\/}} $\in$ {\it{prg\/}}) $\wedge$ ({\it{i\/}} $\not\in\;${\bf{N}}${}$)) $\rightarrow$ ({\rm{mnext}}\,({\it{prg\/}}, {\it{e\/}}, {\it{i\/}})\index{mnext} $=$ {\rm{mnext}}\,({\it{prg\/}}, {\it{e\/}}, {\tt{0}})\index{mnext})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  numberp-mnext \\ \index{numberp-mnext}
({\it{e\/}} $\in$ {\it{prg\/}}) $\rightarrow$ ({\rm{mnext}}\,({\it{prg\/}}, {\it{e\/}}, {\it{i\/}})\index{mnext} $\in\;${\bf{N}}${}$)
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  mchoose-chooses \\ \index{mchoose-chooses}
{\rm{listp}}\,({\it{prg\/}}) $\rightarrow$ ({\rm{mchoose}}\,({\it{prg\/}}, {\it{i\/}})\index{mchoose} $\in$ {\it{prg\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mchoose-fixes \\ \index{mchoose-fixes}
({\rm{listp}}\,({\it{prg\/}}) $\wedge$ ({\it{i\/}} $\not\in\;${\bf{N}}${}$)) $\rightarrow$ ({\rm{mchoose}}\,({\it{prg\/}}, {\it{i\/}})\index{mchoose} $=$ {\rm{mchoose}}\,({\it{prg\/}}, {\tt{0}})\index{mchoose})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mnext-choice-1 \\ \index{mnext-choice-1}
({\it{e\/}} $\in$ {\it{prg\/}}) $\rightarrow$ ({\rm{mnext}}\,({\it{prg\/}}, {\it{e\/}}, {\it{i\/}})\index{mnext} $\not<$ {\it{i\/}})
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  mnext-choice-2-simplified \\ \index{mnext-choice-2-simplified}
\=\+({\it{e\/}} $<$ {\it{n\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+({\it{i\/}} $+$ \=\+{\bf if }{\it{e\/}} $<$ ({\it{i\/}} ${}${\bf{mod}}${}$ {\it{n\/}})$\;\;${\bf then }{\it{e\/}} $+$ ({\it{n\/}} $-$ ({\it{i\/}} ${}${\bf{mod}}${}$ {\it{n\/}})) \\ 
{\bf else }{\it{e\/}} $-$ ({\it{i\/}} ${}${\bf{mod}}${}$ {\it{n\/}})$\;${\bf  endif}\-) \\ 
${}${\bf{mod}}${}$$\;\;\;\;${\it{n\/}})\- \\ 
$=$$\;\;\;\;${\rm{fix}}\,({\it{e\/}}))\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  mnext-choice-2 \\ \index{mnext-choice-2}
({\it{e\/}} $\in$ {\it{prg\/}}) $\rightarrow$ ({\rm{mchoose}}\,({\it{prg\/}}, {\rm{mnext}}\,({\it{prg\/}}, {\it{e\/}}, {\it{i\/}})\index{mnext})\index{mchoose} $=$ {\it{e\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-of-add1 \\ \index{remainder-of-add1}
\=\+(({\it{x\/}} $<$ ({\it{a\/}} ${}${\bf{mod}}${}$ {\it{b\/}})) $\wedge$ ({\it{x\/}} $<$ (($1\;+$ {\it{a\/}}) ${}${\bf{mod}}${}$ {\it{b\/}}))) \\ 
$\rightarrow$$\;\;\;\;$((($1\;+$ {\it{a\/}}) ${}${\bf{mod}}${}$ {\it{b\/}}) $=$ ($1\;+$ ({\it{a\/}} ${}${\bf{mod}}${}$ {\it{b\/}})))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-of-add1-1 \\ \index{remainder-of-add1-1}
(({\it{x\/}} $\not<$ ({\it{a\/}} ${}${\bf{mod}}${}$ {\it{b\/}})) $\wedge$ ({\it{x\/}} $<$ (($1\;+$ {\it{a\/}}) ${}${\bf{mod}}${}$ {\it{b\/}}))) $\rightarrow$ (({\it{a\/}} ${}${\bf{mod}}${}$ {\it{b\/}}) $=$ {\rm{fix}}\,({\it{x\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-of-add1-2 \\ \index{remainder-of-add1-2}
\=\+(({\it{x\/}} $<$ ({\it{a\/}} ${}${\bf{mod}}${}$ {\it{b\/}})) $\wedge$ ({\it{x\/}} $\not<$ (($1\;+$ {\it{a\/}}) ${}${\bf{mod}}${}$ {\it{b\/}}))) \\ 
$\rightarrow$$\;\;\;\;$(((($1\;+$ {\it{a\/}}) ${}${\bf{mod}}${}$ {\it{b\/}}) $=$ {\tt{0}}) $\wedge$ (({\it{a\/}} ${}${\bf{mod}}${}$ {\it{b\/}}) $=$ ({\it{b\/}} $-\;1$)))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-of-add1-3 \\ \index{remainder-of-add1-3}
\=\+(\=\+({\it{x\/}} $\not<$ ({\it{a\/}} ${}${\bf{mod}}${}$ {\it{b\/}})) \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $<$ {\it{b\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\not=$ ({\it{a\/}} ${}${\bf{mod}}${}$ {\it{b\/}})) \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\not<$ (($1\;+$ {\it{a\/}}) ${}${\bf{mod}}${}$ {\it{b\/}})))\- \\ 
$\rightarrow$$\;\;\;\;$((($1\;+$ {\it{a\/}}) ${}${\bf{mod}}${}$ {\it{b\/}}) $=$ ($1\;+$ ({\it{a\/}} ${}${\bf{mod}}${}$ {\it{b\/}})))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-of-add1-3-1 \\ \index{remainder-of-add1-3-1}
\=\+(\=\+({\rm{position}}\,({\it{prg\/}}, {\it{e\/}})\index{position} $\not<$ ({\it{i\/}} ${}${\bf{mod}}${}$ {\rm{length}}\,({\it{prg\/}})\index{length})) \\ 
$\wedge$$\;\;\;\;$({\rm{position}}\,({\it{prg\/}}, {\it{e\/}})\index{position} $\not<$ (($1\;+$ {\it{i\/}}) ${}${\bf{mod}}${}$ {\rm{length}}\,({\it{prg\/}})\index{length})) \\ 
$\wedge$$\;\;\;\;$({\rm{nth}}\,({\it{prg\/}}, {\it{i\/}} ${}${\bf{mod}}${}$ {\rm{length}}\,({\it{prg\/}})\index{length})\index{nth} $\not=$ {\it{e\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{e\/}} $\in$ {\it{prg\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$((($1\;+$ {\it{i\/}}) ${}${\bf{mod}}${}$ {\rm{length}}\,({\it{prg\/}})\index{length}) $=$ ($1\;+$ ({\it{i\/}} ${}${\bf{mod}}${}$ {\rm{length}}\,({\it{prg\/}})\index{length})))\-
\end{tabbing}
			   		       

\noindent{\sc Event}:   Disable mchoose.

\addvspace{18pt}

\noindent{\sc Event}:   Disable mnext.

\addvspace{18pt}

\begin{verbatim};;; The Statement Interpreter 

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{n} \\  
{\rm{n}}\,({\it{old\/}}, {\it{new\/}}, {\it{e\/}})\index{n} $=$ {\rm{apply\$}}\,({\rm{car}}\,({\it{e\/}}), {\rm{append}}\,({\rm{list}}\,({\it{old\/}}, {\it{new\/}}), {\rm{cdr}}\,({\it{e\/}})))
\end{tabbing}


\begin{tabbing}{\sc Definition}:\index{exists-successor}$\;\;$
{\rm{exists-successor}}\,({\it{old\/}}, {\it{e\/}})\index{exists-successor} $\leftrightarrow$ $\exists\;${\it{new\/}}$\;${\rm{n}}\,({\it{old\/}}, {\it{new\/}}, {\it{e\/}})\index{n}\index{exists}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  exists-successor-implies \\ \index{exists-successor-implies}
{\rm{exists-successor}}\,({\it{old\/}}, {\it{e\/}})\index{exists-successor} $\rightarrow$ {\rm{n}}\,({\it{old\/}}, {\rm{newx}}\,({\it{e\/}}, {\it{old\/}})\index{newx}, {\it{e\/}})\index{n}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  prove-exists-successor \\ \index{prove-exists-successor}
{\rm{n}}\,({\it{old\/}}, {\it{new\/}}, {\it{e\/}})\index{n} $\rightarrow$ {\rm{exists-successor}}\,({\it{old\/}}, {\it{e\/}})\index{exists-successor}
\end{tabbing}


\noindent{\sc Event}:   Disable exists-successor.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{ms} \\  
\=\+{\rm{ms}}\,({\it{prg\/}}, {\it{i\/}})\index{ms} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }{\rm{n}}\,(\=\+{\rm{ms}}\,({\it{prg\/}}, {\it{i\/}} $-\;1$)\index{ms}, \\ 
{\rm{newx}}\,({\rm{mchoose}}\,({\it{prg\/}}, {\it{i\/}} $-\;1$)\index{mchoose}, {\rm{ms}}\,({\it{prg\/}}, {\it{i\/}} $-\;1$)\index{ms})\index{newx}, \\ 
{\rm{mchoose}}\,({\it{prg\/}}, {\it{i\/}} $-\;1$)\index{mchoose})\-\index{n} \\ 
{\bf then }{\rm{newx}}\,({\rm{mchoose}}\,({\it{prg\/}}, {\it{i\/}} $-\;1$)\index{mchoose}, {\rm{ms}}\,({\it{prg\/}}, {\it{i\/}} $-\;1$)\index{ms})\index{newx} \\ 
{\bf else }{\rm{ms}}\,({\it{prg\/}}, {\it{i\/}} $-\;1$)\index{ms}$\;${\bf  endif}\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  ms-transition-successful \\ \index{ms-transition-successful}
\=\+({\rm{listp}}\,({\it{prg\/}}) $\wedge$ {\rm{n}}\,({\rm{ms}}\,({\it{prg\/}}, {\it{i\/}})\index{ms}, {\it{new\/}}, {\rm{mchoose}}\,({\it{prg\/}}, {\it{i\/}})\index{mchoose})\index{n}) \\ 
$\rightarrow$$\;\;\;\;${\rm{n}}\,({\rm{ms}}\,({\it{prg\/}}, {\it{i\/}})\index{ms}, {\rm{ms}}\,({\it{prg\/}}, $1\;+$ {\it{i\/}})\index{ms}, {\rm{mchoose}}\,({\it{prg\/}}, {\it{i\/}})\index{mchoose})\index{n}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ms-transition-idle \\ \index{ms-transition-idle}
\=\+(\=\+{\rm{listp}}\,({\it{prg\/}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{n}}\,({\rm{ms}}\,({\it{prg\/}}, {\it{i\/}})\index{ms}, {\rm{newx}}\,({\rm{mchoose}}\,({\it{prg\/}}, {\it{i\/}})\index{mchoose}, {\rm{ms}}\,({\it{prg\/}}, {\it{i\/}})\index{ms})\index{newx}, {\rm{mchoose}}\,({\it{prg\/}}, {\it{i\/}})\index{mchoose})\index{n}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{ms}}\,({\it{prg\/}}, $1\;+$ {\it{i\/}})\index{ms} $=$ {\rm{ms}}\,({\it{prg\/}}, {\it{i\/}})\index{ms})\-
\end{tabbing}


\begin{verbatim};;; Characterizing an Arbitrary Computation

\end{verbatim}\begin{tabbing}{\sc Conservative Axiom}:  computation \\ \index{computation}
\=\+({\rm{listp}}\,({\it{prg\/}}) $\rightarrow$ ({\rm{choose}}\,({\it{prg\/}}, {\it{i\/}})\index{choose} $\in$ {\it{prg\/}})) \\ 
$\wedge$$\;\;\;\;$(({\it{e\/}} $\in$ {\it{prg\/}}) $\rightarrow$ ({\rm{next}}\,({\it{prg\/}}, {\it{e\/}}, {\it{i\/}})\index{next} $\not<$ {\it{i\/}})) \\ 
$\wedge$$\;\;\;\;$(({\it{e\/}} $\in$ {\it{prg\/}}) $\rightarrow$ ({\rm{choose}}\,({\it{prg\/}}, {\rm{next}}\,({\it{prg\/}}, {\it{e\/}}, {\it{i\/}})\index{next})\index{choose} $=$ {\it{e\/}})) \\ 
$\wedge$$\;\;\;\;$(\=\+({\rm{listp}}\,({\it{prg\/}}) $\wedge$ {\rm{n}}\,({\rm{s}}\,({\it{prg\/}}, {\it{i\/}})\index{s}, {\it{new\/}}, {\rm{choose}}\,({\it{prg\/}}, {\it{i\/}})\index{choose})\index{n}) \\ 
$\rightarrow$$\;\;\;\;${\rm{n}}\,({\rm{s}}\,({\it{prg\/}}, {\it{i\/}})\index{s}, {\rm{s}}\,({\it{prg\/}}, $1\;+$ {\it{i\/}})\index{s}, {\rm{choose}}\,({\it{prg\/}}, {\it{i\/}})\index{choose})\index{n})\- \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\rm{listp}}\,({\it{prg\/}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{n}}\,({\rm{s}}\,({\it{prg\/}}, {\it{i\/}})\index{s}, {\rm{newx}}\,({\rm{choose}}\,({\it{prg\/}}, {\it{i\/}})\index{choose}, {\rm{s}}\,({\it{prg\/}}, {\it{i\/}})\index{s})\index{newx}, {\rm{choose}}\,({\it{prg\/}}, {\it{i\/}})\index{choose})\index{n}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{s}}\,({\it{prg\/}}, $1\;+$ {\it{i\/}})\index{s} $=$ {\rm{s}}\,({\it{prg\/}}, {\it{i\/}})\index{s}))\- \\ 
$\wedge$$\;\;\;\;$(({\it{e\/}} $\in$ {\it{prg\/}}) $\rightarrow$ ({\rm{next}}\,({\it{prg\/}}, {\it{e\/}}, {\it{i\/}})\index{next} $\in\;${\bf{N}}${}$)) \\ 
$\wedge$$\;\;\;\;$(({\rm{listp}}\,({\it{prg\/}}) $\wedge$ ({\it{i\/}} $\not\in\;${\bf{N}}${}$)) $\rightarrow$ ({\rm{s}}\,({\it{prg\/}}, {\it{i\/}})\index{s} $=$ {\rm{s}}\,({\it{prg\/}}, {\tt{0}})\index{s})) \\ 
$\wedge$$\;\;\;\;$(({\rm{listp}}\,({\it{prg\/}}) $\wedge$ ({\it{i\/}} $\not\in\;${\bf{N}}${}$)) $\rightarrow$ ({\rm{choose}}\,({\it{prg\/}}, {\it{i\/}})\index{choose} $=$ {\rm{choose}}\,({\it{prg\/}}, {\tt{0}})\index{choose})) \\ 
$\wedge$$\;\;\;\;$((({\it{e\/}} $\in$ {\it{prg\/}}) $\wedge$ ({\it{i\/}} $\not\in\;${\bf{N}}${}$)) $\rightarrow$ ({\rm{next}}\,({\it{prg\/}}, {\it{e\/}}, {\it{i\/}})\index{next} $=$ {\rm{next}}\,({\it{prg\/}}, {\it{e\/}}, {\tt{0}})\index{next}))\-
\end{tabbing}\noindent Simultaneously, we introduce the new function symbols {\it choose\/}, {\it next\/}, and {\it s\/}.


\noindent{\sc Event}:   Disable mnext-fixes.

\addvspace{18pt}

\noindent{\sc Event}:   Disable numberp-mnext.

\addvspace{18pt}

\noindent{\sc Event}:   Disable mchoose-chooses.

\addvspace{18pt}

\noindent{\sc Event}:   Disable mchoose-fixes.

\addvspace{18pt}

\noindent{\sc Event}:   Disable mnext-choice-1.

\addvspace{18pt}

\noindent{\sc Event}:   Disable mnext-choice-2-simplified.

\addvspace{18pt}

\noindent{\sc Event}:   Disable mnext-choice-2.

\addvspace{18pt}

\noindent{\sc Event}:   Disable remainder-of-add1.

\addvspace{18pt}

\noindent{\sc Event}:   Disable remainder-of-add1-1.

\addvspace{18pt}

\noindent{\sc Event}:   Disable remainder-of-add1-2.

\addvspace{18pt}

\noindent{\sc Event}:   Disable remainder-of-add1-3.

\addvspace{18pt}

\noindent{\sc Event}:   Disable remainder-of-add1-3-1.

\addvspace{18pt}


\noindent{\sc Event}:   Disable exists-successor-implies.

\addvspace{18pt}

\noindent{\sc Event}:   Disable prove-exists-successor.

\addvspace{18pt}

\noindent{\sc Event}:   Disable ms-transition-successful.

\addvspace{18pt}

\noindent{\sc Event}:   Disable ms-transition-idle.

\addvspace{18pt}


\noindent{\sc Event}:   Disable n.

\addvspace{18pt}

\begin{verbatim};;; The Predicate Interpreter

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{eval} \\  
{\rm{eval}}\,({\it{pred\/}}, {\it{state\/}})\index{eval} $=$ {\rm{eval\$}}\,({\bf{t}}, {\it{pred\/}}, {\rm{list}}\,({\rm{cons}}\,({\tt{'}}{\tt{state}}, {\it{state\/}})))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  eval-not \\ \index{eval-not}
{\rm{eval}}\,({\rm{list}}\,({\tt{'}}{\tt{not}}, {\it{p\/}}), {\it{state\/}})\index{eval} $=$ ($\neg$ {\rm{eval}}\,({\it{p\/}}, {\it{state\/}})\index{eval})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  eval-and \\ \index{eval-and}
{\rm{eval}}\,({\rm{list}}\,({\tt{'}}{\tt{and}}, {\it{p\/}}, {\it{q\/}}), {\it{state\/}})\index{eval} $=$ ({\rm{eval}}\,({\it{p\/}}, {\it{state\/}})\index{eval} $\wedge$ {\rm{eval}}\,({\it{q\/}}, {\it{state\/}})\index{eval})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  eval-or \\ \index{eval-or}
{\rm{eval}}\,({\rm{list}}\,({\tt{'}}{\tt{or}}, {\it{p\/}}, {\it{q\/}}), {\it{state\/}})\index{eval} $=$ ({\rm{eval}}\,({\it{p\/}}, {\it{state\/}})\index{eval} $\vee$ {\rm{eval}}\,({\it{q\/}}, {\it{state\/}})\index{eval})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  eval-implies \\ \index{eval-implies}
{\rm{eval}}\,({\rm{list}}\,({\tt{'}}{\tt{implies}}, {\it{p\/}}, {\it{q\/}}), {\it{state\/}})\index{eval} $=$ ({\rm{eval}}\,({\it{p\/}}, {\it{state\/}})\index{eval} $\rightarrow$ {\rm{eval}}\,({\it{q\/}}, {\it{state\/}})\index{eval})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  eval-iff \\ \index{eval-iff}
{\rm{eval}}\,({\rm{list}}\,({\tt{'}}{\tt{iff}}, {\it{p\/}}, {\it{q\/}}), {\it{state\/}})\index{eval} $=$ ({\rm{eval}}\,({\it{p\/}}, {\it{state\/}})\index{eval} $\leftrightarrow$ {\rm{eval}}\,({\it{q\/}}, {\it{state\/}})\index{eval})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  eval-equal \\ \index{eval-equal}
{\rm{eval}}\,({\rm{list}}\,({\tt{'}}{\tt{equal}}, {\it{p\/}}, {\it{q\/}}), {\it{state\/}})\index{eval} $=$ ({\rm{eval}}\,({\it{p\/}}, {\it{state\/}})\index{eval} $=$ {\rm{eval}}\,({\it{q\/}}, {\it{state\/}})\index{eval})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  eval-true \\ \index{eval-true}
{\rm{eval}}\,({\tt{'}}{\tt{(}}{\tt{true}}{\tt{)}}, {\it{state\/}})\index{eval} $=$ {\bf{t}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  eval-false \\ \index{eval-false}
{\rm{eval}}\,({\tt{'}}{\tt{(}}{\tt{false}}{\tt{)}}, {\it{state\/}})\index{eval} $=$ {\bf{f}}
\end{tabbing}


\noindent{\sc Event}:   Disable eval.

\addvspace{18pt}


\begin{verbatim};;; The Stability Operator:  Unless

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{unless} \\  
\=\+{\rm{unless}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{unless} \\ 
$\leftrightarrow$$\;\;\;\;$$\forall\;${\it{old\/}}, {\it{new\/}}, {\it{e\/}}$\;$(\=\+(\=\+({\it{e\/}} $\in$ {\it{prg\/}}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{n}}\,({\it{old\/}}, {\it{new\/}}, {\it{e\/}})\index{n} \\ 
$\wedge$$\;\;\;\;${\rm{eval}}\,({\rm{list}}\,({\tt{'}}{\tt{and}}, {\it{p\/}}, {\rm{list}}\,({\tt{'}}{\tt{not}}, {\it{q\/}})), {\it{old\/}})\index{eval})\-)\- \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\rm{list}}\,({\tt{'}}{\tt{or}}, {\it{p\/}}, {\it{q\/}}), {\it{new\/}})\index{eval})\-\index{forall}\-
\end{tabbing}


\noindent{\sc Event}:   Disable unless.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  prove-unless \\ \index{prove-unless}
\=\+(\=\+(\=\+({\rm{eu}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{eu} $\in$ {\it{prg\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{n}}\,({\rm{oldu}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{oldu}, {\rm{newu}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{newu}, {\rm{eu}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{eu})\index{n} \\ 
$\wedge$$\;\;\;\;${\rm{eval}}\,({\it{p\/}}, {\rm{oldu}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{oldu})\index{eval} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{eval}}\,({\it{q\/}}, {\rm{oldu}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{oldu})\index{eval}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{eval}}\,({\it{p\/}}, {\rm{newu}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{newu})\index{eval} $\vee$ {\rm{eval}}\,({\it{q\/}}, {\rm{newu}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{newu})\index{eval}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{unless}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{unless}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  unless-implies \\ \index{unless-implies}
\=\+(\=\+{\rm{unless}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{unless} \\ 
$\wedge$$\;\;\;\;$({\it{e\/}} $\in$ {\it{prg\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{n}}\,({\it{old\/}}, {\it{new\/}}, {\it{e\/}})\index{n} \\ 
$\wedge$$\;\;\;\;${\rm{eval}}\,({\it{p\/}}, {\it{old\/}})\index{eval} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{eval}}\,({\it{q\/}}, {\it{old\/}})\index{eval}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\rm{list}}\,({\tt{'}}{\tt{or}}, {\it{p\/}}, {\it{q\/}}), {\it{new\/}})\index{eval}\-
\end{tabbing}


\noindent{\sc Event}:   Disable prove-unless.

\addvspace{18pt}

\noindent{\sc Event}:   Disable unless-implies.

\addvspace{18pt}


\begin{verbatim};;; The Progress Operator:  Leads-To

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{leads-to} \\  
\=\+{\rm{leads-to}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{leads-to} \\ 
$\leftrightarrow$$\;\;\;\;$$\forall\;${\it{i\/}}$\;$({\rm{eval}}\,({\it{p\/}}, {\rm{s}}\,({\it{prg\/}}, {\it{i\/}})\index{s})\index{eval} $\rightarrow$ $\exists\;${\it{j\/}}$\;$(({\it{j\/}} $\not<$ {\it{i\/}}) $\wedge$ {\rm{eval}}\,({\it{q\/}}, {\rm{s}}\,({\it{prg\/}}, {\it{j\/}})\index{s})\index{eval})\index{exists})\index{forall}\-
\end{tabbing}


\noindent{\sc Event}:   Disable leads-to.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  prove-leads-to \\ \index{prove-leads-to}
\=\+(\=\+{\rm{eval}}\,({\it{p\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{ileads})\index{s})\index{eval} \\ 
$\rightarrow$$\;\;\;\;$(({\it{j\/}} $\not<$ {\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{ileads}) $\wedge$ {\rm{eval}}\,({\it{q\/}}, {\rm{s}}\,({\it{prg\/}}, {\it{j\/}})\index{s})\index{eval}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  leads-to-implies \\ \index{leads-to-implies}
\=\+({\rm{leads-to}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{leads-to} $\wedge$ {\rm{eval}}\,({\it{p\/}}, {\rm{s}}\,({\it{prg\/}}, {\it{i\/}})\index{s})\index{eval}) \\ 
$\rightarrow$$\;\;\;\;$(({\rm{jleads}}\,({\it{i\/}}, {\it{prg\/}}, {\it{q\/}})\index{jleads} $\not<$ {\it{i\/}}) $\wedge$ {\rm{eval}}\,({\it{q\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jleads}}\,({\it{i\/}}, {\it{prg\/}}, {\it{q\/}})\index{jleads})\index{s})\index{eval})\-
\end{tabbing}


\noindent{\sc Event}:   Disable prove-leads-to.

\addvspace{18pt}

\noindent{\sc Event}:   Disable leads-to-implies.

\addvspace{18pt}

\begin{verbatim};;; The Most Effective Trace

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{schedulable} \\  
{\rm{schedulable}}\,({\it{prg\/}})\index{schedulable} $\leftrightarrow$ $\forall\;${\it{i\/}}$\;$$\exists\;${\it{new\/}}$\;${\rm{n}}\,({\rm{s}}\,({\it{prg\/}}, {\it{i\/}})\index{s}, {\it{new\/}}, {\rm{choose}}\,({\it{prg\/}}, {\it{i\/}})\index{choose})\index{n}\index{exists}\index{forall}
\end{tabbing}


\noindent{\sc Event}:   Disable schedulable.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  prove-schedulable \\ \index{prove-schedulable}
{\rm{n}}\,({\rm{s}}\,({\it{prg\/}}, {\rm{is}}\,({\it{prg\/}})\index{is})\index{s}, {\it{new\/}}, {\rm{choose}}\,({\it{prg\/}}, {\rm{is}}\,({\it{prg\/}})\index{is})\index{choose})\index{n} $\rightarrow$ {\rm{schedulable}}\,({\it{prg\/}})\index{schedulable}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  schedulable-implies \\ \index{schedulable-implies}
{\rm{schedulable}}\,({\it{prg\/}})\index{schedulable} $\rightarrow$ {\rm{n}}\,({\rm{s}}\,({\it{prg\/}}, {\it{i\/}})\index{s}, {\rm{news}}\,({\it{i\/}}, {\it{prg\/}})\index{news}, {\rm{choose}}\,({\it{prg\/}}, {\it{i\/}})\index{choose})\index{n}
\end{tabbing}


\noindent{\sc Event}:   Disable prove-schedulable.

\addvspace{18pt}

\noindent{\sc Event}:   Disable schedulable-implies.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  schedulable-implies-effective-computation \\ \index{schedulable-implies-effective-c!omputation}
\=\+({\rm{schedulable}}\,({\it{prg\/}})\index{schedulable} $\wedge$ {\rm{listp}}\,({\it{prg\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{n}}\,({\rm{s}}\,({\it{prg\/}}, {\it{i\/}})\index{s}, {\rm{s}}\,({\it{prg\/}}, $1\;+$ {\it{i\/}})\index{s}, {\rm{choose}}\,({\it{prg\/}}, {\it{i\/}})\index{choose})\index{n}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  computation-n \\ \index{computation-n}
\=\+({\rm{schedulable}}\,({\it{prg\/}})\index{schedulable} $\wedge$ ({\it{e\/}} $\in$ {\it{prg\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{n}}\,({\rm{s}}\,({\it{prg\/}}, {\rm{next}}\,({\it{prg\/}}, {\it{e\/}}, {\it{i\/}})\index{next})\index{s}, {\rm{s}}\,({\it{prg\/}}, $1\;+$ {\rm{next}}\,({\it{prg\/}}, {\it{e\/}}, {\it{i\/}})\index{next})\index{s}, {\it{e\/}})\index{n}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  effective-idle \\ \index{effective-idle}
\=\+{\rm{listp}}\,({\it{prg\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{s}}\,({\it{prg\/}}, $1\;+$ {\it{i\/}})\index{s} $=$ {\rm{s}}\,({\it{prg\/}}, {\it{i\/}})\index{s}) \\ 
$\vee$$\;\;\;\;${\rm{n}}\,({\rm{s}}\,({\it{prg\/}}, {\it{i\/}})\index{s}, {\rm{s}}\,({\it{prg\/}}, $1\;+$ {\it{i\/}})\index{s}, {\rm{choose}}\,({\it{prg\/}}, {\it{i\/}})\index{choose})\index{n})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable effective-idle.

\addvspace{18pt}

\begin{verbatim};;; Leads-To Proof Rules

\end{verbatim}\begin{tabbing}{\sc Theorem}:  leads-to-transitive \\ \index{leads-to-transitive}
({\rm{leads-to}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{leads-to} $\wedge$ {\rm{leads-to}}\,({\it{q\/}}, {\it{r\/}}, {\it{prg\/}})\index{leads-to}) $\rightarrow$ {\rm{leads-to}}\,({\it{p\/}}, {\it{r\/}}, {\it{prg\/}})\index{leads-to}
\end{tabbing}


\noindent{\sc Event}:   Disable leads-to-transitive.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  leads-to-transitive-general \\ \index{leads-to-transitive-general}
\=\+(\=\+{\rm{leads-to}}\,({\it{p-1\/}}, {\it{q-1\/}}, {\it{prg\/}})\index{leads-to} \\ 
$\wedge$$\;\;\;\;${\rm{leads-to}}\,({\it{q-2\/}}, {\it{r-1\/}}, {\it{prg\/}})\index{leads-to} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{eval}}\,({\it{q-1\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jleads}}\,({\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{r\/}})\index{ileads}, {\it{prg\/}}, {\it{q-1\/}})\index{jleads})\index{s})\index{eval} \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\it{q-2\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jleads}}\,({\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{r\/}})\index{ileads}, {\it{prg\/}}, {\it{q-1\/}})\index{jleads})\index{s})\index{eval})\- \\ 
$\wedge$$\;\;\;\;$({\rm{eval}}\,({\it{p\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{r\/}})\index{ileads})\index{s})\index{eval} $\rightarrow$ {\rm{eval}}\,({\it{p-1\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{r\/}})\index{ileads})\index{s})\index{eval}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{eval}}\,({\it{r-1\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jleads}}\,({\rm{jleads}}\,({\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{r\/}})\index{ileads}, {\it{prg\/}}, {\it{q-1\/}})\index{jleads}, {\it{prg\/}}, {\it{r-1\/}})\index{jleads})\index{s})\index{eval} \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,(\=\+{\it{r\/}}, \\ 
{\rm{s}}\,({\it{prg\/}}, {\rm{jleads}}\,({\rm{jleads}}\,({\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{r\/}})\index{ileads}, {\it{prg\/}}, {\it{q-1\/}})\index{jleads}, {\it{prg\/}}, {\it{r-1\/}})\index{jleads})\index{s})\-\index{eval})\-)\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,({\it{p\/}}, {\it{r\/}}, {\it{prg\/}})\index{leads-to}\-
\end{tabbing}


\noindent{\sc Event}:   Disable leads-to-transitive-general.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  q-leads-to-q \\ \index{q-leads-to-q}
{\rm{leads-to}}\,({\it{q\/}}, {\it{q\/}}, {\it{prg\/}})\index{leads-to}
\end{tabbing}


\noindent{\sc Event}:   Disable q-leads-to-q.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  false-leads-to-anything \\ \index{false-leads-to-anything}
{\rm{leads-to}}\,({\tt{'}}{\tt{(}}{\tt{false}}{\tt{)}}, {\it{p\/}}, {\it{prg\/}})\index{leads-to}
\end{tabbing}


\noindent{\sc Event}:   Disable false-leads-to-anything.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  p-implies-q-leads-to \\ \index{p-implies-q-leads-to}
\=\+({\rm{eval}}\,({\it{p\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{ileads})\index{s})\index{eval} $\rightarrow$ {\rm{eval}}\,({\it{q\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{ileads})\index{s})\index{eval}) \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{leads-to}\-
\end{tabbing}


\noindent{\sc Event}:   Disable p-implies-q-leads-to.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  leads-to-strengthen-left \\ \index{leads-to-strengthen-left}
\=\+(\=\+({\rm{eval}}\,({\it{q\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{ileads}}\,({\it{q\/}}, {\it{prg\/}}, {\it{r\/}})\index{ileads})\index{s})\index{eval} $\rightarrow$ {\rm{eval}}\,({\it{p\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{ileads}}\,({\it{q\/}}, {\it{prg\/}}, {\it{r\/}})\index{ileads})\index{s})\index{eval}) \\ 
$\wedge$$\;\;\;\;${\rm{leads-to}}\,({\it{p\/}}, {\it{r\/}}, {\it{prg\/}})\index{leads-to})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,({\it{q\/}}, {\it{r\/}}, {\it{prg\/}})\index{leads-to}\-
\end{tabbing}


\noindent{\sc Event}:   Disable leads-to-strengthen-left.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  leads-to-weaken-right \\ \index{leads-to-weaken-right}
\=\+(\=\+(\=\+{\rm{eval}}\,({\it{q\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jleads}}\,({\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{r\/}})\index{ileads}, {\it{prg\/}}, {\it{q\/}})\index{jleads})\index{s})\index{eval} \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\it{r\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jleads}}\,({\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{r\/}})\index{ileads}, {\it{prg\/}}, {\it{q\/}})\index{jleads})\index{s})\index{eval})\- \\ 
$\wedge$$\;\;\;\;${\rm{leads-to}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{leads-to})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,({\it{p\/}}, {\it{r\/}}, {\it{prg\/}})\index{leads-to}\-
\end{tabbing}


\noindent{\sc Event}:   Disable leads-to-weaken-right.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  leads-to-modify-both \\ \index{leads-to-modify-both}
\=\+(\=\+({\rm{eval}}\,({\it{p\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{ileads})\index{s})\index{eval} $\rightarrow$ {\rm{eval}}\,({\it{p-1\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{ileads})\index{s})\index{eval}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{eval}}\,({\it{q-1\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jleads}}\,({\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{ileads}, {\it{prg\/}}, {\it{q-1\/}})\index{jleads})\index{s})\index{eval} \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\it{q\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jleads}}\,({\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{ileads}, {\it{prg\/}}, {\it{q-1\/}})\index{jleads})\index{s})\index{eval})\- \\ 
$\wedge$$\;\;\;\;${\rm{leads-to}}\,({\it{p-1\/}}, {\it{q-1\/}}, {\it{prg\/}})\index{leads-to})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{leads-to}\-
\end{tabbing}


\noindent{\sc Event}:   Disable leads-to-modify-both.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  disjoin-left \\ \index{disjoin-left}
\=\+({\rm{leads-to}}\,({\it{p\/}}, {\it{r\/}}, {\it{prg\/}})\index{leads-to} $\wedge$ {\rm{leads-to}}\,({\it{q\/}}, {\it{r\/}}, {\it{prg\/}})\index{leads-to}) \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,({\rm{list}}\,({\tt{'}}{\tt{or}}, {\it{p\/}}, {\it{q\/}}), {\it{r\/}}, {\it{prg\/}})\index{leads-to}\-
\end{tabbing}


\noindent{\sc Event}:   Disable disjoin-left.

\addvspace{18pt}


\begin{tabbing}{\sc Theorem}:  disjoin-left-general \\ \index{disjoin-left-general}
\=\+(\=\+{\rm{leads-to}}\,({\it{p-1\/}}, {\it{q-1\/}}, {\it{prg\/}})\index{leads-to} \\ 
$\wedge$$\;\;\;\;${\rm{leads-to}}\,({\it{p-2\/}}, {\it{q-2\/}}, {\it{prg\/}})\index{leads-to} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{eval}}\,({\it{p\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{ileads})\index{s})\index{eval} \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\rm{list}}\,({\tt{'}}{\tt{or}}, {\it{p-1\/}}, {\it{p-2\/}}), {\rm{s}}\,({\it{prg\/}}, {\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{ileads})\index{s})\index{eval})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{eval}}\,({\it{q-1\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jleads}}\,({\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{ileads}, {\it{prg\/}}, {\it{q-1\/}})\index{jleads})\index{s})\index{eval} \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\it{q\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jleads}}\,({\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{ileads}, {\it{prg\/}}, {\it{q-1\/}})\index{jleads})\index{s})\index{eval})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{eval}}\,({\it{q-2\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jleads}}\,({\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{ileads}, {\it{prg\/}}, {\it{q-2\/}})\index{jleads})\index{s})\index{eval} \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\it{q\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jleads}}\,({\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{ileads}, {\it{prg\/}}, {\it{q-2\/}})\index{jleads})\index{s})\index{eval})\-)\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{leads-to}\-
\end{tabbing}


\noindent{\sc Event}:   Disable disjoin-left-general.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  cancellation-leads-to \\ \index{cancellation-leads-to}
\=\+({\rm{leads-to}}\,({\it{p\/}}, {\rm{list}}\,({\tt{'}}{\tt{or}}, {\it{q\/}}, {\it{b\/}}), {\it{prg\/}})\index{leads-to} $\wedge$ {\rm{leads-to}}\,({\it{b\/}}, {\it{r\/}}, {\it{prg\/}})\index{leads-to}) \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,({\it{p\/}}, {\rm{list}}\,({\tt{'}}{\tt{or}}, {\it{q\/}}, {\it{r\/}}), {\it{prg\/}})\index{leads-to}\-
\end{tabbing}


\noindent{\sc Event}:   Disable cancellation-leads-to.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  cancellation-leads-to-general \\ \index{cancellation-leads-to-general}
\=\+(\=\+{\rm{leads-to}}\,({\it{p-1\/}}, {\it{d\/}}, {\it{prg\/}})\index{leads-to} \\ 
$\wedge$$\;\;\;\;${\rm{leads-to}}\,({\it{b\/}}, {\it{r-1\/}}, {\it{prg\/}})\index{leads-to} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{eval}}\,(\=\+{\rm{list}}\,({\tt{'}}{\tt{and}}, {\it{d\/}}, {\rm{list}}\,({\tt{'}}{\tt{not}}, {\it{b\/}})), \\ 
{\rm{s}}\,({\it{prg\/}}, {\rm{jleads}}\,({\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{r\/}})\index{ileads}, {\it{prg\/}}, {\it{d\/}})\index{jleads})\index{s})\-\index{eval} \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\it{r\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jleads}}\,({\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{r\/}})\index{ileads}, {\it{prg\/}}, {\it{d\/}})\index{jleads})\index{s})\index{eval})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{eval}}\,({\it{r-1\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jleads}}\,({\rm{jleads}}\,({\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{r\/}})\index{ileads}, {\it{prg\/}}, {\it{d\/}})\index{jleads}, {\it{prg\/}}, {\it{r-1\/}})\index{jleads})\index{s})\index{eval} \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\it{r\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jleads}}\,({\rm{jleads}}\,({\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{r\/}})\index{ileads}, {\it{prg\/}}, {\it{d\/}})\index{jleads}, {\it{prg\/}}, {\it{r-1\/}})\index{jleads})\index{s})\index{eval})\- \\ 
$\wedge$$\;\;\;\;$({\rm{eval}}\,({\it{p\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{r\/}})\index{ileads})\index{s})\index{eval} $\rightarrow$ {\rm{eval}}\,({\it{p-1\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{r\/}})\index{ileads})\index{s})\index{eval}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,({\it{p\/}}, {\it{r\/}}, {\it{prg\/}})\index{leads-to}\-
\end{tabbing}


\noindent{\sc Event}:   Disable cancellation-leads-to-general.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{ensures-interval} \\  
\=\+{\rm{ensures-interval}}\,({\it{prg\/}}, {\it{q\/}}, {\it{top\/}}, {\it{i\/}})\index{ensures-interval} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{top\/}} $<$ {\it{i\/}}$\;\;${\bf then }{\rm{fix}}\,({\it{top\/}}) \\ 
{\bf elseif }{\rm{eval}}\,({\it{q\/}}, {\rm{s}}\,({\it{prg\/}}, {\it{i\/}})\index{s})\index{eval}$\;\;${\bf then }{\rm{fix}}\,({\it{i\/}}) \\ 
{\bf else }{\rm{ensures-interval}}\,({\it{prg\/}}, {\it{q\/}}, {\it{top\/}}, $1\;+$ {\it{i\/}})\index{ensures-interval}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ensures-interval-fixes \\ \index{ensures-interval-fixes}
\=\+({\rm{listp}}\,({\it{prg\/}}) $\wedge$ ({\it{i\/}} $\not\in\;${\bf{N}}${}$)) \\ 
$\rightarrow$$\;\;\;\;$({\rm{ensures-interval}}\,({\it{prg\/}}, {\it{q\/}}, {\it{top\/}}, {\it{i\/}})\index{ensures-interval} $=$ {\rm{ensures-interval}}\,({\it{prg\/}}, {\it{q\/}}, {\it{top\/}}, {\tt{0}})\index{ensures-interval})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ensures-interval-bigger \\ \index{ensures-interval-bigger}
({\rm{ensures-interval}}\,({\it{prg\/}}, {\it{q\/}}, {\it{top\/}}, {\it{i\/}})\index{ensures-interval} $<$ {\it{i\/}}) $=$ ({\it{top\/}} $<$ {\it{i\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  psp-proves-something \\ \index{psp-proves-something}
\=\+(\=\+{\rm{leads-to}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{leads-to} \\ 
$\wedge$$\;\;\;\;${\rm{unless}}\,({\it{r\/}}, {\it{b\/}}, {\it{prg\/}})\index{unless} \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{prg\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{eval}}\,({\it{p\/}}, {\rm{s}}\,({\it{prg\/}}, {\it{base\/}})\index{s})\index{eval} \\ 
$\wedge$$\;\;\;\;${\rm{eval}}\,({\it{r\/}}, {\rm{s}}\,({\it{prg\/}}, {\it{i\/}})\index{s})\index{eval} \\ 
$\wedge$$\;\;\;\;$({\rm{jleads}}\,({\it{base\/}}, {\it{prg\/}}, {\it{q\/}})\index{jleads} $<$ {\it{top\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{jleads}}\,({\it{base\/}}, {\it{prg\/}}, {\it{q\/}})\index{jleads} $\not<$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{final\/}} $=$ {\rm{list}}\,({\tt{'}}{\tt{or}}, {\it{q\/}}, {\it{b\/}})))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,(\=\+{\rm{list}}\,({\tt{'}}{\tt{or}}, {\rm{list}}\,({\tt{'}}{\tt{and}}, {\it{q\/}}, {\it{r\/}}), {\it{b\/}}), \\ 
{\rm{s}}\,({\it{prg\/}}, {\rm{ensures-interval}}\,({\it{prg\/}}, {\it{final\/}}, {\it{top\/}}, {\it{i\/}})\index{ensures-interval})\index{s})\-\index{eval}\-
\end{tabbing}


\noindent{\sc Event}:   Disable psp-proves-something.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  psp \\ \index{psp}
\=\+({\rm{leads-to}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{leads-to} $\wedge$ {\rm{unless}}\,({\it{r\/}}, {\it{b\/}}, {\it{prg\/}})\index{unless} $\wedge$ {\rm{listp}}\,({\it{prg\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,({\rm{list}}\,({\tt{'}}{\tt{and}}, {\it{p\/}}, {\it{r\/}}), {\rm{list}}\,({\tt{'}}{\tt{or}}, {\rm{list}}\,({\tt{'}}{\tt{and}}, {\it{q\/}}, {\it{r\/}}), {\it{b\/}}), {\it{prg\/}})\index{leads-to}\-
\end{tabbing}


\noindent{\sc Event}:   Disable psp.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  psp-general \\ \index{psp-general}
\=\+(\=\+{\rm{leads-to}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{leads-to} \\ 
$\wedge$$\;\;\;\;${\rm{unless}}\,({\it{r\/}}, {\it{b\/}}, {\it{prg\/}})\index{unless} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{eval}}\,({\it{pr\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{ileads}}\,({\it{pr\/}}, {\it{prg\/}}, {\it{qb\/}})\index{ileads})\index{s})\index{eval} \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\rm{list}}\,({\tt{'}}{\tt{and}}, {\it{p\/}}, {\it{r\/}}), {\rm{s}}\,({\it{prg\/}}, {\rm{ileads}}\,({\it{pr\/}}, {\it{prg\/}}, {\it{qb\/}})\index{ileads})\index{s})\index{eval})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{eval}}\,(\=\+{\rm{list}}\,({\tt{'}}{\tt{or}}, {\rm{list}}\,({\tt{'}}{\tt{and}}, {\it{q\/}}, {\it{r\/}}), {\it{b\/}}), \\ 
{\rm{s}}\,(\=\+{\it{prg\/}}, \\ 
{\rm{jleads}}\,({\rm{ileads}}\,({\it{pr\/}}, {\it{prg\/}}, {\it{qb\/}})\index{ileads}, {\it{prg\/}}, {\rm{list}}\,({\tt{'}}{\tt{or}}, {\rm{list}}\,({\tt{'}}{\tt{and}}, {\it{q\/}}, {\it{r\/}}), {\it{b\/}}))\index{jleads})\-\index{s})\-\index{eval} \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,(\=\+{\it{qb\/}}, \\ 
{\rm{s}}\,(\=\+{\it{prg\/}}, \\ 
{\rm{jleads}}\,(\=\+{\rm{ileads}}\,({\it{pr\/}}, {\it{prg\/}}, {\it{qb\/}})\index{ileads}, \\ 
{\it{prg\/}}, \\ 
{\rm{list}}\,({\tt{'}}{\tt{or}}, {\rm{list}}\,({\tt{'}}{\tt{and}}, {\it{q\/}}, {\it{r\/}}), {\it{b\/}}))\-\index{jleads})\-\index{s})\-\index{eval})\- \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{prg\/}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,({\it{pr\/}}, {\it{qb\/}}, {\it{prg\/}})\index{leads-to}\-
\end{tabbing}


\noindent{\sc Event}:   Disable psp-general.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  leads-to-true \\ \index{leads-to-true}
{\rm{leads-to}}\,({\it{p\/}}, {\tt{'}}{\tt{(}}{\tt{true}}{\tt{)}}, {\it{prg\/}})\index{leads-to}
\end{tabbing}

\begin{verbatim};;; Initial Condition and Invariants

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{initial-condition}$\;\;$
{\rm{initial-condition}}\,({\it{ic\/}}, {\it{prg\/}})\index{initial-condition} $=$ {\rm{eval}}\,({\it{ic\/}}, {\rm{s}}\,({\it{prg\/}}, {\tt{0}})\index{s})\index{eval}
\end{tabbing}


\noindent{\sc Event}:   Disable initial-condition.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{invariant}$\;\;$
{\rm{invariant}}\,({\it{inv\/}}, {\it{prg\/}})\index{invariant} $\leftrightarrow$ $\forall\;${\it{i\/}}$\;${\rm{eval}}\,({\it{inv\/}}, {\rm{s}}\,({\it{prg\/}}, {\it{i\/}})\index{s})\index{eval}\index{forall}
\end{tabbing}


\noindent{\sc Event}:   Disable invariant.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  prove-invariant \\ \index{prove-invariant}
{\rm{eval}}\,({\it{inv\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{ii}}\,({\it{inv\/}}, {\it{prg\/}})\index{ii})\index{s})\index{eval} $\rightarrow$ {\rm{invariant}}\,({\it{inv\/}}, {\it{prg\/}})\index{invariant}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  invariant-implies \\ \index{invariant-implies}
{\rm{invariant}}\,({\it{inv\/}}, {\it{prg\/}})\index{invariant} $\rightarrow$ {\rm{eval}}\,({\it{inv\/}}, {\rm{s}}\,({\it{prg\/}}, {\it{i\/}})\index{s})\index{eval}
\end{tabbing}


\noindent{\sc Event}:   Disable prove-invariant.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  invariant-consequence \\ \index{invariant-consequence}
\=\+(\=\+{\rm{invariant}}\,({\it{p\/}}, {\it{prg\/}})\index{invariant} \\ 
$\wedge$$\;\;\;\;$({\rm{eval}}\,({\it{p\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{ii}}\,({\it{q\/}}, {\it{prg\/}})\index{ii})\index{s})\index{eval} $\rightarrow$ {\rm{eval}}\,({\it{q\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{ii}}\,({\it{q\/}}, {\it{prg\/}})\index{ii})\index{s})\index{eval}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{invariant}}\,({\it{q\/}}, {\it{prg\/}})\index{invariant}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  invariants-persist-general \\ \index{invariants-persist-general}
\=\+({\rm{unless}}\,({\it{p\/}}, {\tt{'}}{\tt{(}}{\tt{false}}{\tt{)}}, {\it{prg\/}})\index{unless} $\wedge$ {\rm{eval}}\,({\it{p\/}}, {\rm{s}}\,({\it{prg\/}}, {\it{i\/}})\index{s})\index{eval} $\wedge$ {\rm{listp}}\,({\it{prg\/}}) $\wedge$ ({\it{j\/}} $\not<$ {\it{i\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\it{p\/}}, {\rm{s}}\,({\it{prg\/}}, {\it{j\/}})\index{s})\index{eval}\-
\end{tabbing}


\noindent{\sc Event}:   Disable invariants-persist-general.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  unless-proves-invariant \\ \index{unless-proves-invariant}
\=\+(\=\+{\rm{initial-condition}}\,({\it{ic\/}}, {\it{prg\/}})\index{initial-condition} \\ 
$\wedge$$\;\;\;\;${\rm{unless}}\,({\it{p\/}}, {\tt{'}}{\tt{(}}{\tt{false}}{\tt{)}}, {\it{prg\/}})\index{unless} \\ 
$\wedge$$\;\;\;\;$({\rm{eval}}\,({\it{ic\/}}, {\rm{s}}\,({\it{prg\/}}, {\tt{0}})\index{s})\index{eval} $\rightarrow$ {\rm{eval}}\,({\it{p\/}}, {\rm{s}}\,({\it{prg\/}}, {\tt{0}})\index{s})\index{eval}) \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{prg\/}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{invariant}}\,({\it{p\/}}, {\it{prg\/}})\index{invariant}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  leads-to-false-invariant \\ \index{leads-to-false-invariant}
\=\+(\=\+{\rm{leads-to}}\,({\it{p\/}}, {\tt{'}}{\tt{(}}{\tt{false}}{\tt{)}}, {\it{prg\/}})\index{leads-to} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{eval}}\,({\rm{list}}\,({\tt{'}}{\tt{not}}, {\it{p\/}}), {\rm{s}}\,({\it{prg\/}}, {\rm{ii}}\,({\it{inv\/}}, {\it{prg\/}})\index{ii})\index{s})\index{eval} \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\it{inv\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{ii}}\,({\it{inv\/}}, {\it{prg\/}})\index{ii})\index{s})\index{eval})\-)\- \\ 
$\rightarrow$$\;\;\;\;${\rm{invariant}}\,({\it{inv\/}}, {\it{prg\/}})\index{invariant}\-
\end{tabbing}

\begin{verbatim};;; Eventual Stability


\end{verbatim}\begin{tabbing}{\sc Definition}:\index{eventually-stable} \\  
{\rm{eventually-stable}}\,({\it{r\/}}, {\it{prg\/}})\index{eventually-stable} $\leftrightarrow$ $\exists\;${\it{i\/}}$\;$$\forall\;${\it{j\/}}$\;$(({\it{j\/}} $\not<$ {\it{i\/}}) $\rightarrow$ {\rm{eval}}\,({\it{r\/}}, {\rm{s}}\,({\it{prg\/}}, {\it{j\/}})\index{s})\index{eval})\index{forall}\index{exists}
\end{tabbing}


\noindent{\sc Event}:   Disable eventually-stable.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  prove-eventually-stable \\ \index{prove-eventually-stable}
\=\+(({\rm{jes}}\,({\it{i\/}}, {\it{prg\/}}, {\it{r\/}})\index{jes} $\not<$ {\it{i\/}}) $\rightarrow$ {\rm{eval}}\,({\it{r\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jes}}\,({\it{i\/}}, {\it{prg\/}}, {\it{r\/}})\index{jes})\index{s})\index{eval}) \\ 
$\rightarrow$$\;\;\;\;${\rm{eventually-stable}}\,({\it{r\/}}, {\it{prg\/}})\index{eventually-stable}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  eventually-stable-implies \\ \index{eventually-stable-implies}
({\rm{eventually-stable}}\,({\it{r\/}}, {\it{prg\/}})\index{eventually-stable} $\wedge$ ({\it{j\/}} $\not<$ {\rm{ies}}\,({\it{prg\/}}, {\it{r\/}})\index{ies})) $\rightarrow$ {\rm{eval}}\,({\it{r\/}}, {\rm{s}}\,({\it{prg\/}}, {\it{j\/}})\index{s})\index{eval}
\end{tabbing}


\noindent{\sc Event}:   Disable prove-eventually-stable.

\addvspace{18pt}

\noindent{\sc Event}:   Disable eventually-stable-implies.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  not-leads-to-proves-eventually-stable \\ \index{not-leads-to-proves-eventually-!stable}
\=\+(\=\+($\neg$ {\rm{leads-to}}\,({\it{p\/}}, {\it{not-r\/}}, {\it{prg\/}})\index{leads-to}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{eval}}\,({\it{not-r\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jes}}\,({\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{not-r\/}})\index{ileads}, {\it{prg\/}}, {\it{r\/}})\index{jes})\index{s})\index{eval}) \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\it{r\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jes}}\,({\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{not-r\/}})\index{ileads}, {\it{prg\/}}, {\it{r\/}})\index{jes})\index{s})\index{eval})\-)\- \\ 
$\rightarrow$$\;\;\;\;${\rm{eventually-stable}}\,({\it{r\/}}, {\it{prg\/}})\index{eventually-stable}\-
\end{tabbing}


\noindent{\sc Event}:   Disable not-leads-to-proves-eventually-stable.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  not-eventually-stable-proves-leads-to \\ \index{not-eventually-stable-proves-le!ads-to}
\=\+(\=\+($\neg$ {\rm{eventually-stable}}\,({\it{not-q\/}}, {\it{prg\/}})\index{eventually-stable}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{eval}}\,({\it{not-q\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jes}}\,({\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{ileads}, {\it{prg\/}}, {\it{not-q\/}})\index{jes})\index{s})\index{eval}) \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\it{q\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jes}}\,({\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{ileads}, {\it{prg\/}}, {\it{not-q\/}})\index{jes})\index{s})\index{eval})\-)\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{leads-to}\-
\end{tabbing}


\noindent{\sc Event}:   Disable not-eventually-stable-proves-leads-to.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  true-leads-to-proves-not-eventually-stable \\ \index{true-leads-to-proves-not-eventu!ally-stable}
\=\+(\=\+{\rm{leads-to}}\,({\tt{'}}{\tt{(}}{\tt{true}}{\tt{)}}, {\it{not-r\/}}, {\it{prg\/}})\index{leads-to} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{eval}}\,({\it{not-r\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jleads}}\,({\rm{ies}}\,({\it{prg\/}}, {\it{r\/}})\index{ies}, {\it{prg\/}}, {\it{not-r\/}})\index{jleads})\index{s})\index{eval} \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{eval}}\,({\it{r\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jleads}}\,({\rm{ies}}\,({\it{prg\/}}, {\it{r\/}})\index{ies}, {\it{prg\/}}, {\it{not-r\/}})\index{jleads})\index{s})\index{eval}))\-)\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{eventually-stable}}\,({\it{r\/}}, {\it{prg\/}})\index{eventually-stable})\-
\end{tabbing}


\noindent{\sc Event}:   Disable true-leads-to-proves-not-eventually-stable.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  eventually-stable-proves-not-true-leads-to \\ \index{eventually-stable-proves-not-tr!ue-leads-to}
\=\+(\=\+{\rm{eventually-stable}}\,({\it{not-q\/}}, {\it{prg\/}})\index{eventually-stable} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{eval}}\,({\it{not-q\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jleads}}\,({\rm{ies}}\,({\it{prg\/}}, {\it{not-q\/}})\index{ies}, {\it{prg\/}}, {\it{q\/}})\index{jleads})\index{s})\index{eval} \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{eval}}\,({\it{q\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jleads}}\,({\rm{ies}}\,({\it{prg\/}}, {\it{not-q\/}})\index{ies}, {\it{prg\/}}, {\it{q\/}})\index{jleads})\index{s})\index{eval}))\-)\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{leads-to}}\,({\tt{'}}{\tt{(}}{\tt{true}}{\tt{)}}, {\it{q\/}}, {\it{prg\/}})\index{leads-to})\-
\end{tabbing}


\noindent{\sc Event}:   Disable eventually-stable-proves-not-true-leads-to.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  eventually-stable-weaken \\ \index{eventually-stable-weaken}
\=\+(\=\+{\rm{eventually-stable}}\,({\it{p\/}}, {\it{prg\/}})\index{eventually-stable} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{eval}}\,({\it{p\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jes}}\,({\rm{ies}}\,({\it{prg\/}}, {\it{p\/}})\index{ies}, {\it{prg\/}}, {\it{r\/}})\index{jes})\index{s})\index{eval} \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\it{r\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jes}}\,({\rm{ies}}\,({\it{prg\/}}, {\it{p\/}})\index{ies}, {\it{prg\/}}, {\it{r\/}})\index{jes})\index{s})\index{eval})\-)\- \\ 
$\rightarrow$$\;\;\;\;${\rm{eventually-stable}}\,({\it{r\/}}, {\it{prg\/}})\index{eventually-stable}\-
\end{tabbing}


\noindent{\sc Event}:   Disable eventually-stable-weaken.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  eventually-stable-conjunction \\ \index{eventually-stable-conjunction}
\=\+(\=\+{\rm{eventually-stable}}\,({\it{p\/}}, {\it{prg\/}})\index{eventually-stable} \\ 
$\wedge$$\;\;\;\;${\rm{eventually-stable}}\,({\it{q\/}}, {\it{prg\/}})\index{eventually-stable} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{eval}}\,(\=\+{\rm{list}}\,({\tt{'}}{\tt{and}}, {\it{p\/}}, {\it{q\/}}), \\ 
{\rm{s}}\,(\=\+{\it{prg\/}}, \\ 
{\rm{jes}}\,(\=\+\=\+{\bf if }{\rm{ies}}\,({\it{prg\/}}, {\it{p\/}})\index{ies} $<$ {\rm{ies}}\,({\it{prg\/}}, {\it{q\/}})\index{ies}$\;\;${\bf then }{\rm{ies}}\,({\it{prg\/}}, {\it{q\/}})\index{ies} \\ 
{\bf else }{\rm{ies}}\,({\it{prg\/}}, {\it{p\/}})\index{ies}$\;${\bf  endif}\-, \\ 
{\it{prg\/}}, \\ 
{\it{r\/}})\-\index{jes})\-\index{s})\-\index{eval} \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,(\=\+{\it{r\/}}, \\ 
{\rm{s}}\,(\=\+{\it{prg\/}}, \\ 
{\rm{jes}}\,(\=\+\=\+{\bf if }{\rm{ies}}\,({\it{prg\/}}, {\it{p\/}})\index{ies} $<$ {\rm{ies}}\,({\it{prg\/}}, {\it{q\/}})\index{ies}$\;\;${\bf then }{\rm{ies}}\,({\it{prg\/}}, {\it{q\/}})\index{ies} \\ 
{\bf else }{\rm{ies}}\,({\it{prg\/}}, {\it{p\/}})\index{ies}$\;${\bf  endif}\-, \\ 
{\it{prg\/}}, \\ 
{\it{r\/}})\-\index{jes})\-\index{s})\-\index{eval})\-)\- \\ 
$\rightarrow$$\;\;\;\;${\rm{eventually-stable}}\,({\it{r\/}}, {\it{prg\/}})\index{eventually-stable}\-
\end{tabbing}


\noindent{\sc Event}:   Disable eventually-stable-conjunction.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  eventually-stable-false \\ \index{eventually-stable-false}
\=\+(\=\+{\rm{leads-to}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{leads-to} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{eval}}\,({\it{q\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jleads}}\,({\rm{ies}}\,({\it{prg\/}}, {\it{p\/}})\index{ies}, {\it{prg\/}}, {\it{q\/}})\index{jleads})\index{s})\index{eval} \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{eval}}\,({\it{p\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jleads}}\,({\rm{ies}}\,({\it{prg\/}}, {\it{p\/}})\index{ies}, {\it{prg\/}}, {\it{q\/}})\index{jleads})\index{s})\index{eval}))\-)\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{eventually-stable}}\,({\it{p\/}}, {\it{prg\/}})\index{eventually-stable})\-
\end{tabbing}


\noindent{\sc Event}:   Disable eventually-stable-false.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  stable-occurs-proves-eventually-stable \\ \index{stable-occurs-proves-eventually!-stable}
\=\+({\rm{listp}}\,({\it{prg\/}}) $\wedge$ {\rm{unless}}\,({\it{p\/}}, {\tt{'}}{\tt{(}}{\tt{false}}{\tt{)}}, {\it{prg\/}})\index{unless} $\wedge$ {\rm{leads-to}}\,({\tt{'}}{\tt{(}}{\tt{true}}{\tt{)}}, {\it{p\/}}, {\it{prg\/}})\index{leads-to}) \\ 
$\rightarrow$$\;\;\;\;${\rm{eventually-stable}}\,({\it{p\/}}, {\it{prg\/}})\index{eventually-stable}\-
\end{tabbing}


\noindent{\sc Event}:   Disable stable-occurs-proves-eventually-stable.

\addvspace{18pt}



\begin{verbatim};;; The Basic Ensures Operator 

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{ensures} \\  
\=\+{\rm{ensures}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{ensures} \\ 
$\leftrightarrow$$\;\;\;\;$$\exists\;${\it{e\/}}$\;$(\=\+({\it{e\/}} $\in$ {\it{prg\/}}) \\ 
$\wedge$$\;\;\;\;$$\forall\;${\it{old\/}}, {\it{new\/}}$\;$(\=\+(\=\+{\rm{n}}\,({\it{old\/}}, {\it{new\/}}, {\it{e\/}})\index{n} \\ 
$\wedge$$\;\;\;\;${\rm{eval}}\,({\rm{list}}\,({\tt{'}}{\tt{and}}, {\it{p\/}}, {\rm{list}}\,({\tt{'}}{\tt{not}}, {\it{q\/}})), {\it{old\/}})\index{eval})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\it{q\/}}, {\it{new\/}})\index{eval})\-\index{forall})\-\index{exists}\-
\end{tabbing}


\noindent{\sc Event}:   Disable ensures.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  prove-ensures \\ \index{prove-ensures}
\=\+(\=\+({\it{e\/}} $\in$ {\it{prg\/}}) \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\rm{n}}\,({\rm{olde}}\,({\it{e\/}}, {\it{p\/}}, {\it{q\/}})\index{olde}, {\rm{newe}}\,({\it{e\/}}, {\it{p\/}}, {\it{q\/}})\index{newe}, {\it{e\/}})\index{n} \\ 
$\wedge$$\;\;\;\;${\rm{eval}}\,({\it{p\/}}, {\rm{olde}}\,({\it{e\/}}, {\it{p\/}}, {\it{q\/}})\index{olde})\index{eval} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{eval}}\,({\it{q\/}}, {\rm{olde}}\,({\it{e\/}}, {\it{p\/}}, {\it{q\/}})\index{olde})\index{eval}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\it{q\/}}, {\rm{newe}}\,({\it{e\/}}, {\it{p\/}}, {\it{q\/}})\index{newe})\index{eval})\-)\- \\ 
$\rightarrow$$\;\;\;\;${\rm{ensures}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{ensures}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ensures-implies \\ \index{ensures-implies}
\=\+({\rm{ensures}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{ensures} $\rightarrow$ ({\rm{ee}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{ee} $\in$ {\it{prg\/}})) \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\rm{ensures}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{ensures} \\ 
$\wedge$$\;\;\;\;${\rm{n}}\,({\it{old\/}}, {\it{new\/}}, {\rm{ee}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{ee})\index{n} \\ 
$\wedge$$\;\;\;\;${\rm{eval}}\,({\it{p\/}}, {\it{old\/}})\index{eval} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{eval}}\,({\it{q\/}}, {\it{old\/}})\index{eval}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\it{q\/}}, {\it{new\/}})\index{eval})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable prove-ensures.

\addvspace{18pt}

\noindent{\sc Event}:   Disable ensures-implies.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  ensures-proves-something \\ \index{ensures-proves-something}
\=\+(\=\+{\rm{ensures}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{ensures} \\ 
$\wedge$$\;\;\;\;${\rm{unless}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{unless} \\ 
$\wedge$$\;\;\;\;${\rm{schedulable}}\,({\it{prg\/}})\index{schedulable} \\ 
$\wedge$$\;\;\;\;$({\rm{next}}\,({\it{prg\/}}, {\rm{ee}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{ee}, {\it{base\/}})\index{next} $<$ {\it{top\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{next}}\,({\it{prg\/}}, {\rm{ee}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{ee}, {\it{base\/}})\index{next} $\not<$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not<$ {\it{base\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{eval}}\,({\it{p\/}}, {\rm{s}}\,({\it{prg\/}}, {\it{i\/}})\index{s})\index{eval})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\it{q\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{ensures-interval}}\,({\it{prg\/}}, {\it{q\/}}, {\it{top\/}}, {\it{i\/}})\index{ensures-interval})\index{s})\index{eval}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  the-interval-of-ensures \\ \index{the-interval-of-ensures}
\=\+(\=\+{\rm{ensures}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{ensures} \\ 
$\wedge$$\;\;\;\;${\rm{unless}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{unless} \\ 
$\wedge$$\;\;\;\;${\rm{schedulable}}\,({\it{prg\/}})\index{schedulable} \\ 
$\wedge$$\;\;\;\;${\rm{eval}}\,({\it{p\/}}, {\rm{s}}\,({\it{prg\/}}, {\it{i\/}})\index{s})\index{eval})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\it{q\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{ensures-interval}}\,({\it{prg\/}}, {\it{q\/}}, $1\;+$ {\rm{next}}\,({\it{prg\/}}, {\rm{ee}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{ee}, {\it{i\/}})\index{next}, {\it{i\/}})\index{ensures-interval})\index{s})\index{eval}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ensures-proves-leads-to \\ \index{ensures-proves-leads-to}
\=\+({\rm{schedulable}}\,({\it{prg\/}})\index{schedulable} $\wedge$ {\rm{unless}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{unless} $\wedge$ {\rm{ensures}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{ensures}) \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{leads-to}\-
\end{tabbing}


\noindent{\sc Event}:   Disable ensures-proves-something.

\addvspace{18pt}

\noindent{\sc Event}:   Disable the-interval-of-ensures.

\addvspace{18pt}


\noindent{\sc Event}:   Disable ensures-proves-leads-to.

\addvspace{18pt}

\begin{verbatim};;; Total Programs, Statements are Assignments

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{total} \\  
{\rm{total}}\,({\it{prg\/}})\index{total} $\leftrightarrow$ $\forall\;${\it{e\/}}$\;$(({\it{e\/}} $\in$ {\it{prg\/}}) $\rightarrow$ $\forall\;${\it{old\/}}$\;$$\exists\;${\it{new\/}}$\;${\rm{n}}\,({\it{old\/}}, {\it{new\/}}, {\it{e\/}})\index{n}\index{exists}\index{forall})\index{forall}
\end{tabbing}


\noindent{\sc Event}:   Disable total.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  prove-total \\ \index{prove-total}
(({\rm{et}}\,({\it{prg\/}})\index{et} $\in$ {\it{prg\/}}) $\rightarrow$ {\rm{n}}\,({\rm{oldt}}\,({\it{prg\/}})\index{oldt}, {\it{new\/}}, {\rm{et}}\,({\it{prg\/}})\index{et})\index{n}) $\rightarrow$ {\rm{total}}\,({\it{prg\/}})\index{total}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  total-implies \\ \index{total-implies}
({\rm{total}}\,({\it{prg\/}})\index{total} $\wedge$ ({\it{e\/}} $\in$ {\it{prg\/}})) $\rightarrow$ {\rm{n}}\,({\it{old\/}}, {\rm{newt}}\,({\it{e\/}}, {\it{old\/}})\index{newt}, {\it{e\/}})\index{n}
\end{tabbing}


\noindent{\sc Event}:   Disable prove-total.

\addvspace{18pt}

\noindent{\sc Event}:   Disable total-implies.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  total-implies-schedulable \\ \index{total-implies-schedulable}
({\rm{total}}\,({\it{prg\/}})\index{total} $\wedge$ {\rm{listp}}\,({\it{prg\/}})) $\rightarrow$ {\rm{schedulable}}\,({\it{prg\/}})\index{schedulable}
\end{tabbing}


\begin{verbatim};;; Enabled Transitions

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{enabling-condition} \\  
\=\+{\rm{enabling-condition}}\,({\it{c\/}}, {\it{e\/}}, {\it{prg\/}})\index{enabling-condition} \\ 
$\leftrightarrow$$\;\;\;\;$(\=\+({\it{e\/}} $\in$ {\it{prg\/}}) \\ 
$\wedge$$\;\;\;\;$$\forall\;${\it{old\/}}, {\it{new\/}}$\;$({\rm{n}}\,({\it{old\/}}, {\it{new\/}}, {\it{e\/}})\index{n} $\rightarrow$ {\rm{eval}}\,({\it{c\/}}, {\it{old\/}})\index{eval})\index{forall} \\ 
$\wedge$$\;\;\;\;$$\forall\;${\it{old\/}}$\;$({\rm{eval}}\,({\it{c\/}}, {\it{old\/}})\index{eval} $\rightarrow$ $\exists\;${\it{new\/}}$\;${\rm{n}}\,({\it{old\/}}, {\it{new\/}}, {\it{e\/}})\index{n}\index{exists})\index{forall})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable enabling-condition.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  prove-enabling-condition \\ \index{prove-enabling-condition}
\=\+(\=\+({\it{e\/}} $\in$ {\it{prg\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{n}}\,({\rm{oldc}}\,({\it{c\/}}, {\it{e\/}})\index{oldc}, {\rm{newc}}\,({\it{c\/}}, {\it{e\/}})\index{newc}, {\it{e\/}})\index{n} $\rightarrow$ {\rm{eval}}\,({\it{c\/}}, {\rm{oldc}}\,({\it{c\/}}, {\it{e\/}})\index{oldc})\index{eval}) \\ 
$\wedge$$\;\;\;\;$({\rm{eval}}\,({\it{c\/}}, {\rm{oldc-1}}\,({\it{c\/}}, {\it{e\/}})\index{oldc-1})\index{eval} $\rightarrow$ {\rm{n}}\,({\rm{oldc-1}}\,({\it{c\/}}, {\it{e\/}})\index{oldc-1}, {\it{new\/}}, {\it{e\/}})\index{n}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{enabling-condition}}\,({\it{c\/}}, {\it{e\/}}, {\it{prg\/}})\index{enabling-condition}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  enabling-condition-implies \\ \index{enabling-condition-implies}
\=\+({\rm{enabling-condition}}\,({\it{c\/}}, {\it{e\/}}, {\it{prg\/}})\index{enabling-condition} $\rightarrow$ ({\it{e\/}} $\in$ {\it{prg\/}})) \\ 
$\wedge$$\;\;\;\;$(({\rm{enabling-condition}}\,({\it{c\/}}, {\it{e\/}}, {\it{prg\/}})\index{enabling-condition} $\wedge$ {\rm{n}}\,({\it{old\/}}, {\it{new\/}}, {\it{e\/}})\index{n}) $\rightarrow$ {\rm{eval}}\,({\it{c\/}}, {\it{old\/}})\index{eval}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\rm{enabling-condition}}\,({\it{c\/}}, {\it{e\/}}, {\it{prg\/}})\index{enabling-condition} $\wedge$ {\rm{eval}}\,({\it{c\/}}, {\it{old\/}})\index{eval}) \\ 
$\rightarrow$$\;\;\;\;${\rm{n}}\,({\it{old\/}}, {\rm{newc-1}}\,({\it{e\/}}, {\it{old\/}})\index{newc-1}, {\it{e\/}})\index{n})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable prove-enabling-condition.

\addvspace{18pt}

\noindent{\sc Event}:   Disable enabling-condition-implies.

\addvspace{18pt}

\begin{verbatim};;; Ensures with Enabling

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{e-ensures} \\  
\=\+{\rm{e-ensures}}\,({\it{p\/}}, {\it{q\/}}, {\it{c\/}}, {\it{prg\/}})\index{e-ensures} \\ 
$\leftrightarrow$$\;\;\;\;$$\exists\;${\it{e\/}}$\;$(\=\+({\it{e\/}} $\in$ {\it{prg\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{enabling-condition}}\,({\it{c\/}}, {\it{e\/}}, {\it{prg\/}})\index{enabling-condition} \\ 
$\wedge$$\;\;\;\;$$\forall\;${\it{old\/}}, {\it{new\/}}$\;$(\=\+(\=\+{\rm{n}}\,({\it{old\/}}, {\it{new\/}}, {\it{e\/}})\index{n} \\ 
$\wedge$$\;\;\;\;${\rm{eval}}\,({\rm{list}}\,({\tt{'}}{\tt{and}}, {\it{p\/}}, {\rm{list}}\,({\tt{'}}{\tt{not}}, {\it{q\/}})), {\it{old\/}})\index{eval})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\it{q\/}}, {\it{new\/}})\index{eval})\-\index{forall})\-\index{exists}\-
\end{tabbing}


\noindent{\sc Event}:   Disable e-ensures.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  prove-e-ensures \\ \index{prove-e-ensures}
\=\+(\=\+({\it{e\/}} $\in$ {\it{prg\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{enabling-condition}}\,({\it{c\/}}, {\it{e\/}}, {\it{prg\/}})\index{enabling-condition} \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\rm{n}}\,({\rm{oldee}}\,({\it{e\/}}, {\it{p\/}}, {\it{q\/}})\index{oldee}, {\rm{newee}}\,({\it{e\/}}, {\it{p\/}}, {\it{q\/}})\index{newee}, {\it{e\/}})\index{n} \\ 
$\wedge$$\;\;\;\;${\rm{eval}}\,({\rm{list}}\,({\tt{'}}{\tt{and}}, {\it{p\/}}, {\rm{list}}\,({\tt{'}}{\tt{not}}, {\it{q\/}})), {\rm{oldee}}\,({\it{e\/}}, {\it{p\/}}, {\it{q\/}})\index{oldee})\index{eval})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\it{q\/}}, {\rm{newee}}\,({\it{e\/}}, {\it{p\/}}, {\it{q\/}})\index{newee})\index{eval})\-)\- \\ 
$\rightarrow$$\;\;\;\;${\rm{e-ensures}}\,({\it{p\/}}, {\it{q\/}}, {\it{c\/}}, {\it{prg\/}})\index{e-ensures}\-
\end{tabbing}


\noindent{\sc Event}:   Disable prove-e-ensures.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{e-ensures-enabling} \\  
\=\+{\rm{e-ensures-enabling}}\,({\it{p\/}}, {\it{q\/}}, {\it{c\/}}, {\it{prg\/}})\index{e-ensures-enabling} \\ 
$\leftrightarrow$$\;\;\;\;$$\exists\;${\it{e\/}}$\;$(\=\+({\it{e\/}} $\in$ {\it{prg\/}}) \\ 
$\wedge$$\;\;\;\;$$\forall\;${\it{old\/}}, {\it{new\/}}$\;$(\=\+({\rm{n}}\,({\it{old\/}}, {\it{new\/}}, {\it{e\/}})\index{n} $\rightarrow$ {\rm{eval}}\,({\it{c\/}}, {\it{old\/}})\index{eval}) \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\rm{n}}\,({\it{old\/}}, {\it{new\/}}, {\it{e\/}})\index{n} \\ 
$\wedge$$\;\;\;\;${\rm{eval}}\,(\=\+{\rm{list}}\,(\=\+{\tt{'}}{\tt{and}}, \\ 
{\it{p\/}}, \\ 
{\rm{list}}\,({\tt{'}}{\tt{not}}, {\it{q\/}}))\-, \\ 
{\it{old\/}})\-\index{eval})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\it{q\/}}, {\it{new\/}})\index{eval})\-)\-\index{forall} \\ 
$\wedge$$\;\;\;\;$$\forall\;${\it{old\/}}$\;$({\rm{eval}}\,({\it{c\/}}, {\it{old\/}})\index{eval} $\rightarrow$ $\exists\;${\it{new\/}}$\;${\rm{n}}\,({\it{old\/}}, {\it{new\/}}, {\it{e\/}})\index{n}\index{exists})\index{forall})\-\index{exists}\-
\end{tabbing}


\noindent{\sc Event}:   Disable e-ensures-enabling.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  help-prove-e-ensures \\ \index{help-prove-e-ensures}
\=\+(\=\+({\it{e\/}} $\in$ {\it{prg\/}}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{n}}\,({\rm{oldeee}}\,({\it{c\/}}, {\it{e\/}}, {\it{p\/}}, {\it{q\/}})\index{oldeee}, {\rm{neweee}}\,({\it{c\/}}, {\it{e\/}}, {\it{p\/}}, {\it{q\/}})\index{neweee}, {\it{e\/}})\index{n} \\ 
$\rightarrow$$\;\;\;\;$({\rm{eval}}\,({\it{c\/}}, {\rm{oldeee}}\,({\it{c\/}}, {\it{e\/}}, {\it{p\/}}, {\it{q\/}})\index{oldeee})\index{eval} $\wedge$ {\rm{eval}}\,({\it{q\/}}, {\rm{neweee}}\,({\it{c\/}}, {\it{e\/}}, {\it{p\/}}, {\it{q\/}})\index{neweee})\index{eval}))\- \\ 
$\wedge$$\;\;\;\;$({\rm{eval}}\,({\it{c\/}}, {\rm{oldeee-1}}\,({\it{c\/}}, {\it{e\/}})\index{oldeee-1})\index{eval} $\rightarrow$ {\rm{n}}\,({\rm{oldeee-1}}\,({\it{c\/}}, {\it{e\/}})\index{oldeee-1}, {\it{new\/}}, {\it{e\/}})\index{n}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{eval}}\,({\it{c\/}}, {\rm{oldeee}}\,({\it{c\/}}, {\it{e\/}}, {\it{p\/}}, {\it{q\/}})\index{oldeee})\index{eval} \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\rm{list}}\,({\tt{'}}{\tt{and}}, {\it{p\/}}, {\rm{list}}\,({\tt{'}}{\tt{not}}, {\it{q\/}})), {\rm{oldeee}}\,({\it{c\/}}, {\it{e\/}}, {\it{p\/}}, {\it{q\/}})\index{oldeee})\index{eval})\-)\- \\ 
$\rightarrow$$\;\;\;\;${\rm{e-ensures}}\,({\it{p\/}}, {\it{q\/}}, {\it{c\/}}, {\it{prg\/}})\index{e-ensures}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  e-ensures-implies \\ \index{e-ensures-implies}
\=\+({\rm{e-ensures}}\,({\it{p\/}}, {\it{q\/}}, {\it{c\/}}, {\it{prg\/}})\index{e-ensures} $\rightarrow$ ({\rm{eee}}\,({\it{c\/}}, {\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{eee} $\in$ {\it{prg\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{e-ensures}}\,({\it{p\/}}, {\it{q\/}}, {\it{c\/}}, {\it{prg\/}})\index{e-ensures} $\rightarrow$ {\rm{enabling-condition}}\,({\it{c\/}}, {\rm{eee}}\,({\it{c\/}}, {\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{eee}, {\it{prg\/}})\index{enabling-condition}) \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\rm{e-ensures}}\,({\it{p\/}}, {\it{q\/}}, {\it{c\/}}, {\it{prg\/}})\index{e-ensures} \\ 
$\wedge$$\;\;\;\;${\rm{n}}\,({\it{old\/}}, {\it{new\/}}, {\rm{eee}}\,({\it{c\/}}, {\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{eee})\index{n} \\ 
$\wedge$$\;\;\;\;${\rm{eval}}\,({\rm{list}}\,({\tt{'}}{\tt{and}}, {\it{p\/}}, {\rm{list}}\,({\tt{'}}{\tt{not}}, {\it{q\/}})), {\it{old\/}})\index{eval})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\it{q\/}}, {\it{new\/}})\index{eval})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable e-ensures-implies.

\addvspace{18pt}

\noindent{\sc Event}:   Disable help-prove-e-ensures.

\addvspace{18pt}


\begin{verbatim};;; Union Theorems

\end{verbatim}\begin{tabbing}{\sc Theorem}:  total-union-1 \\ \index{total-union-1}
{\rm{total}}\,({\rm{append}}\,({\it{prg-1\/}}, {\it{prg-2\/}}))\index{total} $\rightarrow$ ({\rm{total}}\,({\it{prg-1\/}})\index{total} $\wedge$ {\rm{total}}\,({\it{prg-2\/}})\index{total})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  total-union-2 \\ \index{total-union-2}
({\rm{total}}\,({\it{prg-1\/}})\index{total} $\wedge$ {\rm{total}}\,({\it{prg-2\/}})\index{total}) $\rightarrow$ {\rm{total}}\,({\rm{append}}\,({\it{prg-1\/}}, {\it{prg-2\/}}))\index{total}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  total-union \\ \index{total-union}
{\rm{total}}\,({\rm{append}}\,({\it{prg-1\/}}, {\it{prg-2\/}}))\index{total} $=$ ({\rm{total}}\,({\it{prg-1\/}})\index{total} $\wedge$ {\rm{total}}\,({\it{prg-2\/}})\index{total})
\end{tabbing}



\noindent{\sc Event}:   Disable total-union-1.

\addvspace{18pt}

\noindent{\sc Event}:   Disable total-union-2.

\addvspace{18pt}


\begin{tabbing}{\sc Theorem}:  unless-union-1 \\ \index{unless-union-1}
\=\+{\rm{unless}}\,({\it{p\/}}, {\it{q\/}}, {\rm{append}}\,({\it{prg-1\/}}, {\it{prg-2\/}}))\index{unless} \\ 
$\rightarrow$$\;\;\;\;$({\rm{unless}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg-1\/}})\index{unless} $\wedge$ {\rm{unless}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg-2\/}})\index{unless})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  unless-union-2 \\ \index{unless-union-2}
\=\+({\rm{unless}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg-1\/}})\index{unless} $\wedge$ {\rm{unless}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg-2\/}})\index{unless}) \\ 
$\rightarrow$$\;\;\;\;${\rm{unless}}\,({\it{p\/}}, {\it{q\/}}, {\rm{append}}\,({\it{prg-1\/}}, {\it{prg-2\/}}))\index{unless}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  unless-union \\ \index{unless-union}
\=\+{\rm{unless}}\,({\it{p\/}}, {\it{q\/}}, {\rm{append}}\,({\it{prg-1\/}}, {\it{prg-2\/}}))\index{unless} \\ 
$=$$\;\;\;\;$({\rm{unless}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg-1\/}})\index{unless} $\wedge$ {\rm{unless}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg-2\/}})\index{unless})\-
\end{tabbing}


\noindent{\sc Event}:   Disable unless-union-1.

\addvspace{18pt}

\noindent{\sc Event}:   Disable unless-union-2.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  ensures-union-1 \\ \index{ensures-union-1}
\=\+{\rm{ensures}}\,({\it{p\/}}, {\it{q\/}}, {\rm{append}}\,({\it{prg-1\/}}, {\it{prg-2\/}}))\index{ensures} \\ 
$\rightarrow$$\;\;\;\;$({\rm{ensures}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg-1\/}})\index{ensures} $\vee$ {\rm{ensures}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg-2\/}})\index{ensures})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ensures-union-2 \\ \index{ensures-union-2}
\=\+({\rm{ensures}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg-1\/}})\index{ensures} $\vee$ {\rm{ensures}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg-2\/}})\index{ensures}) \\ 
$\rightarrow$$\;\;\;\;${\rm{ensures}}\,({\it{p\/}}, {\it{q\/}}, {\rm{append}}\,({\it{prg-1\/}}, {\it{prg-2\/}}))\index{ensures}\-
\end{tabbing}



\noindent{\sc Event}:   Disable ensures-union-1.

\addvspace{18pt}

\noindent{\sc Event}:   Disable ensures-union-2.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  ensures-union \\ \index{ensures-union}
\=\+{\rm{ensures}}\,({\it{p\/}}, {\it{q\/}}, {\rm{append}}\,({\it{prg-1\/}}, {\it{prg-2\/}}))\index{ensures} \\ 
$=$$\;\;\;\;$({\rm{ensures}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg-1\/}})\index{ensures} $\vee$ {\rm{ensures}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg-2\/}})\index{ensures})\-
\end{tabbing}



\begin{verbatim};;; Help Prove Total, Unless, and Ensures.


\end{verbatim}\begin{tabbing}{\sc Definition}:\index{total-sufficient} \\  
\=\+{\rm{total-sufficient}}\,({\it{statement\/}}, {\it{program\/}}, {\it{old\/}}, {\it{new\/}})\index{total-sufficient} \\ 
$=$$\;\;\;\;$(({\it{statement\/}} $\in$ {\it{program\/}}) $\rightarrow$ {\rm{n}}\,({\it{old\/}}, {\it{new\/}}, {\it{statement\/}})\index{n})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  help-prove-total \\ \index{help-prove-total}
{\rm{total-sufficient}}\,({\rm{et}}\,({\it{prg\/}})\index{et}, {\it{prg\/}}, {\rm{oldt}}\,({\it{prg\/}})\index{oldt}, {\it{new\/}})\index{total-sufficient} $\rightarrow$ {\rm{total}}\,({\it{prg\/}})\index{total}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{unless-sufficient} \\  
\=\+{\rm{unless-sufficient}}\,({\it{statement\/}}, {\it{program\/}}, {\it{old\/}}, {\it{new\/}}, {\it{p\/}}, {\it{q\/}})\index{unless-sufficient} \\ 
$=$$\;\;\;\;$(\=\+(\=\+({\it{statement\/}} $\in$ {\it{program\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{n}}\,({\it{old\/}}, {\it{new\/}}, {\it{statement\/}})\index{n} \\ 
$\wedge$$\;\;\;\;${\rm{eval}}\,({\it{p\/}}, {\it{old\/}})\index{eval} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{eval}}\,({\it{q\/}}, {\it{old\/}})\index{eval}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\rm{list}}\,({\tt{'}}{\tt{or}}, {\it{p\/}}, {\it{q\/}}), {\it{new\/}})\index{eval})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  help-prove-unless \\ \index{help-prove-unless}
\=\+{\rm{unless-sufficient}}\,({\rm{eu}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{eu}, {\it{prg\/}}, {\rm{oldu}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{oldu}, {\rm{newu}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{newu}, {\it{p\/}}, {\it{q\/}})\index{unless-sufficient} \\ 
$\rightarrow$$\;\;\;\;${\rm{unless}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{unless}\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{ensures-key} \\  
\=\+{\rm{ensures-key}}\,({\it{statement\/}}, {\it{program\/}}, {\it{old\/}}, {\it{new\/}}, {\it{p\/}}, {\it{q\/}})\index{ensures-key} \\ 
$=$$\;\;\;\;$(\=\+({\it{statement\/}} $\in$ {\it{program\/}}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\rm{n}}\,({\it{old\/}}, {\it{new\/}}, {\it{statement\/}})\index{n} $\wedge$ {\rm{eval}}\,({\it{p\/}}, {\it{old\/}})\index{eval} $\wedge$ ($\neg$ {\rm{eval}}\,({\it{q\/}}, {\it{old\/}})\index{eval})) \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\it{q\/}}, {\it{new\/}})\index{eval})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  help-prove-ensures \\ \index{help-prove-ensures}
\=\+{\rm{ensures-key}}\,({\it{statement\/}}, {\it{prg\/}}, {\rm{olde}}\,({\it{statement\/}}, {\it{p\/}}, {\it{q\/}})\index{olde}, {\rm{newe}}\,({\it{statement\/}}, {\it{p\/}}, {\it{q\/}})\index{newe}, {\it{p\/}}, {\it{q\/}})\index{ensures-key} \\ 
$\rightarrow$$\;\;\;\;${\rm{ensures}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{ensures}\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{ensures-rest} \\  
\=\+{\rm{ensures-rest}}\,({\it{statement\/}}, {\it{key\/}}, {\it{program\/}}, {\it{old\/}}, {\it{new\/}}, {\it{p\/}}, {\it{q\/}})\index{ensures-rest} \\ 
$=$$\;\;\;\;$(\=\+(\=\+({\it{statement\/}} $\in$ {\it{program\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{statement\/}} $\not=$ {\it{key\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{n}}\,({\it{old\/}}, {\it{new\/}}, {\it{statement\/}})\index{n} \\ 
$\wedge$$\;\;\;\;${\rm{eval}}\,({\it{p\/}}, {\it{old\/}})\index{eval} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{eval}}\,({\it{q\/}}, {\it{old\/}})\index{eval}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\it{p\/}}, {\it{new\/}})\index{eval})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  help-prove-unless-ensures \\ \index{help-prove-unless-ensures}
\=\+(\=\+{\rm{ensures-key}}\,({\it{statement\/}}, {\it{prg\/}}, {\rm{oldu}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{oldu}, {\rm{newu}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{newu}, {\it{p\/}}, {\it{q\/}})\index{ensures-key} \\ 
$\wedge$$\;\;\;\;${\rm{ensures-rest}}\,(\=\+{\rm{eu}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{eu}, \\ 
{\it{statement\/}}, \\ 
{\it{prg\/}}, \\ 
{\rm{oldu}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{oldu}, \\ 
{\rm{newu}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{newu}, \\ 
{\it{p\/}}, \\ 
{\it{q\/}})\-\index{ensures-rest})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{unless}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{unless}\-
\end{tabbing}


\begin{verbatim};;; Strengthening and Weakening Unless and Ensures

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{stronger-p} \\  
{\rm{stronger-p}}\,({\it{p\/}}, {\it{q\/}})\index{stronger-p} $\leftrightarrow$ $\forall\;${\it{state\/}}$\;$({\rm{eval}}\,({\it{p\/}}, {\it{state\/}})\index{eval} $\rightarrow$ {\rm{eval}}\,({\it{q\/}}, {\it{state\/}})\index{eval})\index{forall}
\end{tabbing}


\noindent{\sc Event}:   Disable stronger-p.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  stronger-p-implies \\ \index{stronger-p-implies}
({\rm{stronger-p}}\,({\it{p\/}}, {\it{q\/}})\index{stronger-p} $\wedge$ {\rm{eval}}\,({\it{p\/}}, {\it{state\/}})\index{eval}) $\rightarrow$ {\rm{eval}}\,({\it{q\/}}, {\it{state\/}})\index{eval}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  stronger-p-rewrite \\ \index{stronger-p-rewrite}
{\rm{stronger-p}}\,({\it{p\/}}, {\it{q\/}})\index{stronger-p} $=$ ({\rm{eval}}\,({\it{p\/}}, {\rm{states}}\,({\it{p\/}}, {\it{q\/}})\index{states})\index{eval} $\rightarrow$ {\rm{eval}}\,({\it{q\/}}, {\rm{states}}\,({\it{p\/}}, {\it{q\/}})\index{states})\index{eval})
\end{tabbing}


\noindent{\sc Event}:   Disable stronger-p-implies.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{equal-p} \\  
{\rm{equal-p}}\,({\it{p\/}}, {\it{q\/}})\index{equal-p} $\leftrightarrow$ $\forall\;${\it{state\/}}$\;$({\rm{eval}}\,({\it{p\/}}, {\it{state\/}})\index{eval} $=$ {\rm{eval}}\,({\it{q\/}}, {\it{state\/}})\index{eval})\index{forall}
\end{tabbing}


\noindent{\sc Event}:   Disable equal-p.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  equal-p-implies \\ \index{equal-p-implies}
{\rm{equal-p}}\,({\it{p\/}}, {\it{q\/}})\index{equal-p} $\rightarrow$ ({\rm{eval}}\,({\it{p\/}}, {\it{state\/}})\index{eval} $=$ {\rm{eval}}\,({\it{q\/}}, {\it{state\/}})\index{eval})
\end{tabbing}


\noindent{\sc Event}:   Disable equal-p-implies.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  equal-p-rewrite \\ \index{equal-p-rewrite}
{\rm{equal-p}}\,({\it{p\/}}, {\it{q\/}})\index{equal-p} $=$ ({\rm{eval}}\,({\it{p\/}}, {\rm{statee}}\,({\it{p\/}}, {\it{q\/}})\index{statee})\index{eval} $=$ {\rm{eval}}\,({\it{q\/}}, {\rm{statee}}\,({\it{p\/}}, {\it{q\/}})\index{statee})\index{eval})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  equal-p-commutative \\ \index{equal-p-commutative}
{\rm{equal-p}}\,({\it{p\/}}, {\it{q\/}})\index{equal-p} $=$ {\rm{equal-p}}\,({\it{q\/}}, {\it{p\/}})\index{equal-p}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ensures-strengthen-left \\ \index{ensures-strengthen-left}
({\rm{ensures}}\,({\it{q\/}}, {\it{r\/}}, {\it{prg\/}})\index{ensures} $\wedge$ {\rm{stronger-p}}\,({\it{p\/}}, {\it{q\/}})\index{stronger-p}) $\rightarrow$ {\rm{ensures}}\,({\it{p\/}}, {\it{r\/}}, {\it{prg\/}})\index{ensures}
\end{tabbing}


\noindent{\sc Event}:   Disable ensures-strengthen-left.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  ensures-weaken-right \\ \index{ensures-weaken-right}
({\rm{ensures}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{ensures} $\wedge$ {\rm{stronger-p}}\,({\it{q\/}}, {\it{r\/}})\index{stronger-p}) $\rightarrow$ {\rm{ensures}}\,({\it{p\/}}, {\it{r\/}}, {\it{prg\/}})\index{ensures}
\end{tabbing}


\noindent{\sc Event}:   Disable ensures-weaken-right.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  unless-weaken-right \\ \index{unless-weaken-right}
({\rm{unless}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{unless} $\wedge$ {\rm{stronger-p}}\,({\it{q\/}}, {\it{r\/}})\index{stronger-p}) $\rightarrow$ {\rm{unless}}\,({\it{p\/}}, {\it{r\/}}, {\it{prg\/}})\index{unless}
\end{tabbing}


\noindent{\sc Event}:   Disable unless-weaken-right.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  unless-equal-p \\ \index{unless-equal-p}
{\rm{equal-p}}\,({\it{p\/}}, {\it{q\/}})\index{equal-p} $\rightarrow$ ({\rm{unless}}\,({\it{p\/}}, {\it{r\/}}, {\it{prg\/}})\index{unless} $=$ {\rm{unless}}\,({\it{q\/}}, {\it{r\/}}, {\it{prg\/}})\index{unless})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  unless-conjunction \\ \index{unless-conjunction}
\=\+({\rm{unless}}\,({\it{p-1\/}}, {\it{q\/}}, {\it{prg\/}})\index{unless} $\wedge$ {\rm{unless}}\,({\it{p-2\/}}, {\it{q\/}}, {\it{prg\/}})\index{unless} $\wedge$ {\rm{equal-p}}\,({\it{p\/}}, {\rm{list}}\,({\tt{'}}{\tt{and}}, {\it{p-1\/}}, {\it{p-2\/}}))\index{equal-p}) \\ 
$\rightarrow$$\;\;\;\;${\rm{unless}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{unless}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  unless-disjunction \\ \index{unless-disjunction}
\=\+({\rm{unless}}\,({\it{p-1\/}}, {\it{q\/}}, {\it{prg\/}})\index{unless} $\wedge$ {\rm{unless}}\,({\it{p-2\/}}, {\it{q\/}}, {\it{prg\/}})\index{unless} $\wedge$ {\rm{equal-p}}\,({\it{p\/}}, {\rm{list}}\,({\tt{'}}{\tt{or}}, {\it{p-1\/}}, {\it{p-2\/}}))\index{equal-p}) \\ 
$\rightarrow$$\;\;\;\;${\rm{unless}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{unless}\-
\end{tabbing}


\begin{verbatim};;; Fairness Theorems


\end{verbatim}\begin{tabbing}{\sc Theorem}:  unconditional-fairness \\ \index{unconditional-fairness}
({\rm{unless}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{unless} $\wedge$ {\rm{ensures}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{ensures} $\wedge$ {\rm{total}}\,({\it{prg\/}})\index{total}) $\rightarrow$ {\rm{leads-to}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{leads-to}
\end{tabbing}


\noindent{\sc Event}:   Disable unconditional-fairness.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  unconditional-fairness-general \\ \index{unconditional-fairness-general}
\=\+(\=\+{\rm{unless}}\,({\it{p-1\/}}, {\it{q-1\/}}, {\it{prg\/}})\index{unless} \\ 
$\wedge$$\;\;\;\;${\rm{ensures}}\,({\it{p-2\/}}, {\it{q-2\/}}, {\it{prg\/}})\index{ensures} \\ 
$\wedge$$\;\;\;\;$({\rm{eval}}\,({\it{p\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{ileads})\index{s})\index{eval} $\rightarrow$ {\rm{eval}}\,({\it{p-1\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{ileads})\index{s})\index{eval}) \\ 
$\wedge$$\;\;\;\;${\rm{stronger-p}}\,({\it{p-1\/}}, {\it{p-2\/}})\index{stronger-p} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{eval}}\,({\it{q-1\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jleads}}\,({\rm{ileads}}\,({\it{p-1\/}}, {\it{prg\/}}, {\it{q\/}})\index{ileads}, {\it{prg\/}}, {\it{q-1\/}})\index{jleads})\index{s})\index{eval} \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\it{q\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jleads}}\,({\rm{ileads}}\,({\it{p-1\/}}, {\it{prg\/}}, {\it{q\/}})\index{ileads}, {\it{prg\/}}, {\it{q-1\/}})\index{jleads})\index{s})\index{eval})\- \\ 
$\wedge$$\;\;\;\;${\rm{stronger-p}}\,({\it{q-2\/}}, {\it{q-1\/}})\index{stronger-p} \\ 
$\wedge$$\;\;\;\;${\rm{total}}\,({\it{prg\/}})\index{total})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{leads-to}\-
\end{tabbing}


\noindent{\sc Event}:   Disable unconditional-fairness-general.

\addvspace{18pt}


\begin{tabbing}{\sc Conservative Axiom}:  strong-fairness \\ \index{strong-fairness}
\=\+(\=\+{\rm{unless}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{unless} \\ 
$\wedge$$\;\;\;\;${\rm{e-ensures}}\,({\it{p\/}}, {\it{q\/}}, {\it{c\/}}, {\it{prg\/}})\index{e-ensures} \\ 
$\wedge$$\;\;\;\;${\rm{leads-to}}\,({\it{p\/}}, {\rm{list}}\,({\tt{'}}{\tt{or}}, {\it{q\/}}, {\it{c\/}}), {\it{prg\/}})\index{leads-to} \\ 
$\wedge$$\;\;\;\;${\rm{strongly-fair}}\,({\it{prg\/}})\index{strongly-fair})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{leads-to}\-
\end{tabbing}\noindent Simultaneously, we introduce the new function symbol {\it strongly-fair\/}.


\noindent{\sc Event}:   Disable strong-fairness.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  strong-fairness-general \\ \index{strong-fairness-general}
\=\+(\=\+{\rm{unless}}\,({\it{p-1\/}}, {\it{q-1\/}}, {\it{prg\/}})\index{unless} \\ 
$\wedge$$\;\;\;\;${\rm{e-ensures}}\,({\it{p-2\/}}, {\it{q-2\/}}, {\it{c\/}}, {\it{prg\/}})\index{e-ensures} \\ 
$\wedge$$\;\;\;\;${\rm{leads-to}}\,({\it{p\/}}, {\rm{list}}\,({\tt{'}}{\tt{or}}, {\it{q\/}}, {\it{c\/}}), {\it{prg\/}})\index{leads-to} \\ 
$\wedge$$\;\;\;\;$({\rm{eval}}\,({\it{p\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{ileads})\index{s})\index{eval} $\rightarrow$ {\rm{eval}}\,({\it{p-1\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{ileads})\index{s})\index{eval}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{eval}}\,({\it{p-1\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{ileads}}\,({\it{p-1\/}}, {\it{prg\/}}, {\rm{list}}\,({\tt{'}}{\tt{or}}, {\it{q-1\/}}, {\it{c\/}}))\index{ileads})\index{s})\index{eval} \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\it{p\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{ileads}}\,({\it{p-1\/}}, {\it{prg\/}}, {\rm{list}}\,({\tt{'}}{\tt{or}}, {\it{q-1\/}}, {\it{c\/}}))\index{ileads})\index{s})\index{eval})\- \\ 
$\wedge$$\;\;\;\;${\rm{stronger-p}}\,({\it{p-1\/}}, {\it{p-2\/}})\index{stronger-p} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{eval}}\,({\it{q-1\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jleads}}\,({\rm{ileads}}\,({\it{p-1\/}}, {\it{prg\/}}, {\it{q\/}})\index{ileads}, {\it{prg\/}}, {\it{q-1\/}})\index{jleads})\index{s})\index{eval} \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\it{q\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jleads}}\,({\rm{ileads}}\,({\it{p-1\/}}, {\it{prg\/}}, {\it{q\/}})\index{ileads}, {\it{prg\/}}, {\it{q-1\/}})\index{jleads})\index{s})\index{eval})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{eval}}\,(\=\+{\rm{list}}\,({\tt{'}}{\tt{or}}, {\it{q\/}}, {\it{c\/}}), \\ 
{\rm{s}}\,(\=\+{\it{prg\/}}, \\ 
{\rm{jleads}}\,({\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\rm{list}}\,({\tt{'}}{\tt{or}}, {\it{q-1\/}}, {\it{c\/}}))\index{ileads}, {\it{prg\/}}, {\rm{list}}\,({\tt{'}}{\tt{or}}, {\it{q\/}}, {\it{c\/}}))\index{jleads})\-\index{s})\-\index{eval} \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,(\=\+{\rm{list}}\,({\tt{'}}{\tt{or}}, {\it{q-1\/}}, {\it{c\/}}), \\ 
{\rm{s}}\,(\=\+{\it{prg\/}}, \\ 
{\rm{jleads}}\,(\=\+{\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\rm{list}}\,({\tt{'}}{\tt{or}}, {\it{q-1\/}}, {\it{c\/}}))\index{ileads}, \\ 
{\it{prg\/}}, \\ 
{\rm{list}}\,({\tt{'}}{\tt{or}}, {\it{q\/}}, {\it{c\/}}))\-\index{jleads})\-\index{s})\-\index{eval})\- \\ 
$\wedge$$\;\;\;\;${\rm{stronger-p}}\,({\it{q-2\/}}, {\it{q-1\/}})\index{stronger-p} \\ 
$\wedge$$\;\;\;\;${\rm{strongly-fair}}\,({\it{prg\/}})\index{strongly-fair})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{leads-to}\-
\end{tabbing}



\noindent{\sc Event}:   Disable strong-fairness-general.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{wfw} \\  
\=\+{\rm{wfw}}\,({\it{i\/}}, {\it{j\/}}, {\it{p\/}}, {\it{q\/}}, {\it{c\/}}, {\it{prg\/}})\index{wfw} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $<$ {\it{j\/}} \\ 
{\bf then }\=\+{\bf if }{\rm{eval}}\,({\it{q\/}}, {\rm{s}}\,({\it{prg\/}}, {\it{i\/}})\index{s})\index{eval}$\;\;${\bf then }{\it{i\/}} \\ 
{\bf elseif }{\rm{eval}}\,({\it{p\/}}, {\rm{s}}\,({\it{prg\/}}, {\it{i\/}})\index{s})\index{eval} \\ 
{\bf then }\=\+{\bf if }{\rm{eval}}\,({\it{c\/}}, {\rm{s}}\,({\it{prg\/}}, {\it{i\/}})\index{s})\index{eval}$\;\;${\bf then }{\rm{wfw}}\,($1\;+$ {\it{i\/}}, {\it{j\/}}, {\it{p\/}}, {\it{q\/}}, {\it{c\/}}, {\it{prg\/}})\index{wfw} \\ 
{\bf else }{\it{i\/}}$\;${\bf  endif}\- \\ 
{\bf else }{\it{i\/}}$\;${\bf  endif}\- \\ 
{\bf else }{\rm{fix}}\,({\it{i\/}})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  wfw-bigger \\ \index{wfw-bigger}
{\rm{wfw}}\,({\it{i\/}}, {\it{j\/}}, {\it{p\/}}, {\it{q\/}}, {\it{c\/}}, {\it{prg\/}})\index{wfw} $\not<$ {\it{i\/}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  about-wfw \\ \index{about-wfw}
\=\+({\rm{unless}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{unless} $\wedge$ {\rm{listp}}\,({\it{prg\/}}) $\wedge$ {\rm{eval}}\,({\it{p\/}}, {\rm{s}}\,({\it{prg\/}}, {\it{i\/}})\index{s})\index{eval} $\wedge$ ({\it{j\/}} $\not<$ {\it{i\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{eval}}\,({\it{q\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{wfw}}\,({\it{i\/}}, {\it{j\/}}, {\it{p\/}}, {\it{q\/}}, {\it{c\/}}, {\it{prg\/}})\index{wfw})\index{s})\index{eval} \\ 
$\vee$$\;\;\;\;$(\=\+{\rm{eval}}\,({\it{p\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{wfw}}\,({\it{i\/}}, {\it{j\/}}, {\it{p\/}}, {\it{q\/}}, {\it{c\/}}, {\it{prg\/}})\index{wfw})\index{s})\index{eval} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{eval}}\,({\it{q\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{wfw}}\,({\it{i\/}}, {\it{j\/}}, {\it{p\/}}, {\it{q\/}}, {\it{c\/}}, {\it{prg\/}})\index{wfw})\index{s})\index{eval}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{eval}}\,({\it{c\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{wfw}}\,({\it{i\/}}, {\it{j\/}}, {\it{p\/}}, {\it{q\/}}, {\it{c\/}}, {\it{prg\/}})\index{wfw})\index{s})\index{eval}))\- \\ 
$\vee$$\;\;\;\;$(\=\+({\rm{wfw}}\,({\it{i\/}}, {\it{j\/}}, {\it{p\/}}, {\it{q\/}}, {\it{c\/}}, {\it{prg\/}})\index{wfw} $=$ {\rm{fix}}\,({\it{j\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{eval}}\,({\it{p\/}}, {\rm{s}}\,({\it{prg\/}}, {\it{j\/}})\index{s})\index{eval} $\vee$ {\rm{eval}}\,({\it{q\/}}, {\rm{s}}\,({\it{prg\/}}, {\it{j\/}})\index{s})\index{eval}))\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{witness} \\  
\=\+{\rm{witness}}\,({\it{p\/}}, {\it{q\/}}, {\it{c\/}}, {\it{prg\/}})\index{witness} \\ 
$=$$\;\;\;\;${\rm{wfw}}\,(\=\+{\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{ileads}, \\ 
{\rm{next}}\,({\it{prg\/}}, {\rm{eee}}\,({\it{c\/}}, {\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{eee}, {\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{ileads})\index{next}, \\ 
{\it{p\/}}, \\ 
{\it{q\/}}, \\ 
{\it{c\/}}, \\ 
{\it{prg\/}})\-\index{wfw}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  weak-fairness \\ \index{weak-fairness}
\=\+(\=\+{\rm{unless}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{unless} \\ 
$\wedge$$\;\;\;\;${\rm{e-ensures}}\,({\it{p\/}}, {\it{q\/}}, {\it{c\/}}, {\it{prg\/}})\index{e-ensures} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{eval}}\,({\rm{list}}\,({\tt{'}}{\tt{and}}, {\it{p\/}}, {\rm{list}}\,({\tt{'}}{\tt{not}}, {\it{q\/}})), {\rm{s}}\,({\it{prg\/}}, {\rm{witness}}\,({\it{p\/}}, {\it{q\/}}, {\it{c\/}}, {\it{prg\/}})\index{witness})\index{s})\index{eval} \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\it{c\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{witness}}\,({\it{p\/}}, {\it{q\/}}, {\it{c\/}}, {\it{prg\/}})\index{witness})\index{s})\index{eval})\-)\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{leads-to}\-
\end{tabbing}


\noindent{\sc Event}:   Disable weak-fairness.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  weak-fairness-general \\ \index{weak-fairness-general}
\=\+(\=\+{\rm{unless}}\,({\it{p-1\/}}, {\it{q-1\/}}, {\it{prg\/}})\index{unless} \\ 
$\wedge$$\;\;\;\;${\rm{e-ensures}}\,({\it{p-2\/}}, {\it{q-2\/}}, {\it{c\/}}, {\it{prg\/}})\index{e-ensures} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{eval}}\,({\rm{list}}\,({\tt{'}}{\tt{and}}, {\it{p-1\/}}, {\rm{list}}\,({\tt{'}}{\tt{not}}, {\it{q-1\/}})), {\rm{s}}\,({\it{prg\/}}, {\rm{witness}}\,({\it{p-1\/}}, {\it{q-1\/}}, {\it{c\/}}, {\it{prg\/}})\index{witness})\index{s})\index{eval} \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\it{c\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{witness}}\,({\it{p-1\/}}, {\it{q-1\/}}, {\it{c\/}}, {\it{prg\/}})\index{witness})\index{s})\index{eval})\- \\ 
$\wedge$$\;\;\;\;$({\rm{eval}}\,({\it{p\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{ileads})\index{s})\index{eval} $\rightarrow$ {\rm{eval}}\,({\it{p-1\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{ileads}}\,({\it{p\/}}, {\it{prg\/}}, {\it{q\/}})\index{ileads})\index{s})\index{eval}) \\ 
$\wedge$$\;\;\;\;${\rm{stronger-p}}\,({\it{p-1\/}}, {\it{p-2\/}})\index{stronger-p} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{eval}}\,({\it{q-1\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jleads}}\,({\rm{ileads}}\,({\it{p-1\/}}, {\it{prg\/}}, {\it{q\/}})\index{ileads}, {\it{prg\/}}, {\it{q-1\/}})\index{jleads})\index{s})\index{eval} \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\it{q\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{jleads}}\,({\rm{ileads}}\,({\it{p-1\/}}, {\it{prg\/}}, {\it{q\/}})\index{ileads}, {\it{prg\/}}, {\it{q-1\/}})\index{jleads})\index{s})\index{eval})\- \\ 
$\wedge$$\;\;\;\;${\rm{stronger-p}}\,({\it{q-2\/}}, {\it{q-1\/}})\index{stronger-p})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,({\it{p\/}}, {\it{q\/}}, {\it{prg\/}})\index{leads-to}\-
\end{tabbing}


\noindent{\sc Event}:   Disable weak-fairness-general.

\addvspace{18pt}

\noindent{\sc Event}:   Disable witness.

\addvspace{18pt}


\begin{tabbing}{\sc Theorem}:  deadlock-freedom-witness \\ \index{deadlock-freedom-witness}
\=\+(\=\+{\rm{unless}}\,({\it{inv\/}}, {\tt{'}}{\tt{(}}{\tt{false}}{\tt{)}}, {\it{prg\/}})\index{unless} \\ 
$\wedge$$\;\;\;\;${\rm{enabling-condition}}\,({\it{c\/}}, {\it{e\/}}, {\it{prg\/}})\index{enabling-condition} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{eval}}\,({\it{inv\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{next}}\,({\it{prg\/}}, {\it{e\/}}, {\rm{ileads}}\,({\it{inv\/}}, {\it{prg\/}}, {\tt{'}}{\tt{(}}{\tt{false}}{\tt{)}})\index{ileads})\index{next})\index{s})\index{eval} \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{eval}}\,({\it{c\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{next}}\,({\it{prg\/}}, {\it{e\/}}, {\rm{ileads}}\,({\it{inv\/}}, {\it{prg\/}}, {\tt{'}}{\tt{(}}{\tt{false}}{\tt{)}})\index{ileads})\index{next})\index{s})\index{eval}))\- \\ 
$\wedge$$\;\;\;\;${\rm{schedulable}}\,({\it{prg\/}})\index{schedulable})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,({\it{inv\/}}, {\tt{'}}{\tt{(}}{\tt{false}}{\tt{)}}, {\it{prg\/}})\index{leads-to}\-
\end{tabbing}


\noindent{\sc Event}:   Disable deadlock-freedom-witness.

\addvspace{18pt}


\begin{tabbing}{\sc Conservative Axiom}:  deadlock-freedom \\ \index{deadlock-freedom}
\=\+(\=\+{\rm{unless}}\,({\it{inv\/}}, {\tt{'}}{\tt{(}}{\tt{false}}{\tt{)}}, {\it{prg\/}})\index{unless} \\ 
$\wedge$$\;\;\;\;${\rm{enabling-condition}}\,({\it{c\/}}, {\it{e\/}}, {\it{prg\/}})\index{enabling-condition} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{eval}}\,({\it{inv\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{next}}\,({\it{prg\/}}, {\it{e\/}}, {\rm{ileads}}\,({\it{inv\/}}, {\it{prg\/}}, {\tt{'}}{\tt{(}}{\tt{false}}{\tt{)}})\index{ileads})\index{next})\index{s})\index{eval} \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{eval}}\,({\it{c\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{next}}\,({\it{prg\/}}, {\it{e\/}}, {\rm{ileads}}\,({\it{inv\/}}, {\it{prg\/}}, {\tt{'}}{\tt{(}}{\tt{false}}{\tt{)}})\index{ileads})\index{next})\index{s})\index{eval}))\- \\ 
$\wedge$$\;\;\;\;${\rm{deadlock-free}}\,({\it{prg\/}})\index{deadlock-free})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,({\it{inv\/}}, {\tt{'}}{\tt{(}}{\tt{false}}{\tt{)}}, {\it{prg\/}})\index{leads-to}\-
\end{tabbing}\noindent Simultaneously, we introduce the new function symbol {\it deadlock-free\/}.

\begin{tabbing}{\sc Theorem}:  deadlock-freedom-general \\ \index{deadlock-freedom-general}
\=\+(\=\+{\rm{unless}}\,({\it{inv\/}}, {\tt{'}}{\tt{(}}{\tt{false}}{\tt{)}}, {\it{prg\/}})\index{unless} \\ 
$\wedge$$\;\;\;\;${\rm{enabling-condition}}\,({\it{c\/}}, {\it{e\/}}, {\it{prg\/}})\index{enabling-condition} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{eval}}\,({\it{inv\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{next}}\,({\it{prg\/}}, {\it{e\/}}, {\rm{ileads}}\,({\it{inv\/}}, {\it{prg\/}}, {\tt{'}}{\tt{(}}{\tt{false}}{\tt{)}})\index{ileads})\index{next})\index{s})\index{eval} \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{eval}}\,({\it{c\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{next}}\,({\it{prg\/}}, {\it{e\/}}, {\rm{ileads}}\,({\it{inv\/}}, {\it{prg\/}}, {\tt{'}}{\tt{(}}{\tt{false}}{\tt{)}})\index{ileads})\index{next})\index{s})\index{eval}))\- \\ 
$\wedge$$\;\;\;\;$(($\neg$ {\rm{eval}}\,({\it{inv\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{ii}}\,({\it{p\/}}, {\it{prg\/}})\index{ii})\index{s})\index{eval}) $\rightarrow$ {\rm{eval}}\,({\it{p\/}}, {\rm{s}}\,({\it{prg\/}}, {\rm{ii}}\,({\it{p\/}}, {\it{prg\/}})\index{ii})\index{s})\index{eval}) \\ 
$\wedge$$\;\;\;\;${\rm{deadlock-free}}\,({\it{prg\/}})\index{deadlock-free})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{invariant}}\,({\it{p\/}}, {\it{prg\/}})\index{invariant}\-
\end{tabbing}


\noindent{\sc Event}:   Enable eval.

\addvspace{18pt}

\noindent{\sc Event}:   Enable n.

\addvspace{18pt}

\begin{verbatim};;; Some Helpful Definitions and Theorems

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{update-assoc} \\  
\=\+{\rm{update-assoc}}\,({\it{key\/}}, {\it{value\/}}, {\it{alist\/}})\index{update-assoc} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{alist\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{caar}}\,({\it{alist\/}}) $=$ {\it{key\/}}$\;\;${\bf then }{\rm{cons}}\,({\rm{cons}}\,({\it{key\/}}, {\it{value\/}}), {\rm{cdr}}\,({\it{alist\/}})) \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\it{alist\/}}), {\rm{update-assoc}}\,({\it{key\/}}, {\it{value\/}}, {\rm{cdr}}\,({\it{alist\/}}))\index{update-assoc})$\;${\bf  endif}\- \\ 
{\bf else }{\rm{list}}\,({\rm{cons}}\,({\it{key\/}}, {\it{value\/}}))$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  simplify-assoc \\ \index{simplify-assoc}
\=\+{\rm{assoc}}\,({\it{key-1\/}}, {\rm{update-assoc}}\,({\it{key-2\/}}, {\it{value\/}}, {\it{alist\/}})\index{update-assoc}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{key-1\/}} $=$ {\it{key-2\/}}$\;\;${\bf then }{\rm{cons}}\,({\it{key-1\/}}, {\it{value\/}}) \\ 
{\bf else }{\rm{assoc}}\,({\it{key-1\/}}, {\it{alist\/}})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{add1-mod} \\  
\=\+{\rm{add1-mod}}\,({\it{n\/}}, {\it{x\/}})\index{add1-mod} \\ 
$=$$\;\;\;\;$\=\+{\bf if }($1\;+$ {\it{x\/}}) $<$ {\it{n\/}}$\;\;${\bf then }$1\;+$ {\it{x\/}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{sub1-mod} \\  
\=\+{\rm{sub1-mod}}\,({\it{n\/}}, {\it{x\/}})\index{sub1-mod} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $<$ {\it{n\/}} \\ 
{\bf then }\=\+{\bf if }{\it{x\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\it{n\/}} $-\;1$ \\ 
{\bf else }{\it{x\/}} $-\;1$$\;${\bf  endif}\- \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{uc} \\  
\=\+{\rm{uc}}\,({\it{old\/}}, {\it{new\/}}, {\it{keys\/}}, {\it{excpt\/}})\index{uc} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{keys\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{car}}\,({\it{keys\/}}) $\in$ {\it{excpt\/}}$\;\;${\bf then }{\rm{uc}}\,({\it{old\/}}, {\it{new\/}}, {\rm{cdr}}\,({\it{keys\/}}), {\it{excpt\/}})\index{uc} \\ 
{\bf elseif }{\rm{assoc}}\,({\rm{car}}\,({\it{keys\/}}), {\it{old\/}}) $=$ {\rm{assoc}}\,({\rm{car}}\,({\it{keys\/}}), {\it{new\/}}) \\ 
{\bf then }{\rm{uc}}\,({\it{old\/}}, {\it{new\/}}, {\rm{cdr}}\,({\it{keys\/}}), {\it{excpt\/}})\index{uc} \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  uc-basic-property \\ \index{uc-basic-property}
\=\+({\rm{uc}}\,({\it{old\/}}, {\it{new\/}}, {\it{keys\/}}, {\it{excpt\/}})\index{uc} $\wedge$ ({\it{key\/}} $\in$ {\it{keys\/}}) $\wedge$ ({\it{key\/}} $\not\in$ {\it{excpt\/}})) \\ 
$\rightarrow$$\;\;\;\;$(({\rm{assoc}}\,({\it{key\/}}, {\it{old\/}}) $=$ {\rm{assoc}}\,({\it{key\/}}, {\it{new\/}})) $=$ {\bf{t}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  uc-commutative \\ \index{uc-commutative}
{\rm{uc}}\,({\it{old\/}}, {\it{new\/}}, {\it{keys\/}}, {\it{excpt\/}})\index{uc} $=$ {\rm{uc}}\,({\it{new\/}}, {\it{old\/}}, {\it{keys\/}}, {\it{excpt\/}})\index{uc}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  uc-reflexive \\ \index{uc-reflexive}
{\rm{uc}}\,({\it{list\/}}, {\it{list\/}}, {\it{keys\/}}, {\it{excpt\/}})\index{uc}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  uc-of-update-assoc \\ \index{uc-of-update-assoc}
\=\+{\rm{uc}}\,({\it{list-1\/}}, {\rm{update-assoc}}\,({\it{key\/}}, {\it{value\/}}, {\it{list-2\/}})\index{update-assoc}, {\it{keys\/}}, {\it{excpt\/}})\index{uc} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{key\/}} $\in$ {\it{excpt\/}}$\;\;${\bf then }{\rm{uc}}\,({\it{list-1\/}}, {\it{list-2\/}}, {\it{keys\/}}, {\it{excpt\/}})\index{uc} \\ 
{\bf elseif }{\it{key\/}} $\in$ {\it{keys\/}} \\ 
{\bf then }\=\+({\rm{assoc}}\,({\it{key\/}}, {\it{list-1\/}}) $=$ {\rm{cons}}\,({\it{key\/}}, {\it{value\/}})) \\ 
$\wedge$$\;\;\;\;${\rm{uc}}\,({\it{list-1\/}}, {\it{list-2\/}}, {\it{keys\/}}, {\rm{cons}}\,({\it{key\/}}, {\it{excpt\/}}))\index{uc}\- \\ 
{\bf else }{\rm{uc}}\,({\it{list-1\/}}, {\it{list-2\/}}, {\it{keys\/}}, {\it{excpt\/}})\index{uc}$\;${\bf  endif}\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  strip-cars-append \\ \index{strip-cars-append}
{\rm{strip-cars}}\,({\rm{append}}\,({\it{a\/}}, {\it{b\/}})) $=$ {\rm{append}}\,({\rm{strip-cars}}\,({\it{a\/}}), {\rm{strip-cars}}\,({\it{b\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  uc-append \\ \index{uc-append}
\=\+{\rm{uc}}\,({\it{old\/}}, {\it{new\/}}, {\rm{append}}\,({\it{a\/}}, {\it{b\/}}), {\it{excpt\/}})\index{uc} \\ 
$=$$\;\;\;\;$({\rm{uc}}\,({\it{old\/}}, {\it{new\/}}, {\it{a\/}}, {\it{excpt\/}})\index{uc} $\wedge$ {\rm{uc}}\,({\it{old\/}}, {\it{new\/}}, {\it{b\/}}, {\it{excpt\/}})\index{uc})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  uc-commutative-2 \\ \index{uc-commutative-2}
{\rm{uc}}\,({\it{old\/}}, {\it{new\/}}, {\rm{append}}\,({\it{a\/}}, {\it{b\/}}), {\it{excpt\/}})\index{uc} $=$ {\rm{uc}}\,({\it{old\/}}, {\it{new\/}}, {\rm{append}}\,({\it{b\/}}, {\it{a\/}}), {\it{excpt\/}})\index{uc}
\end{tabbing}


\noindent{\sc Event}:   Disable uc-append.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  key-not-member-strip-cars \\ \index{key-not-member-strip-cars}
({\it{key\/}} $\not\in$ {\rm{strip-cars}}\,({\it{alist\/}})) $\rightarrow$ ({\rm{assoc}}\,({\it{key\/}}, {\it{alist\/}}) $=$ {\bf{f}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  uc-property \\ \index{uc-property}
\=\+(\=\+{\rm{uc}}\,({\it{old\/}}, {\it{new\/}}, {\rm{append}}\,({\rm{strip-cars}}\,({\it{old\/}}), {\rm{strip-cars}}\,({\it{new\/}})), {\it{excpt\/}})\index{uc} \\ 
$\wedge$$\;\;\;\;$({\it{key\/}} $\not\in$ {\it{excpt\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$(({\rm{assoc}}\,({\it{key\/}}, {\it{old\/}}) $=$ {\rm{assoc}}\,({\it{key\/}}, {\it{new\/}})) $=$ {\bf{t}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  about-uc \\ \index{about-uc}
\=\+({\rm{uc}}\,({\it{a\/}}, {\it{b\/}}, {\rm{append}}\,({\rm{strip-cars}}\,({\it{a\/}}), {\rm{strip-cars}}\,({\it{b\/}})), {\it{excpt\/}})\index{uc} $\wedge$ ({\it{key\/}} $\not\in$ {\it{excpt\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{assoc}}\,({\it{key\/}}, {\it{a\/}}) $=$ {\rm{assoc}}\,({\it{key\/}}, {\it{b\/}}))\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{changed} \\  
{\rm{changed}}\,({\it{old\/}}, {\it{new\/}}, {\it{excpt\/}})\index{changed} $=$ {\rm{uc}}\,({\it{old\/}}, {\it{new\/}}, {\rm{strip-cars}}\,({\rm{append}}\,({\it{old\/}}, {\it{new\/}})), {\it{excpt\/}})\index{uc}
\end{tabbing}


\noindent{\sc Event}:   Make the library {\tt{"interpreter"}}.

\addvspace{18pt}

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