\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}; bcdS.bm: a BCD code checker, with serial (bit) input, but built 
;          STRUCTURELY.
;    The key lesson is that it helps (and is in fact necessary) to 
;    reduce the sysd to a generalized sysd, with just the 
;    "important" lines: Paillet's variables d'etats non-eliminables
;     expressed in terms of each other. See SY-B2 below.
;
;    Note: Proving the A2 lemmas about the generalized sysd brings 
;    2 issues:
;    - they don't seem to be used at all.
;    - A2-PC loops on its own (no rule!) and is therefore so far
;      unprovable...
;

;;; CIRCUIT in SUGARED form:

; note: registers are initialized with F instead of 0, since coded
; at logical level.
#|
(setq sysd '(sy-BCDS (x)
(Y01 S not x)
(Y02 S not x)
(Y03 S not YR3)
(Y04 S not YR1)
(Y05 S not YR2)
(Y06 S not YR3)
(Y07 S not YR1)
(Y08 S not YR3)
(Y11 S and3 Y01 YR1 YR3)
(Y12 S and3 Y02 YR2 Y03)
(Y13 S and3 Y04 Y05 Y06)
(Y14 S and3 x Y07 Y08)
(Y15 S and3 x YR1 YR3)
(Y21 S or Y11 Y12)
(Y22 S or Y13 Y14)
(Y23 S or YR2 Y15)
(YR1 R F Y21)
(YR2 R F Y22)
(YR3 R F Y23)
(Y31 S not YR1)
(Y32 S not YR2)
(Y41 S and4 x Y31 Y32 YR3)
(Yout S not Y41)
))

(setq bcdS '(  |#
; BM DEFINITIONS and A2 LEMMAS, generated by BMSYSD:
; comb_and3.bm: Logical And combinational element, with 3 inputs
; U7-DONE

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{and3}$\;\;$
{\rm{and3}}\,({\it{u1\/}}, {\it{u2\/}}, {\it{u3\/}})\index{and3} $=$ ({\it{u1\/}} $\wedge$ {\it{u2\/}} $\wedge$ {\it{u3\/}})
\end{tabbing}

\begin{verbatim}; Everything below generated by: (bmcomb 'and3 '() '(x1 x2 x3))

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

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

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

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

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

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

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

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

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

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

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

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

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

; eof:comb_and3.bm

; comb_and4.bm: Logical And combinational element, with 4 inputs
; U7-DONE

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{and4}$\;\;$
{\rm{and4}}\,({\it{u1\/}}, {\it{u2\/}}, {\it{u3\/}}, {\it{u4\/}})\index{and4} $=$ ({\it{u1\/}} $\wedge$ {\it{u2\/}} $\wedge$ {\it{u3\/}} $\wedge$ {\it{u4\/}})
\end{tabbing}

\begin{verbatim}; Everything below generated by: (bmcomb 'and4 '() '(x1 x2 x3 x4))

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{s-and4} \\  
\=\+{\rm{s-and4}}\,({\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}}, {\it{x4\/}})\index{s-and4} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{empty}}\,({\it{x1\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{a}}\,(\=\+{\rm{s-and4}}\,({\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-and4}, \\ 
{\rm{and4}}\,({\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{and4})\-\index{a}$\;${\bf  endif}\-\-
\end{tabbing}

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

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

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

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

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

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

\begin{tabbing}{\sc Theorem}:  a2-lc-s-and4 \\ \index{a2-lc-s-and4}
\=\+($\neg$ {\rm{empty}}\,({\it{x1\/}})\index{empty}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{l}}\,({\rm{s-and4}}\,({\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}}, {\it{x4\/}})\index{s-and4})\index{l} $=$ {\rm{and4}}\,({\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{and4})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-pc-s-and4 \\ \index{a2-pc-s-and4}
{\rm{p}}\,({\rm{s-and4}}\,({\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}}, {\it{x4\/}})\index{s-and4})\index{p} $=$ {\rm{s-and4}}\,({\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-and4}
\end{tabbing}

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

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

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

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

; eof:comb_and4.bm


\end{verbatim}\begin{tabbing}{\sc Definition}:\index{topor-sy-bcds} \\  
\=\+{\rm{topor-sy-bcds}}\,({\it{ln\/}})\index{topor-sy-bcds} \\ 
$=$$\;\;\;\;$\=\+{\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-bcds} \\  
\=\+{\rm{sy-bcds}}\,({\it{ln\/}}, {\it{x\/}})\index{sy-bcds} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{ln\/}} $=$ {\tt{'}}{\tt{y01}}$\;\;${\bf then }{\rm{s-not}}\,({\it{x\/}})\index{s-not} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y02}}$\;\;${\bf then }{\rm{s-not}}\,({\it{x\/}})\index{s-not} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y03}}$\;\;${\bf then }{\rm{s-not}}\,({\rm{sy-bcds}}\,({\tt{'}}{\tt{yr3}}, {\it{x\/}})\index{sy-bcds})\index{s-not} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y04}}$\;\;${\bf then }{\rm{s-not}}\,({\rm{sy-bcds}}\,({\tt{'}}{\tt{yr1}}, {\it{x\/}})\index{sy-bcds})\index{s-not} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y05}}$\;\;${\bf then }{\rm{s-not}}\,({\rm{sy-bcds}}\,({\tt{'}}{\tt{yr2}}, {\it{x\/}})\index{sy-bcds})\index{s-not} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y06}}$\;\;${\bf then }{\rm{s-not}}\,({\rm{sy-bcds}}\,({\tt{'}}{\tt{yr3}}, {\it{x\/}})\index{sy-bcds})\index{s-not} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y07}}$\;\;${\bf then }{\rm{s-not}}\,({\rm{sy-bcds}}\,({\tt{'}}{\tt{yr1}}, {\it{x\/}})\index{sy-bcds})\index{s-not} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y08}}$\;\;${\bf then }{\rm{s-not}}\,({\rm{sy-bcds}}\,({\tt{'}}{\tt{yr3}}, {\it{x\/}})\index{sy-bcds})\index{s-not} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y11}} \\ 
{\bf then }{\rm{s-and3}}\,({\rm{sy-bcds}}\,({\tt{'}}{\tt{y01}}, {\it{x\/}})\index{sy-bcds}, {\rm{sy-bcds}}\,({\tt{'}}{\tt{yr1}}, {\it{x\/}})\index{sy-bcds}, {\rm{sy-bcds}}\,({\tt{'}}{\tt{yr3}}, {\it{x\/}})\index{sy-bcds})\index{s-and3} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y12}} \\ 
{\bf then }{\rm{s-and3}}\,({\rm{sy-bcds}}\,({\tt{'}}{\tt{y02}}, {\it{x\/}})\index{sy-bcds}, {\rm{sy-bcds}}\,({\tt{'}}{\tt{yr2}}, {\it{x\/}})\index{sy-bcds}, {\rm{sy-bcds}}\,({\tt{'}}{\tt{y03}}, {\it{x\/}})\index{sy-bcds})\index{s-and3} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y13}} \\ 
{\bf then }{\rm{s-and3}}\,({\rm{sy-bcds}}\,({\tt{'}}{\tt{y04}}, {\it{x\/}})\index{sy-bcds}, {\rm{sy-bcds}}\,({\tt{'}}{\tt{y05}}, {\it{x\/}})\index{sy-bcds}, {\rm{sy-bcds}}\,({\tt{'}}{\tt{y06}}, {\it{x\/}})\index{sy-bcds})\index{s-and3} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y14}}$\;\;${\bf then }{\rm{s-and3}}\,({\it{x\/}}, {\rm{sy-bcds}}\,({\tt{'}}{\tt{y07}}, {\it{x\/}})\index{sy-bcds}, {\rm{sy-bcds}}\,({\tt{'}}{\tt{y08}}, {\it{x\/}})\index{sy-bcds})\index{s-and3} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y15}}$\;\;${\bf then }{\rm{s-and3}}\,({\it{x\/}}, {\rm{sy-bcds}}\,({\tt{'}}{\tt{yr1}}, {\it{x\/}})\index{sy-bcds}, {\rm{sy-bcds}}\,({\tt{'}}{\tt{yr3}}, {\it{x\/}})\index{sy-bcds})\index{s-and3} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y21}}$\;\;${\bf then }{\rm{s-or}}\,({\rm{sy-bcds}}\,({\tt{'}}{\tt{y11}}, {\it{x\/}})\index{sy-bcds}, {\rm{sy-bcds}}\,({\tt{'}}{\tt{y12}}, {\it{x\/}})\index{sy-bcds})\index{s-or} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y22}}$\;\;${\bf then }{\rm{s-or}}\,({\rm{sy-bcds}}\,({\tt{'}}{\tt{y13}}, {\it{x\/}})\index{sy-bcds}, {\rm{sy-bcds}}\,({\tt{'}}{\tt{y14}}, {\it{x\/}})\index{sy-bcds})\index{s-or} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y23}}$\;\;${\bf then }{\rm{s-or}}\,({\rm{sy-bcds}}\,({\tt{'}}{\tt{yr2}}, {\it{x\/}})\index{sy-bcds}, {\rm{sy-bcds}}\,({\tt{'}}{\tt{y15}}, {\it{x\/}})\index{sy-bcds})\index{s-or} \\ 
{\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}}\,({\bf{f}}, {\rm{sy-bcds}}\,({\tt{'}}{\tt{y21}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-bcds})\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}}\,({\bf{f}}, {\rm{sy-bcds}}\,({\tt{'}}{\tt{y22}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-bcds})\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}}\,({\bf{f}}, {\rm{sy-bcds}}\,({\tt{'}}{\tt{y23}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-bcds})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y31}}$\;\;${\bf then }{\rm{s-not}}\,({\rm{sy-bcds}}\,({\tt{'}}{\tt{yr1}}, {\it{x\/}})\index{sy-bcds})\index{s-not} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y32}}$\;\;${\bf then }{\rm{s-not}}\,({\rm{sy-bcds}}\,({\tt{'}}{\tt{yr2}}, {\it{x\/}})\index{sy-bcds})\index{s-not} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y41}} \\ 
{\bf then }{\rm{s-and4}}\,({\it{x\/}}, {\rm{sy-bcds}}\,({\tt{'}}{\tt{y31}}, {\it{x\/}})\index{sy-bcds}, {\rm{sy-bcds}}\,({\tt{'}}{\tt{y32}}, {\it{x\/}})\index{sy-bcds}, {\rm{sy-bcds}}\,({\tt{'}}{\tt{yr3}}, {\it{x\/}})\index{sy-bcds})\index{s-and4} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yout}}$\;\;${\bf then }{\rm{s-not}}\,({\rm{sy-bcds}}\,({\tt{'}}{\tt{y41}}, {\it{x\/}})\index{sy-bcds})\index{s-not} \\ 
{\bf else }{\rm{sfix}}\,({\it{x\/}})\index{sfix}$\;${\bf  endif}\-\-
\end{tabbing}

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

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

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

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

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

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

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

;;; Circuit CORRECTNESS /Paillet:

; BCD-Lbits defines a correct binary coded decimal, b0 is 
; most-significant. It assumes the bits are logical though (in
; contrast to bcd.bm).
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{bcd-lbits} \\  
{\rm{bcd-lbits}}\,({\it{b0\/}}, {\it{b1\/}}, {\it{b2\/}}, {\it{b3\/}})\index{bcd-lbits} $=$ (({\it{b0\/}} $=$ {\bf{f}}) $\vee$ (({\it{b1\/}} $=$ {\bf{f}}) $\wedge$ ({\it{b2\/}} $=$ {\bf{f}})))
\end{tabbing}

\begin{verbatim}; CORRECTNESS:

;;; WHAT PAILLET ACTUALLY PROVES: 
;;; redone-exactly, to show that we can do it too! And to teach us 
;;; how to do some nasty BM control: doing everything backwards!

;; FIRST he starts from the Register-equations, where of course he 
;; doesn't mention the initial values... In our case we have to 
;; PROVE them:
;; NOTES: 1: even though the expansion hints look gruesome, they 
;; are immediate to find out: expand everything once around the 
;; register-loop.
;;        2: we push the P's in, because otherwise clearly the eq's 
;; will loop, even though of course, they are still provable (done).
;;        3: doing all 3 equations at once is clearer than 1 by 1,
;; since the hint gets given only once, and one doesn't have to
;; disable all other proved equations while doing the next one in
;; order to prevent looping.
;;        4: if we give the most general expression: 
;; if empty x e ... then ; 
;; we get a self-looping rule since it applies to its rhs, which is 
;; still usable, as long as we USE it and DISABLE it simultaneously.
;; But that means we have to specify each use individually, and that
;; could be a pain.  
;;	  5: Fundamentally, this is an UNFOLDING rule, i.e. rhs is
;; more complex than lhs.  BM can't deal with that, except in the
;; context of a recursive DEFN, which is exactly the same thing,
;; and for which BM has hardwired smarts. Maybe that's the right 
;; way to handle UNFOLDING rewrites? Create a DEFN for them and
;; prove equality, and then use the DEFN:

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{sy-b2} \\  
\=\+{\rm{sy-b2}}\,({\it{ln\/}}, {\it{x\/}})\index{sy-b2} \\ 
$=$$\;\;\;\;$\=\+{\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}}\,(\=\+{\bf{f}}, \\ 
{\rm{s-or}}\,(\=\+{\rm{s-and3}}\,(\=\+{\rm{s-not}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{s-not}, \\ 
{\rm{sy-b2}}\,({\tt{'}}{\tt{yr1}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b2}, \\ 
{\rm{sy-b2}}\,({\tt{'}}{\tt{yr3}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b2})\-\index{s-and3}, \\ 
{\rm{s-and3}}\,(\=\+{\rm{s-not}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{s-not}, \\ 
{\rm{sy-b2}}\,({\tt{'}}{\tt{yr2}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b2}, \\ 
{\rm{s-not}}\,({\rm{sy-b2}}\,({\tt{'}}{\tt{yr3}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b2})\index{s-not})\-\index{s-and3})\-\index{s-or})\-\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}}\,(\=\+{\bf{f}}, \\ 
{\rm{s-or}}\,(\=\+{\rm{s-and3}}\,(\=\+{\rm{s-not}}\,({\rm{sy-b2}}\,({\tt{'}}{\tt{yr1}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b2})\index{s-not}, \\ 
{\rm{s-not}}\,({\rm{sy-b2}}\,({\tt{'}}{\tt{yr2}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b2})\index{s-not}, \\ 
{\rm{s-not}}\,({\rm{sy-b2}}\,({\tt{'}}{\tt{yr3}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b2})\index{s-not})\-\index{s-and3}, \\ 
{\rm{s-and3}}\,(\=\+{\rm{p}}\,({\it{x\/}})\index{p}, \\ 
{\rm{s-not}}\,({\rm{sy-b2}}\,({\tt{'}}{\tt{yr1}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b2})\index{s-not}, \\ 
{\rm{s-not}}\,({\rm{sy-b2}}\,({\tt{'}}{\tt{yr3}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b2})\index{s-not})\-\index{s-and3})\-\index{s-or})\-\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}}\,(\=\+{\bf{f}}, \\ 
{\rm{s-or}}\,(\=\+{\rm{sy-b2}}\,({\tt{'}}{\tt{yr2}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b2}, \\ 
{\rm{s-and3}}\,(\=\+{\rm{p}}\,({\it{x\/}})\index{p}, \\ 
{\rm{sy-b2}}\,({\tt{'}}{\tt{yr1}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b2}, \\ 
{\rm{sy-b2}}\,({\tt{'}}{\tt{yr3}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b2})\-\index{s-and3})\-\index{s-or})\-\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 (Sugar) generated by:
; (vp (bma2sysd-aux 'sy-B2 'sy-B2 '(x) '(and3 or and4 not)))
; with A2-PC disabled because last time we tried it looped, and we 
; don't need it.

;; A2-Begin-SY-B2

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

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

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

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

\begin{verbatim};(PROVE-LEMMA A2-PC-SY-B2 (REWRITE)
;    (EQUAL (P (SY-B2 LN X)) (SY-B2 LN (P X)))
;    ((DISABLE S-AND3 S-OR S-AND4 S-NOT A2-IC-S-AND3 A2-IC-S-OR
;              A2-IC-S-AND4 A2-IC-S-NOT)))

;; A2-End-SY-B2

; BCDS-is-B2 is the essence of this simplification.  
; Note that replacing the conjunction by:
; (implies (or (equal ln 'YR1) (equal ln 'YR2) (equal ln 'YR3))
;          (equal (sy-bcds ln x) (sy-B2 ln x)))
; makes it UNPROVABLE by BM, because the induction hyp needs to be 
; all 3 together, which BM won't do unless there is an explicit AND
; The thm is proved below in 2 immediates cases (on empty x).

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

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

\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}:  bcds-eq-yout \\ \index{bcds-eq-yout}
\=\+{\rm{sy-bcds}}\,({\tt{'}}{\tt{yout}}, {\it{x\/}})\index{sy-bcds} \\ 
$=$$\;\;\;\;${\rm{s-not}}\,({\rm{s-and4}}\,(\=\+{\it{x\/}}, \\ 
{\rm{s-not}}\,({\rm{sy-b2}}\,({\tt{'}}{\tt{yr1}}, {\it{x\/}})\index{sy-b2})\index{s-not}, \\ 
{\rm{s-not}}\,({\rm{sy-b2}}\,({\tt{'}}{\tt{yr2}}, {\it{x\/}})\index{sy-b2})\index{s-not}, \\ 
{\rm{sy-b2}}\,({\tt{'}}{\tt{yr3}}, {\it{x\/}})\index{sy-b2})\-\index{s-and4})\index{s-not}\-
\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 BCDS-IS-B2 we can carry everything over.  This
; follows Paillet.

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

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

\addvspace{18pt}


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

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

\addvspace{18pt}


\begin{tabbing}{\sc Theorem}:  bcds-paillet-2 \\ \index{bcds-paillet-2}
\=\+({\rm{len}}\,({\it{x\/}})\index{len} $=$ {\tt{2}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{l}}\,({\rm{sy-b2}}\,({\tt{'}}{\tt{yr1}}, {\it{x\/}})\index{sy-b2})\index{l} $=$ {\bf{f}}) \\ 
$\wedge$$\;\;\;\;$({\rm{l}}\,({\rm{sy-b2}}\,({\tt{'}}{\tt{yr2}}, {\it{x\/}})\index{sy-b2})\index{l} $=$ {\bf{t}}) \\ 
$\wedge$$\;\;\;\;$({\rm{l}}\,({\rm{sy-b2}}\,({\tt{'}}{\tt{yr3}}, {\it{x\/}})\index{sy-b2})\index{l} $=$ {\bf{f}}))\-\-
\end{tabbing}

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

\addvspace{18pt}

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

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

\addvspace{18pt}

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

\end{verbatim}\begin{tabbing}{\sc Theorem}:  bcds-paillet-3 \\ \index{bcds-paillet-3}
\=\+(({\rm{len}}\,({\it{x\/}})\index{len} $=$ {\tt{3}}) $\wedge$ {\rm{s-boolp}}\,({\it{x\/}})\index{s-boolp}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{l}}\,({\rm{sy-b2}}\,({\tt{'}}{\tt{yr1}}, {\it{x\/}})\index{sy-b2})\index{l} $=$ ($\neg$ {\rm{l}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{l})) \\ 
$\wedge$$\;\;\;\;$({\rm{l}}\,({\rm{sy-b2}}\,({\tt{'}}{\tt{yr2}}, {\it{x\/}})\index{sy-b2})\index{l} $=$ {\rm{l}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{l}) \\ 
$\wedge$$\;\;\;\;$({\rm{l}}\,({\rm{sy-b2}}\,({\tt{'}}{\tt{yr3}}, {\it{x\/}})\index{sy-b2})\index{l} $=$ {\bf{t}}))\-\-
\end{tabbing}

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

\addvspace{18pt}

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

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

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  bcds-paillet-4 \\ \index{bcds-paillet-4}
\=\+(({\rm{len}}\,({\it{x\/}})\index{len} $=$ {\tt{4}}) $\wedge$ {\rm{s-boolp}}\,({\it{x\/}})\index{s-boolp}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{l}}\,({\rm{sy-b2}}\,({\tt{'}}{\tt{yr1}}, {\it{x\/}})\index{sy-b2})\index{l} $=$ (($\neg$ {\rm{l}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{l}) $\wedge$ ($\neg$ {\rm{l}}\,({\rm{p}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{p})\index{l}))) \\ 
$\wedge$$\;\;\;\;$({\rm{l}}\,({\rm{sy-b2}}\,({\tt{'}}{\tt{yr2}}, {\it{x\/}})\index{sy-b2})\index{l} $=$ {\bf{f}}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{l}}\,({\rm{sy-b2}}\,({\tt{'}}{\tt{yr3}}, {\it{x\/}})\index{sy-b2})\index{l} \\ 
$=$$\;\;\;\;$({\rm{l}}\,({\rm{p}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{p})\index{l} $\vee$ ({\rm{l}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{l} $\wedge$ ($\neg$ {\rm{l}}\,({\rm{p}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{p})\index{l}))))\-)\-\-
\end{tabbing}

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

\addvspace{18pt}

\begin{verbatim}; and his conclusion:

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

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

\addvspace{18pt}

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

\end{verbatim}\begin{tabbing}{\sc Theorem}:  bcds-paillet-4out-correct \\ \index{bcds-paillet-4out-correct}
\=\+(({\rm{len}}\,({\it{x\/}})\index{len} $=$ {\tt{4}}) $\wedge$ {\rm{s-boolp}}\,({\it{x\/}})\index{s-boolp}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{l}}\,({\rm{sy-bcds}}\,({\tt{'}}{\tt{yout}}, {\it{x\/}})\index{sy-bcds})\index{l} \\ 
$=$$\;\;\;\;${\rm{bcd-lbits}}\,({\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-lbits})\-\-
\end{tabbing}

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

\addvspace{18pt}

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

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

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

\addvspace{18pt}

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


; The following lemma was thought to help, but in fact it just 
; slows things:
;
;(prove-lemma STR-remainder-len (rewrite)
;(implies (and (not (zerop p)) (not (empty x)))
;	 (equal (remainder (len x) p)
;		(if (equal (remainder (len (P x)) p) (sub1 p))
;		    0
;		    (add1 (remainder (len (P x)) p)))))
;((disable remainder) ; so we go directly to ARI-remainder-add1
; (enable LEN) ; explicit
; )
;)

\end{verbatim}\begin{tabbing}{\sc Theorem}:  bcds-paillet-r-correct \\ \index{bcds-paillet-r-correct}
\=\+(($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) $\wedge$ {\rm{s-boolp}}\,({\it{x\/}})\index{s-boolp}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+{\rm{l}}\,({\rm{sy-b2}}\,({\tt{'}}{\tt{yr1}}, {\it{x\/}})\index{sy-b2})\index{l} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\rm{len}}\,({\it{x\/}})\index{len} ${}${\bf{mod}}${}$ {\tt{4}}) $=$ {\tt{1}}$\;\;${\bf then }{\bf{f}} \\ 
{\bf elseif }({\rm{len}}\,({\it{x\/}})\index{len} ${}${\bf{mod}}${}$ {\tt{4}}) $=$ {\tt{2}}$\;\;${\bf then }{\bf{f}} \\ 
{\bf elseif }({\rm{len}}\,({\it{x\/}})\index{len} ${}${\bf{mod}}${}$ {\tt{4}}) $=$ {\tt{3}}$\;\;${\bf then }$\neg$ {\rm{l}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{l} \\ 
{\bf else }($\neg$ {\rm{l}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{l}) $\wedge$ ($\neg$ {\rm{l}}\,({\rm{p}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{p})\index{l})$\;${\bf  endif}\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{l}}\,({\rm{sy-b2}}\,({\tt{'}}{\tt{yr2}}, {\it{x\/}})\index{sy-b2})\index{l} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\rm{len}}\,({\it{x\/}})\index{len} ${}${\bf{mod}}${}$ {\tt{4}}) $=$ {\tt{1}}$\;\;${\bf then }{\bf{f}} \\ 
{\bf elseif }({\rm{len}}\,({\it{x\/}})\index{len} ${}${\bf{mod}}${}$ {\tt{4}}) $=$ {\tt{2}}$\;\;${\bf then }{\bf{t}} \\ 
{\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 }{\bf{f}}$\;${\bf  endif}\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{l}}\,({\rm{sy-b2}}\,({\tt{'}}{\tt{yr3}}, {\it{x\/}})\index{sy-b2})\index{l} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\rm{len}}\,({\it{x\/}})\index{len} ${}${\bf{mod}}${}$ {\tt{4}}) $=$ {\tt{1}}$\;\;${\bf then }{\bf{f}} \\ 
{\bf elseif }({\rm{len}}\,({\it{x\/}})\index{len} ${}${\bf{mod}}${}$ {\tt{4}}) $=$ {\tt{2}}$\;\;${\bf then }{\bf{f}} \\ 
{\bf elseif }({\rm{len}}\,({\it{x\/}})\index{len} ${}${\bf{mod}}${}$ {\tt{4}}) $=$ {\tt{3}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }\=\+{\rm{l}}\,({\rm{p}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{p})\index{l} \\ 
$\vee$$\;\;\;\;$({\rm{l}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{l} $\wedge$ ($\neg$ {\rm{l}}\,({\rm{p}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{p})\index{l}))\-$\;${\bf  endif}\-)\-)\-\-
\end{tabbing}

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

\end{verbatim}\begin{tabbing}{\sc Theorem}:  bcds-paillet-yout-correct \\ \index{bcds-paillet-yout-correct}
\=\+(($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) $\wedge$ {\rm{s-boolp}}\,({\it{x\/}})\index{s-boolp}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{l}}\,({\rm{sy-bcds}}\,({\tt{'}}{\tt{yout}}, {\it{x\/}})\index{sy-bcds})\index{l} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\rm{len}}\,({\it{x\/}})\index{len} ${}${\bf{mod}}${}$ {\tt{4}}) $=$ {\tt{0}} \\ 
{\bf then }{\rm{bcd-lbits}}\,({\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-lbits} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-)\-\-
\end{tabbing}
\begin{verbatim}; we also check the claim we make in the Ccube89 report, that we 
; need only one "build-up" lemma (R-correct). In works fine 
; (same # cases, time) with the (obvious) expand hint we used
; in BCDS-eq-Yout:
; (expand (SY-BCDS 'Yout x)
;	 (SY-BCDS 'Y41 x)
;	 (SY-BCDS 'Y31 x)
;	 (SY-BCDS 'Y32 x)
;	 )
; once again confirming that reifying rewrite lemmas which do not 
; involve induction does not really benefit Boyer-Moore, even 
; though it benefit humans!

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