\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}; bcdSbi.bm: = bcdS, but with integer bits instead of booleans on the wires.
;   LESSONS:
;    - the quality of the proofs is not degraded, we usually get the same
;      case splits, except sometime with one or two more cases.
;    - the timing is degraded by 50% on average, with a range of 20% to 300%
; So in general we should stick (or start) with a boolean model of 0 and 1,
; but if for some crucial reason we have to go numerical, it's no major
; disaster.
;

;;; CIRCUIT in SUGARED form:
#|
(setq sysd '(sy-BCDSBI (x)
(Y01 S bnot x)
(Y02 S bnot x)
(Y03 S bnot YR3)
(Y04 S bnot YR1)
(Y05 S bnot YR2)
(Y06 S bnot YR3)
(Y07 S bnot YR1)
(Y08 S bnot YR3)
(Y11 S band3 Y01 YR1 YR3)
(Y12 S band3 Y02 YR2 Y03)
(Y13 S band3 Y04 Y05 Y06)
(Y14 S band3 x Y07 Y08)
(Y15 S band3 x YR1 YR3)
(Y21 S bor Y11 Y12)
(Y22 S bor Y13 Y14)
(Y23 S bor YR2 Y15)
(YR1 R 0 Y21)
(YR2 R 0 Y22)
(YR3 R 0 Y23)
(Y31 S bnot YR1)
(Y32 S bnot YR2)
(Y41 S band4 x Y31 Y32 YR3)
(Yout S bnot Y41)
))

(setq bcdSbi '( |#
; this load entered by hand, because needed in the SPEC
; comb_band.bm: Binary And combinational element
; U7-DONE

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{band} \\  
\=\+{\rm{band}}\,({\it{u\/}}, {\it{v\/}})\index{band} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{u\/}} $=$ {\tt{0}}) $\vee$ ({\it{v\/}} $=$ {\tt{0}})$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\tt{1}}$\;${\bf  endif}\-\-
\end{tabbing}
	   
\begin{verbatim}; Everything below generated by: (bmcomb 'band '() '(x y))

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

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

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

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

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

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

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

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

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

\begin{tabbing}{\sc Theorem}:  a2-hc-s-band \\ \index{a2-hc-s-band}
\=\+(($\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-band}}\,({\it{x\/}}, {\it{y\/}})\index{s-band})\index{h} $=$ {\rm{band}}\,({\rm{h}}\,({\it{x\/}})\index{h}, {\rm{h}}\,({\it{y\/}})\index{h})\index{band})\-
\end{tabbing}

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

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

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

; eof:comb_band.bm


; BM DEFINITIONS and A2 LEMMAS, generated by BMSYSD:
; comb_band3.bm: Binary And3 combinational element
; U7-DONE

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{band3} \\  
\=\+{\rm{band3}}\,({\it{u1\/}}, {\it{u2\/}}, {\it{u3\/}})\index{band3} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{u1\/}} $=$ {\tt{0}}) $\vee$ ({\it{u2\/}} $=$ {\tt{0}}) $\vee$ ({\it{u3\/}} $=$ {\tt{0}})$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\tt{1}}$\;${\bf  endif}\-\-
\end{tabbing}
	   
\begin{verbatim}; Everything below generated by: (bmcomb 'band3 '() '(x1 x2 x3))

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

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

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

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

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

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

\begin{tabbing}{\sc Theorem}:  a2-ic-s-band3 \\ \index{a2-ic-s-band3}
\=\+(({\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-band3}}\,({\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-band3} \\ 
$=$$\;\;\;\;${\rm{i}}\,({\rm{band3}}\,({\it{c\_x1\/}}, {\it{c\_x2\/}}, {\it{c\_x3\/}})\index{band3}, {\rm{s-band3}}\,({\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{s-band3})\index{i})\-\-
\end{tabbing}

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

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

\begin{tabbing}{\sc Theorem}:  a2-hc-s-band3 \\ \index{a2-hc-s-band3}
\=\+(($\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-band3}}\,({\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{s-band3})\index{h} $=$ {\rm{band3}}\,({\rm{h}}\,({\it{x1\/}})\index{h}, {\rm{h}}\,({\it{x2\/}})\index{h}, {\rm{h}}\,({\it{x3\/}})\index{h})\index{band3})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-bc-s-band3 \\ \index{a2-bc-s-band3}
\=\+(({\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-band3}}\,({\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{s-band3})\index{b} $=$ {\rm{s-band3}}\,({\rm{b}}\,({\it{x1\/}})\index{b}, {\rm{b}}\,({\it{x2\/}})\index{b}, {\rm{b}}\,({\it{x3\/}})\index{b})\index{s-band3})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-bnc-s-band3 \\ \index{a2-bnc-s-band3}
\=\+(({\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-band3}}\,({\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{s-band3})\index{bn} $=$ {\rm{s-band3}}\,({\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-band3})\-
\end{tabbing}

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

; eof:comb_band3.bm

; comb_bor.bm: Binary Or combinational element
; U7-DONE

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{bor} \\  
\=\+{\rm{bor}}\,({\it{u\/}}, {\it{v\/}})\index{bor} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{u\/}} $=$ {\tt{0}}) $\wedge$ ({\it{v\/}} $=$ {\tt{0}})$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\tt{1}}$\;${\bf  endif}\-\-
\end{tabbing}
	   
\begin{verbatim}; Everything below generated by: (bmcomb 'bor '() '(x y))

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

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

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

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

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

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

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

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

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

\begin{tabbing}{\sc Theorem}:  a2-hc-s-bor \\ \index{a2-hc-s-bor}
\=\+(($\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-bor}}\,({\it{x\/}}, {\it{y\/}})\index{s-bor})\index{h} $=$ {\rm{bor}}\,({\rm{h}}\,({\it{x\/}})\index{h}, {\rm{h}}\,({\it{y\/}})\index{h})\index{bor})\-
\end{tabbing}

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

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

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

; eof:comb_bor.bm

; comb_band4.bm: Binary And4 combinational element
; U7-DONE

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{band4} \\  
\=\+{\rm{band4}}\,({\it{u1\/}}, {\it{u2\/}}, {\it{u3\/}}, {\it{u4\/}})\index{band4} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{u1\/}} $=$ {\tt{0}}) $\vee$ ({\it{u2\/}} $=$ {\tt{0}}) $\vee$ ({\it{u3\/}} $=$ {\tt{0}}) $\vee$ ({\it{u4\/}} $=$ {\tt{0}})$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\tt{1}}$\;${\bf  endif}\-\-
\end{tabbing}
	   
\begin{verbatim}; Everything below generated by: (bmcomb 'band4 '() '(x1 x2 x3 x4))

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

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

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

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

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

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

\begin{tabbing}{\sc Theorem}:  a2-ic-s-band4 \\ \index{a2-ic-s-band4}
\=\+(({\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}) $\wedge$ ({\rm{len}}\,({\it{x3\/}})\index{len} $=$ {\rm{len}}\,({\it{x4\/}})\index{len})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{s-band4}}\,({\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}, {\rm{i}}\,({\it{c\_x4\/}}, {\it{x4\/}})\index{i})\index{s-band4} \\ 
$=$$\;\;\;\;${\rm{i}}\,({\rm{band4}}\,({\it{c\_x1\/}}, {\it{c\_x2\/}}, {\it{c\_x3\/}}, {\it{c\_x4\/}})\index{band4}, {\rm{s-band4}}\,({\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}}, {\it{x4\/}})\index{s-band4})\index{i})\-\-
\end{tabbing}

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

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

\begin{tabbing}{\sc Theorem}:  a2-hc-s-band4 \\ \index{a2-hc-s-band4}
\=\+(\=\+($\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}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{x3\/}})\index{len} $=$ {\rm{len}}\,({\it{x4\/}})\index{len}))\-)\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{h}}\,({\rm{s-band4}}\,({\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}}, {\it{x4\/}})\index{s-band4})\index{h} $=$ {\rm{band4}}\,({\rm{h}}\,({\it{x1\/}})\index{h}, {\rm{h}}\,({\it{x2\/}})\index{h}, {\rm{h}}\,({\it{x3\/}})\index{h}, {\rm{h}}\,({\it{x4\/}})\index{h})\index{band4})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-bc-s-band4 \\ \index{a2-bc-s-band4}
\=\+(({\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}) $\wedge$ ({\rm{len}}\,({\it{x3\/}})\index{len} $=$ {\rm{len}}\,({\it{x4\/}})\index{len})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{b}}\,({\rm{s-band4}}\,({\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}}, {\it{x4\/}})\index{s-band4})\index{b} $=$ {\rm{s-band4}}\,({\rm{b}}\,({\it{x1\/}})\index{b}, {\rm{b}}\,({\it{x2\/}})\index{b}, {\rm{b}}\,({\it{x3\/}})\index{b}, {\rm{b}}\,({\it{x4\/}})\index{b})\index{s-band4})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-bnc-s-band4 \\ \index{a2-bnc-s-band4}
\=\+(({\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}) $\wedge$ ({\rm{len}}\,({\it{x3\/}})\index{len} $=$ {\rm{len}}\,({\it{x4\/}})\index{len})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{bn}}\,({\it{n\/}}, {\rm{s-band4}}\,({\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}}, {\it{x4\/}})\index{s-band4})\index{bn} \\ 
$=$$\;\;\;\;${\rm{s-band4}}\,({\rm{bn}}\,({\it{n\/}}, {\it{x1\/}})\index{bn}, {\rm{bn}}\,({\it{n\/}}, {\it{x2\/}})\index{bn}, {\rm{bn}}\,({\it{n\/}}, {\it{x3\/}})\index{bn}, {\rm{bn}}\,({\it{n\/}}, {\it{x4\/}})\index{bn})\index{s-band4})\-\-
\end{tabbing}

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

; eof:comb_band4.bm

; comb_bnot.bm: Binary Not combinational element
; U7-DONE

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{bnot} \\  
\=\+{\rm{bnot}}\,({\it{u\/}})\index{bnot} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{u\/}} $=$ {\tt{0}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}
	   
\begin{verbatim}; Everything below generated by: (bmcomb 'bnot '() '(x))

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

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

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

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

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

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

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

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

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

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

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

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

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

; eof:comb_bnot.bm


\end{verbatim}\begin{tabbing}{\sc Definition}:\index{topor-sy-bcdsbi} \\  
\=\+{\rm{topor-sy-bcdsbi}}\,({\it{ln\/}})\index{topor-sy-bcdsbi} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{ln\/}} $=$ {\tt{'}}{\tt{y01}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y02}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y03}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y04}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y05}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y06}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y07}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y08}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y11}}$\;\;${\bf then }{\tt{2}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y12}}$\;\;${\bf then }{\tt{2}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y13}}$\;\;${\bf then }{\tt{2}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y14}}$\;\;${\bf then }{\tt{2}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y15}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y21}}$\;\;${\bf then }{\tt{3}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y22}}$\;\;${\bf then }{\tt{3}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y23}}$\;\;${\bf then }{\tt{2}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yr1}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yr2}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yr3}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y31}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y32}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y41}}$\;\;${\bf then }{\tt{2}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yout}}$\;\;${\bf then }{\tt{3}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{sy-bcdsbi} \\  
\=\+{\rm{sy-bcdsbi}}\,({\it{ln\/}}, {\it{x\/}})\index{sy-bcdsbi} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{ln\/}} $=$ {\tt{'}}{\tt{y01}}$\;\;${\bf then }{\rm{s-bnot}}\,({\it{x\/}})\index{s-bnot} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y02}}$\;\;${\bf then }{\rm{s-bnot}}\,({\it{x\/}})\index{s-bnot} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y03}}$\;\;${\bf then }{\rm{s-bnot}}\,({\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{yr3}}, {\it{x\/}})\index{sy-bcdsbi})\index{s-bnot} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y04}}$\;\;${\bf then }{\rm{s-bnot}}\,({\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{yr1}}, {\it{x\/}})\index{sy-bcdsbi})\index{s-bnot} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y05}}$\;\;${\bf then }{\rm{s-bnot}}\,({\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{yr2}}, {\it{x\/}})\index{sy-bcdsbi})\index{s-bnot} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y06}}$\;\;${\bf then }{\rm{s-bnot}}\,({\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{yr3}}, {\it{x\/}})\index{sy-bcdsbi})\index{s-bnot} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y07}}$\;\;${\bf then }{\rm{s-bnot}}\,({\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{yr1}}, {\it{x\/}})\index{sy-bcdsbi})\index{s-bnot} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y08}}$\;\;${\bf then }{\rm{s-bnot}}\,({\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{yr3}}, {\it{x\/}})\index{sy-bcdsbi})\index{s-bnot} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y11}} \\ 
{\bf then }{\rm{s-band3}}\,(\=\+{\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{y01}}, {\it{x\/}})\index{sy-bcdsbi}, \\ 
{\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{yr1}}, {\it{x\/}})\index{sy-bcdsbi}, \\ 
{\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{yr3}}, {\it{x\/}})\index{sy-bcdsbi})\-\index{s-band3} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y12}} \\ 
{\bf then }{\rm{s-band3}}\,(\=\+{\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{y02}}, {\it{x\/}})\index{sy-bcdsbi}, \\ 
{\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{yr2}}, {\it{x\/}})\index{sy-bcdsbi}, \\ 
{\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{y03}}, {\it{x\/}})\index{sy-bcdsbi})\-\index{s-band3} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y13}} \\ 
{\bf then }{\rm{s-band3}}\,(\=\+{\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{y04}}, {\it{x\/}})\index{sy-bcdsbi}, \\ 
{\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{y05}}, {\it{x\/}})\index{sy-bcdsbi}, \\ 
{\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{y06}}, {\it{x\/}})\index{sy-bcdsbi})\-\index{s-band3} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y14}} \\ 
{\bf then }{\rm{s-band3}}\,({\it{x\/}}, {\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{y07}}, {\it{x\/}})\index{sy-bcdsbi}, {\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{y08}}, {\it{x\/}})\index{sy-bcdsbi})\index{s-band3} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y15}} \\ 
{\bf then }{\rm{s-band3}}\,({\it{x\/}}, {\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{yr1}}, {\it{x\/}})\index{sy-bcdsbi}, {\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{yr3}}, {\it{x\/}})\index{sy-bcdsbi})\index{s-band3} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y21}} \\ 
{\bf then }{\rm{s-bor}}\,({\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{y11}}, {\it{x\/}})\index{sy-bcdsbi}, {\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{y12}}, {\it{x\/}})\index{sy-bcdsbi})\index{s-bor} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y22}} \\ 
{\bf then }{\rm{s-bor}}\,({\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{y13}}, {\it{x\/}})\index{sy-bcdsbi}, {\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{y14}}, {\it{x\/}})\index{sy-bcdsbi})\index{s-bor} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y23}} \\ 
{\bf then }{\rm{s-bor}}\,({\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{yr2}}, {\it{x\/}})\index{sy-bcdsbi}, {\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{y15}}, {\it{x\/}})\index{sy-bcdsbi})\index{s-bor} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yr1}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{0}}, {\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{y21}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-bcdsbi})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yr2}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{0}}, {\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{y22}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-bcdsbi})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yr3}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{0}}, {\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{y23}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-bcdsbi})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y31}}$\;\;${\bf then }{\rm{s-bnot}}\,({\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{yr1}}, {\it{x\/}})\index{sy-bcdsbi})\index{s-bnot} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y32}}$\;\;${\bf then }{\rm{s-bnot}}\,({\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{yr2}}, {\it{x\/}})\index{sy-bcdsbi})\index{s-bnot} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y41}} \\ 
{\bf then }{\rm{s-band4}}\,(\=\+{\it{x\/}}, \\ 
{\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{y31}}, {\it{x\/}})\index{sy-bcdsbi}, \\ 
{\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{y32}}, {\it{x\/}})\index{sy-bcdsbi}, \\ 
{\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{yr3}}, {\it{x\/}})\index{sy-bcdsbi})\-\index{s-band4} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yout}}$\;\;${\bf then }{\rm{s-bnot}}\,({\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{y41}}, {\it{x\/}})\index{sy-bcdsbi})\index{s-bnot} \\ 
{\bf else }{\rm{sfix}}\,({\it{x\/}})\index{sfix}$\;${\bf  endif}\-\-
\end{tabbing}

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

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

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

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

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

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

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

;;; Circuit CORRECTNESS /Paillet:

; BCD-bits defines a correct binary coded decimal, b0 is most-significant.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{bcd-bits} \\  
{\rm{bcd-bits}}\,({\it{b0\/}}, {\it{b1\/}}, {\it{b2\/}}, {\it{b3\/}})\index{bcd-bits} $=$ (({\it{b0\/}} $=$ {\tt{0}}) $\vee$ (({\it{b1\/}} $=$ {\tt{0}}) $\wedge$ ({\it{b2\/}} $=$ {\tt{0}})))
\end{tabbing}

\begin{verbatim}; CORRECTNESS:

;;; WHAT PAILLET ACTUALLY PROVES: 

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{sy-b2i} \\  
\=\+{\rm{sy-b2i}}\,({\it{ln\/}}, {\it{x\/}})\index{sy-b2i} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{ln\/}} $=$ {\tt{'}}{\tt{yr1}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,(\=\+{\tt{0}}, \\ 
{\rm{s-bor}}\,(\=\+{\rm{s-band3}}\,(\=\+{\rm{s-bnot}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{s-bnot}, \\ 
{\rm{sy-b2i}}\,({\tt{'}}{\tt{yr1}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b2i}, \\ 
{\rm{sy-b2i}}\,({\tt{'}}{\tt{yr3}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b2i})\-\index{s-band3}, \\ 
{\rm{s-band3}}\,(\=\+{\rm{s-bnot}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{s-bnot}, \\ 
{\rm{sy-b2i}}\,({\tt{'}}{\tt{yr2}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b2i}, \\ 
{\rm{s-bnot}}\,({\rm{sy-b2i}}\,({\tt{'}}{\tt{yr3}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b2i})\index{s-bnot})\-\index{s-band3})\-\index{s-bor})\-\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yr2}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,(\=\+{\tt{0}}, \\ 
{\rm{s-bor}}\,(\=\+{\rm{s-band3}}\,(\=\+{\rm{s-bnot}}\,({\rm{sy-b2i}}\,({\tt{'}}{\tt{yr1}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b2i})\index{s-bnot}, \\ 
{\rm{s-bnot}}\,({\rm{sy-b2i}}\,({\tt{'}}{\tt{yr2}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b2i})\index{s-bnot}, \\ 
{\rm{s-bnot}}\,({\rm{sy-b2i}}\,({\tt{'}}{\tt{yr3}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b2i})\index{s-bnot})\-\index{s-band3}, \\ 
{\rm{s-band3}}\,(\=\+{\rm{p}}\,({\it{x\/}})\index{p}, \\ 
{\rm{s-bnot}}\,({\rm{sy-b2i}}\,({\tt{'}}{\tt{yr1}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b2i})\index{s-bnot}, \\ 
{\rm{s-bnot}}\,({\rm{sy-b2i}}\,({\tt{'}}{\tt{yr3}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b2i})\index{s-bnot})\-\index{s-band3})\-\index{s-bor})\-\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yr3}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,(\=\+{\tt{0}}, \\ 
{\rm{s-bor}}\,(\=\+{\rm{sy-b2i}}\,({\tt{'}}{\tt{yr2}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b2i}, \\ 
{\rm{s-band3}}\,(\=\+{\rm{p}}\,({\it{x\/}})\index{p}, \\ 
{\rm{sy-b2i}}\,({\tt{'}}{\tt{yr1}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b2i}, \\ 
{\rm{sy-b2i}}\,({\tt{'}}{\tt{yr3}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b2i})\-\index{s-band3})\-\index{s-bor})\-\index{i}$\;${\bf  endif}\- \\ 
{\bf else }{\rm{sfix}}\,({\it{x\/}})\index{sfix}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; B2 is just a GENERALIZED sysd, and our A2 lemmas should still be true: 
; The following were generated by:
; (vp (bma2sysd-aux 'sy-b2i 'sy-b2i '(x) '(band3 bor band4 bnot)))
; with A2-PC preemptively disabled.

;; A2-Begin-SY-B2I

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

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

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

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

\begin{verbatim};(PROVE-LEMMA A2-PC-SY-B2I (REWRITE)
;    (EQUAL (P (SY-B2I LN X)) (SY-B2I LN (P X)))
;    ((DISABLE S-BAND3 S-BOR S-BAND4 S-BNOT A2-IC-S-BAND3 A2-IC-S-BOR
;              A2-IC-S-BAND4 A2-IC-S-BNOT)))

;; A2-End-SY-B2I

; BCDS-is-B2i is the essence of this simplification.  

\end{verbatim}\begin{tabbing}{\sc Theorem}:  bcdsbi-is-b2i \\ \index{bcdsbi-is-b2i}
\=\+({\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{yr1}}, {\it{x\/}})\index{sy-bcdsbi} $=$ {\rm{sy-b2i}}\,({\tt{'}}{\tt{yr1}}, {\it{x\/}})\index{sy-b2i}) \\ 
$\wedge$$\;\;\;\;$({\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{yr2}}, {\it{x\/}})\index{sy-bcdsbi} $=$ {\rm{sy-b2i}}\,({\tt{'}}{\tt{yr2}}, {\it{x\/}})\index{sy-b2i}) \\ 
$\wedge$$\;\;\;\;$({\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{yr3}}, {\it{x\/}})\index{sy-bcdsbi} $=$ {\rm{sy-b2i}}\,({\tt{'}}{\tt{yr3}}, {\it{x\/}})\index{sy-b2i})\-
\end{tabbing}

\begin{verbatim}; at this point we should never need SY-BCDSBI anymore:
\end{verbatim}
\noindent{\sc Event}:   Disable sy-bcdsbi.

\addvspace{18pt}

\begin{verbatim}; and also he does the expansion for Yout once and for all:
; Note: A-POSTERIORI analysis indicates that this lemma is not really useful
; to BM, which is usual, since it's just a non-recursive rewrite, and we might
; as well give the expand hint at the right place.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  bcdsbi-eq-yout \\ \index{bcdsbi-eq-yout}
\=\+{\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{yout}}, {\it{x\/}})\index{sy-bcdsbi} \\ 
$=$$\;\;\;\;${\rm{s-bnot}}\,({\rm{s-band4}}\,(\=\+{\it{x\/}}, \\ 
{\rm{s-bnot}}\,({\rm{sy-b2i}}\,({\tt{'}}{\tt{yr1}}, {\it{x\/}})\index{sy-b2i})\index{s-bnot}, \\ 
{\rm{s-bnot}}\,({\rm{sy-b2i}}\,({\tt{'}}{\tt{yr2}}, {\it{x\/}})\index{sy-b2i})\index{s-bnot}, \\ 
{\rm{sy-b2i}}\,({\tt{'}}{\tt{yr3}}, {\it{x\/}})\index{sy-b2i})\-\index{s-band4})\index{s-bnot}\-
\end{tabbing}

\begin{verbatim};; SECOND, he proves things about his DEROULEMENTS:
; note: all thms below are "one-shot", i.e. disabled and enabled explicitely
; NOTE: at this point we express everything in terms of B2; obviously
;       with BCDSBI-IS-B2i we can carry everything over.  This follows Paillet.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  bcdsbi-paillet-1 \\ \index{bcdsbi-paillet-1}
\=\+({\rm{len}}\,({\it{x\/}})\index{len} $=$ {\tt{1}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{l}}\,({\rm{sy-b2i}}\,({\tt{'}}{\tt{yr1}}, {\it{x\/}})\index{sy-b2i})\index{l} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{l}}\,({\rm{sy-b2i}}\,({\tt{'}}{\tt{yr2}}, {\it{x\/}})\index{sy-b2i})\index{l} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{l}}\,({\rm{sy-b2i}}\,({\tt{'}}{\tt{yr3}}, {\it{x\/}})\index{sy-b2i})\index{l} $=$ {\tt{0}}))\-\-
\end{tabbing}

\noindent{\sc Event}:   Disable bcdsbi-paillet-1.

\addvspace{18pt}


\begin{tabbing}{\sc Theorem}:  bcdsbi-paillet-1out \\ \index{bcdsbi-paillet-1out}
({\rm{len}}\,({\it{x\/}})\index{len} $=$ {\tt{1}}) $\rightarrow$ ({\rm{l}}\,({\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{yout}}, {\it{x\/}})\index{sy-bcdsbi})\index{l} $=$ {\tt{1}})
\end{tabbing}

\noindent{\sc Event}:   Disable bcdsbi-paillet-1out.

\addvspace{18pt}


\begin{tabbing}{\sc Theorem}:  bcdsbi-paillet-2 \\ \index{bcdsbi-paillet-2}
\=\+({\rm{len}}\,({\it{x\/}})\index{len} $=$ {\tt{2}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{l}}\,({\rm{sy-b2i}}\,({\tt{'}}{\tt{yr1}}, {\it{x\/}})\index{sy-b2i})\index{l} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{l}}\,({\rm{sy-b2i}}\,({\tt{'}}{\tt{yr2}}, {\it{x\/}})\index{sy-b2i})\index{l} $=$ {\tt{1}}) \\ 
$\wedge$$\;\;\;\;$({\rm{l}}\,({\rm{sy-b2i}}\,({\tt{'}}{\tt{yr3}}, {\it{x\/}})\index{sy-b2i})\index{l} $=$ {\tt{0}}))\-\-
\end{tabbing}

\noindent{\sc Event}:   Disable bcdsbi-paillet-2.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  bcdsbi-paillet-2out \\ \index{bcdsbi-paillet-2out}
({\rm{len}}\,({\it{x\/}})\index{len} $=$ {\tt{2}}) $\rightarrow$ ({\rm{l}}\,({\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{yout}}, {\it{x\/}})\index{sy-bcdsbi})\index{l} $=$ {\tt{1}})
\end{tabbing}

\noindent{\sc Event}:   Disable bcdsbi-paillet-2out.

\addvspace{18pt}

\begin{verbatim}; Note that the "bitp" hyp is not explicit in Paillet...  

\end{verbatim}\begin{tabbing}{\sc Theorem}:  bcdsbi-paillet-3 \\ \index{bcdsbi-paillet-3}
\=\+(({\rm{len}}\,({\it{x\/}})\index{len} $=$ {\tt{3}}) $\wedge$ {\rm{s-bitp}}\,({\it{x\/}})\index{s-bitp}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{l}}\,({\rm{sy-b2i}}\,({\tt{'}}{\tt{yr1}}, {\it{x\/}})\index{sy-b2i})\index{l} $=$ {\rm{bnot}}\,({\rm{l}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{l})\index{bnot}) \\ 
$\wedge$$\;\;\;\;$({\rm{l}}\,({\rm{sy-b2i}}\,({\tt{'}}{\tt{yr2}}, {\it{x\/}})\index{sy-b2i})\index{l} $=$ {\rm{l}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{l}) \\ 
$\wedge$$\;\;\;\;$({\rm{l}}\,({\rm{sy-b2i}}\,({\tt{'}}{\tt{yr3}}, {\it{x\/}})\index{sy-b2i})\index{l} $=$ {\tt{1}}))\-\-
\end{tabbing}

\noindent{\sc Event}:   Disable bcdsbi-paillet-3.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  bcdsbi-paillet-3out \\ \index{bcdsbi-paillet-3out}
(({\rm{len}}\,({\it{x\/}})\index{len} $=$ {\tt{3}}) $\wedge$ {\rm{s-bitp}}\,({\it{x\/}})\index{s-bitp}) $\rightarrow$ ({\rm{l}}\,({\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{yout}}, {\it{x\/}})\index{sy-bcdsbi})\index{l} $=$ {\tt{1}})
\end{tabbing}

\noindent{\sc Event}:   Disable bcdsbi-paillet-3out.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  bcdsbi-paillet-4 \\ \index{bcdsbi-paillet-4}
\=\+(({\rm{len}}\,({\it{x\/}})\index{len} $=$ {\tt{4}}) $\wedge$ {\rm{s-bitp}}\,({\it{x\/}})\index{s-bitp}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{l}}\,({\rm{sy-b2i}}\,({\tt{'}}{\tt{yr1}}, {\it{x\/}})\index{sy-b2i})\index{l} $=$ {\rm{band}}\,({\rm{bnot}}\,({\rm{l}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{l})\index{bnot}, {\rm{bnot}}\,({\rm{l}}\,({\rm{p}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{p})\index{l})\index{bnot})\index{band}) \\ 
$\wedge$$\;\;\;\;$({\rm{l}}\,({\rm{sy-b2i}}\,({\tt{'}}{\tt{yr2}}, {\it{x\/}})\index{sy-b2i})\index{l} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{l}}\,({\rm{sy-b2i}}\,({\tt{'}}{\tt{yr3}}, {\it{x\/}})\index{sy-b2i})\index{l} \\ 
$=$$\;\;\;\;${\rm{bor}}\,({\rm{l}}\,({\rm{p}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{p})\index{l}, {\rm{band}}\,({\rm{l}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{l}, {\rm{bnot}}\,({\rm{l}}\,({\rm{p}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{p})\index{l})\index{bnot})\index{band})\index{bor})\-)\-\-
\end{tabbing}

\noindent{\sc Event}:   Disable bcdsbi-paillet-4.

\addvspace{18pt}

\begin{verbatim}; and his conclusion:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  bcdsbi-paillet-4out \\ \index{bcdsbi-paillet-4out}
\=\+(({\rm{len}}\,({\it{x\/}})\index{len} $=$ {\tt{4}}) $\wedge$ {\rm{s-bitp}}\,({\it{x\/}})\index{s-bitp}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{l}}\,({\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{yout}}, {\it{x\/}})\index{sy-bcdsbi})\index{l} \\ 
$=$$\;\;\;\;${\rm{bor}}\,({\rm{bnot}}\,({\rm{l}}\,({\it{x\/}})\index{l})\index{bnot}, {\rm{band}}\,({\rm{bnot}}\,({\rm{l}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{l})\index{bnot}, {\rm{bnot}}\,({\rm{l}}\,({\rm{p}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{p})\index{l})\index{bnot})\index{band})\index{bor})\-\-
\end{tabbing}

\noindent{\sc Event}:   Disable bcdsbi-paillet-4out.

\addvspace{18pt}

\begin{verbatim}; from which he leaves to the reader the real conclusion:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  bcdsbi-paillet-4out-correct \\ \index{bcdsbi-paillet-4out-correct}
\=\+(({\rm{len}}\,({\it{x\/}})\index{len} $=$ {\tt{4}}) $\wedge$ {\rm{s-bitp}}\,({\it{x\/}})\index{s-bitp}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{l}}\,({\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{yout}}, {\it{x\/}})\index{sy-bcdsbi})\index{l} \\ 
$=$$\;\;\;\;${\rm{bobi}}\,({\rm{bcd-bits}}\,({\rm{l}}\,({\it{x\/}})\index{l}, {\rm{l}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{l}, {\rm{l}}\,({\rm{p}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{p})\index{l}, {\rm{l}}\,({\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{p})\index{p})\index{l})\index{bcd-bits})\index{bobi})\-\-
\end{tabbing}

\noindent{\sc Event}:   Disable bcdsbi-paillet-4out-correct.

\addvspace{18pt}

\begin{verbatim}; and the last "re-initialization" condition:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  bcdsbi-paillet-5 \\ \index{bcdsbi-paillet-5}
\=\+(({\rm{len}}\,({\it{x\/}})\index{len} $=$ {\tt{5}}) $\wedge$ {\rm{s-bitp}}\,({\it{x\/}})\index{s-bitp}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{l}}\,({\rm{sy-b2i}}\,({\tt{'}}{\tt{yr1}}, {\it{x\/}})\index{sy-b2i})\index{l} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{l}}\,({\rm{sy-b2i}}\,({\tt{'}}{\tt{yr2}}, {\it{x\/}})\index{sy-b2i})\index{l} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{l}}\,({\rm{sy-b2i}}\,({\tt{'}}{\tt{yr3}}, {\it{x\/}})\index{sy-b2i})\index{l} $=$ {\tt{0}}))\-\-
\end{tabbing}

\noindent{\sc Event}:   Disable bcdsbi-paillet-5.

\addvspace{18pt}

\begin{verbatim};;; WHAT I CAN PROVE! :

\end{verbatim}\begin{tabbing}{\sc Theorem}:  bcdsbi-paillet-r-correct \\ \index{bcdsbi-paillet-r-correct}
\=\+(($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) $\wedge$ {\rm{s-bitp}}\,({\it{x\/}})\index{s-bitp}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+{\rm{l}}\,({\rm{sy-b2i}}\,({\tt{'}}{\tt{yr1}}, {\it{x\/}})\index{sy-b2i})\index{l} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\rm{len}}\,({\it{x\/}})\index{len} ${}${\bf{mod}}${}$ {\tt{4}}) $=$ {\tt{1}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }({\rm{len}}\,({\it{x\/}})\index{len} ${}${\bf{mod}}${}$ {\tt{4}}) $=$ {\tt{2}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }({\rm{len}}\,({\it{x\/}})\index{len} ${}${\bf{mod}}${}$ {\tt{4}}) $=$ {\tt{3}}$\;\;${\bf then }{\rm{bnot}}\,({\rm{l}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{l})\index{bnot} \\ 
{\bf else }{\rm{band}}\,({\rm{bnot}}\,({\rm{l}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{l})\index{bnot}, {\rm{bnot}}\,({\rm{l}}\,({\rm{p}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{p})\index{l})\index{bnot})\index{band}$\;${\bf  endif}\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{l}}\,({\rm{sy-b2i}}\,({\tt{'}}{\tt{yr2}}, {\it{x\/}})\index{sy-b2i})\index{l} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\rm{len}}\,({\it{x\/}})\index{len} ${}${\bf{mod}}${}$ {\tt{4}}) $=$ {\tt{1}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }({\rm{len}}\,({\it{x\/}})\index{len} ${}${\bf{mod}}${}$ {\tt{4}}) $=$ {\tt{2}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }({\rm{len}}\,({\it{x\/}})\index{len} ${}${\bf{mod}}${}$ {\tt{4}}) $=$ {\tt{3}}$\;\;${\bf then }{\rm{l}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{l} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{l}}\,({\rm{sy-b2i}}\,({\tt{'}}{\tt{yr3}}, {\it{x\/}})\index{sy-b2i})\index{l} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\rm{len}}\,({\it{x\/}})\index{len} ${}${\bf{mod}}${}$ {\tt{4}}) $=$ {\tt{1}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }({\rm{len}}\,({\it{x\/}})\index{len} ${}${\bf{mod}}${}$ {\tt{4}}) $=$ {\tt{2}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }({\rm{len}}\,({\it{x\/}})\index{len} ${}${\bf{mod}}${}$ {\tt{4}}) $=$ {\tt{3}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\rm{bor}}\,(\=\+{\rm{l}}\,({\rm{p}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{p})\index{l}, \\ 
{\rm{band}}\,({\rm{l}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{l}, {\rm{bnot}}\,({\rm{l}}\,({\rm{p}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{p})\index{l})\index{bnot})\index{band})\-\index{bor}$\;${\bf  endif}\-)\-)\-\-
\end{tabbing}

\begin{verbatim}; and finally, the true, general correctness of Paillet#5 :

\end{verbatim}\begin{tabbing}{\sc Theorem}:  bcdsbi-paillet-yout-correct \\ \index{bcdsbi-paillet-yout-correct}
\=\+(($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) $\wedge$ {\rm{s-bitp}}\,({\it{x\/}})\index{s-bitp}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{l}}\,({\rm{sy-bcdsbi}}\,({\tt{'}}{\tt{yout}}, {\it{x\/}})\index{sy-bcdsbi})\index{l} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\rm{len}}\,({\it{x\/}})\index{len} ${}${\bf{mod}}${}$ {\tt{4}}) $=$ {\tt{0}} \\ 
{\bf then }{\rm{bobi}}\,({\rm{bcd-bits}}\,({\rm{l}}\,({\it{x\/}})\index{l}, {\rm{l}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{l}, {\rm{l}}\,({\rm{p}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{p})\index{l}, {\rm{l}}\,({\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{p})\index{p})\index{l})\index{bcd-bits})\index{bobi} \\ 
{\bf else }{\tt{1}}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{verbatim}; eof: bcdsbi.bm
;))
\end{verbatim}
%\end{list}
\printindex
\end{document}
