\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 Alex Bronstein and Carolyn Talcott.  All Rights
 Reserved.

 You may copy and distribute verbatim copies of this Nqthm-1992 event script as
 you receive it, in any medium, including embedding it verbatim in derivative
 works, provided that you conspicuously and appropriately publish on each copy
 a valid copyright notice "Copyright (C) 1994 by Alex Bronstein and Carolyn
 Talcott.  All Rights Reserved."

 NO WARRANTY

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

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

|#

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

\addvspace{18pt}
\begin{verbatim}; multadd.bm: an iterative multiplier, built from an adder;
;    This is Paillet #7.
;    Note: this is the first multi-input circuit which forced the 
;    EQ-LEN hyps. Also, we prove the same Deroulement as Paillet, 
;    an induction over the macrocycle would be illegible to specify
;    and let alone prove.
;

;;; CIRCUIT in SUGARED form:
#|
(setq sysd '(sy-MULTADD (Xx Xy)
(Y1 S mux Ydone Xx Y3)
(YN R 0 Y1)         ; initially called l2 in Paillet, but then renamed to N
(Y3 S dec YN)
(Y4 S dec Y3)
(Y5 S dec Xx)
(Y6 S mux Ydone Y5 Y4)
(Y7 S eq0 Y6)
(Yt S or Y7 Y8)
(Ydone R T Yt)
(Y8 S eq0 Xy)
(Y9 S eq0 Xx)
(Y0 S const 0 Xx)
(Y10 S mux Y9 Y0 Xy)
(Y11 S mux Ydone Y10 Y12)
(Yout R 0 Y11)
(Y12 S plus Y10 Yout)
))

(setq multadd '(  |#
; BM DEFINITIONS and A2 LEMMAS, generated by BMSYSD:
; comb_dec.bm: DECrement combinational element (with dec 0 = 0 )
; U7-DONE

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{dec}$\;\;$
{\rm{dec}}\,({\it{u\/}})\index{dec} $=$ ({\it{u\/}} $-\;1$)
\end{tabbing}

\begin{verbatim}; Everything below generated by: (bmcomb 'dec '() '(x))

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{s-dec} \\  
\=\+{\rm{s-dec}}\,({\it{x\/}})\index{s-dec} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{a}}\,({\rm{s-dec}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{s-dec}, {\rm{dec}}\,({\rm{l}}\,({\it{x\/}})\index{l})\index{dec})\index{a}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};; A2-Begin-S-DEC

\end{verbatim}\begin{tabbing}{\sc Theorem}:  a2-empty-s-dec \\ \index{a2-empty-s-dec}
{\rm{empty}}\,({\rm{s-dec}}\,({\it{x\/}})\index{s-dec})\index{empty} $=$ {\rm{empty}}\,({\it{x\/}})\index{empty}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-e-s-dec \\ \index{a2-e-s-dec}
({\rm{s-dec}}\,({\it{x\/}})\index{s-dec} $=$ {\sc{e}}\index{e}) $=$ {\rm{empty}}\,({\it{x\/}})\index{empty}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-lp-s-dec \\ \index{a2-lp-s-dec}
{\rm{len}}\,({\rm{s-dec}}\,({\it{x\/}})\index{s-dec})\index{len} $=$ {\rm{len}}\,({\it{x\/}})\index{len}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-lpe-s-dec \\ \index{a2-lpe-s-dec}
{\rm{eqlen}}\,({\rm{s-dec}}\,({\it{x\/}})\index{s-dec}, {\it{x\/}})\index{eqlen}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-ic-s-dec \\ \index{a2-ic-s-dec}
{\rm{s-dec}}\,({\rm{i}}\,({\it{c\_x\/}}, {\it{x\/}})\index{i})\index{s-dec} $=$ {\rm{i}}\,({\rm{dec}}\,({\it{c\_x\/}})\index{dec}, {\rm{s-dec}}\,({\it{x\/}})\index{s-dec})\index{i}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-lc-s-dec \\ \index{a2-lc-s-dec}
($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) $\rightarrow$ ({\rm{l}}\,({\rm{s-dec}}\,({\it{x\/}})\index{s-dec})\index{l} $=$ {\rm{dec}}\,({\rm{l}}\,({\it{x\/}})\index{l})\index{dec})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-pc-s-dec \\ \index{a2-pc-s-dec}
{\rm{p}}\,({\rm{s-dec}}\,({\it{x\/}})\index{s-dec})\index{p} $=$ {\rm{s-dec}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{s-dec}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-hc-s-dec \\ \index{a2-hc-s-dec}
($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) $\rightarrow$ ({\rm{h}}\,({\rm{s-dec}}\,({\it{x\/}})\index{s-dec})\index{h} $=$ {\rm{dec}}\,({\rm{h}}\,({\it{x\/}})\index{h})\index{dec})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-bc-s-dec \\ \index{a2-bc-s-dec}
{\rm{b}}\,({\rm{s-dec}}\,({\it{x\/}})\index{s-dec})\index{b} $=$ {\rm{s-dec}}\,({\rm{b}}\,({\it{x\/}})\index{b})\index{s-dec}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-bnc-s-dec \\ \index{a2-bnc-s-dec}
{\rm{bn}}\,({\it{n\/}}, {\rm{s-dec}}\,({\it{x\/}})\index{s-dec})\index{bn} $=$ {\rm{s-dec}}\,({\rm{bn}}\,({\it{n\/}}, {\it{x\/}})\index{bn})\index{s-dec}
\end{tabbing}

\begin{verbatim};; A2-End-S-DEC

; eof:comb_dec.bm

; comb_eq0.bm: (slightly abstract) equal to 0 test, could be done with: XOR 1 u
; U7-DONE

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{eq0}$\;\;$
{\rm{eq0}}\,({\it{u\/}})\index{eq0} $=$ ({\it{u\/}} $\simeq {\tt{0}}$)
\end{tabbing}

\begin{verbatim}; Everything below generated by: (bmcomb 'eq0 '() '(x))

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{s-eq0} \\  
\=\+{\rm{s-eq0}}\,({\it{x\/}})\index{s-eq0} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{a}}\,({\rm{s-eq0}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{s-eq0}, {\rm{eq0}}\,({\rm{l}}\,({\it{x\/}})\index{l})\index{eq0})\index{a}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};; A2-Begin-S-EQ0

\end{verbatim}\begin{tabbing}{\sc Theorem}:  a2-empty-s-eq0 \\ \index{a2-empty-s-eq0}
{\rm{empty}}\,({\rm{s-eq0}}\,({\it{x\/}})\index{s-eq0})\index{empty} $=$ {\rm{empty}}\,({\it{x\/}})\index{empty}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-e-s-eq0 \\ \index{a2-e-s-eq0}
({\rm{s-eq0}}\,({\it{x\/}})\index{s-eq0} $=$ {\sc{e}}\index{e}) $=$ {\rm{empty}}\,({\it{x\/}})\index{empty}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-lp-s-eq0 \\ \index{a2-lp-s-eq0}
{\rm{len}}\,({\rm{s-eq0}}\,({\it{x\/}})\index{s-eq0})\index{len} $=$ {\rm{len}}\,({\it{x\/}})\index{len}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-lpe-s-eq0 \\ \index{a2-lpe-s-eq0}
{\rm{eqlen}}\,({\rm{s-eq0}}\,({\it{x\/}})\index{s-eq0}, {\it{x\/}})\index{eqlen}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-ic-s-eq0 \\ \index{a2-ic-s-eq0}
{\rm{s-eq0}}\,({\rm{i}}\,({\it{c\_x\/}}, {\it{x\/}})\index{i})\index{s-eq0} $=$ {\rm{i}}\,({\rm{eq0}}\,({\it{c\_x\/}})\index{eq0}, {\rm{s-eq0}}\,({\it{x\/}})\index{s-eq0})\index{i}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-lc-s-eq0 \\ \index{a2-lc-s-eq0}
($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) $\rightarrow$ ({\rm{l}}\,({\rm{s-eq0}}\,({\it{x\/}})\index{s-eq0})\index{l} $=$ {\rm{eq0}}\,({\rm{l}}\,({\it{x\/}})\index{l})\index{eq0})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-pc-s-eq0 \\ \index{a2-pc-s-eq0}
{\rm{p}}\,({\rm{s-eq0}}\,({\it{x\/}})\index{s-eq0})\index{p} $=$ {\rm{s-eq0}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{s-eq0}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-hc-s-eq0 \\ \index{a2-hc-s-eq0}
($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) $\rightarrow$ ({\rm{h}}\,({\rm{s-eq0}}\,({\it{x\/}})\index{s-eq0})\index{h} $=$ {\rm{eq0}}\,({\rm{h}}\,({\it{x\/}})\index{h})\index{eq0})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-bc-s-eq0 \\ \index{a2-bc-s-eq0}
{\rm{b}}\,({\rm{s-eq0}}\,({\it{x\/}})\index{s-eq0})\index{b} $=$ {\rm{s-eq0}}\,({\rm{b}}\,({\it{x\/}})\index{b})\index{s-eq0}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-bnc-s-eq0 \\ \index{a2-bnc-s-eq0}
{\rm{bn}}\,({\it{n\/}}, {\rm{s-eq0}}\,({\it{x\/}})\index{s-eq0})\index{bn} $=$ {\rm{s-eq0}}\,({\rm{bn}}\,({\it{n\/}}, {\it{x\/}})\index{bn})\index{s-eq0}
\end{tabbing}

\begin{verbatim};; A2-End-S-EQ0

; eof:comb_eq0.bm

; comb_mux.bm: Mux combinational element, i.e. "if".
; U7-DONE

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{mux} \\  
\=\+{\rm{mux}}\,({\it{u1\/}}, {\it{u2\/}}, {\it{u3\/}})\index{mux} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{u1\/}}$\;\;${\bf then }{\it{u2\/}} \\ 
{\bf else }{\it{u3\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; everything below generated by: (bmcomb 'mux '() '(x1 x2 x3))
; with the EXCEPTIONS/HAND-MODIFICATIONS given below.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{s-mux} \\  
\=\+{\rm{s-mux}}\,({\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{s-mux} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{empty}}\,({\it{x1\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{a}}\,({\rm{s-mux}}\,({\rm{p}}\,({\it{x1\/}})\index{p}, {\rm{p}}\,({\it{x2\/}})\index{p}, {\rm{p}}\,({\it{x3\/}})\index{p})\index{s-mux}, {\rm{mux}}\,({\rm{l}}\,({\it{x1\/}})\index{l}, {\rm{l}}\,({\it{x2\/}})\index{l}, {\rm{l}}\,({\it{x3\/}})\index{l})\index{mux})\index{a}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; SMUX-is-SIF can make things much simpler on occasions:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  smux-is-sif \\ \index{smux-is-sif}
{\rm{s-mux}}\,({\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{s-mux} $=$ {\rm{s-if}}\,({\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{s-if}
\end{tabbing}


\noindent{\sc Event}:   Disable smux-is-sif.

\addvspace{18pt}

\begin{verbatim}; We take advantage of SMUX-is-SIF for all inductive proofs. To do so we
; HAND-MODIFY the code generated by Sugar to replace all the hints by
;   - A2-EMPTY, A2-PC replace hint with: ((enable smux-is-sif)) 
;   - A2-LP, A2-IC, A2-HC, A2-BC: ((enable smux-is-sif) (disable len))
;   - A2-BNC: ((enable smux-is-sif) (disable bn len))

;; A2-Begin-S-MUX

\end{verbatim}\begin{tabbing}{\sc Theorem}:  a2-empty-s-mux \\ \index{a2-empty-s-mux}
{\rm{empty}}\,({\rm{s-mux}}\,({\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{s-mux})\index{empty} $=$ {\rm{empty}}\,({\it{x1\/}})\index{empty}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-e-s-mux \\ \index{a2-e-s-mux}
({\rm{s-mux}}\,({\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{s-mux} $=$ {\sc{e}}\index{e}) $=$ {\rm{empty}}\,({\it{x1\/}})\index{empty}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-lp-s-mux \\ \index{a2-lp-s-mux}
{\rm{len}}\,({\rm{s-mux}}\,({\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{s-mux})\index{len} $=$ {\rm{len}}\,({\it{x1\/}})\index{len}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-lpe-s-mux \\ \index{a2-lpe-s-mux}
{\rm{eqlen}}\,({\rm{s-mux}}\,({\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{s-mux}, {\it{x1\/}})\index{eqlen}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-ic-s-mux \\ \index{a2-ic-s-mux}
\=\+(({\rm{len}}\,({\it{x1\/}})\index{len} $=$ {\rm{len}}\,({\it{x2\/}})\index{len}) $\wedge$ ({\rm{len}}\,({\it{x2\/}})\index{len} $=$ {\rm{len}}\,({\it{x3\/}})\index{len})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{s-mux}}\,({\rm{i}}\,({\it{c\_x1\/}}, {\it{x1\/}})\index{i}, {\rm{i}}\,({\it{c\_x2\/}}, {\it{x2\/}})\index{i}, {\rm{i}}\,({\it{c\_x3\/}}, {\it{x3\/}})\index{i})\index{s-mux} \\ 
$=$$\;\;\;\;${\rm{i}}\,({\rm{mux}}\,({\it{c\_x1\/}}, {\it{c\_x2\/}}, {\it{c\_x3\/}})\index{mux}, {\rm{s-mux}}\,({\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{s-mux})\index{i})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-lc-s-mux \\ \index{a2-lc-s-mux}
($\neg$ {\rm{empty}}\,({\it{x1\/}})\index{empty}) $\rightarrow$ ({\rm{l}}\,({\rm{s-mux}}\,({\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{s-mux})\index{l} $=$ {\rm{mux}}\,({\rm{l}}\,({\it{x1\/}})\index{l}, {\rm{l}}\,({\it{x2\/}})\index{l}, {\rm{l}}\,({\it{x3\/}})\index{l})\index{mux})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-pc-s-mux \\ \index{a2-pc-s-mux}
{\rm{p}}\,({\rm{s-mux}}\,({\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{s-mux})\index{p} $=$ {\rm{s-mux}}\,({\rm{p}}\,({\it{x1\/}})\index{p}, {\rm{p}}\,({\it{x2\/}})\index{p}, {\rm{p}}\,({\it{x3\/}})\index{p})\index{s-mux}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-hc-s-mux \\ \index{a2-hc-s-mux}
\=\+(($\neg$ {\rm{empty}}\,({\it{x1\/}})\index{empty}) $\wedge$ (({\rm{len}}\,({\it{x1\/}})\index{len} $=$ {\rm{len}}\,({\it{x2\/}})\index{len}) $\wedge$ ({\rm{len}}\,({\it{x2\/}})\index{len} $=$ {\rm{len}}\,({\it{x3\/}})\index{len}))) \\ 
$\rightarrow$$\;\;\;\;$({\rm{h}}\,({\rm{s-mux}}\,({\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{s-mux})\index{h} $=$ {\rm{mux}}\,({\rm{h}}\,({\it{x1\/}})\index{h}, {\rm{h}}\,({\it{x2\/}})\index{h}, {\rm{h}}\,({\it{x3\/}})\index{h})\index{mux})\-
\end{tabbing}

\begin{verbatim};old:    ((DISABLE MUX S-MUX) (ENABLE H LEN) (INDUCT (S-MUX X1 X2 X3)))

\end{verbatim}\begin{tabbing}{\sc Theorem}:  a2-bc-s-mux \\ \index{a2-bc-s-mux}
\=\+(({\rm{len}}\,({\it{x1\/}})\index{len} $=$ {\rm{len}}\,({\it{x2\/}})\index{len}) $\wedge$ ({\rm{len}}\,({\it{x2\/}})\index{len} $=$ {\rm{len}}\,({\it{x3\/}})\index{len})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{b}}\,({\rm{s-mux}}\,({\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{s-mux})\index{b} $=$ {\rm{s-mux}}\,({\rm{b}}\,({\it{x1\/}})\index{b}, {\rm{b}}\,({\it{x2\/}})\index{b}, {\rm{b}}\,({\it{x3\/}})\index{b})\index{s-mux})\-
\end{tabbing}

\begin{verbatim};old:    ((DISABLE MUX) (ENABLE B LEN) (INDUCT (S-MUX X1 X2 X3)))

\end{verbatim}\begin{tabbing}{\sc Theorem}:  a2-bnc-s-mux \\ \index{a2-bnc-s-mux}
\=\+(({\rm{len}}\,({\it{x1\/}})\index{len} $=$ {\rm{len}}\,({\it{x2\/}})\index{len}) $\wedge$ ({\rm{len}}\,({\it{x2\/}})\index{len} $=$ {\rm{len}}\,({\it{x3\/}})\index{len})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{bn}}\,({\it{n\/}}, {\rm{s-mux}}\,({\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{s-mux})\index{bn} $=$ {\rm{s-mux}}\,({\rm{bn}}\,({\it{n\/}}, {\it{x1\/}})\index{bn}, {\rm{bn}}\,({\it{n\/}}, {\it{x2\/}})\index{bn}, {\rm{bn}}\,({\it{n\/}}, {\it{x3\/}})\index{bn})\index{s-mux})\-
\end{tabbing}

\begin{verbatim};old: ((DISABLE MUX S-MUX))

;; A2-End-S-MUX

; eof:comb_mux.bm

; comb_plus.bm: Plus combinational element.
; U7-DONE

;   no character function definition since BM already knows about Plus..

; Everything below generated by:     (bmcomb 'plus '() '(x y))

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{s-plus} \\  
\=\+{\rm{s-plus}}\,({\it{x\/}}, {\it{y\/}})\index{s-plus} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{a}}\,({\rm{s-plus}}\,({\rm{p}}\,({\it{x\/}})\index{p}, {\rm{p}}\,({\it{y\/}})\index{p})\index{s-plus}, {\rm{l}}\,({\it{x\/}})\index{l} $+$ {\rm{l}}\,({\it{y\/}})\index{l})\index{a}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};; A2-Begin-S-PLUS

\end{verbatim}\begin{tabbing}{\sc Theorem}:  a2-empty-s-plus \\ \index{a2-empty-s-plus}
{\rm{empty}}\,({\rm{s-plus}}\,({\it{x\/}}, {\it{y\/}})\index{s-plus})\index{empty} $=$ {\rm{empty}}\,({\it{x\/}})\index{empty}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-e-s-plus \\ \index{a2-e-s-plus}
({\rm{s-plus}}\,({\it{x\/}}, {\it{y\/}})\index{s-plus} $=$ {\sc{e}}\index{e}) $=$ {\rm{empty}}\,({\it{x\/}})\index{empty}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-lp-s-plus \\ \index{a2-lp-s-plus}
{\rm{len}}\,({\rm{s-plus}}\,({\it{x\/}}, {\it{y\/}})\index{s-plus})\index{len} $=$ {\rm{len}}\,({\it{x\/}})\index{len}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-lpe-s-plus \\ \index{a2-lpe-s-plus}
{\rm{eqlen}}\,({\rm{s-plus}}\,({\it{x\/}}, {\it{y\/}})\index{s-plus}, {\it{x\/}})\index{eqlen}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-ic-s-plus \\ \index{a2-ic-s-plus}
\=\+({\rm{len}}\,({\it{x\/}})\index{len} $=$ {\rm{len}}\,({\it{y\/}})\index{len}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{s-plus}}\,({\rm{i}}\,({\it{c\_x\/}}, {\it{x\/}})\index{i}, {\rm{i}}\,({\it{c\_y\/}}, {\it{y\/}})\index{i})\index{s-plus} $=$ {\rm{i}}\,({\it{c\_x\/}} $+$ {\it{c\_y\/}}, {\rm{s-plus}}\,({\it{x\/}}, {\it{y\/}})\index{s-plus})\index{i})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-lc-s-plus \\ \index{a2-lc-s-plus}
($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) $\rightarrow$ ({\rm{l}}\,({\rm{s-plus}}\,({\it{x\/}}, {\it{y\/}})\index{s-plus})\index{l} $=$ ({\rm{l}}\,({\it{x\/}})\index{l} $+$ {\rm{l}}\,({\it{y\/}})\index{l}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-pc-s-plus \\ \index{a2-pc-s-plus}
{\rm{p}}\,({\rm{s-plus}}\,({\it{x\/}}, {\it{y\/}})\index{s-plus})\index{p} $=$ {\rm{s-plus}}\,({\rm{p}}\,({\it{x\/}})\index{p}, {\rm{p}}\,({\it{y\/}})\index{p})\index{s-plus}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-hc-s-plus \\ \index{a2-hc-s-plus}
\=\+(($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) $\wedge$ ({\rm{len}}\,({\it{x\/}})\index{len} $=$ {\rm{len}}\,({\it{y\/}})\index{len})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{h}}\,({\rm{s-plus}}\,({\it{x\/}}, {\it{y\/}})\index{s-plus})\index{h} $=$ ({\rm{h}}\,({\it{x\/}})\index{h} $+$ {\rm{h}}\,({\it{y\/}})\index{h}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-bc-s-plus \\ \index{a2-bc-s-plus}
({\rm{len}}\,({\it{x\/}})\index{len} $=$ {\rm{len}}\,({\it{y\/}})\index{len}) $\rightarrow$ ({\rm{b}}\,({\rm{s-plus}}\,({\it{x\/}}, {\it{y\/}})\index{s-plus})\index{b} $=$ {\rm{s-plus}}\,({\rm{b}}\,({\it{x\/}})\index{b}, {\rm{b}}\,({\it{y\/}})\index{b})\index{s-plus})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-bnc-s-plus \\ \index{a2-bnc-s-plus}
({\rm{len}}\,({\it{x\/}})\index{len} $=$ {\rm{len}}\,({\it{y\/}})\index{len}) $\rightarrow$ ({\rm{bn}}\,({\it{n\/}}, {\rm{s-plus}}\,({\it{x\/}}, {\it{y\/}})\index{s-plus})\index{bn} $=$ {\rm{s-plus}}\,({\rm{bn}}\,({\it{n\/}}, {\it{x\/}})\index{bn}, {\rm{bn}}\,({\it{n\/}}, {\it{y\/}})\index{bn})\index{s-plus})
\end{tabbing}

\begin{verbatim};; A2-End-S-PLUS

; eof:comb_plus.bm


\end{verbatim}\begin{tabbing}{\sc Definition}:\index{topor-sy-multadd} \\  
\=\+{\rm{topor-sy-multadd}}\,({\it{ln\/}})\index{topor-sy-multadd} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{ln\/}} $=$ {\tt{'}}{\tt{y1}}$\;\;${\bf then }{\tt{2}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yn}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y3}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y4}}$\;\;${\bf then }{\tt{2}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y5}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y6}}$\;\;${\bf then }{\tt{3}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y7}}$\;\;${\bf then }{\tt{4}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yt}}$\;\;${\bf then }{\tt{5}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ydone}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y8}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y9}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y0}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y10}}$\;\;${\bf then }{\tt{2}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y11}}$\;\;${\bf then }{\tt{4}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yout}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y12}}$\;\;${\bf then }{\tt{3}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};Parameter found: 0 in: (Y0 S CONST 0 XX)
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{sy-multadd} \\  
\=\+{\rm{sy-multadd}}\,({\it{ln\/}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-multadd} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{ln\/}} $=$ {\tt{'}}{\tt{y1}} \\ 
{\bf then }{\rm{s-mux}}\,({\rm{sy-multadd}}\,({\tt{'}}{\tt{ydone}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-multadd}, {\it{xx\/}}, {\rm{sy-multadd}}\,({\tt{'}}{\tt{y3}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-multadd})\index{s-mux} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yn}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xx\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{0}}, {\rm{sy-multadd}}\,({\tt{'}}{\tt{y1}}, {\rm{p}}\,({\it{xx\/}})\index{p}, {\rm{p}}\,({\it{xy\/}})\index{p})\index{sy-multadd})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y3}}$\;\;${\bf then }{\rm{s-dec}}\,({\rm{sy-multadd}}\,({\tt{'}}{\tt{yn}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-multadd})\index{s-dec} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y4}}$\;\;${\bf then }{\rm{s-dec}}\,({\rm{sy-multadd}}\,({\tt{'}}{\tt{y3}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-multadd})\index{s-dec} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y5}}$\;\;${\bf then }{\rm{s-dec}}\,({\it{xx\/}})\index{s-dec} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y6}} \\ 
{\bf then }{\rm{s-mux}}\,(\=\+{\rm{sy-multadd}}\,({\tt{'}}{\tt{ydone}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-multadd}, \\ 
{\rm{sy-multadd}}\,({\tt{'}}{\tt{y5}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-multadd}, \\ 
{\rm{sy-multadd}}\,({\tt{'}}{\tt{y4}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-multadd})\-\index{s-mux} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y7}}$\;\;${\bf then }{\rm{s-eq0}}\,({\rm{sy-multadd}}\,({\tt{'}}{\tt{y6}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-multadd})\index{s-eq0} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yt}} \\ 
{\bf then }{\rm{s-or}}\,({\rm{sy-multadd}}\,({\tt{'}}{\tt{y7}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-multadd}, {\rm{sy-multadd}}\,({\tt{'}}{\tt{y8}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-multadd})\index{s-or} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ydone}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xx\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\bf{t}}, {\rm{sy-multadd}}\,({\tt{'}}{\tt{yt}}, {\rm{p}}\,({\it{xx\/}})\index{p}, {\rm{p}}\,({\it{xy\/}})\index{p})\index{sy-multadd})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y8}}$\;\;${\bf then }{\rm{s-eq0}}\,({\it{xy\/}})\index{s-eq0} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y9}}$\;\;${\bf then }{\rm{s-eq0}}\,({\it{xx\/}})\index{s-eq0} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y0}}$\;\;${\bf then }{\rm{s-const}}\,({\tt{0}}, {\it{xx\/}})\index{s-const} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y10}} \\ 
{\bf then }{\rm{s-mux}}\,({\rm{sy-multadd}}\,({\tt{'}}{\tt{y9}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-multadd}, {\rm{sy-multadd}}\,({\tt{'}}{\tt{y0}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-multadd}, {\it{xy\/}})\index{s-mux} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y11}} \\ 
{\bf then }{\rm{s-mux}}\,(\=\+{\rm{sy-multadd}}\,({\tt{'}}{\tt{ydone}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-multadd}, \\ 
{\rm{sy-multadd}}\,({\tt{'}}{\tt{y10}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-multadd}, \\ 
{\rm{sy-multadd}}\,({\tt{'}}{\tt{y12}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-multadd})\-\index{s-mux} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yout}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xx\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{0}}, {\rm{sy-multadd}}\,({\tt{'}}{\tt{y11}}, {\rm{p}}\,({\it{xx\/}})\index{p}, {\rm{p}}\,({\it{xy\/}})\index{p})\index{sy-multadd})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y12}} \\ 
{\bf then }{\rm{s-plus}}\,({\rm{sy-multadd}}\,({\tt{'}}{\tt{y10}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-multadd}, {\rm{sy-multadd}}\,({\tt{'}}{\tt{yout}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-multadd})\index{s-plus} \\ 
{\bf else }{\rm{sfix}}\,({\it{xx\/}})\index{sfix}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};; A2-Begin-SY-MULTADD

\end{verbatim}\begin{tabbing}{\sc Theorem}:  a2-empty-sy-multadd \\ \index{a2-empty-sy-multadd}
({\rm{len}}\,({\it{xx\/}})\index{len} $=$ {\rm{len}}\,({\it{xy\/}})\index{len}) $\rightarrow$ ({\rm{empty}}\,({\rm{sy-multadd}}\,({\it{ln\/}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-multadd})\index{empty} $=$ {\rm{empty}}\,({\it{xx\/}})\index{empty})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-e-sy-multadd \\ \index{a2-e-sy-multadd}
({\rm{len}}\,({\it{xx\/}})\index{len} $=$ {\rm{len}}\,({\it{xy\/}})\index{len}) $\rightarrow$ (({\rm{sy-multadd}}\,({\it{ln\/}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-multadd} $=$ {\sc{e}}\index{e}) $=$ {\rm{empty}}\,({\it{xx\/}})\index{empty})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-lp-sy-multadd \\ \index{a2-lp-sy-multadd}
({\rm{len}}\,({\it{xx\/}})\index{len} $=$ {\rm{len}}\,({\it{xy\/}})\index{len}) $\rightarrow$ ({\rm{len}}\,({\rm{sy-multadd}}\,({\it{ln\/}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-multadd})\index{len} $=$ {\rm{len}}\,({\it{xx\/}})\index{len})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-lpe-sy-multadd \\ \index{a2-lpe-sy-multadd}
({\rm{len}}\,({\it{xx\/}})\index{len} $=$ {\rm{len}}\,({\it{xy\/}})\index{len}) $\rightarrow$ {\rm{eqlen}}\,({\rm{sy-multadd}}\,({\it{ln\/}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-multadd}, {\it{xx\/}})\index{eqlen}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-pc-sy-multadd \\ \index{a2-pc-sy-multadd}
\=\+({\rm{len}}\,({\it{xx\/}})\index{len} $=$ {\rm{len}}\,({\it{xy\/}})\index{len}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{p}}\,({\rm{sy-multadd}}\,({\it{ln\/}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-multadd})\index{p} $=$ {\rm{sy-multadd}}\,({\it{ln\/}}, {\rm{p}}\,({\it{xx\/}})\index{p}, {\rm{p}}\,({\it{xy\/}})\index{p})\index{sy-multadd})\-
\end{tabbing}

\begin{verbatim};; A2-End-SY-MULTADD

;;; Circuit CORRECTNESS /Paillet:

; first we get the simplified (generalized) sysd:

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{sy-m2} \\  
\=\+{\rm{sy-m2}}\,({\it{ln\/}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-m2} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{ln\/}} $=$ {\tt{'}}{\tt{yn}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xx\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,(\=\+{\tt{0}}, \\ 
{\rm{s-mux}}\,(\=\+{\rm{sy-m2}}\,({\tt{'}}{\tt{ydone}}, {\rm{p}}\,({\it{xx\/}})\index{p}, {\rm{p}}\,({\it{xy\/}})\index{p})\index{sy-m2}, \\ 
{\rm{p}}\,({\it{xx\/}})\index{p}, \\ 
{\rm{s-dec}}\,({\rm{sy-m2}}\,({\tt{'}}{\tt{yn}}, {\rm{p}}\,({\it{xx\/}})\index{p}, {\rm{p}}\,({\it{xy\/}})\index{p})\index{sy-m2})\index{s-dec})\-\index{s-mux})\-\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ydone}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xx\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,(\=\+{\bf{t}}, \\ 
{\rm{s-or}}\,(\=\+{\rm{s-eq0}}\,({\rm{s-mux}}\,(\=\+{\rm{sy-m2}}\,({\tt{'}}{\tt{ydone}}, {\rm{p}}\,({\it{xx\/}})\index{p}, {\rm{p}}\,({\it{xy\/}})\index{p})\index{sy-m2}, \\ 
{\rm{s-dec}}\,({\rm{p}}\,({\it{xx\/}})\index{p})\index{s-dec}, \\ 
{\rm{s-dec}}\,({\rm{s-dec}}\,({\rm{sy-m2}}\,({\tt{'}}{\tt{yn}}, {\rm{p}}\,({\it{xx\/}})\index{p}, {\rm{p}}\,({\it{xy\/}})\index{p})\index{sy-m2})\index{s-dec})\index{s-dec})\-\index{s-mux})\index{s-eq0}, \\ 
{\rm{s-eq0}}\,({\rm{p}}\,({\it{xy\/}})\index{p})\index{s-eq0})\-\index{s-or})\-\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yout}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xx\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,(\=\+{\tt{0}}, \\ 
{\rm{s-mux}}\,(\=\+{\rm{sy-m2}}\,({\tt{'}}{\tt{ydone}}, {\rm{p}}\,({\it{xx\/}})\index{p}, {\rm{p}}\,({\it{xy\/}})\index{p})\index{sy-m2}, \\ 
{\rm{s-mux}}\,({\rm{s-eq0}}\,({\rm{p}}\,({\it{xx\/}})\index{p})\index{s-eq0}, {\rm{s-const}}\,({\tt{0}}, {\rm{p}}\,({\it{xx\/}})\index{p})\index{s-const}, {\rm{p}}\,({\it{xy\/}})\index{p})\index{s-mux}, \\ 
{\rm{s-plus}}\,(\=\+{\rm{s-mux}}\,(\=\+{\rm{s-eq0}}\,({\rm{p}}\,({\it{xx\/}})\index{p})\index{s-eq0}, \\ 
{\rm{s-const}}\,({\tt{0}}, {\rm{p}}\,({\it{xx\/}})\index{p})\index{s-const}, \\ 
{\rm{p}}\,({\it{xy\/}})\index{p})\-\index{s-mux}, \\ 
{\rm{sy-m2}}\,({\tt{'}}{\tt{yout}}, {\rm{p}}\,({\it{xx\/}})\index{p}, {\rm{p}}\,({\it{xy\/}})\index{p})\index{sy-m2})\-\index{s-plus})\-\index{s-mux})\-\index{i}$\;${\bf  endif}\- \\ 
{\bf else }{\rm{sfix}}\,({\it{xx\/}})\index{sfix}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; M2 is just a GENERALIZED sysd, and our A2 lemmas should still be 
; true. The following were (Sugar) generated by:
; (vp (bma2sysd-aux 'sy-M2 'sy-M2 '(Xx Xy) 
;                   '(DEC OR EQ0 CONST MUX PLUS)))
; and then A2-PC was taken out by hand, preemptively.

;; A2-Begin-SY-M2

\end{verbatim}\begin{tabbing}{\sc Theorem}:  a2-empty-sy-m2 \\ \index{a2-empty-sy-m2}
({\rm{len}}\,({\it{xx\/}})\index{len} $=$ {\rm{len}}\,({\it{xy\/}})\index{len}) $\rightarrow$ ({\rm{empty}}\,({\rm{sy-m2}}\,({\it{ln\/}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-m2})\index{empty} $=$ {\rm{empty}}\,({\it{xx\/}})\index{empty})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-e-sy-m2 \\ \index{a2-e-sy-m2}
({\rm{len}}\,({\it{xx\/}})\index{len} $=$ {\rm{len}}\,({\it{xy\/}})\index{len}) $\rightarrow$ (({\rm{sy-m2}}\,({\it{ln\/}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-m2} $=$ {\sc{e}}\index{e}) $=$ {\rm{empty}}\,({\it{xx\/}})\index{empty})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-lp-sy-m2 \\ \index{a2-lp-sy-m2}
({\rm{len}}\,({\it{xx\/}})\index{len} $=$ {\rm{len}}\,({\it{xy\/}})\index{len}) $\rightarrow$ ({\rm{len}}\,({\rm{sy-m2}}\,({\it{ln\/}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-m2})\index{len} $=$ {\rm{len}}\,({\it{xx\/}})\index{len})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-lpe-sy-m2 \\ \index{a2-lpe-sy-m2}
({\rm{len}}\,({\it{xx\/}})\index{len} $=$ {\rm{len}}\,({\it{xy\/}})\index{len}) $\rightarrow$ {\rm{eqlen}}\,({\rm{sy-m2}}\,({\it{ln\/}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-m2}, {\it{xx\/}})\index{eqlen}
\end{tabbing}

\begin{verbatim};(PROVE-LEMMA A2-PC-SY-M2 (REWRITE)
;    (IMPLIES (EQUAL (LEN XX) (LEN XY))
;             (EQUAL (P (SY-M2 LN XX XY)) (SY-M2 LN (P XX) (P XY))))
;    ((DISABLE LEN S-DEC S-OR S-EQ0 S-CONST S-MUX S-PLUS A2-IC-S-DEC
;              A2-IC-S-OR A2-IC-S-EQ0 A2-IC-S-CONST A2-IC-S-MUX
;              A2-IC-S-PLUS)
;     (ENABLE STR-ADD1-LEN-P)))

;; A2-End-SY-M2

; This KEY equality lemma is proved immediately, 2 cases
; on empty Xx:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  multadd-is-m2 \\ \index{multadd-is-m2}
\=\+({\rm{sy-multadd}}\,({\tt{'}}{\tt{yout}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-multadd} $=$ {\rm{sy-m2}}\,({\tt{'}}{\tt{yout}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-m2}) \\ 
$\wedge$$\;\;\;\;$({\rm{sy-multadd}}\,({\tt{'}}{\tt{ydone}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-multadd} $=$ {\rm{sy-m2}}\,({\tt{'}}{\tt{ydone}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-m2}) \\ 
$\wedge$$\;\;\;\;$({\rm{sy-multadd}}\,({\tt{'}}{\tt{yn}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-multadd} $=$ {\rm{sy-m2}}\,({\tt{'}}{\tt{yn}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-m2})\-
\end{tabbing}

\begin{verbatim}; Note: simplified sysd was obtained w/ same hint as above minus 
; induction and M2 expansions, and replacing sy-multadd by sy-m2 
; by hand, IN:
;(dcl dummy ())
;(prove-lemma d1 ()
;(implies (not (empty Xx))
;	 (equal (sy-multadd 'Ydone Xx Xy) (dummy)))
;)


; The FUNDAMENTAL invariant property for the circuit is:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  multadd-correct-m2-inv \\ \index{multadd-correct-m2-inv}
\=\+(\=\+({\it{xa\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{xb\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $<$ ($1\;+$ ($1\;+$ {\it{xa\/}}))) \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{k\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{xa\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{xb\/}} $\not\simeq {\tt{0}}$))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+{\rm{l}}\,({\rm{sy-m2}}\,({\tt{'}}{\tt{yout}}, {\rm{s-constl}}\,({\it{xa\/}}, {\it{k\/}})\index{s-constl}, {\rm{s-constl}}\,({\it{xb\/}}, {\it{k\/}})\index{s-constl})\index{sy-m2})\index{l} \\ 
$=$$\;\;\;\;$({\it{xb\/}} $*$ ({\it{k\/}} $-\;1$)))\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{l}}\,({\rm{sy-m2}}\,({\tt{'}}{\tt{ydone}}, {\rm{s-constl}}\,({\it{xa\/}}, {\it{k\/}})\index{s-constl}, {\rm{s-constl}}\,({\it{xb\/}}, {\it{k\/}})\index{s-constl})\index{sy-m2})\index{l} \\ 
$=$$\;\;\;\;$({\it{xa\/}} $=$ ({\it{k\/}} $-\;1$)))\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{l}}\,({\rm{sy-m2}}\,({\tt{'}}{\tt{yn}}, {\rm{s-constl}}\,({\it{xa\/}}, {\it{k\/}})\index{s-constl}, {\rm{s-constl}}\,({\it{xb\/}}, {\it{k\/}})\index{s-constl})\index{sy-m2})\index{l} \\ 
$=$$\;\;\;\;$({\it{xa\/}} $-$ (({\it{k\/}} $-\;1$) $-\;1$)))\-)\-\-
\end{tabbing}

\begin{verbatim}; Now it's just a matter of instantiating it to the right 
; Deroulement, and moving to MULTADD.

; NOTE: in a first draft of this proof, we first went to the 
; identical theorem in terms of M2, and then passed over trivially.
; Attempting direct results about SY-MULTADD during experimentation
; is asking for trouble...

; NOTE: factoring out below Xx and Xy in the hyps as is done below
; yields a true,provable, but UNUSABLE rewrite thm because Xa and 
; Xb are FREE. It looks cuter though, so we may want it that way
; in FINAL thms.


\end{verbatim}\begin{tabbing}{\sc Theorem}:  multadd-correct \\ \index{multadd-correct}
\=\+(\=\+({\it{xa\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{xb\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{xa\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{xb\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{xx\/}} $=$ {\rm{s-constl}}\,({\it{xa\/}}, $1\;+$ {\it{xa\/}})\index{s-constl}) \\ 
$\wedge$$\;\;\;\;$({\it{xy\/}} $=$ {\rm{s-constl}}\,({\it{xb\/}}, $1\;+$ {\it{xa\/}})\index{s-constl}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{l}}\,({\rm{sy-multadd}}\,({\tt{'}}{\tt{yout}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-multadd})\index{l} $=$ ({\it{xb\/}} $*$ {\it{xa\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{l}}\,({\rm{sy-multadd}}\,({\tt{'}}{\tt{ydone}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-multadd})\index{l} $=$ {\bf{t}}))\-\-
\end{tabbing}

\begin{verbatim}; And of treating the case where either input is 0 separately:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  multadd-correct-case-0 \\ \index{multadd-correct-case-0}
\=\+(\=\+({\it{xa\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{xb\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$(({\it{xa\/}} $\simeq {\tt{0}}$) $\vee$ ({\it{xb\/}} $\simeq {\tt{0}}$)) \\ 
$\wedge$$\;\;\;\;$({\it{xx\/}} $=$ {\rm{s-constl}}\,({\it{xa\/}}, {\tt{2}})\index{s-constl}) \\ 
$\wedge$$\;\;\;\;$({\it{xy\/}} $=$ {\rm{s-constl}}\,({\it{xb\/}}, {\tt{2}})\index{s-constl}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{l}}\,({\rm{sy-multadd}}\,({\tt{'}}{\tt{yout}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-multadd})\index{l} $=$ ({\it{xb\/}} $*$ {\it{xa\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{l}}\,({\rm{sy-multadd}}\,({\tt{'}}{\tt{ydone}}, {\it{xx\/}}, {\it{xy\/}})\index{sy-multadd})\index{l} $=$ {\bf{t}}))\-\-
\end{tabbing}

\begin{verbatim}; eof: multadd.bm
;))

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