\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}; serial.bm: a register, writable in parallel, and readable 
; serially.  This is Paillet example 3
;
; IMPORTANT NOTE: originally, we proved this multi-circuit WITHOUT 
; EQ-LEN hyps, because we got lucky and all the inputs were
; Registered, so it didn't matter.  We now go to the more general
; version for uniformity, even though it will be enormously more
; expensive, and will force EQ-LEN hyps in the correctness thms.  
; It might be worth remembering though that for circuits where all 
; inputs are immmediately Registered, we can do away with the 
; EQ-LEN hyp.
;
; OTHER IMPORTANT NOTE: all the comments below concerning various 
; ways of phrasing the hypotheses were written when EMPTY was still
; ENABLED.

;;; CIRCUIT in SUGARED form:  (after flattening out, yuck...)

#|
(setq sysd '(sy-SERIAL (xC x1 x2 x3)
(YC0 S const 0 xC)
(YM3 S mux xC x3 YC0)
(Y3 R 'a3 YM3)
(YM2 S mux xC x2 Y3)
(Y2 R 'a2 YM2)
(YM1 S mux xC x1 Y2)
(Y1 R 'a1 YM1)
))

(setq serial '( |#
; BM DEFINITIONS and A2 LEMMAS, generated by BMSYSD:
; comb_mux.bm: Mux combinational element, i.e. "if".
; U7-DONE

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

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

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

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

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


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

\addvspace{18pt}

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

;; A2-Begin-S-MUX

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

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

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

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

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

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

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

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

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

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

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

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

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

;; A2-End-S-MUX

; eof:comb_mux.bm


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

\begin{verbatim};Parameter found: 0 in: (YC0 S CONST 0 XC)
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{sy-serial} \\  
\=\+{\rm{sy-serial}}\,({\it{ln\/}}, {\it{xc\/}}, {\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{sy-serial} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{ln\/}} $=$ {\tt{'}}{\tt{yc0}}$\;\;${\bf then }{\rm{s-const}}\,({\tt{0}}, {\it{xc\/}})\index{s-const} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ym3}}$\;\;${\bf then }{\rm{s-mux}}\,({\it{xc\/}}, {\it{x3\/}}, {\rm{sy-serial}}\,({\tt{'}}{\tt{yc0}}, {\it{xc\/}}, {\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{sy-serial})\index{s-mux} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y3}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xc\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{'}}{\tt{a3}}, {\rm{sy-serial}}\,({\tt{'}}{\tt{ym3}}, {\rm{p}}\,({\it{xc\/}})\index{p}, {\rm{p}}\,({\it{x1\/}})\index{p}, {\rm{p}}\,({\it{x2\/}})\index{p}, {\rm{p}}\,({\it{x3\/}})\index{p})\index{sy-serial})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ym2}}$\;\;${\bf then }{\rm{s-mux}}\,({\it{xc\/}}, {\it{x2\/}}, {\rm{sy-serial}}\,({\tt{'}}{\tt{y3}}, {\it{xc\/}}, {\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{sy-serial})\index{s-mux} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y2}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xc\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{'}}{\tt{a2}}, {\rm{sy-serial}}\,({\tt{'}}{\tt{ym2}}, {\rm{p}}\,({\it{xc\/}})\index{p}, {\rm{p}}\,({\it{x1\/}})\index{p}, {\rm{p}}\,({\it{x2\/}})\index{p}, {\rm{p}}\,({\it{x3\/}})\index{p})\index{sy-serial})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ym1}}$\;\;${\bf then }{\rm{s-mux}}\,({\it{xc\/}}, {\it{x1\/}}, {\rm{sy-serial}}\,({\tt{'}}{\tt{y2}}, {\it{xc\/}}, {\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{sy-serial})\index{s-mux} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y1}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xc\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{'}}{\tt{a1}}, {\rm{sy-serial}}\,({\tt{'}}{\tt{ym1}}, {\rm{p}}\,({\it{xc\/}})\index{p}, {\rm{p}}\,({\it{x1\/}})\index{p}, {\rm{p}}\,({\it{x2\/}})\index{p}, {\rm{p}}\,({\it{x3\/}})\index{p})\index{sy-serial})\index{i}$\;${\bf  endif}\- \\ 
{\bf else }{\rm{sfix}}\,({\it{xc\/}})\index{sfix}$\;${\bf  endif}\-\-
\end{tabbing}

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

\end{verbatim}\begin{tabbing}{\sc Theorem}:  a2-empty-sy-serial \\ \index{a2-empty-sy-serial}
\=\+(({\rm{len}}\,({\it{xc\/}})\index{len} $=$ {\rm{len}}\,({\it{x1\/}})\index{len}) $\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{empty}}\,({\rm{sy-serial}}\,({\it{ln\/}}, {\it{xc\/}}, {\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{sy-serial})\index{empty} $=$ {\rm{empty}}\,({\it{xc\/}})\index{empty})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-e-sy-serial \\ \index{a2-e-sy-serial}
\=\+(({\rm{len}}\,({\it{xc\/}})\index{len} $=$ {\rm{len}}\,({\it{x1\/}})\index{len}) $\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{sy-serial}}\,({\it{ln\/}}, {\it{xc\/}}, {\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{sy-serial} $=$ {\sc{e}}\index{e}) $=$ {\rm{empty}}\,({\it{xc\/}})\index{empty})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-lp-sy-serial \\ \index{a2-lp-sy-serial}
\=\+(({\rm{len}}\,({\it{xc\/}})\index{len} $=$ {\rm{len}}\,({\it{x1\/}})\index{len}) $\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{len}}\,({\rm{sy-serial}}\,({\it{ln\/}}, {\it{xc\/}}, {\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{sy-serial})\index{len} $=$ {\rm{len}}\,({\it{xc\/}})\index{len})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-lpe-sy-serial \\ \index{a2-lpe-sy-serial}
\=\+(({\rm{len}}\,({\it{xc\/}})\index{len} $=$ {\rm{len}}\,({\it{x1\/}})\index{len}) $\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{eqlen}}\,({\rm{sy-serial}}\,({\it{ln\/}}, {\it{xc\/}}, {\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{sy-serial}, {\it{xc\/}})\index{eqlen}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-pc-sy-serial \\ \index{a2-pc-sy-serial}
\=\+(({\rm{len}}\,({\it{xc\/}})\index{len} $=$ {\rm{len}}\,({\it{x1\/}})\index{len}) $\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{p}}\,({\rm{sy-serial}}\,({\it{ln\/}}, {\it{xc\/}}, {\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{sy-serial})\index{p} \\ 
$=$$\;\;\;\;${\rm{sy-serial}}\,({\it{ln\/}}, {\rm{p}}\,({\it{xc\/}})\index{p}, {\rm{p}}\,({\it{x1\/}})\index{p}, {\rm{p}}\,({\it{x2\/}})\index{p}, {\rm{p}}\,({\it{x3\/}})\index{p})\index{sy-serial})\-\-
\end{tabbing}

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

;;; Circuit CORRECTNESS /Paillet:

; SPECIFICATION:

; Here we interpret Paillet as talking about last-chars implicitely

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{serial-spec-l} \\  
\=\+{\rm{serial-spec-l}}\,({\it{xc\/}}, {\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{serial-spec-l} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{l}}\,({\rm{p}}\,({\it{xc\/}})\index{p})\index{l}$\;\;${\bf then }{\rm{l}}\,({\rm{p}}\,({\it{x1\/}})\index{p})\index{l} \\ 
{\bf elseif }{\rm{l}}\,({\rm{p}}\,({\rm{p}}\,({\it{xc\/}})\index{p})\index{p})\index{l}$\;\;${\bf then }{\rm{l}}\,({\rm{p}}\,({\rm{p}}\,({\it{x2\/}})\index{p})\index{p})\index{l} \\ 
{\bf elseif }{\rm{l}}\,({\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xc\/}})\index{p})\index{p})\index{p})\index{l}$\;\;${\bf then }{\rm{l}}\,({\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{x3\/}})\index{p})\index{p})\index{p})\index{l} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}


\begin{verbatim}; Here we intepret Paillet as really talking about streams (and 
; correct for the missing initial values):

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{serial-spec} \\  
\=\+{\rm{serial-spec}}\,({\it{xc\/}}, {\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{serial-spec} \\ 
$=$$\;\;\;\;${\rm{i}}\,(\=\+{\tt{'}}{\tt{a1}}, \\ 
{\rm{s-if}}\,(\=\+{\rm{p}}\,({\it{xc\/}})\index{p}, \\ 
{\rm{p}}\,({\it{x1\/}})\index{p}, \\ 
{\rm{i}}\,(\=\+{\tt{'}}{\tt{a2}}, \\ 
{\rm{s-if}}\,(\=\+{\rm{p}}\,({\rm{p}}\,({\it{xc\/}})\index{p})\index{p}, \\ 
{\rm{p}}\,({\rm{p}}\,({\it{x2\/}})\index{p})\index{p}, \\ 
{\rm{i}}\,(\=\+{\tt{'}}{\tt{a3}}, \\ 
{\rm{s-if}}\,({\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xc\/}})\index{p})\index{p})\index{p}, {\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{x3\/}})\index{p})\index{p})\index{p}, {\rm{s-const}}\,({\tt{0}}, {\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xc\/}})\index{p})\index{p})\index{p})\index{s-const})\index{s-if})\-\index{i})\-\index{s-if})\-\index{i})\-\index{s-if})\-\index{i}\-
\end{tabbing}


\begin{verbatim}; CORRECTNESS:

; note: we don't need EQ-LEN hyp here, although it was tried and 
; didn't hurt.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  serial-correct-l \\ \index{serial-correct-l}
\=\+(\=\+($\neg$ {\rm{empty}}\,({\it{xc\/}})\index{empty}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{empty}}\,({\rm{p}}\,({\it{xc\/}})\index{p})\index{empty}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{empty}}\,({\rm{p}}\,({\rm{p}}\,({\it{xc\/}})\index{p})\index{p})\index{empty}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{empty}}\,({\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xc\/}})\index{p})\index{p})\index{p})\index{empty}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{l}}\,({\rm{sy-serial}}\,({\tt{'}}{\tt{y1}}, {\it{xc\/}}, {\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{sy-serial})\index{l} $=$ {\rm{serial-spec-l}}\,({\it{xc\/}}, {\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{serial-spec-l})\-
\end{tabbing}

\begin{verbatim}; Note: we shouldn't need the EQ-LEN hyp here, since it's just an unfolding..

\end{verbatim}\begin{tabbing}{\sc Theorem}:  serial-correct \\ \index{serial-correct}
\=\+($\neg$ {\rm{empty}}\,({\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xc\/}})\index{p})\index{p})\index{p})\index{empty}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{sy-serial}}\,({\tt{'}}{\tt{y1}}, {\it{xc\/}}, {\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{sy-serial} $=$ {\rm{serial-spec}}\,({\it{xc\/}}, {\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{serial-spec})\-
\end{tabbing}

\begin{verbatim}; NOTE that above we have a choice of how we phrase the hypothesis:
;   1: (and (not (empty xC)) (not (empty (p xC))) 
;           (not (empty (p (p xC)))) (not (empty (p (p (p xC))))))
;     is highly redundant but says everything needed and so solves 
;     in 1 step.
;   2: (not (empty (p (p (p xC)))))  concise, -> many cases (but 
;     LESS time!)
;   3: (not (empty (Pn 3 xC))) concise, -> same # cases as 2, but 
;     more time.
; Rewrite lemmas such as:
;(prove-lemma not-empty-Pn (rewrite)
;(equal (not (empty (Pn n x)))
;       (if (zerop n)
;	   (not (empty x))
;	   (and (not (empty x))
;		(not (empty (Pn (sub1 n) (P x)))))))
;)
; although true, have no effect on the hypothesis expansion, 
; unfortunately..


; Another property listed as "correctess" in Paillet is:
; Note that here we have translated P .. into L P .., because
; if we try to understand this last Paillet property as speaking of
; streams, then the Hypothesis: P3 C = 1 and P2 C = P C = 0
; doesn't make any sense!!!
; in fact he acknowledges that "these computations are supposed to 
; be made in a temporal interval corresponding to one cycle, but 
; this interval is not indicated in the calculus to avoid too much
; notation".  Formally of course, we don't have that luxury... 

; Again, we don't need the EQ-LEN hyp, although when we tested it, 
; it threw BM into a loop, until we DISABLED LEN; this trick might
; carry over!!

\end{verbatim}\begin{tabbing}{\sc Theorem}:  serial-correct-specialcase-l \\ \index{serial-correct-specialcase-l}
\=\+(\=\+({\rm{l}}\,({\rm{p}}\,({\it{xc\/}})\index{p})\index{l} $=$ {\bf{f}}) \\ 
$\wedge$$\;\;\;\;$({\rm{l}}\,({\rm{p}}\,({\rm{p}}\,({\it{xc\/}})\index{p})\index{p})\index{l} $=$ {\bf{f}}) \\ 
$\wedge$$\;\;\;\;$({\rm{l}}\,({\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xc\/}})\index{p})\index{p})\index{p})\index{l} $=$ {\bf{t}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{empty}}\,({\it{xc\/}})\index{empty}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{empty}}\,({\rm{p}}\,({\it{xc\/}})\index{p})\index{empty}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{empty}}\,({\rm{p}}\,({\rm{p}}\,({\it{xc\/}})\index{p})\index{p})\index{empty}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{empty}}\,({\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xc\/}})\index{p})\index{p})\index{p})\index{empty}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{l}}\,({\rm{sy-serial}}\,({\tt{'}}{\tt{y1}}, {\it{xc\/}}, {\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{sy-serial})\index{l} $=$ {\rm{l}}\,({\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{x3\/}})\index{p})\index{p})\index{p})\index{l}) \\ 
$\wedge$$\;\;\;\;$({\rm{l}}\,({\rm{p}}\,({\rm{sy-serial}}\,({\tt{'}}{\tt{y1}}, {\it{xc\/}}, {\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{sy-serial})\index{p})\index{l} $=$ {\rm{l}}\,({\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{x2\/}})\index{p})\index{p})\index{p})\index{l}) \\ 
$\wedge$$\;\;\;\;$({\rm{l}}\,({\rm{p}}\,({\rm{p}}\,({\rm{sy-serial}}\,({\tt{'}}{\tt{y1}}, {\it{xc\/}}, {\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{sy-serial})\index{p})\index{p})\index{l} $=$ {\rm{l}}\,({\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{x1\/}})\index{p})\index{p})\index{p})\index{l}))\-\-
\end{tabbing}

\begin{verbatim}; Note above that using the (redundant) hypothesis:
; (not (empty xC)) (not (empty (p xC))) (not (empty (p (p xC)))) 
; (not (empty (p (p (p xC)))))
; makes the proof instantaneous, since otherwise BM goes through 
; eliminations to realize the "equal" hyps imply it.

; eof: serial.bm
;))


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