\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}; bcd.bm: a BCD code checker, with serial (bit) input.
;  . we have proved correctness w/ registers init to 0 (i.e. 
;   reality) AND for ARBITRARY init values ('r0,'r1); although it 
;   doesn't REALLY MEAN anything since the combinationals interpret
;   that as ones... 2/6/89
;  . we have also expressed the correctness hypothesis in various
;   ways, to analyze idiom trade-offs for expressing that the 
;   "first 3 chars don't matter".
;

;;; CIRCUIT in SUGARED form:
#|
(setq sysd '(sy-BCD (x)
(Y0 R 'r0 x)
(Y1 R 'r1 Y0)
(Y2 S bor Y0 Y1)
(Yout S bnand x Y2)
))

(setq bcd '( |#
; BM DEFINITIONS and A2 LEMMAS, generated by BMSYSD:
; 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_bnand.bm: Binary Nand combinational element
; U7-DONE

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

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

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

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

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

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

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

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

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

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

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

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

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

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

; eof:comb_bnand.bm


\end{verbatim}\begin{tabbing}{\sc Definition}:\index{topor-sy-bcd} \\  
\=\+{\rm{topor-sy-bcd}}\,({\it{ln\/}})\index{topor-sy-bcd} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{ln\/}} $=$ {\tt{'}}{\tt{y0}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y1}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y2}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yout}}$\;\;${\bf then }{\tt{2}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{sy-bcd} \\  
\=\+{\rm{sy-bcd}}\,({\it{ln\/}}, {\it{x\/}})\index{sy-bcd} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{ln\/}} $=$ {\tt{'}}{\tt{y0}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{'}}{\tt{r0}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y1}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{'}}{\tt{r1}}, {\rm{sy-bcd}}\,({\tt{'}}{\tt{y0}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-bcd})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y2}}$\;\;${\bf then }{\rm{s-bor}}\,({\rm{sy-bcd}}\,({\tt{'}}{\tt{y0}}, {\it{x\/}})\index{sy-bcd}, {\rm{sy-bcd}}\,({\tt{'}}{\tt{y1}}, {\it{x\/}})\index{sy-bcd})\index{s-bor} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yout}}$\;\;${\bf then }{\rm{s-bnand}}\,({\it{x\/}}, {\rm{sy-bcd}}\,({\tt{'}}{\tt{y2}}, {\it{x\/}})\index{sy-bcd})\index{s-bnand} \\ 
{\bf else }{\rm{sfix}}\,({\it{x\/}})\index{sfix}$\;${\bf  endif}\-\-
\end{tabbing}

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

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

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

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

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

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

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

;;; 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}; BCD-Spec defines what the circuit is supposed to compute, by its
; last char.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{bcd-spec} \\  
{\rm{bcd-spec}}\,({\it{x\/}})\index{bcd-spec} $=$ {\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}
\end{tabbing}

\begin{verbatim}; CORRECTNESS:
; original correctness statement:
\end{verbatim}\begin{tabbing}{\sc Theorem}:  bcd-correct \\ \index{bcd-correct}
\=\+(\=\+($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{empty}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{empty}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{empty}}\,({\rm{p}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{p})\index{empty}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{empty}}\,({\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{p})\index{p})\index{empty}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{bibo}}\,({\rm{l}}\,({\rm{sy-bcd}}\,({\tt{'}}{\tt{yout}}, {\it{x\/}})\index{sy-bcd})\index{l})\index{bibo} $=$ {\rm{bcd-spec}}\,({\it{x\/}})\index{bcd-spec})\-
\end{tabbing}

\begin{verbatim}; alternative: implicitely using P(n+1) x /=e => P(n) x,..,Px,x /=e
;   ALSO works, with many more time and more CASES because BM 
;   explores all the "obviously impossible" cases and takes some 
;   time reducing the hyp to F.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  bcd-correct2 \\ \index{bcd-correct2}
($\neg$ {\rm{empty}}\,({\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{p})\index{p})\index{empty}) $\rightarrow$ ({\rm{bibo}}\,({\rm{l}}\,({\rm{sy-bcd}}\,({\tt{'}}{\tt{yout}}, {\it{x\/}})\index{sy-bcd})\index{l})\index{bibo} $=$ {\rm{bcd-spec}}\,({\it{x\/}})\index{bcd-spec})
\end{tabbing}

\begin{verbatim}; alternative: use the Pn operator instead of explicit P's in hyp:
;   ALSO works, with same number of CASES as explicit P's, but a 
;   little bit more time due to the expansions of Pn required.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  bcd-correct3 \\ \index{bcd-correct3}
($\neg$ {\rm{empty}}\,({\rm{pn}}\,({\tt{3}}, {\it{x\/}})\index{pn})\index{empty}) $\rightarrow$ ({\rm{bibo}}\,({\rm{l}}\,({\rm{sy-bcd}}\,({\tt{'}}{\tt{yout}}, {\it{x\/}})\index{sy-bcd})\index{l})\index{bibo} $=$ {\rm{bcd-spec}}\,({\it{x\/}})\index{bcd-spec})
\end{tabbing}

\begin{verbatim}; alternative: use LENgth > 3 instead of Pn or explicit P's.
;   ALSO works, with same number of CASES and time as Pn
\end{verbatim}\begin{tabbing}{\sc Theorem}:  bcd-correct4 \\ \index{bcd-correct4}
({\tt{3}} $<$ {\rm{len}}\,({\it{x\/}})\index{len}) $\rightarrow$ ({\rm{bibo}}\,({\rm{l}}\,({\rm{sy-bcd}}\,({\tt{'}}{\tt{yout}}, {\it{x\/}})\index{sy-bcd})\index{l})\index{bibo} $=$ {\rm{bcd-spec}}\,({\it{x\/}})\index{bcd-spec})
\end{tabbing}

\begin{verbatim};; one can give a CONTRIVED reading of Paillet's as pure streams:

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{bcd-bits-s} \\  
\=\+{\rm{bcd-bits-s}}\,({\it{b0\/}}, {\it{b1\/}}, {\it{b2\/}}, {\it{b3\/}})\index{bcd-bits-s} \\ 
$=$$\;\;\;\;${\rm{s-or}}\,(\=\+{\rm{s-equal}}\,({\it{b0\/}}, {\rm{s-const}}\,({\tt{0}}, {\it{b0\/}})\index{s-const})\index{s-equal}, \\ 
{\rm{s-and}}\,({\rm{s-equal}}\,({\it{b1\/}}, {\rm{s-const}}\,({\tt{0}}, {\it{b1\/}})\index{s-const})\index{s-equal}, {\rm{s-equal}}\,({\it{b2\/}}, {\rm{s-const}}\,({\tt{0}}, {\it{b2\/}})\index{s-const})\index{s-equal})\index{s-and})\-\index{s-or}\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{bcd-spec-s} \\  
{\rm{bcd-spec-s}}\,({\it{x\/}})\index{bcd-spec-s} $=$ {\rm{bcd-bits-s}}\,({\it{x\/}}, {\rm{p}}\,({\it{x\/}})\index{p}, {\rm{p}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{p}, {\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{p})\index{p})\index{bcd-bits-s}
\end{tabbing}

\begin{verbatim}; but do NOT have the equality Yout = BCD-Spec-S because of the 
; initial 3 values output by the circuit.  To get around that, we 
; could:
;    - redefine BCD-Spec-S to be a big IF statement on the length 
;      of x, and put in the explicit values computed by the 
;      circuit, obtained by evaluating SY-BCD in rloop.  
;      [ A major pain ]
;    - somehow express that we're not looking at the first 3 values
;      output. 
;      We could use (RST (RST (RST ... ) = (RST (RST (RST ... ) but
;      clearly that would not work, since we currently have nothing
;      about RST.
; Note that this is essentially the PIPELINE problem.  
; So far, the best approach seems to talk about L(sysd) which is
; most natural.
; NOTE: now that we've defined B (instead of RST) to deal with 
; pipelines, and entered its theory, the above discussioon is moot.


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