\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}; sadder.bm: a serial adder (adds the last 2 values of the input)
; This is Paillet example 4, which has a totally fuzzy, and almost
; meaningless SPECIFICATION (verification condition).  Instead, we
; provide our OWN specs, in many different tastes:
; - in terms of stringfuns: correct-1-S
; - in terms of Lastchars (more intuitive):
; - with a "Done" line
; - or predicting "good" times (len x = 0 modulo 2)
;

;;; CIRCUIT in SUGARED form: 
#|
(setq sysd '(sy-SADDER (x)
(Y1 R 'a0 x) ; arbitrary initial value
(Y2 S plus Y1 x)
(Ydone R 1 Y4) ; specific initial value
(Y4 S bnot Ydone)
(Yout S bmux Ydone x Y2)
))

(setq sadder '(  |#
; BM DEFINITIONS and A2 LEMMAS, generated by BMSYSD:
; comb_plus.bm: Plus combinational element.
; U7-DONE

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

; eof:comb_plus.bm

; 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

; comb_mux.bm: Mux combinational element, i.e. "if", but with 
; U7-DONE
;      control input binary-encoded (i.e. 0=F or 1=T) hardwired, no ref to bobi

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

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


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

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

\end{verbatim}\begin{tabbing}{\sc Theorem}:  sbmux-is-sif \\ \index{sbmux-is-sif}
{\rm{s-bmux}}\,({\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}})\index{s-bmux} $=$ {\rm{s-if}}\,({\rm{s-equal}}\,({\it{x1\/}}, {\rm{s-const}}\,({\tt{1}}, {\it{x1\/}})\index{s-const})\index{s-equal}, {\it{x2\/}}, {\it{x3\/}})\index{s-if}
\end{tabbing}


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

\addvspace{18pt}

\begin{verbatim}; We take advantage of SBMUX-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 sbmux-is-sif)) 
;   - A2-LP, A2-IC, A2-HC, A2-BC: ((enable sbmux-is-sif) (disable len))
;   - A2-BNC: ((enable sbmux-is-sif) (disable bn len))

;; A2-Begin-S-BMUX

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

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

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

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

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

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

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

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

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

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

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

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

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

;; A2-End-S-BMUX

; eof:comb_bmux.bm


\end{verbatim}\begin{tabbing}{\sc Definition}:\index{topor-sy-sadder} \\  
\=\+{\rm{topor-sy-sadder}}\,({\it{ln\/}})\index{topor-sy-sadder} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\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{ydone}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y4}}$\;\;${\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-sadder} \\  
\=\+{\rm{sy-sadder}}\,({\it{ln\/}}, {\it{x\/}})\index{sy-sadder} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\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{a0}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y2}}$\;\;${\bf then }{\rm{s-plus}}\,({\rm{sy-sadder}}\,({\tt{'}}{\tt{y1}}, {\it{x\/}})\index{sy-sadder}, {\it{x\/}})\index{s-plus} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ydone}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{1}}, {\rm{sy-sadder}}\,({\tt{'}}{\tt{y4}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-sadder})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y4}}$\;\;${\bf then }{\rm{s-bnot}}\,({\rm{sy-sadder}}\,({\tt{'}}{\tt{ydone}}, {\it{x\/}})\index{sy-sadder})\index{s-bnot} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yout}} \\ 
{\bf then }{\rm{s-bmux}}\,({\rm{sy-sadder}}\,({\tt{'}}{\tt{ydone}}, {\it{x\/}})\index{sy-sadder}, {\it{x\/}}, {\rm{sy-sadder}}\,({\tt{'}}{\tt{y2}}, {\it{x\/}})\index{sy-sadder})\index{s-bmux} \\ 
{\bf else }{\rm{sfix}}\,({\it{x\/}})\index{sfix}$\;${\bf  endif}\-\-
\end{tabbing}

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

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

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

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

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

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

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

;;; Circuit CORRECTNESS /Paillet:

;; we can do the actual Deroulement, which is a very WEAK spec 
;; indeed..

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

\begin{verbatim};; or we can prove the natural spec:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  sadder-correct-1 \\ \index{sadder-correct-1}
\=\+($\neg$ {\rm{empty}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{empty}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{l}}\,({\rm{sy-sadder}}\,({\tt{'}}{\tt{yout}}, {\it{x\/}})\index{sy-sadder})\index{l} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{l}}\,({\rm{sy-sadder}}\,({\tt{'}}{\tt{ydone}}, {\it{x\/}})\index{sy-sadder})\index{l} $=$ {\tt{1}}$\;\;${\bf then }{\rm{l}}\,({\it{x\/}})\index{l} \\ 
{\bf else }{\rm{l}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{l} $+$ {\rm{l}}\,({\it{x\/}})\index{l}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sadder-but-wiser \\ \index{sadder-but-wiser}
{\tt{'}}{\tt{horning-said-that}}
\end{tabbing}

\begin{verbatim};; There are 2 lessons from the above lemma:
;; 1) if you're reading this in the thesis, congratulations 
;;    for reading so far.
;; 2) if someone claims he proved some formula mechanically,
;;    make sure the formula means something...


;; we could look at it in terms of STRING-FUNS:

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{sadder-spec-s} \\  
\=\+{\rm{sadder-spec-s}}\,({\it{x\/}})\index{sadder-spec-s} \\ 
$=$$\;\;\;\;${\rm{s-if}}\,(\=\+{\rm{s-equal}}\,({\rm{sy-sadder}}\,({\tt{'}}{\tt{ydone}}, {\it{x\/}})\index{sy-sadder}, {\rm{s-const}}\,({\tt{1}}, {\rm{sy-sadder}}\,({\tt{'}}{\tt{ydone}}, {\it{x\/}})\index{sy-sadder})\index{s-const})\index{s-equal}, \\ 
{\it{x\/}}, \\ 
{\rm{s-plus}}\,({\rm{p}}\,({\it{x\/}})\index{p}, {\it{x\/}})\index{s-plus})\-\index{s-if}\-
\end{tabbing}

\begin{verbatim}; one "trick" which makes this weird (non-MLP looking) spec work:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  s-plus-one-off \\ \index{s-plus-one-off}
($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) $\rightarrow$ ({\rm{s-plus}}\,({\rm{i}}\,({\it{u\/}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{i}, {\it{x\/}})\index{s-plus} $=$ {\rm{i}}\,({\it{u\/}} $+$ {\rm{h}}\,({\it{x\/}})\index{h}, {\rm{s-plus}}\,({\rm{p}}\,({\it{x\/}})\index{p}, {\it{x\/}})\index{s-plus})\index{i})
\end{tabbing}

\begin{verbatim}; and the second "trick" is that the off-by-one sum, and the 
; toggling contribute to working things out:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  sadder-correct-1-s-key \\ \index{sadder-correct-1-s-key}
\=\+{\rm{s-if}}\,(\=\+{\rm{s-equal}}\,({\rm{sy-sadder}}\,({\tt{'}}{\tt{ydone}}, {\it{x\/}})\index{sy-sadder}, {\rm{s-const}}\,({\tt{1}}, {\rm{sy-sadder}}\,({\tt{'}}{\tt{ydone}}, {\it{x\/}})\index{sy-sadder})\index{s-const})\index{s-equal}, \\ 
{\it{x\/}}, \\ 
{\rm{i}}\,({\it{u\/}}, {\rm{s-plus}}\,({\rm{p}}\,({\it{x\/}})\index{p}, {\it{x\/}})\index{s-plus})\index{i})\-\index{s-if} \\ 
$=$$\;\;\;\;${\rm{s-if}}\,(\=\+{\rm{s-equal}}\,({\rm{sy-sadder}}\,({\tt{'}}{\tt{ydone}}, {\it{x\/}})\index{sy-sadder}, {\rm{s-const}}\,({\tt{1}}, {\rm{sy-sadder}}\,({\tt{'}}{\tt{ydone}}, {\it{x\/}})\index{sy-sadder})\index{s-const})\index{s-equal}, \\ 
{\it{x\/}}, \\ 
{\rm{s-plus}}\,({\rm{p}}\,({\it{x\/}})\index{p}, {\it{x\/}})\index{s-plus})\-\index{s-if}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sadder-correct-1-s \\ \index{sadder-correct-1-s}
{\rm{sy-sadder}}\,({\tt{'}}{\tt{yout}}, {\it{x\/}})\index{sy-sadder} $=$ {\rm{sadder-spec-s}}\,({\it{x\/}})\index{sadder-spec-s}
\end{tabbing}

\begin{verbatim};; Going back to looking in terms of Last-chars, we would most 
;; likely only specify (more partially):

\end{verbatim}\begin{tabbing}{\sc Theorem}:  sadder-correct-2 \\ \index{sadder-correct-2}
\=\+(($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) $\wedge$ ($\neg$ {\rm{empty}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{empty}) $\wedge$ ({\rm{l}}\,({\rm{sy-sadder}}\,({\tt{'}}{\tt{ydone}}, {\it{x\/}})\index{sy-sadder})\index{l} $=$ {\tt{0}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{l}}\,({\rm{sy-sadder}}\,({\tt{'}}{\tt{yout}}, {\it{x\/}})\index{sy-sadder})\index{l} $=$ ({\rm{l}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{l} $+$ {\rm{l}}\,({\it{x\/}})\index{l}))\-
\end{tabbing}

\begin{verbatim}; Note: sadder-correct-2 is proved immediately from correct-1 or 
; correct-1-S, or can be obtained from scratch with the same hints 
; as correct-1. 
; The fact that such a partial spec is BM-provable probably depends
; on the fact that it requires NO induction.  In cases with 
; induction, too weak a spec would probably not go through.  In
; other words, we might have to specify a second property which 
; also specifies what happens in the "previous" or "uninteresting" 
; (Done not raised) cases.

; Another way to look at the spec is to PREDICT the timing of the 
; output, as opposed to just looking at the Done (Ydone) line.
; This of course will not always be possible. The key to the
; prediction is:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  sadder-correct-3-ydone \\ \index{sadder-correct-3-ydone}
\=\+($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{l}}\,({\rm{sy-sadder}}\,({\tt{'}}{\tt{ydone}}, {\it{x\/}})\index{sy-sadder})\index{l} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\rm{len}}\,({\it{x\/}})\index{len} ${}${\bf{mod}}${}$ {\tt{2}}) $=$ {\tt{0}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\tt{1}}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{verbatim}; or with a bit more work we can prove the 2-tick rhythm:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  sadder-correct-3 \\ \index{sadder-correct-3}
\=\+(($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) $\wedge$ (({\rm{len}}\,({\it{x\/}})\index{len} ${}${\bf{mod}}${}$ {\tt{2}}) $=$ {\tt{0}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{l}}\,({\rm{sy-sadder}}\,({\tt{'}}{\tt{yout}}, {\it{x\/}})\index{sy-sadder})\index{l} $=$ ({\rm{l}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{l} $+$ {\rm{l}}\,({\it{x\/}})\index{l}))\-
\end{tabbing}

\begin{verbatim}; Note: removing the hyp: (not (empty (P x))) is not harmful,
; but it just forces BM into a couple of cases and 1 elimination 
; before it gets to the real meat.

; eof: sadder.bm
;))

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