\documentstyle[makeidx]{article}
\makeindex
%\setlength{\oddsidemargin}{.5in}
%\setlength{\evensidemargin}{.5in}
%\setlength{\textwidth}{5.8in}
\begin{document}
%\setlength{\parindent}{0pt}
%\newcounter{bean}
%\begin{list}{\arabic{bean}.}{\usecounter{bean}\setlength{\leftmargin}{0pt}\setlength{\rightmargin}{0pt}\setlength{\listparindent}{20pt}\setlength{\parsep}{5pt}}
%\item[]

\begin{verbatim}#|

 Copyright (C) 1994 by Computational Logic, Inc.  All Rights Reserved.

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

 NO WARRANTY

 Computational Logic, Inc. PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT
 IS PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED,
 INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND
 FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND
 PERFORMANCE OF THE SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU
 ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.

 IN NO EVENT WILL Computational Logic, Inc. BE LIABLE TO YOU FOR ANY DAMAGES,
 ANY LOST PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL
 DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT
 NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES
 SUSTAINED BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF
 SUCH DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.
|#

; The Correctness of a Piton Big Number Addition Program
; J Strother Moore

; This file corresponds to Chapter 3 of CLI Tech Report 22,
; "Piton:  A Verified Assembly Level Language".

\end{verbatim}
\noindent{\sc Event}:   Start with the library {\tt{"piton"}} using the compiled version.

\addvspace{18pt}


\noindent{\sc Event}:   Enable plus-0.

\addvspace{18pt}

\noindent{\sc Event}:   Enable commutativity-of-plus.

\addvspace{18pt}

\noindent{\sc Event}:   Enable commutativity2-of-plus.

\addvspace{18pt}

\noindent{\sc Event}:   Enable associativity-of-plus.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  plus-add1-1 \\ \index{plus-add1-1}
(($1\;+$ {\it{x\/}}) $+$ {\it{y\/}}) $=$ ($1\;+$ ({\it{x\/}} $+$ {\it{y\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  plus-add1-2 \\ \index{plus-add1-2}
({\it{x\/}} $+$ ($1\;+$ {\it{y\/}})) $=$ ($1\;+$ ({\it{x\/}} $+$ {\it{y\/}}))
\end{tabbing}


\noindent{\sc Event}:   Enable equal-plus-0.

\addvspace{18pt}


\noindent{\sc Event}:   Enable times-0.

\addvspace{18pt}


\noindent{\sc Event}:   Enable times-add1.

\addvspace{18pt}


\noindent{\sc Event}:   Enable times-distributes-over-plus.

\addvspace{18pt}


\noindent{\sc Event}:   Enable commutativity-of-times.

\addvspace{18pt}


\noindent{\sc Event}:   Enable commutativity2-of-times.

\addvspace{18pt}


\noindent{\sc Event}:   Enable associativity-of-times.

\addvspace{18pt}


\noindent{\sc Event}:   Enable equal-times-0.

\addvspace{18pt}


\noindent{\sc Event}:   Enable difference-elim.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  difference-elim-rewrite1 \\ \index{difference-elim-rewrite1}
(({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{x\/}} $\not<$ {\it{y\/}})) $\rightarrow$ (({\it{y\/}} $+$ ({\it{x\/}} $-$ {\it{y\/}})) $=$ {\it{x\/}})
\end{tabbing}


\noindent{\sc Event}:   Enable lessp-remainder.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  lessp-remainder-linear \\ \index{lessp-remainder-linear}
({\it{y\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ (({\it{x\/}} ${}${\bf{mod}}${}$ {\it{y\/}}) $<$ {\it{y\/}})
\end{tabbing}


\noindent{\sc Event}:   Enable remainder-quotient-elim.

\addvspace{18pt}

\noindent{\sc Event}:   Enable plus-remainder-times-quotient.

\addvspace{18pt}

\noindent{\sc Event}:   Enable lessp-quotient.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  lessp-quotient-linear \\ \index{lessp-quotient-linear}
(({\it{x\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{y\/}} $\not=$ {\tt{1}})) $\rightarrow$ (({\it{x\/}} $\div$ {\it{y\/}}) $<$ {\it{x\/}})
\end{tabbing}


\noindent{\sc Event}:   Enable not-lessp-quotient.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  not-lessp-times \\ \index{not-lessp-times}
({\it{x\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ (({\it{x\/}} $*$ {\it{y\/}}) $\not<$ {\it{y\/}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{nat-$>$bign} \\  
\=\+{\rm{nat-$>$bign}}\,({\it{n\/}}, {\it{base\/}}, {\it{size\/}})\index{nat-$>$bign} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{size\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{nat}}, {\it{n\/}} ${}${\bf{mod}}${}$ {\it{base\/}})\index{tag}, \\ 
{\rm{nat-$>$bign}}\,({\it{n\/}} $\div$ {\it{base\/}}, {\it{base\/}}, {\it{size\/}} $-\;1$)\index{nat-$>$bign})\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{bign-$>$nat} \\  
\=\+{\rm{bign-$>$nat}}\,({\it{a\/}}, {\it{base\/}})\index{bign-$>$nat} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{a\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\rm{untag}}\,({\rm{car}}\,({\it{a\/}}))\index{untag} $+$ ({\it{base\/}} $*$ {\rm{bign-$>$nat}}\,({\rm{cdr}}\,({\it{a\/}}), {\it{base\/}})\index{bign-$>$nat})$\;${\bf  endif}\-\-
\end{tabbing}
      
\begin{tabbing}{\sc Definition}:\index{bignp} \\  
\=\+{\rm{bignp}}\,({\it{a\/}}, {\it{base\/}})\index{bignp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{a\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\it{a\/}} $=$ {\bf{nil}} \\ 
{\bf else }\=\+{\rm{listp}}\,({\rm{car}}\,({\it{a\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{type}}\,({\rm{car}}\,({\it{a\/}}))\index{type} $=$ {\tt{'}}{\tt{nat}}) \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\rm{car}}\,({\it{a\/}}))\index{untag} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\rm{car}}\,({\it{a\/}}))\index{untag} $<$ {\it{base\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{cddr}}\,({\rm{car}}\,({\it{a\/}})) $=$ {\bf{nil}}) \\ 
$\wedge$$\;\;\;\;${\rm{bignp}}\,({\rm{cdr}}\,({\it{a\/}}), {\it{base\/}})\index{bignp}\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bignp-nat-$>$bign \\ \index{bignp-nat-$>$bign}
({\it{base\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ {\rm{bignp}}\,({\rm{nat-$>$bign}}\,({\it{n\/}}, {\it{base\/}}, {\it{size\/}})\index{nat-$>$bign}, {\it{base\/}})\index{bignp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-nat-$>$bign \\ \index{length-nat-$>$bign}
({\it{base\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ ({\rm{length}}\,({\rm{nat-$>$bign}}\,({\it{n\/}}, {\it{base\/}}, {\it{size\/}})\index{nat-$>$bign})\index{length} $=$ {\rm{fix}}\,({\it{size\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-quotient-times \\ \index{lessp-quotient-times}
({\it{n\/}} $<$ ({\it{b\/}} $*$ {\it{e\/}})) $\rightarrow$ ((({\it{n\/}} $\div$ {\it{b\/}}) $<$ {\it{e\/}}) $=$ {\bf{t}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bign-$>$nat-$>$bign \\ \index{bign-$>$nat-$>$bign}
\=\+(({\it{n\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\tt{1}} $<$ {\it{base\/}}) $\wedge$ ({\it{n\/}} $<$ {\rm{exp}}\,({\it{base\/}}, {\it{size\/}})\index{exp})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{bign-$>$nat}}\,({\rm{nat-$>$bign}}\,({\it{n\/}}, {\it{base\/}}, {\it{size\/}})\index{nat-$>$bign}, {\it{base\/}})\index{bign-$>$nat} $=$ {\it{n\/}})\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{tv-$>$nat} \\  
\=\+{\rm{tv-$>$nat}}\,({\it{c\/}})\index{tv-$>$nat} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{c\/}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{big-add-array} \\  
\=\+{\rm{big-add-array}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}}, {\it{base\/}})\index{big-add-array} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{a\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{nat}}, \\ 
\=\+({\rm{untag}}\,({\rm{car}}\,({\it{a\/}}))\index{untag} $+$ {\rm{untag}}\,({\rm{car}}\,({\it{b\/}}))\index{untag} $+$ {\rm{tv-$>$nat}}\,({\it{c\/}})\index{tv-$>$nat}) \\ 
${}${\bf{mod}}${}$$\;\;\;\;${\it{base\/}}\-)\-\index{tag}, \\ 
{\rm{big-add-array}}\,(\=\+{\rm{cdr}}\,({\it{a\/}}), \\ 
{\rm{cdr}}\,({\it{b\/}}), \\ 
\=\+(\=\+{\rm{untag}}\,({\rm{car}}\,({\it{a\/}}))\index{untag} \\ 
$+$$\;\;\;\;${\rm{untag}}\,({\rm{car}}\,({\it{b\/}}))\index{untag} \\ 
$+$$\;\;\;\;${\rm{tv-$>$nat}}\,({\it{c\/}})\index{tv-$>$nat})\- \\ 
$\not<$$\;\;\;\;${\it{base\/}}\-, \\ 
{\it{base\/}})\-\index{big-add-array})\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{big-add-carry-out} \\  
\=\+{\rm{big-add-carry-out}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}}, {\it{base\/}})\index{big-add-carry-out} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{a\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\rm{bool}}\,({\it{c\/}})\index{bool} \\ 
{\bf else }{\rm{big-add-carry-out}}\,(\=\+{\rm{cdr}}\,({\it{a\/}}), \\ 
{\rm{cdr}}\,({\it{b\/}}), \\ 
\=\+(\=\+{\rm{untag}}\,({\rm{car}}\,({\it{a\/}}))\index{untag} \\ 
$+$$\;\;\;\;${\rm{untag}}\,({\rm{car}}\,({\it{b\/}}))\index{untag} \\ 
$+$$\;\;\;\;${\rm{tv-$>$nat}}\,({\it{c\/}})\index{tv-$>$nat})\- \\ 
$\not<$$\;\;\;\;${\it{base\/}}\-, \\ 
{\it{base\/}})\-\index{big-add-carry-out}$\;${\bf  endif}\-\-
\end{tabbing}


\noindent{\sc Event}:   Enable difference-x-x.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  remainder-carryout1 \\ \index{remainder-carryout1}
\=\+(({\it{i\/}} $<$ {\it{base\/}}) $\wedge$ ({\it{j\/}} $<$ {\it{base\/}}) $\wedge$ (($1\;+$ ({\it{i\/}} $+$ {\it{j\/}})) $\not<$ {\it{base\/}})) \\ 
$\rightarrow$$\;\;\;\;$((($1\;+$ ({\it{i\/}} $+$ {\it{j\/}})) ${}${\bf{mod}}${}$ {\it{base\/}}) $=$ (($1\;+$ ({\it{i\/}} $+$ {\it{j\/}})) $-$ {\it{base\/}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-carryout0 \\ \index{remainder-carryout0}
\=\+(({\it{i\/}} $<$ {\it{base\/}}) $\wedge$ ({\it{j\/}} $<$ {\it{base\/}}) $\wedge$ (({\it{i\/}} $+$ {\it{j\/}}) $\not<$ {\it{base\/}})) \\ 
$\rightarrow$$\;\;\;\;$((({\it{i\/}} $+$ {\it{j\/}}) ${}${\bf{mod}}${}$ {\it{base\/}}) $=$ (({\it{i\/}} $+$ {\it{j\/}}) $-$ {\it{base\/}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  interpretation-of-big-add-results \\ \index{interpretation-of-big-add-result!s}
\=\+(\=\+{\rm{bignp}}\,({\it{a\/}}, {\it{base\/}})\index{bignp} \\ 
$\wedge$$\;\;\;\;${\rm{bignp}}\,({\it{b\/}}, {\it{base\/}})\index{bignp} \\ 
$\wedge$$\;\;\;\;$({\rm{length}}\,({\it{a\/}})\index{length} $=$ {\rm{length}}\,({\it{b\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;$({\it{base\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{base\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{bign-$>$nat}}\,(\=\+{\rm{append}}\,(\=\+{\rm{big-add-array}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}}, {\it{base\/}})\index{big-add-array}, \\ 
{\rm{list}}\,({\rm{tag}}\,(\=\+{\tt{'}}{\tt{nat}}, \\ 
{\rm{bool-to-nat}}\,({\rm{untag}}\,({\rm{big-add-carry-out}}\,(\=\+{\it{a\/}}, \\ 
{\it{b\/}}, \\ 
{\it{c\/}}, \\ 
{\it{base\/}})\-\index{big-add-carry-out})\index{untag})\index{bool-to-nat})\-\index{tag}))\-, \\ 
{\it{base\/}})\-\index{bign-$>$nat} \\ 
$=$$\;\;\;\;$({\rm{bign-$>$nat}}\,({\it{a\/}}, {\it{base\/}})\index{bign-$>$nat} $+$ {\rm{bign-$>$nat}}\,({\it{b\/}}, {\it{base\/}})\index{bign-$>$nat} $+$ {\rm{tv-$>$nat}}\,({\it{c\/}})\index{tv-$>$nat}))\-\-
\end{tabbing}

\begin{verbatim}; The above theorem is just about all of the mathematical content of
; this exercise.  It remains relate the functions big-add-array and big-add-carry-out
; to a Piton program.



\end{verbatim}
\noindent{\sc Event}:   Disable tv-$>$nat.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  equal-lessp-n-1 \\ \index{equal-lessp-n-1}
({\it{n\/}} $<$ {\tt{1}}) $=$ ({\it{n\/}} $\simeq {\tt{0}}$)
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{big-add-array-loop} \\  
\=\+{\rm{big-add-array-loop}}\,({\it{i\/}}, {\it{a-array\/}}, {\it{b-array\/}}, {\it{n\/}}, {\it{c\/}}, {\it{base\/}})\index{big-add-array-loop} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{n\/}} $-\;1$) $\simeq {\tt{0}}$ \\ 
{\bf then }{\rm{put}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{nat}}, \\ 
\=\+(\=\+{\rm{untag}}\,({\rm{get}}\,({\it{i\/}}, {\it{a-array\/}})\index{get})\index{untag} \\ 
$+$$\;\;\;\;${\rm{untag}}\,({\rm{get}}\,({\it{i\/}}, {\it{b-array\/}})\index{get})\index{untag} \\ 
$+$$\;\;\;\;${\rm{tv-$>$nat}}\,({\it{c\/}})\index{tv-$>$nat})\- \\ 
${}${\bf{mod}}${}$$\;\;\;\;${\it{base\/}}\-)\-\index{tag}, \\ 
{\it{i\/}}, \\ 
{\it{a-array\/}})\-\index{put} \\ 
{\bf else }{\rm{big-add-array-loop}}\,(\=\+$1\;+$ {\it{i\/}}, \\ 
{\rm{put}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{nat}}, \\ 
\=\+(\=\+{\rm{untag}}\,({\rm{get}}\,({\it{i\/}}, {\it{a-array\/}})\index{get})\index{untag} \\ 
$+$$\;\;\;\;${\rm{untag}}\,({\rm{get}}\,({\it{i\/}}, {\it{b-array\/}})\index{get})\index{untag} \\ 
$+$$\;\;\;\;${\rm{tv-$>$nat}}\,({\it{c\/}})\index{tv-$>$nat})\- \\ 
${}${\bf{mod}}${}$$\;\;\;\;${\it{base\/}}\-)\-\index{tag}, \\ 
{\it{i\/}}, \\ 
{\it{a-array\/}})\-\index{put}, \\ 
{\it{b-array\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
\=\+(\=\+{\rm{untag}}\,({\rm{get}}\,({\it{i\/}}, {\it{a-array\/}})\index{get})\index{untag} \\ 
$+$$\;\;\;\;${\rm{untag}}\,({\rm{get}}\,({\it{i\/}}, {\it{b-array\/}})\index{get})\index{untag} \\ 
$+$$\;\;\;\;${\rm{tv-$>$nat}}\,({\it{c\/}})\index{tv-$>$nat})\- \\ 
$\not<$$\;\;\;\;${\it{base\/}}\-, \\ 
{\it{base\/}})\-\index{big-add-array-loop}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{big-add-carry-out-loop} \\  
\=\+{\rm{big-add-carry-out-loop}}\,({\it{i\/}}, {\it{a-array\/}}, {\it{b-array\/}}, {\it{n\/}}, {\it{c\/}}, {\it{base\/}})\index{big-add-carry-out-loop} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{n\/}} $-\;1$) $\simeq {\tt{0}}$ \\ 
{\bf then }{\rm{bool}}\,(\=\+(\=\+{\rm{untag}}\,({\rm{get}}\,({\it{i\/}}, {\it{a-array\/}})\index{get})\index{untag} \\ 
$+$$\;\;\;\;${\rm{untag}}\,({\rm{get}}\,({\it{i\/}}, {\it{b-array\/}})\index{get})\index{untag} \\ 
$+$$\;\;\;\;${\rm{tv-$>$nat}}\,({\it{c\/}})\index{tv-$>$nat})\- \\ 
$\not<$$\;\;\;\;${\it{base\/}}\-)\index{bool} \\ 
{\bf else }{\rm{big-add-carry-out-loop}}\,(\=\+$1\;+$ {\it{i\/}}, \\ 
{\rm{put}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{nat}}, \\ 
\=\+(\=\+{\rm{untag}}\,({\rm{get}}\,({\it{i\/}}, {\it{a-array\/}})\index{get})\index{untag} \\ 
$+$$\;\;\;\;${\rm{untag}}\,({\rm{get}}\,({\it{i\/}}, {\it{b-array\/}})\index{get})\index{untag} \\ 
$+$$\;\;\;\;${\rm{tv-$>$nat}}\,({\it{c\/}})\index{tv-$>$nat})\- \\ 
${}${\bf{mod}}${}$$\;\;\;\;${\it{base\/}}\-)\-\index{tag}, \\ 
{\it{i\/}}, \\ 
{\it{a-array\/}})\-\index{put}, \\ 
{\it{b-array\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
\=\+(\=\+{\rm{untag}}\,({\rm{get}}\,({\it{i\/}}, {\it{a-array\/}})\index{get})\index{untag} \\ 
$+$$\;\;\;\;${\rm{untag}}\,({\rm{get}}\,({\it{i\/}}, {\it{b-array\/}})\index{get})\index{untag} \\ 
$+$$\;\;\;\;${\rm{tv-$>$nat}}\,({\it{c\/}})\index{tv-$>$nat})\- \\ 
$\not<$$\;\;\;\;${\it{base\/}}\-, \\ 
{\it{base\/}})\-\index{big-add-carry-out-loop}$\;${\bf  endif}\-\-
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  get-is-car-nth-cdr \\ \index{get-is-car-nth-cdr}
{\rm{get}}\,({\it{i\/}}, {\it{a\/}})\index{get} $=$ {\rm{car}}\,({\rm{nth-cdr}}\,({\it{i\/}}, {\it{a\/}})\index{nth-cdr})
\end{tabbing}


\noindent{\sc Event}:   Enable length-put.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  nth-cdr-add1 \\ \index{nth-cdr-add1}
{\rm{nth-cdr}}\,($1\;+$ {\it{i\/}}, {\it{x\/}})\index{nth-cdr} $=$ {\rm{cdr}}\,({\rm{nth-cdr}}\,({\it{i\/}}, {\it{x\/}})\index{nth-cdr})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  nth-cdr-put-at \\ \index{nth-cdr-put-at}
\=\+({\it{i\/}} $<$ {\rm{length}}\,({\it{a\/}})\index{length}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{nth-cdr}}\,({\it{i\/}}, {\rm{put}}\,({\it{val\/}}, {\it{i\/}}, {\it{a\/}})\index{put})\index{nth-cdr} $=$ {\rm{cons}}\,({\it{val\/}}, {\rm{cdr}}\,({\rm{nth-cdr}}\,({\it{i\/}}, {\it{a\/}})\index{nth-cdr})))\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{hint1} \\  
\=\+{\rm{hint1}}\,({\it{i\/}}, {\it{a\/}}, {\it{b\/}}, {\it{c\/}}, {\it{base\/}})\index{hint1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $<$ {\rm{length}}\,({\it{a\/}})\index{length} \\ 
{\bf then }{\rm{hint1}}\,(\=\+$1\;+$ {\it{i\/}}, \\ 
{\rm{put}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{nat}}, \\ 
\=\+(\=\+{\rm{untag}}\,({\rm{get}}\,({\it{i\/}}, {\it{a\/}})\index{get})\index{untag} \\ 
$+$$\;\;\;\;${\rm{untag}}\,({\rm{get}}\,({\it{i\/}}, {\it{b\/}})\index{get})\index{untag} \\ 
$+$$\;\;\;\;${\rm{tv-$>$nat}}\,({\it{c\/}})\index{tv-$>$nat})\- \\ 
${}${\bf{mod}}${}$$\;\;\;\;${\it{base\/}}\-)\-\index{tag}, \\ 
{\it{i\/}}, \\ 
{\it{a\/}})\-\index{put}, \\ 
{\it{b\/}}, \\ 
\=\+({\rm{untag}}\,({\rm{get}}\,({\it{i\/}}, {\it{a\/}})\index{get})\index{untag} $+$ {\rm{untag}}\,({\rm{get}}\,({\it{i\/}}, {\it{b\/}})\index{get})\index{untag} $+$ {\rm{tv-$>$nat}}\,({\it{c\/}})\index{tv-$>$nat}) \\ 
$\not<$$\;\;\;\;${\it{base\/}}\-, \\ 
{\it{base\/}})\-\index{hint1} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  listp-nth-cdr \\ \index{listp-nth-cdr}
{\rm{listp}}\,({\rm{nth-cdr}}\,({\it{i\/}}, {\it{a\/}})\index{nth-cdr}) $=$ ({\it{i\/}} $<$ {\rm{length}}\,({\it{a\/}})\index{length})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  nth-cdr-put-before \\ \index{nth-cdr-put-before}
\=\+(({\it{j\/}} $<$ {\it{i\/}}) $\wedge$ ({\it{j\/}} $<$ {\rm{length}}\,({\it{a\/}})\index{length})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{nth-cdr}}\,({\it{i\/}}, {\rm{put}}\,({\it{val\/}}, {\it{j\/}}, {\it{a\/}})\index{put})\index{nth-cdr} $=$ {\rm{nth-cdr}}\,({\it{i\/}}, {\it{a\/}})\index{nth-cdr})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  difference-equal-1 \\ \index{difference-equal-1}
\=\+(({\it{i\/}} $<$ {\rm{length}}\,({\it{a\/}})\index{length}) $\wedge$ ({\it{i\/}} $\not<$ ({\rm{length}}\,({\it{a\/}})\index{length} $-\;1$))) \\ 
$\rightarrow$$\;\;\;\;$(({\rm{length}}\,({\it{a\/}})\index{length} $-$ {\it{i\/}}) $=$ {\tt{1}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  big-add-array-loop-on-list-of-length-1 \\ \index{big-add-array-loop-on-list-of-le!ngth-1}
\=\+{\rm{big-add-array-loop}}\,({\it{i\/}}, {\it{a\/}}, {\it{b\/}}, {\tt{1}}, {\it{c\/}}, {\it{base\/}})\index{big-add-array-loop} \\ 
$=$$\;\;\;\;${\rm{put}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{nat}}, \\ 
\=\+({\rm{untag}}\,({\rm{get}}\,({\it{i\/}}, {\it{a\/}})\index{get})\index{untag} $+$ {\rm{untag}}\,({\rm{get}}\,({\it{i\/}}, {\it{b\/}})\index{get})\index{untag} $+$ {\rm{tv-$>$nat}}\,({\it{c\/}})\index{tv-$>$nat}) \\ 
${}${\bf{mod}}${}$$\;\;\;\;${\it{base\/}}\-)\-\index{tag}, \\ 
{\it{i\/}}, \\ 
{\it{a\/}})\-\index{put}\-
\end{tabbing}


\noindent{\sc Event}:   Enable equal-length-0.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  equal-length-1 \\ \index{equal-length-1}
({\rm{length}}\,({\it{a\/}})\index{length} $=$ {\tt{1}}) $=$ ({\rm{listp}}\,({\it{a\/}}) $\wedge$ ({\rm{cdr}}\,({\it{a\/}}) $\simeq\;${{\bf{nil}}}${}$))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  nlistp-cdr-nth-cdr \\ \index{nlistp-cdr-nth-cdr}
{\rm{listp}}\,({\rm{cdr}}\,({\rm{nth-cdr}}\,({\it{i\/}}, {\it{a\/}})\index{nth-cdr})) $=$ ({\it{i\/}} $<$ ({\rm{length}}\,({\it{a\/}})\index{length} $-\;1$))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  big-add-array-on-list-of-length-1 \\ \index{big-add-array-on-list-of-length!-1}
\=\+({\rm{listp}}\,({\it{a\/}}) $\wedge$ ({\rm{cdr}}\,({\it{a\/}}) $\simeq\;${{\bf{nil}}}${}$)) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{big-add-array}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}}, {\it{base\/}})\index{big-add-array} \\ 
$=$$\;\;\;\;${\rm{list}}\,({\rm{tag}}\,(\=\+{\tt{'}}{\tt{nat}}, \\ 
\=\+({\rm{untag}}\,({\rm{car}}\,({\it{a\/}}))\index{untag} $+$ {\rm{untag}}\,({\rm{car}}\,({\it{b\/}}))\index{untag} $+$ {\rm{tv-$>$nat}}\,({\it{c\/}})\index{tv-$>$nat}) \\ 
${}${\bf{mod}}${}$$\;\;\;\;${\it{base\/}}\-)\-\index{tag}))\-\-
\end{tabbing}

\begin{verbatim}; The following lemma is intended only for use in the inductive step
; of mathematical-big-add-v-big-add-array-loop-generalized, where we
; replace i by (add1 i) and need to transform the lhs difference to
; the rhs sub1.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  difference-add1-new \\ \index{difference-add1-new}
({\rm{length}}\,({\it{a\/}})\index{length} $-$ ($1\;+$ {\it{i\/}})) $=$ (({\rm{length}}\,({\it{a\/}})\index{length} $-$ {\it{i\/}}) $-\;1$)
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-big-add-array-loop \\ \index{length-big-add-array-loop}
\=\+(({\it{i\/}} $<$ {\rm{length}}\,({\it{a\/}})\index{length}) $\wedge$ ({\rm{length}}\,({\it{a\/}})\index{length} $\not<$ ({\it{i\/}} $+$ {\it{n\/}}))) \\ 
$\rightarrow$$\;\;\;\;$({\rm{length}}\,({\rm{big-add-array-loop}}\,({\it{i\/}}, {\it{a\/}}, {\it{b\/}}, {\it{n\/}}, {\it{c\/}}, {\it{base\/}})\index{big-add-array-loop})\index{length} $=$ {\rm{length}}\,({\it{a\/}})\index{length})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  car-nth-cdr-put \\ \index{car-nth-cdr-put}
\=\+(({\it{i\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{j\/}} $\in\;${\bf{N}}${}$)) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{car}}\,({\rm{nth-cdr}}\,({\it{i\/}}, {\rm{put}}\,({\it{val\/}}, {\it{j\/}}, {\it{a\/}})\index{put})\index{nth-cdr}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $=$ {\it{j\/}}$\;\;${\bf then }{\it{val\/}} \\ 
{\bf else }{\rm{car}}\,({\rm{nth-cdr}}\,({\it{i\/}}, {\it{a\/}})\index{nth-cdr})$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  car-nth-cdr-big-add-array-loop \\ \index{car-nth-cdr-big-add-array-loop}
\=\+(({\it{k\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{i\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{k\/}} $<$ {\it{i\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{car}}\,({\rm{nth-cdr}}\,({\it{k\/}}, {\rm{big-add-array-loop}}\,({\it{i\/}}, {\it{a\/}}, {\it{b\/}}, {\it{n\/}}, {\it{c\/}}, {\it{base\/}})\index{big-add-array-loop})\index{nth-cdr}) \\ 
$=$$\;\;\;\;${\rm{car}}\,({\rm{nth-cdr}}\,({\it{k\/}}, {\it{a\/}})\index{nth-cdr}))\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  equal-nth-cdr-nil \\ \index{equal-nth-cdr-nil}
{\rm{bignp}}\,({\it{a\/}}, {\it{base\/}})\index{bignp} $\rightarrow$ (({\bf{nil}} $=$ {\rm{nth-cdr}}\,({\it{i\/}}, {\it{a\/}})\index{nth-cdr}) $=$ ({\rm{fix}}\,({\it{i\/}}) $=$ {\rm{length}}\,({\it{a\/}})\index{length}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  equal-cddr-nth-cdr-nil \\ \index{equal-cddr-nth-cdr-nil}
\=\+{\rm{bignp}}\,({\it{a\/}}, {\it{base\/}})\index{bignp} \\ 
$\rightarrow$$\;\;\;\;$(({\bf{nil}} $=$ {\rm{cddr}}\,({\rm{nth-cdr}}\,({\it{i\/}}, {\it{a\/}})\index{nth-cdr})) $=$ (($1\;+$ ($1\;+$ {\it{i\/}})) $=$ {\rm{length}}\,({\it{a\/}})\index{length}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bignp-put \\ \index{bignp-put}
\=\+(\=\+({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\rm{length}}\,({\it{a\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;${\rm{bignp}}\,({\it{a\/}}, {\it{base\/}})\index{bignp} \\ 
$\wedge$$\;\;\;\;$({\it{val\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{val\/}} $<$ {\it{base\/}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{bignp}}\,({\rm{put}}\,({\rm{list}}\,({\tt{'}}{\tt{nat}}, {\it{val\/}}), {\it{i\/}}, {\it{a\/}})\index{put}, {\it{base\/}})\index{bignp}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  cons-car-cdr-hack \\ \index{cons-car-cdr-hack}
({\rm{cons}}\,({\it{a\/}}, {\rm{cdr}}\,({\it{x\/}})) $=$ {\it{x\/}}) $=$ ({\rm{listp}}\,({\it{x\/}}) $\wedge$ ({\it{a\/}} $=$ {\rm{car}}\,({\it{x\/}})))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  big-add-array-is-big-add-array-loop-generalized \\ \index{big-add-array-is-big-add-array-!loop-generalized}
\=\+(\=\+({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\rm{length}}\,({\it{a\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;${\rm{bignp}}\,({\it{a\/}}, {\it{base\/}})\index{bignp} \\ 
$\wedge$$\;\;\;\;$({\it{base\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{base\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{big-add-array}}\,({\rm{nth-cdr}}\,({\it{i\/}}, {\it{a\/}})\index{nth-cdr}, {\rm{nth-cdr}}\,({\it{i\/}}, {\it{b\/}})\index{nth-cdr}, {\it{c\/}}, {\it{base\/}})\index{big-add-array} \\ 
$=$$\;\;\;\;${\rm{nth-cdr}}\,({\it{i\/}}, {\rm{big-add-array-loop}}\,({\it{i\/}}, {\it{a\/}}, {\it{b\/}}, {\rm{length}}\,({\it{a\/}})\index{length} $-$ {\it{i\/}}, {\it{c\/}}, {\it{base\/}})\index{big-add-array-loop})\index{nth-cdr})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  big-add-array-is-big-add-array-loop \\ \index{big-add-array-is-big-add-array-!loop}
\=\+({\rm{listp}}\,({\it{a\/}}) $\wedge$ {\rm{bignp}}\,({\it{a\/}}, {\it{base\/}})\index{bignp} $\wedge$ ({\it{base\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\tt{1}} $<$ {\it{base\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{big-add-array}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}}, {\it{base\/}})\index{big-add-array} \\ 
$=$$\;\;\;\;${\rm{big-add-array-loop}}\,({\tt{0}}, {\it{a\/}}, {\it{b\/}}, {\rm{length}}\,({\it{a\/}})\index{length}, {\it{c\/}}, {\it{base\/}})\index{big-add-array-loop})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  big-add-carry-out-on-list-of-length-1 \\ \index{big-add-carry-out-on-list-of-le!ngth-1}
\=\+({\rm{listp}}\,({\it{a\/}}) $\wedge$ ({\rm{cdr}}\,({\it{a\/}}) $\simeq\;${{\bf{nil}}}${}$)) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{big-add-carry-out}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}}, {\it{base\/}})\index{big-add-carry-out} \\ 
$=$$\;\;\;\;${\rm{bool}}\,(\=\+({\rm{untag}}\,({\rm{car}}\,({\it{a\/}}))\index{untag} $+$ {\rm{untag}}\,({\rm{car}}\,({\it{b\/}}))\index{untag} $+$ {\rm{tv-$>$nat}}\,({\it{c\/}})\index{tv-$>$nat}) \\ 
$\not<$$\;\;\;\;${\it{base\/}}\-)\index{bool})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  big-add-carry-out-is-big-add-carry-out-loop-generalized \\ \index{big-add-carry-out-is-big-add-ca!rry-out-loop-generalized}
\=\+(({\it{i\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{i\/}} $<$ {\rm{length}}\,({\it{a\/}})\index{length})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{big-add-carry-out}}\,({\rm{nth-cdr}}\,({\it{i\/}}, {\it{a\/}})\index{nth-cdr}, {\rm{nth-cdr}}\,({\it{i\/}}, {\it{b\/}})\index{nth-cdr}, {\it{c\/}}, {\it{base\/}})\index{big-add-carry-out} \\ 
$=$$\;\;\;\;${\rm{big-add-carry-out-loop}}\,({\it{i\/}}, {\it{a\/}}, {\it{b\/}}, {\rm{length}}\,({\it{a\/}})\index{length} $-$ {\it{i\/}}, {\it{c\/}}, {\it{base\/}})\index{big-add-carry-out-loop})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  big-add-carry-out-is-big-add-carry-out-loop \\ \index{big-add-carry-out-is-big-add-ca!rry-out-loop}
\=\+{\rm{listp}}\,({\it{a\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{big-add-carry-out}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}}, {\it{base\/}})\index{big-add-carry-out} \\ 
$=$$\;\;\;\;${\rm{big-add-carry-out-loop}}\,({\tt{0}}, {\it{a\/}}, {\it{b\/}}, {\rm{length}}\,({\it{a\/}})\index{length}, {\it{c\/}}, {\it{base\/}})\index{big-add-carry-out-loop})\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{big-add-program} \\  
\=\+{\sc{big-add-program}}\index{big-add-program} \\ 
$=$$\;\;\;\;${\tt{'}}{\tt{(}}\=\+{\tt{big-add}} \\ 
{\tt{(}}{\tt{a}}{\tt{ }}{\tt{b}}{\tt{ }}{\tt{n}}{\tt{)}} \\ 
{\tt{nil}} \\ 
{\tt{(}}{\tt{push-constant}}{\tt{ }}{\tt{(}}{\tt{bool}}{\tt{ }}{\tt{f}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}{\tt{push-local}}{\tt{ }}{\tt{a}}{\tt{)}} \\ 
{\tt{(}}{\tt{dl}}{\tt{ }}{\tt{loop}}{\tt{ }}{\tt{nil}}{\tt{ }}{\tt{(}}{\tt{fetch}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}{\tt{push-local}}{\tt{ }}{\tt{b}}{\tt{)}} \\ 
{\tt{(}}{\tt{fetch}}{\tt{)}} \\ 
{\tt{(}}{\tt{add-nat-with-carry}}{\tt{)}} \\ 
{\tt{(}}{\tt{push-local}}{\tt{ }}{\tt{a}}{\tt{)}} \\ 
{\tt{(}}{\tt{deposit}}{\tt{)}} \\ 
{\tt{(}}{\tt{push-local}}{\tt{ }}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}{\tt{sub1-nat}}{\tt{)}} \\ 
{\tt{(}}{\tt{set-local}}{\tt{ }}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}{\tt{test-nat-and-jump}}{\tt{ }}{\tt{zero}}{\tt{ }}{\tt{done}}{\tt{)}} \\ 
{\tt{(}}{\tt{push-local}}{\tt{ }}{\tt{b}}{\tt{)}} \\ 
{\tt{(}}{\tt{push-constant}}{\tt{ }}{\tt{(}}{\tt{nat}}{\tt{ }}{\tt{1}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}{\tt{add-addr}}{\tt{)}} \\ 
{\tt{(}}{\tt{pop-local}}{\tt{ }}{\tt{b}}{\tt{)}} \\ 
{\tt{(}}{\tt{push-local}}{\tt{ }}{\tt{a}}{\tt{)}} \\ 
{\tt{(}}{\tt{push-constant}}{\tt{ }}{\tt{(}}{\tt{nat}}{\tt{ }}{\tt{1}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}{\tt{add-addr}}{\tt{)}} \\ 
{\tt{(}}{\tt{set-local}}{\tt{ }}{\tt{a}}{\tt{)}} \\ 
{\tt{(}}{\tt{jump}}{\tt{ }}{\tt{loop}}{\tt{)}} \\ 
{\tt{(}}{\tt{dl}}{\tt{ }}{\tt{done}}{\tt{ }}{\tt{nil}}{\tt{ }}{\tt{(}}{\tt{ret}}{\tt{)}}{\tt{)}}{\tt{)}}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{big-add-loop-clock} \\  
\=\+{\rm{big-add-loop-clock}}\,({\it{n\/}})\index{big-add-loop-clock} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{n\/}} $=$ {\tt{1}}$\;\;${\bf then }{\tt{11}} \\ 
{\bf else }{\tt{19}} $+$ {\rm{big-add-loop-clock}}\,({\it{n\/}} $-\;1$)\index{big-add-loop-clock}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; The following clock function includes one tick for the CALL.  That is,
; BIG-ADD-CLOCK is the amount of time it takes to execute a CALL of BIG-ADD,
; not just the body of BIG-ADD.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{big-add-clock}$\;\;$
{\rm{big-add-clock}}\,({\it{n\/}})\index{big-add-clock} $=$ ({\tt{3}} $+$ {\rm{big-add-loop-clock}}\,({\it{n\/}})\index{big-add-loop-clock})
\end{tabbing}

\begin{verbatim}; The concept of value in the defs.events is at odds with the
; use of the term in the report.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{array}$\;\;$
{\rm{array}}\,({\it{name\/}}, {\it{segment\/}})\index{array} $=$ {\rm{cdr}}\,({\rm{assoc}}\,({\it{name\/}}, {\it{segment\/}}))
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{put-array} \\  
{\rm{put-array}}\,({\it{a\/}}, {\it{name\/}}, {\it{segment\/}})\index{put-array} $=$ {\rm{put-assoc}}\,({\it{a\/}}, {\it{name\/}}, {\it{segment\/}})\index{put-assoc}
\end{tabbing}


\noindent{\sc Event}:   Disable booleanp.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{tv}$\;\;$
{\rm{tv}}\,({\it{b\/}})\index{tv} $=$ ({\it{b\/}} $=$ {\tt{'}}{\tt{t}})
\end{tabbing}


\noindent{\sc Event}:   Enable assoc-put-assoc-2.

\addvspace{18pt}


\noindent{\sc Event}:   Disable get-is-car-nth-cdr.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  p-step1-opener \\ \index{p-step1-opener}
\=\+{\rm{p-step1}}\,({\rm{cons}}\,({\it{opcode\/}}, {\it{operands\/}}), {\it{p\/}})\index{p-step1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{p-ins-okp}}\,({\rm{cons}}\,({\it{opcode\/}}, {\it{operands\/}}), {\it{p\/}})\index{p-ins-okp} \\ 
{\bf then }{\rm{p-ins-step}}\,({\rm{cons}}\,({\it{opcode\/}}, {\it{operands\/}}), {\it{p\/}})\index{p-ins-step} \\ 
{\bf else }{\rm{p-halt}}\,({\it{p\/}}, {\rm{x-y-error-msg}}\,({\tt{'}}{\tt{p}}, {\it{opcode\/}})\index{x-y-error-msg})\index{p-halt}$\;${\bf  endif}\-\-
\end{tabbing}


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

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  p-opener \\ \index{p-opener}
\=\+({\rm{p}}\,({\it{s\/}}, {\tt{0}})\index{p} $=$ {\it{s\/}}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{p}}\,(\=\+{\rm{p-state}}\,({\it{pc\/}}, {\it{ctrl\/}}, {\it{temp\/}}, {\it{prog\/}}, {\it{data\/}}, {\it{max-ctrl\/}}, {\it{max-temp\/}}, {\it{word-size\/}}, {\it{psw\/}})\index{p-state}, \\ 
$1\;+$ {\it{n\/}})\-\index{p} \\ 
$=$$\;\;\;\;${\rm{p}}\,(\=\+{\rm{p-step}}\,({\rm{p-state}}\,(\=\+{\it{pc\/}}, \\ 
{\it{ctrl\/}}, \\ 
{\it{temp\/}}, \\ 
{\it{prog\/}}, \\ 
{\it{data\/}}, \\ 
{\it{max-ctrl\/}}, \\ 
{\it{max-temp\/}}, \\ 
{\it{word-size\/}}, \\ 
{\it{psw\/}})\-\index{p-state})\index{p-step}, \\ 
{\it{n\/}})\-\index{p})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable p.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  bignp-implies-p-objectp-get \\ \index{bignp-implies-p-objectp-get}
\=\+({\rm{bignp}}\,({\it{a\/}}, {\rm{exp}}\,({\tt{2}}, {\it{word-size\/}})\index{exp})\index{bignp} $\wedge$ ({\it{i\/}} $<$ {\rm{length}}\,({\it{a\/}})\index{length})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{listp}}\,({\rm{get}}\,({\it{i\/}}, {\it{a\/}})\index{get}) \\ 
$\wedge$$\;\;\;\;$({\rm{cddr}}\,({\rm{get}}\,({\it{i\/}}, {\it{a\/}})\index{get}) $=$ {\bf{nil}}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\rm{get}}\,({\it{i\/}}, {\it{a\/}})\index{get}) $=$ {\tt{'}}{\tt{nat}}) \\ 
$\wedge$$\;\;\;\;$({\rm{cadr}}\,({\rm{get}}\,({\it{i\/}}, {\it{a\/}})\index{get}) $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{cadr}}\,({\rm{get}}\,({\it{i\/}}, {\it{a\/}})\index{get}) $<$ {\rm{exp}}\,({\tt{2}}, {\it{word-size\/}})\index{exp}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  booleanp-not-f \\ \index{booleanp-not-f}
({\rm{booleanp}}\,({\it{c\/}})\index{booleanp} $\wedge$ ({\it{c\/}} $\not=$ {\tt{'}}{\tt{f}})) $\rightarrow$ (({\it{c\/}} $=$ {\tt{'}}{\tt{t}}) $=$ {\bf{t}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-1-base \\ \index{lessp-1-base}
({\it{word-size\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ ({\tt{1}} $<$ {\rm{exp}}\,({\tt{2}}, {\it{word-size\/}})\index{exp})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  assoc-put-assoc-2-new \\ \index{assoc-put-assoc-2-new}
({\it{a\/}} $\not=$ {\it{b\/}}) $\rightarrow$ ({\rm{assoc}}\,({\it{a\/}}, {\rm{put-assoc}}\,({\it{val\/}}, {\it{b\/}}, {\it{segment\/}})\index{put-assoc}) $=$ {\rm{assoc}}\,({\it{a\/}}, {\it{segment\/}}))
\end{tabbing}


\noindent{\sc Event}:   Enable definedp-put-assoc.

\addvspace{18pt}

\begin{verbatim}; ??? I am here.  The db is here.  The comment above is wrong.  Since then
; I have changed the theorem by eliminating the hyp (equal p (p-state ...)).
; I see no alternative to simply starting the proof of the thm below over again.
; That is what I have done.  The comment above remains just as a reminder of where
; I was.  It should be deleted when I start afresh.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  booleanp-not-f-tv-$>$nat \\ \index{booleanp-not-f-tv-$>$nat}
({\rm{booleanp}}\,({\it{c\/}})\index{booleanp} $\wedge$ ({\it{c\/}} $\not=$ {\tt{'}}{\tt{f}})) $\rightarrow$ ({\rm{tv-$>$nat}}\,({\it{c\/}})\index{tv-$>$nat} $=$ {\tt{1}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{big-add-loop-correct-hint} \\  
\=\+{\rm{big-add-loop-correct-hint}}\,({\it{a\/}}, {\it{b\/}}, {\it{i\/}}, {\it{data-segment\/}}, {\it{c\/}}, {\it{word-size\/}})\index{big-add-loop-correct-hint} \\ 
$=$$\;\;\;\;$\=\+{\bf if }\=\+{\rm{definedp}}\,({\it{a\/}}, {\it{data-segment\/}})\index{definedp} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\rm{length}}\,({\rm{array}}\,({\it{a\/}}, {\it{data-segment\/}})\index{array})\index{length})\- \\ 
{\bf then }\=\+{\bf if }(({\rm{length}}\,({\rm{array}}\,({\it{a\/}}, {\it{data-segment\/}})\index{array})\index{length} $-$ {\it{i\/}}) $-\;1$) $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{big-add-loop-correct-hint}}\,(\=\+{\it{a\/}}, \\ 
{\it{b\/}}, \\ 
$1\;+$ {\it{i\/}}, \\ 
{\rm{put-assoc}}\,(\=\+{\rm{put}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{nat}}, \\ 
\=\+(\=\+{\rm{untag}}\,({\rm{get}}\,(\=\+{\it{i\/}}, \\ 
{\rm{array}}\,(\=\+{\it{a\/}}, \\ 
{\it{data-segment\/}})\-\index{array})\-\index{get})\index{untag} \\ 
$+$$\;\;\;\;${\rm{untag}}\,({\rm{get}}\,(\=\+{\it{i\/}}, \\ 
{\rm{array}}\,(\=\+{\it{b\/}}, \\ 
{\it{data-segment\/}})\-\index{array})\-\index{get})\index{untag} \\ 
$+$$\;\;\;\;${\rm{bool-to-nat}}\,({\it{c\/}})\index{bool-to-nat})\- \\ 
${}${\bf{mod}}${}$$\;\;\;\;${\rm{exp}}\,(\=\+{\tt{2}}, \\ 
{\it{word-size\/}})\-\index{exp}\-)\-\index{tag}, \\ 
{\it{i\/}}, \\ 
{\rm{array}}\,(\=\+{\it{a\/}}, \\ 
{\it{data-segment\/}})\-\index{array})\-\index{put}, \\ 
{\it{a\/}}, \\ 
{\it{data-segment\/}})\-\index{put-assoc}, \\ 
\=\+{\bf if }\=\+(\=\+{\rm{untag}}\,({\rm{get}}\,(\=\+{\it{i\/}}, \\ 
{\rm{array}}\,(\=\+{\it{a\/}}, \\ 
{\it{data-segment\/}})\-\index{array})\-\index{get})\index{untag} \\ 
$+$$\;\;\;\;${\rm{untag}}\,({\rm{get}}\,(\=\+{\it{i\/}}, \\ 
{\rm{array}}\,(\=\+{\it{b\/}}, \\ 
{\it{data-segment\/}})\-\index{array})\-\index{get})\index{untag} \\ 
$+$$\;\;\;\;${\rm{bool-to-nat}}\,({\it{c\/}})\index{bool-to-nat})\- \\ 
$<$$\;\;\;\;${\rm{exp}}\,({\tt{2}}, {\it{word-size\/}})\index{exp}\- \\ 
{\bf then }{\tt{'}}{\tt{f}} \\ 
{\bf else }{\tt{'}}{\tt{t}}$\;${\bf  endif}\-, \\ 
{\it{word-size\/}})\-\index{big-add-loop-correct-hint}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}


\noindent{\sc Event}:   Enable put-assoc-put-assoc.

\addvspace{18pt}

\begin{verbatim}; I have proved 2 of the 3 cases of this.  I think the remaining case is
; trivial.  I will add it as an axiom and proceed.  The proof takes about
; 3 hours, judging from the two cases I did.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  big-add-loop-correct-generalized \\ \index{big-add-loop-correct-generalize!d}
\=\+(\=\+({\rm{length}}\,({\rm{array}}\,({\it{a\/}}, {\it{data-segment\/}})\index{array})\index{length} $<$ {\rm{exp}}\,({\tt{2}}, {\it{word-size\/}})\index{exp}) \\ 
$\wedge$$\;\;\;\;$({\it{word-size\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{bignp}}\,({\rm{array}}\,({\it{a\/}}, {\it{data-segment\/}})\index{array}, {\rm{exp}}\,({\tt{2}}, {\it{word-size\/}})\index{exp})\index{bignp} \\ 
$\wedge$$\;\;\;\;${\rm{bignp}}\,({\rm{array}}\,({\it{b\/}}, {\it{data-segment\/}})\index{array}, {\rm{exp}}\,({\tt{2}}, {\it{word-size\/}})\index{exp})\index{bignp} \\ 
$\wedge$$\;\;\;\;$({\it{max-temp-stk-size\/}} $\not<$ ($1\;+$ ($1\;+$ ($1\;+$ {\rm{length}}\,({\it{temp-stk\/}})\index{length})))) \\ 
$\wedge$$\;\;\;\;$({\rm{definition}}\,({\tt{'}}{\tt{big-add}}, {\it{prog-segment\/}})\index{definition} $=$ {\sc{big-add-program}}\index{big-add-program}) \\ 
$\wedge$$\;\;\;\;${\rm{definedp}}\,({\it{a\/}}, {\it{data-segment\/}})\index{definedp} \\ 
$\wedge$$\;\;\;\;${\rm{definedp}}\,({\it{b\/}}, {\it{data-segment\/}})\index{definedp} \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $\not=$ {\it{b\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $=$ {\rm{length}}\,({\rm{array}}\,({\it{a\/}}, {\it{data-segment\/}})\index{array})\index{length}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $=$ {\rm{length}}\,({\rm{array}}\,({\it{b\/}}, {\it{data-segment\/}})\index{array})\index{length}) \\ 
$\wedge$$\;\;\;\;${\rm{booleanp}}\,({\it{c\/}})\index{booleanp})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p}}\,(\=\+{\rm{p-state}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{pc}}{\tt{ }}{\tt{(}}{\tt{big-add}}{\tt{ .\ }}{\tt{2}}{\tt{)}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\rm{list}}\,(\=\+{\rm{list}}\,(\=\+{\rm{cons}}\,({\tt{'}}{\tt{a}}, {\rm{list}}\,({\tt{'}}{\tt{addr}}, {\rm{cons}}\,({\it{a\/}}, {\it{i\/}}))), \\ 
{\rm{cons}}\,({\tt{'}}{\tt{b}}, {\rm{list}}\,({\tt{'}}{\tt{addr}}, {\rm{cons}}\,({\it{b\/}}, {\it{i\/}}))), \\ 
{\rm{cons}}\,({\tt{'}}{\tt{n}}, {\rm{list}}\,({\tt{'}}{\tt{nat}}, {\it{n\/}} $-$ {\it{i\/}})))\-, \\ 
{\it{ret-pc\/}})\-, \\ 
{\it{ctrl-stk\/}})\-, \\ 
{\rm{cons}}\,({\rm{list}}\,({\tt{'}}{\tt{addr}}, {\rm{cons}}\,({\it{a\/}}, {\it{i\/}})), {\rm{cons}}\,({\rm{list}}\,({\tt{'}}{\tt{bool}}, {\it{c\/}}), {\it{temp-stk\/}})), \\ 
{\it{prog-segment\/}}, \\ 
{\it{data-segment\/}}, \\ 
{\it{max-ctrl-stk-size\/}}, \\ 
{\it{max-temp-stk-size\/}}, \\ 
{\it{word-size\/}}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}, \\ 
{\rm{big-add-loop-clock}}\,({\it{n\/}} $-$ {\it{i\/}})\index{big-add-loop-clock})\-\index{p} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\it{ret-pc\/}}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{cons}}\,(\=\+{\rm{big-add-carry-out-loop}}\,(\=\+{\it{i\/}}, \\ 
{\rm{array}}\,({\it{a\/}}, {\it{data-segment\/}})\index{array}, \\ 
{\rm{array}}\,({\it{b\/}}, {\it{data-segment\/}})\index{array}, \\ 
{\it{n\/}} $-$ {\it{i\/}}, \\ 
{\rm{tv}}\,({\it{c\/}})\index{tv}, \\ 
{\rm{exp}}\,({\tt{2}}, {\it{word-size\/}})\index{exp})\-\index{big-add-carry-out-loop}, \\ 
{\it{temp-stk\/}})\-, \\ 
{\it{prog-segment\/}}, \\ 
{\rm{put-assoc}}\,(\=\+{\rm{big-add-array-loop}}\,(\=\+{\it{i\/}}, \\ 
{\rm{array}}\,({\it{a\/}}, {\it{data-segment\/}})\index{array}, \\ 
{\rm{array}}\,({\it{b\/}}, {\it{data-segment\/}})\index{array}, \\ 
{\it{n\/}} $-$ {\it{i\/}}, \\ 
{\rm{tv}}\,({\it{c\/}})\index{tv}, \\ 
{\rm{exp}}\,({\tt{2}}, {\it{word-size\/}})\index{exp})\-\index{big-add-array-loop}, \\ 
{\it{a\/}}, \\ 
{\it{data-segment\/}})\-\index{put-assoc}, \\ 
{\it{max-ctrl-stk-size\/}}, \\ 
{\it{max-temp-stk-size\/}}, \\ 
{\it{word-size\/}}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  big-add-loop-correct \\ \index{big-add-loop-correct}
\=\+(\=\+({\rm{length}}\,({\rm{array}}\,({\it{a\/}}, {\it{data-segment\/}})\index{array})\index{length} $<$ {\rm{exp}}\,({\tt{2}}, {\it{word-size\/}})\index{exp}) \\ 
$\wedge$$\;\;\;\;$({\it{word-size\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{bignp}}\,({\rm{array}}\,({\it{a\/}}, {\it{data-segment\/}})\index{array}, {\rm{exp}}\,({\tt{2}}, {\it{word-size\/}})\index{exp})\index{bignp} \\ 
$\wedge$$\;\;\;\;${\rm{bignp}}\,({\rm{array}}\,({\it{b\/}}, {\it{data-segment\/}})\index{array}, {\rm{exp}}\,({\tt{2}}, {\it{word-size\/}})\index{exp})\index{bignp} \\ 
$\wedge$$\;\;\;\;$({\it{max-temp-stk-size\/}} $\not<$ ($1\;+$ ($1\;+$ ($1\;+$ {\rm{length}}\,({\it{temp-stk\/}})\index{length})))) \\ 
$\wedge$$\;\;\;\;$({\rm{definition}}\,({\tt{'}}{\tt{big-add}}, {\it{prog-segment\/}})\index{definition} $=$ {\sc{big-add-program}}\index{big-add-program}) \\ 
$\wedge$$\;\;\;\;${\rm{definedp}}\,({\it{a\/}}, {\it{data-segment\/}})\index{definedp} \\ 
$\wedge$$\;\;\;\;${\rm{definedp}}\,({\it{b\/}}, {\it{data-segment\/}})\index{definedp} \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $\not=$ {\it{b\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $=$ {\rm{length}}\,({\rm{array}}\,({\it{a\/}}, {\it{data-segment\/}})\index{array})\index{length}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $=$ {\rm{length}}\,({\rm{array}}\,({\it{b\/}}, {\it{data-segment\/}})\index{array})\index{length}) \\ 
$\wedge$$\;\;\;\;${\rm{booleanp}}\,({\it{c\/}})\index{booleanp})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p}}\,(\=\+{\rm{p-state}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{pc}}{\tt{ }}{\tt{(}}{\tt{big-add}}{\tt{ .\ }}{\tt{2}}{\tt{)}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\rm{list}}\,(\=\+{\rm{list}}\,(\=\+{\rm{cons}}\,({\tt{'}}{\tt{a}}, {\rm{list}}\,({\tt{'}}{\tt{addr}}, {\rm{cons}}\,({\it{a\/}}, {\tt{0}}))), \\ 
{\rm{cons}}\,({\tt{'}}{\tt{b}}, {\rm{list}}\,({\tt{'}}{\tt{addr}}, {\rm{cons}}\,({\it{b\/}}, {\tt{0}}))), \\ 
{\rm{cons}}\,({\tt{'}}{\tt{n}}, {\rm{list}}\,({\tt{'}}{\tt{nat}}, {\it{n\/}})))\-, \\ 
{\it{ret-pc\/}})\-, \\ 
{\it{ctrl-stk\/}})\-, \\ 
{\rm{cons}}\,(\=\+{\rm{list}}\,({\tt{'}}{\tt{addr}}, {\rm{cons}}\,({\it{a\/}}, {\tt{0}})), \\ 
{\rm{cons}}\,({\rm{list}}\,({\tt{'}}{\tt{bool}}, {\it{c\/}}), {\it{temp-stk\/}}))\-, \\ 
{\it{prog-segment\/}}, \\ 
{\it{data-segment\/}}, \\ 
{\it{max-ctrl-stk-size\/}}, \\ 
{\it{max-temp-stk-size\/}}, \\ 
{\it{word-size\/}}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}, \\ 
{\rm{big-add-loop-clock}}\,({\it{n\/}})\index{big-add-loop-clock})\-\index{p} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\it{ret-pc\/}}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{cons}}\,(\=\+{\rm{big-add-carry-out-loop}}\,(\=\+{\tt{0}}, \\ 
{\rm{array}}\,({\it{a\/}}, {\it{data-segment\/}})\index{array}, \\ 
{\rm{array}}\,({\it{b\/}}, {\it{data-segment\/}})\index{array}, \\ 
{\it{n\/}}, \\ 
{\rm{tv}}\,({\it{c\/}})\index{tv}, \\ 
{\rm{exp}}\,({\tt{2}}, {\it{word-size\/}})\index{exp})\-\index{big-add-carry-out-loop}, \\ 
{\it{temp-stk\/}})\-, \\ 
{\it{prog-segment\/}}, \\ 
{\rm{put-assoc}}\,(\=\+{\rm{big-add-array-loop}}\,(\=\+{\tt{0}}, \\ 
{\rm{array}}\,({\it{a\/}}, {\it{data-segment\/}})\index{array}, \\ 
{\rm{array}}\,({\it{b\/}}, {\it{data-segment\/}})\index{array}, \\ 
{\it{n\/}}, \\ 
{\rm{tv}}\,({\it{c\/}})\index{tv}, \\ 
{\rm{exp}}\,({\tt{2}}, {\it{word-size\/}})\index{exp})\-\index{big-add-array-loop}, \\ 
{\it{a\/}}, \\ 
{\it{data-segment\/}})\-\index{put-assoc}, \\ 
{\it{max-ctrl-stk-size\/}}, \\ 
{\it{max-temp-stk-size\/}}, \\ 
{\it{word-size\/}}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state})\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{big-add-input-conditionp} \\  
\=\+{\rm{big-add-input-conditionp}}\,({\it{a\/}}, {\it{b\/}}, {\it{n\/}}, {\it{p0\/}})\index{big-add-input-conditionp} \\ 
$=$$\;\;\;\;$(\=\+{\rm{definedp}}\,({\it{a\/}}, {\rm{p-data-segment}}\,({\it{p0\/}})\index{p-data-segment})\index{definedp} \\ 
$\wedge$$\;\;\;\;${\rm{definedp}}\,({\it{b\/}}, {\rm{p-data-segment}}\,({\it{p0\/}})\index{p-data-segment})\index{definedp} \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $\not=$ {\it{b\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{bignp}}\,({\rm{array}}\,({\it{a\/}}, {\rm{p-data-segment}}\,({\it{p0\/}})\index{p-data-segment})\index{array}, {\rm{exp}}\,({\tt{2}}, {\rm{p-word-size}}\,({\it{p0\/}})\index{p-word-size})\index{exp})\index{bignp} \\ 
$\wedge$$\;\;\;\;${\rm{bignp}}\,({\rm{array}}\,({\it{b\/}}, {\rm{p-data-segment}}\,({\it{p0\/}})\index{p-data-segment})\index{array}, {\rm{exp}}\,({\tt{2}}, {\rm{p-word-size}}\,({\it{p0\/}})\index{p-word-size})\index{exp})\index{bignp} \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $=$ {\rm{length}}\,({\rm{array}}\,({\it{a\/}}, {\rm{p-data-segment}}\,({\it{p0\/}})\index{p-data-segment})\index{array})\index{length}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $=$ {\rm{length}}\,({\rm{array}}\,({\it{b\/}}, {\rm{p-data-segment}}\,({\it{p0\/}})\index{p-data-segment})\index{array})\index{length}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{p-max-ctrl-stk-size}}\,({\it{p0\/}})\index{p-max-ctrl-stk-size} \\ 
$\not<$$\;\;\;\;$({\tt{5}} $+$ {\rm{p-ctrl-stk-size}}\,({\rm{p-ctrl-stk}}\,({\it{p0\/}})\index{p-ctrl-stk})\index{p-ctrl-stk-size}))\- \\ 
$\wedge$$\;\;\;\;$({\rm{p-max-temp-stk-size}}\,({\it{p0\/}})\index{p-max-temp-stk-size} $\not<$ ({\tt{3}} $+$ {\rm{length}}\,({\rm{p-temp-stk}}\,({\it{p0\/}})\index{p-temp-stk})\index{length})) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $<$ {\rm{exp}}\,({\tt{2}}, {\rm{p-word-size}}\,({\it{p0\/}})\index{p-word-size})\index{exp}) \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\rm{p-ctrl-stk}}\,({\it{p0\/}})\index{p-ctrl-stk}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  not-zerop-wordsize-hack \\ \index{not-zerop-wordsize-hack}
\=\+(({\it{n\/}} $<$ {\rm{exp}}\,({\tt{2}}, {\it{word-size\/}})\index{exp}) $\wedge$ ({\it{n\/}} $\not\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;$((({\it{word-size\/}} $\in\;${\bf{N}}${}$) $=$ {\bf{t}}) $\wedge$ ({\it{word-size\/}} $\not=$ {\tt{0}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  big-add-correct \\ \index{big-add-correct}
\=\+(\=\+({\it{p0\/}} $=$ {\rm{p-state}}\,(\=\+{\it{pc\/}}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{append}}\,(\=\+{\rm{list}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{nat}}, {\it{n\/}})\index{tag}, \\ 
{\rm{tag}}\,({\tt{'}}{\tt{addr}}, {\rm{cons}}\,({\it{b\/}}, {\tt{0}}))\index{tag}, \\ 
{\rm{tag}}\,({\tt{'}}{\tt{addr}}, {\rm{cons}}\,({\it{a\/}}, {\tt{0}}))\index{tag})\-, \\ 
{\it{temp-stk\/}})\-, \\ 
{\it{prog-segment\/}}, \\ 
{\it{data-segment\/}}, \\ 
{\it{max-ctrl-stk-size\/}}, \\ 
{\it{max-temp-stk-size\/}}, \\ 
{\it{word-size\/}}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}) \\ 
$\wedge$$\;\;\;\;$({\rm{p-current-instruction}}\,({\it{p0\/}})\index{p-current-instruction} $=$ {\tt{'}}{\tt{(}}{\tt{call}}{\tt{ }}{\tt{big-add}}{\tt{)}}) \\ 
$\wedge$$\;\;\;\;$({\rm{definition}}\,({\tt{'}}{\tt{big-add}}, {\it{prog-segment\/}})\index{definition} $=$ {\sc{big-add-program}}\index{big-add-program}) \\ 
$\wedge$$\;\;\;\;${\rm{big-add-input-conditionp}}\,({\it{a\/}}, {\it{b\/}}, {\it{n\/}}, {\it{p0\/}})\index{big-add-input-conditionp})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p}}\,({\it{p0\/}}, {\rm{big-add-clock}}\,({\it{n\/}})\index{big-add-clock})\index{p} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{add1-addr}}\,({\it{pc\/}})\index{add1-addr}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{push}}\,(\=\+{\rm{big-add-carry-out}}\,(\=\+{\rm{array}}\,({\it{a\/}}, {\it{data-segment\/}})\index{array}, \\ 
{\rm{array}}\,({\it{b\/}}, {\it{data-segment\/}})\index{array}, \\ 
{\bf{f}}, \\ 
{\rm{exp}}\,({\tt{2}}, {\it{word-size\/}})\index{exp})\-\index{big-add-carry-out}, \\ 
{\it{temp-stk\/}})\-\index{push}, \\ 
{\it{prog-segment\/}}, \\ 
{\rm{put-array}}\,(\=\+{\rm{big-add-array}}\,(\=\+{\rm{array}}\,({\it{a\/}}, {\it{data-segment\/}})\index{array}, \\ 
{\rm{array}}\,({\it{b\/}}, {\it{data-segment\/}})\index{array}, \\ 
{\bf{f}}, \\ 
{\rm{exp}}\,({\tt{2}}, {\it{word-size\/}})\index{exp})\-\index{big-add-array}, \\ 
{\it{a\/}}, \\ 
{\it{data-segment\/}})\-\index{put-array}, \\ 
{\it{max-ctrl-stk-size\/}}, \\ 
{\it{max-temp-stk-size\/}}, \\ 
{\it{word-size\/}}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state})\-\-
\end{tabbing}

\begin{verbatim}; The above thm is not useful as a rewrite rule because p0 occurs
; in the lhs and pc, ctrl-stk, etc., are all free vars.  So to make it
; a rewrite rule we actually substitute (p-state pc ...) for p0 into the
; lhs.  In addition, the append in that initial state is going to be
; conses in applications, so we expand it in the lhs.  In addition,
; the tags are expanded to lists.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  big-add-correct-rewrite-version \\ \index{big-add-correct-rewrite-version}
\=\+(\=\+({\it{p0\/}} $=$ {\rm{p-state}}\,(\=\+{\it{pc\/}}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{append}}\,(\=\+{\rm{list}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{nat}}, {\it{n\/}})\index{tag}, \\ 
{\rm{tag}}\,({\tt{'}}{\tt{addr}}, {\rm{cons}}\,({\it{b\/}}, {\tt{0}}))\index{tag}, \\ 
{\rm{tag}}\,({\tt{'}}{\tt{addr}}, {\rm{cons}}\,({\it{a\/}}, {\tt{0}}))\index{tag})\-, \\ 
{\it{temp-stk\/}})\-, \\ 
{\it{prog-segment\/}}, \\ 
{\it{data-segment\/}}, \\ 
{\it{max-ctrl-stk-size\/}}, \\ 
{\it{max-temp-stk-size\/}}, \\ 
{\it{word-size\/}}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}) \\ 
$\wedge$$\;\;\;\;$({\rm{p-current-instruction}}\,({\it{p0\/}})\index{p-current-instruction} $=$ {\tt{'}}{\tt{(}}{\tt{call}}{\tt{ }}{\tt{big-add}}{\tt{)}}) \\ 
$\wedge$$\;\;\;\;$({\rm{definition}}\,({\tt{'}}{\tt{big-add}}, {\it{prog-segment\/}})\index{definition} $=$ {\sc{big-add-program}}\index{big-add-program}) \\ 
$\wedge$$\;\;\;\;${\rm{big-add-input-conditionp}}\,({\it{a\/}}, {\it{b\/}}, {\it{n\/}}, {\it{p0\/}})\index{big-add-input-conditionp})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p}}\,(\=\+{\rm{p-state}}\,(\=\+{\it{pc\/}}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{cons}}\,(\=\+{\rm{list}}\,({\tt{'}}{\tt{nat}}, {\it{n\/}}), \\ 
{\rm{cons}}\,(\=\+{\rm{list}}\,({\tt{'}}{\tt{addr}}, {\rm{cons}}\,({\it{b\/}}, {\tt{0}})), \\ 
{\rm{cons}}\,({\rm{list}}\,({\tt{'}}{\tt{addr}}, {\rm{cons}}\,({\it{a\/}}, {\tt{0}})), {\it{temp-stk\/}}))\-)\-, \\ 
{\it{prog-segment\/}}, \\ 
{\it{data-segment\/}}, \\ 
{\it{max-ctrl-stk-size\/}}, \\ 
{\it{max-temp-stk-size\/}}, \\ 
{\it{word-size\/}}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}, \\ 
{\rm{big-add-clock}}\,({\it{n\/}})\index{big-add-clock})\-\index{p} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{add1-addr}}\,({\it{pc\/}})\index{add1-addr}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{push}}\,(\=\+{\rm{big-add-carry-out}}\,(\=\+{\rm{array}}\,({\it{a\/}}, {\it{data-segment\/}})\index{array}, \\ 
{\rm{array}}\,({\it{b\/}}, {\it{data-segment\/}})\index{array}, \\ 
{\bf{f}}, \\ 
{\rm{exp}}\,({\tt{2}}, {\it{word-size\/}})\index{exp})\-\index{big-add-carry-out}, \\ 
{\it{temp-stk\/}})\-\index{push}, \\ 
{\it{prog-segment\/}}, \\ 
{\rm{put-array}}\,(\=\+{\rm{big-add-array}}\,(\=\+{\rm{array}}\,({\it{a\/}}, {\it{data-segment\/}})\index{array}, \\ 
{\rm{array}}\,({\it{b\/}}, {\it{data-segment\/}})\index{array}, \\ 
{\bf{f}}, \\ 
{\rm{exp}}\,({\tt{2}}, {\it{word-size\/}})\index{exp})\-\index{big-add-array}, \\ 
{\it{a\/}}, \\ 
{\it{data-segment\/}})\-\index{put-array}, \\ 
{\it{max-ctrl-stk-size\/}}, \\ 
{\it{max-temp-stk-size\/}}, \\ 
{\it{word-size\/}}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable not-zerop-wordsize-hack.

\addvspace{18pt}

\begin{verbatim};  That says all we need to say about BIG-ADD except for how we connect
; this thm to our FM8502 correctness result.  The question is: what has
; to be true about a state p in order for the hyp of

#|
(IMPLIES (AND (PROPER-P-STATEP P0)
              (P-LOADABLEP P0)
              (EQUAL (P-WORD-SIZE P0) 32)
              (EQUAL PN (P P0 N))
              (NOT (ERRORP (P-PSW PN)))
              (EQUAL TS (TYPE-SPECIFICATION (P-DATA-SEGMENT PN))))
         (EQUAL (P-DATA-SEGMENT PN)
                (DISPLAY-M-DATA-SEGMENT
                  (FM8502 (LOAD P0) (FM8502-CLOCK P0 N))
                  TS
                  (LINK-TABLES P0))))
|#

; to be true?

; Let us first identify a state that is suitable for running BIG-ADD.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{main-program} \\  
\=\+{\sc{main-program}}\index{main-program} \\ 
$=$$\;\;\;\;${\tt{'}}{\tt{(}}\=\+{\tt{main}}{\tt{ }}{\tt{nil}}{\tt{ }}{\tt{nil}} \\ 
{\tt{(}}{\tt{push-constant}}{\tt{ }}{\tt{(}}{\tt{addr}}{\tt{ }}{\tt{(}}{\tt{bna}}{\tt{ .\ }}{\tt{0}}{\tt{)}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}{\tt{push-constant}}{\tt{ }}{\tt{(}}{\tt{addr}}{\tt{ }}{\tt{(}}{\tt{bnb}}{\tt{ .\ }}{\tt{0}}{\tt{)}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}{\tt{push-global}}{\tt{ }}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}{\tt{call}}{\tt{ }}{\tt{big-add}}{\tt{)}} \\ 
{\tt{(}}{\tt{pop-global}}{\tt{ }}{\tt{c}}{\tt{)}} \\ 
{\tt{(}}{\tt{ret}}{\tt{)}}{\tt{)}}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{system-initial-state} \\  
\=\+{\rm{system-initial-state}}\,({\it{a\/}}, {\it{b\/}})\index{system-initial-state} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{pc}}{\tt{ }}{\tt{(}}{\tt{main}}{\tt{ .\ }}{\tt{0}}{\tt{)}}{\tt{)}}, \\ 
{\tt{'}}{\tt{(}}{\tt{(}}{\tt{nil}}{\tt{ }}{\tt{(}}{\tt{pc}}{\tt{ }}{\tt{(}}{\tt{main}}{\tt{ .\ }}{\tt{0}}{\tt{)}}{\tt{)}}{\tt{)}}{\tt{)}}, \\ 
{\bf{nil}}, \\ 
{\rm{list}}\,({\sc{main-program}}\index{main-program}, {\sc{big-add-program}}\index{big-add-program}), \\ 
{\rm{list}}\,(\=\+{\rm{cons}}\,({\tt{'}}{\tt{bna}}, {\it{a\/}}), \\ 
{\rm{cons}}\,({\tt{'}}{\tt{bnb}}, {\it{b\/}}), \\ 
{\rm{cons}}\,({\tt{'}}{\tt{n}}, {\rm{list}}\,({\rm{tag}}\,({\tt{'}}{\tt{nat}}, {\rm{length}}\,({\it{a\/}})\index{length})\index{tag})), \\ 
{\rm{cons}}\,({\tt{'}}{\tt{c}}, {\rm{list}}\,({\rm{tag}}\,({\tt{'}}{\tt{nat}}, {\tt{0}})\index{tag})))\-, \\ 
{\tt{10}}, \\ 
{\tt{8}}, \\ 
{\tt{32}}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}\-
\end{tabbing}

\begin{verbatim}; This state takes the following number of clock ticks:

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{system-initial-state-clock} \\  
{\rm{system-initial-state-clock}}\,({\it{a\/}}, {\it{b\/}})\index{system-initial-state-clock} $=$ ({\tt{5}} $+$ {\rm{big-add-clock}}\,({\rm{length}}\,({\it{a\/}})\index{length})\index{big-add-clock})
\end{tabbing}

\begin{verbatim}; The condition under which big-add-initial-state produces a acceptable state for
; the abstract computation to work is

\end{verbatim}
\noindent{\sc Event}:   Disable exp.

\addvspace{18pt}

\noindent{\sc Event}:   Disable *1*exp.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{system-initial-state-okp} \\  
\=\+{\rm{system-initial-state-okp}}\,({\it{a\/}}, {\it{b\/}})\index{system-initial-state-okp} \\ 
$=$$\;\;\;\;$(\=\+{\rm{bignp}}\,({\it{a\/}}, {\rm{exp}}\,({\tt{2}}, {\tt{32}})\index{exp})\index{bignp} \\ 
$\wedge$$\;\;\;\;${\rm{bignp}}\,({\it{b\/}}, {\rm{exp}}\,({\tt{2}}, {\tt{32}})\index{exp})\index{bignp} \\ 
$\wedge$$\;\;\;\;$({\rm{length}}\,({\it{a\/}})\index{length} $=$ {\rm{length}}\,({\it{b\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;$({\rm{length}}\,({\it{a\/}})\index{length} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\rm{length}}\,({\it{a\/}})\index{length} $<$ {\rm{exp}}\,({\tt{2}}, {\tt{32}})\index{exp}))\-\-
\end{tabbing}  

\begin{verbatim}; We prove that system-initial-state-okp lives up to the above claim:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  restructure-system-initial-state-clock \\ \index{restructure-system-initial-state!-clock}
{\rm{system-initial-state-clock}}\,({\it{a\/}}, {\it{b\/}})\index{system-initial-state-clock} $=$ ({\tt{3}} $+$ {\rm{big-add-clock}}\,({\rm{length}}\,({\it{a\/}})\index{length})\index{big-add-clock} $+$ {\tt{2}})
\end{tabbing}


\noindent{\sc Event}:   Disable system-initial-state-clock.

\addvspace{18pt}


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

\addvspace{18pt}

\noindent{\sc Event}:   Disable commutativity-of-plus.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  p-plus \\ \index{p-plus}
{\rm{p}}\,({\it{p\/}}, {\it{i\/}} $+$ {\it{j\/}})\index{p} $=$ {\rm{p}}\,({\rm{p}}\,({\it{p\/}}, {\it{i\/}})\index{p}, {\it{j\/}})\index{p}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  system-correct \\ \index{system-correct}
\=\+{\rm{system-initial-state-okp}}\,({\it{a\/}}, {\it{b\/}})\index{system-initial-state-okp} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p}}\,({\rm{system-initial-state}}\,({\it{a\/}}, {\it{b\/}})\index{system-initial-state}, {\rm{system-initial-state-clock}}\,({\it{a\/}}, {\it{b\/}})\index{system-initial-state-clock})\index{p} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{pc}}{\tt{ }}{\tt{(}}{\tt{main}}{\tt{ .\ }}{\tt{5}}{\tt{)}}{\tt{)}}, \\ 
{\tt{'}}{\tt{(}}{\tt{(}}{\tt{nil}}{\tt{ }}{\tt{(}}{\tt{pc}}{\tt{ }}{\tt{(}}{\tt{main}}{\tt{ .\ }}{\tt{0}}{\tt{)}}{\tt{)}}{\tt{)}}{\tt{)}}, \\ 
{\bf{nil}}, \\ 
{\rm{list}}\,({\sc{main-program}}\index{main-program}, {\sc{big-add-program}}\index{big-add-program}), \\ 
{\rm{list}}\,(\=\+{\rm{cons}}\,({\tt{'}}{\tt{bna}}, {\rm{big-add-array}}\,({\it{a\/}}, {\it{b\/}}, {\bf{f}}, {\rm{exp}}\,({\tt{2}}, {\tt{32}})\index{exp})\index{big-add-array}), \\ 
{\rm{cons}}\,({\tt{'}}{\tt{bnb}}, {\it{b\/}}), \\ 
{\rm{cons}}\,({\tt{'}}{\tt{n}}, {\rm{list}}\,({\rm{tag}}\,({\tt{'}}{\tt{nat}}, {\rm{length}}\,({\it{a\/}})\index{length})\index{tag})), \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{c}}, \\ 
{\rm{list}}\,({\rm{big-add-carry-out}}\,({\it{a\/}}, {\it{b\/}}, {\bf{f}}, {\rm{exp}}\,({\tt{2}}, {\tt{32}})\index{exp})\index{big-add-carry-out}))\-)\-, \\ 
{\tt{10}}, \\ 
{\tt{8}}, \\ 
{\tt{32}}, \\ 
{\tt{'}}{\tt{halt}})\-\index{p-state})\-\-
\end{tabbing}
			 
\begin{verbatim}; Furthermore, if system-initial-state-okp is true then the initial state is
; proper-p-state and its word size is 32, as required by our FM8502 correctness
; result.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  bignp-implies-all-p-objectps \\ \index{bignp-implies-all-p-objectps}
\=\+({\rm{bignp}}\,({\it{a\/}}, {\it{base\/}})\index{bignp} $\wedge$ ({\it{base\/}} $=$ {\rm{exp}}\,({\tt{2}}, {\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size})\index{exp})) \\ 
$\rightarrow$$\;\;\;\;${\rm{all-p-objectps}}\,({\it{a\/}}, {\it{p\/}})\index{all-p-objectps}\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  initial-correctness-conditions \\ \index{initial-correctness-conditions}
\=\+{\rm{system-initial-state-okp}}\,({\it{a\/}}, {\it{b\/}})\index{system-initial-state-okp} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{proper-p-statep}}\,({\rm{system-initial-state}}\,({\it{a\/}}, {\it{b\/}})\index{system-initial-state})\index{proper-p-statep} \\ 
$\wedge$$\;\;\;\;$({\rm{p-word-size}}\,({\rm{system-initial-state}}\,({\it{a\/}}, {\it{b\/}})\index{system-initial-state})\index{p-word-size} $=$ {\tt{32}}))\-\-
\end{tabbing}

\begin{verbatim}; In addition, the final state is not an error and its type-specification is
; easily computed from the input:

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{nat-lst} \\  
\=\+{\rm{nat-lst}}\,({\it{n\/}})\index{nat-lst} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,({\tt{'}}{\tt{nat}}, {\rm{nat-lst}}\,({\it{n\/}} $-\;1$)\index{nat-lst})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  type-lst-big-add-array \\ \index{type-lst-big-add-array}
{\rm{type-lst}}\,({\rm{big-add-array}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}}, {\it{base\/}})\index{big-add-array})\index{type-lst} $=$ {\rm{nat-lst}}\,({\rm{length}}\,({\it{a\/}})\index{length})\index{nat-lst}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  type-lst-bignp \\ \index{type-lst-bignp}
{\rm{bignp}}\,({\it{a\/}}, {\it{base\/}})\index{bignp} $\rightarrow$ ({\rm{type-lst}}\,({\it{a\/}})\index{type-lst} $=$ {\rm{nat-lst}}\,({\rm{length}}\,({\it{a\/}})\index{length})\index{nat-lst})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  car-big-add-carry-out \\ \index{car-big-add-carry-out}
{\rm{car}}\,({\rm{big-add-carry-out}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}}, {\it{base\/}})\index{big-add-carry-out}) $=$ {\tt{'}}{\tt{bool}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  final-correctness-conditions \\ \index{final-correctness-conditions}
\=\+{\rm{system-initial-state-okp}}\,({\it{a\/}}, {\it{b\/}})\index{system-initial-state-okp} \\ 
$\rightarrow$$\;\;\;\;$(\=\+($\neg$ {\rm{errorp}}\,({\rm{p-psw}}\,({\rm{p}}\,(\=\+{\rm{system-initial-state}}\,({\it{a\/}}, {\it{b\/}})\index{system-initial-state}, \\ 
{\rm{system-initial-state-clock}}\,({\it{a\/}}, {\it{b\/}})\index{system-initial-state-clock})\-\index{p})\index{p-psw})\index{errorp}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{type-specification}}\,({\rm{p-data-segment}}\,({\rm{p}}\,(\=\+{\rm{system-initial-state}}\,({\it{a\/}}, {\it{b\/}})\index{system-initial-state}, \\ 
{\rm{system-initial-state-clock}}\,(\=\+{\it{a\/}}, \\ 
{\it{b\/}})\-\index{system-initial-state-clock})\-\index{p})\index{p-data-segment})\index{type-specification} \\ 
$=$$\;\;\;\;${\rm{list}}\,(\=\+{\rm{cons}}\,({\tt{'}}{\tt{bna}}, {\rm{nat-lst}}\,({\rm{length}}\,({\it{a\/}})\index{length})\index{nat-lst}), \\ 
{\rm{cons}}\,({\tt{'}}{\tt{bnb}}, {\rm{nat-lst}}\,({\rm{length}}\,({\it{a\/}})\index{length})\index{nat-lst}), \\ 
{\rm{cons}}\,({\tt{'}}{\tt{n}}, {\rm{list}}\,({\tt{'}}{\tt{nat}})), \\ 
{\rm{cons}}\,({\tt{'}}{\tt{c}}, {\rm{list}}\,({\tt{'}}{\tt{bool}})))\-)\-)\-\-
\end{tabbing}

\begin{verbatim}; This leaves only the question, is the system-initial-state loadable?  That all depends on
; how much room you take up with the data.  It is certainly loadable for some
; values of a and b and some load addresses.  Below we use the load address 0.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  loadable-for-bigns-up-to-length-1000 \\ \index{loadable-for-bigns-up-to-length!-1000}
\=\+({\rm{system-initial-state-okp}}\,({\it{a\/}}, {\it{b\/}})\index{system-initial-state-okp} $\wedge$ ({\rm{length}}\,({\it{a\/}})\index{length} $<$ {\tt{1000}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{p-loadablep}}\,({\rm{system-initial-state}}\,({\it{a\/}}, {\it{b\/}})\index{system-initial-state}, {\tt{0}})\index{p-loadablep}\-
\end{tabbing}
  


\begin{verbatim}; Oh, there is one more thing we might ask, which is whether there are
; any system-initial-state-okps.  There are.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  example-is-system-initial-state-okp \\ \index{example-is-system-initial-state!-okp}
{\rm{system-initial-state-okp}}\,(\=\+{\tt{'}}{\tt{(}}\=\+{\tt{(}}{\tt{nat}}{\tt{ }}{\tt{246838082}}{\tt{)}} \\ 
{\tt{(}}{\tt{nat}}{\tt{ }}{\tt{3116233281}}{\tt{)}} \\ 
{\tt{(}}{\tt{nat}}{\tt{ }}{\tt{42632655}}{\tt{)}} \\ 
{\tt{(}}{\tt{nat}}{\tt{ }}{\tt{0}}{\tt{)}}{\tt{)}}\-, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{(}}{\tt{nat}}{\tt{ }}{\tt{3579363592}}{\tt{)}} \\ 
{\tt{(}}{\tt{nat}}{\tt{ }}{\tt{3979696680}}{\tt{)}} \\ 
{\tt{(}}{\tt{nat}}{\tt{ }}{\tt{7693250}}{\tt{)}} \\ 
{\tt{(}}{\tt{nat}}{\tt{ }}{\tt{0}}{\tt{)}}{\tt{)}}\-)\-\index{system-initial-state-okp}
\end{tabbing}

		  
\begin{tabbing}{\sc Theorem}:  type-specification-hack \\ \index{type-specification-hack}
{\rm{system-initial-state-okp}}\,({\it{a\/}}, {\it{b\/}})\index{system-initial-state-okp} $\rightarrow$ ({\rm{type-lst}}\,({\it{b\/}})\index{type-lst} $=$ {\rm{nat-lst}}\,({\rm{length}}\,({\it{b\/}})\index{length})\index{nat-lst})
\end{tabbing}

\begin{verbatim}; We need to refer to the link tables for a state without knowing
; the actual data, just the size of the data.  So we define the
; function below which constructs the link tables from a generic
; state of the right size.  This will turn out to be EQUAL to the
; link table for any state of that size.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{big-zero} \\  
\=\+{\rm{big-zero}}\,({\it{n\/}})\index{big-zero} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,({\tt{'}}{\tt{(}}{\tt{nat}}{\tt{ }}{\tt{0}}{\tt{)}}, {\rm{big-zero}}\,({\it{n\/}} $-\;1$)\index{big-zero})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; We link for load address 0.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{system-link-tables} \\  
\=\+{\rm{system-link-tables}}\,({\it{n\/}}, {\it{m\/}})\index{system-link-tables} \\ 
$=$$\;\;\;\;${\rm{link-tables}}\,({\rm{system-initial-state}}\,({\rm{big-zero}}\,({\it{n\/}})\index{big-zero}, {\rm{big-zero}}\,({\it{m\/}})\index{big-zero})\index{system-initial-state}, {\tt{0}})\index{link-tables}\-
\end{tabbing}
  
\begin{tabbing}{\sc Theorem}:  length-big-zero \\ \index{length-big-zero}
{\rm{length}}\,({\rm{big-zero}}\,({\it{n\/}})\index{big-zero})\index{length} $=$ {\rm{fix}}\,({\it{n\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  link-tables-length \\ \index{link-tables-length}
\=\+{\rm{link-tables}}\,({\rm{system-initial-state}}\,({\it{a\/}}, {\it{b\/}})\index{system-initial-state}, {\tt{0}})\index{link-tables} \\ 
$=$$\;\;\;\;${\rm{system-link-tables}}\,({\rm{length}}\,({\it{a\/}})\index{length}, {\rm{length}}\,({\it{b\/}})\index{length})\index{system-link-tables}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  system-initial-state-okp-length-hack \\ \index{system-initial-state-okp-length!-hack}
{\rm{system-initial-state-okp}}\,({\it{a\/}}, {\it{b\/}})\index{system-initial-state-okp} $\rightarrow$ ({\rm{length}}\,({\it{b\/}})\index{length} $=$ {\rm{length}}\,({\it{a\/}})\index{length})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{display-answers} \\  
\=\+{\rm{display-answers}}\,({\it{m-state\/}}, {\it{n\/}})\index{display-answers} \\ 
$=$$\;\;\;\;$\=\+{\bf let }\=\+{\it{alist\/}}{\bf $\;$ be$\;\;$}{\rm{display-fm9001-data-segment}}\,(\=\+{\it{m-state\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{bna}}, \\ 
{\rm{nat-lst}}\,({\it{n\/}})\index{nat-lst})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{bnb}}, \\ 
{\rm{nat-lst}}\,({\it{n\/}})\index{nat-lst})\-, \\ 
{\rm{cons}}\,({\tt{'}}{\tt{n}}, {\rm{list}}\,({\tt{'}}{\tt{nat}})), \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{c}}, \\ 
{\rm{list}}\,({\tt{'}}{\tt{bool}}))\-)\-, \\ 
{\rm{system-link-tables}}\,({\it{n\/}}, {\it{n\/}})\index{system-link-tables})\-\index{display-fm9001-data-segment}\- \\ 
{\bf in} \\ 
{\rm{list}}\,({\rm{cdr}}\,({\rm{assoc}}\,({\tt{'}}{\tt{bna}}, {\it{alist\/}})), {\rm{cadr}}\,({\rm{assoc}}\,({\tt{'}}{\tt{c}}, {\it{alist\/}})))$\;${\bf  endlet}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  type-big-add-carry-out \\ \index{type-big-add-carry-out}
{\rm{type}}\,({\rm{big-add-carry-out}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}}, {\it{base\/}})\index{big-add-carry-out})\index{type} $=$ {\tt{'}}{\tt{bool}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  eliminate-piton \\ \index{eliminate-piton}
\=\+({\rm{system-initial-state-okp}}\,({\it{a\/}}, {\it{b\/}})\index{system-initial-state-okp} $\wedge$ ({\rm{length}}\,({\it{a\/}})\index{length} $<$ {\tt{1000}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{display-answers}}\,(\=\+{\rm{fm9001}}\,(\=\+{\rm{load}}\,({\rm{system-initial-state}}\,({\it{a\/}}, {\it{b\/}})\index{system-initial-state}, {\bf{nil}}, {\tt{0}})\index{load}, \\ 
{\rm{fm9001-clock}}\,(\=\+{\rm{system-initial-state}}\,({\it{a\/}}, {\it{b\/}})\index{system-initial-state}, \\ 
{\rm{system-initial-state-clock}}\,({\it{a\/}}, {\it{b\/}})\index{system-initial-state-clock})\-\index{fm9001-clock})\-\index{fm9001}, \\ 
{\rm{length}}\,({\it{a\/}})\index{length})\-\index{display-answers} \\ 
$=$$\;\;\;\;${\rm{list}}\,(\=\+{\rm{big-add-array}}\,({\it{a\/}}, {\it{b\/}}, {\bf{f}}, {\rm{exp}}\,({\tt{2}}, {\tt{32}})\index{exp})\index{big-add-array}, \\ 
{\rm{big-add-carry-out}}\,({\it{a\/}}, {\it{b\/}}, {\bf{f}}, {\rm{exp}}\,({\tt{2}}, {\tt{32}})\index{exp})\index{big-add-carry-out})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  clock-for-concrete-data \\ \index{clock-for-concrete-data}
\=\+\=\+{\bf let }\=\+{\it{a\/}}{\bf $\;$ be$\;\;$}{\tt{'}}{\tt{(}}\=\+{\tt{(}}{\tt{nat}}{\tt{ }}{\tt{246838082}}{\tt{)}} \\ 
{\tt{(}}{\tt{nat}}{\tt{ }}{\tt{3116233281}}{\tt{)}} \\ 
{\tt{(}}{\tt{nat}}{\tt{ }}{\tt{42632655}}{\tt{)}} \\ 
{\tt{(}}{\tt{nat}}{\tt{ }}{\tt{0}}{\tt{)}}{\tt{)}}\-, \\ 
{\it{b\/}}{\bf $\;$ be$\;\;$}{\tt{'}}{\tt{(}}\=\+{\tt{(}}{\tt{nat}}{\tt{ }}{\tt{3579363592}}{\tt{)}} \\ 
{\tt{(}}{\tt{nat}}{\tt{ }}{\tt{3979696680}}{\tt{)}} \\ 
{\tt{(}}{\tt{nat}}{\tt{ }}{\tt{7693250}}{\tt{)}} \\ 
{\tt{(}}{\tt{nat}}{\tt{ }}{\tt{0}}{\tt{)}}{\tt{)}}\-\- \\ 
{\bf in} \\ 
{\rm{fm9001-clock}}\,(\=\+{\rm{system-initial-state}}\,({\it{a\/}}, {\it{b\/}})\index{system-initial-state}, \\ 
{\rm{system-initial-state-clock}}\,({\it{a\/}}, {\it{b\/}})\index{system-initial-state-clock})\-\index{fm9001-clock}$\;${\bf  endlet}\- \\ 
$=$$\;\;\;\;${\tt{190}}\-
\end{tabbing}
                      


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