\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}; corrSL.bm is the FULL version of the Saxe/Leiserson retimed
; correlator.
; PROOF HISTORY:
; - very interestingly, a bug in the first definition I entered was 
; shown by BM reducing a case to: 
;          (IMPLIES (AND (STRINGP X)
;                        (NOT (EQUAL X (E)))
;                        (EQUAL (P X) (E))
;                        (NOT (EQUAL 'A2 (L X))))
;                   (EQUAL 4 (PLUS 1 1 0 1))).
; which is obviously false, and describes precisely the 
; counterexample!
; - a first correctness proof (brute expansion) was obtained in 
; LESS THAN 1 HOUR, and that includes finding out the definition
; was wrong!

;;; (Sugared) Circuits:
#|
(setq A '(SY-A (x)
(Y1 R 'a0 x)
(Y2 S Del 'a0 Y1)
(Y3 R 'a1 Y1)
(Y4 S Del 'a1 Y3)
(Y5 R 'a2 Y3)
(Y6 S Del 'a2 Y5)
(Y7 R 'a3 Y5)
(Y8 S Del 'a3 Y7)
(Y9 S Plus Y6 Y8)
(Y10 S Plus Y4 Y9)
(Yout S Plus Y2 Y10)
))

(setq B '(SY-B (x)
(Z1 R 'a0 x)
(Z2 S Del 'a0 Z1)
(Z3 R 'a1 Z1)
(Z4 S Del 'a1 Z3)
(Z5 S Del 'a2 Z3)
(Z6 R 'a2 Z3)
(Z7 S Del 'a3 Z6)
(Z8 S Plus Z5 Z7)
(Z9 R 2 Z8)
(Z10 S Plus Z4 Z9)
(Zout S Plus Z2 Z10)
))

(setq corrSL '(  |#
; BM DEFINITIONS and A2 LEMMAS, generated by BMSYSD:
; comb_del.bm: Delta combinational element, parametrized.
; U7-DONE

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{del} \\  
\=\+{\rm{del}}\,({\it{val\/}}, {\it{u\/}})\index{del} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{val\/}} $=$ {\it{u\/}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; Everything below generated by SUGAR with:    (bmcomb 'del '(val) '(x))

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

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

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

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

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

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

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

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

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

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

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

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

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

; eof:comb_del.bm


; 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


\end{verbatim}\begin{tabbing}{\sc Definition}:\index{topor-sy-a} \\  
\=\+{\rm{topor-sy-a}}\,({\it{ln\/}})\index{topor-sy-a} \\ 
$=$$\;\;\;\;$\=\+{\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{y3}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y4}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y5}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y6}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y7}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y8}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y9}}$\;\;${\bf then }{\tt{2}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y10}}$\;\;${\bf then }{\tt{3}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yout}}$\;\;${\bf then }{\tt{4}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};Parameter found: 'A0 in: (Y2 S DEL 'A0 Y1)
;Parameter found: 'A1 in: (Y4 S DEL 'A1 Y3)
;Parameter found: 'A2 in: (Y6 S DEL 'A2 Y5)
;Parameter found: 'A3 in: (Y8 S DEL 'A3 Y7)
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{sy-a} \\  
\=\+{\rm{sy-a}}\,({\it{ln\/}}, {\it{x\/}})\index{sy-a} \\ 
$=$$\;\;\;\;$\=\+{\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-del}}\,({\tt{'}}{\tt{a0}}, {\rm{sy-a}}\,({\tt{'}}{\tt{y1}}, {\it{x\/}})\index{sy-a})\index{s-del} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y3}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{'}}{\tt{a1}}, {\rm{sy-a}}\,({\tt{'}}{\tt{y1}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-a})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y4}}$\;\;${\bf then }{\rm{s-del}}\,({\tt{'}}{\tt{a1}}, {\rm{sy-a}}\,({\tt{'}}{\tt{y3}}, {\it{x\/}})\index{sy-a})\index{s-del} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y5}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{'}}{\tt{a2}}, {\rm{sy-a}}\,({\tt{'}}{\tt{y3}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-a})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y6}}$\;\;${\bf then }{\rm{s-del}}\,({\tt{'}}{\tt{a2}}, {\rm{sy-a}}\,({\tt{'}}{\tt{y5}}, {\it{x\/}})\index{sy-a})\index{s-del} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y7}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{'}}{\tt{a3}}, {\rm{sy-a}}\,({\tt{'}}{\tt{y5}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-a})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y8}}$\;\;${\bf then }{\rm{s-del}}\,({\tt{'}}{\tt{a3}}, {\rm{sy-a}}\,({\tt{'}}{\tt{y7}}, {\it{x\/}})\index{sy-a})\index{s-del} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y9}}$\;\;${\bf then }{\rm{s-plus}}\,({\rm{sy-a}}\,({\tt{'}}{\tt{y6}}, {\it{x\/}})\index{sy-a}, {\rm{sy-a}}\,({\tt{'}}{\tt{y8}}, {\it{x\/}})\index{sy-a})\index{s-plus} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y10}}$\;\;${\bf then }{\rm{s-plus}}\,({\rm{sy-a}}\,({\tt{'}}{\tt{y4}}, {\it{x\/}})\index{sy-a}, {\rm{sy-a}}\,({\tt{'}}{\tt{y9}}, {\it{x\/}})\index{sy-a})\index{s-plus} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yout}}$\;\;${\bf then }{\rm{s-plus}}\,({\rm{sy-a}}\,({\tt{'}}{\tt{y2}}, {\it{x\/}})\index{sy-a}, {\rm{sy-a}}\,({\tt{'}}{\tt{y10}}, {\it{x\/}})\index{sy-a})\index{s-plus} \\ 
{\bf else }{\rm{sfix}}\,({\it{x\/}})\index{sfix}$\;${\bf  endif}\-\-
\end{tabbing}

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

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

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

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

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

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

\begin{verbatim};; A2-End-SY-A
; BM DEFINITIONS and A2 LEMMAS, generated by BMSYSD:

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{topor-sy-b} \\  
\=\+{\rm{topor-sy-b}}\,({\it{ln\/}})\index{topor-sy-b} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{ln\/}} $=$ {\tt{'}}{\tt{z1}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z2}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z3}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z4}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z5}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z6}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z7}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z8}}$\;\;${\bf then }{\tt{2}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z9}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z10}}$\;\;${\bf then }{\tt{2}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{zout}}$\;\;${\bf then }{\tt{3}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};Parameter found: 'A0 in: (Z2 S DEL 'A0 Z1)
;Parameter found: 'A1 in: (Z4 S DEL 'A1 Z3)
;Parameter found: 'A2 in: (Z5 S DEL 'A2 Z3)
;Parameter found: 'A3 in: (Z7 S DEL 'A3 Z6)
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{sy-b} \\  
\=\+{\rm{sy-b}}\,({\it{ln\/}}, {\it{x\/}})\index{sy-b} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{ln\/}} $=$ {\tt{'}}{\tt{z1}} \\ 
{\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{z2}}$\;\;${\bf then }{\rm{s-del}}\,({\tt{'}}{\tt{a0}}, {\rm{sy-b}}\,({\tt{'}}{\tt{z1}}, {\it{x\/}})\index{sy-b})\index{s-del} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z3}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{'}}{\tt{a1}}, {\rm{sy-b}}\,({\tt{'}}{\tt{z1}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z4}}$\;\;${\bf then }{\rm{s-del}}\,({\tt{'}}{\tt{a1}}, {\rm{sy-b}}\,({\tt{'}}{\tt{z3}}, {\it{x\/}})\index{sy-b})\index{s-del} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z5}}$\;\;${\bf then }{\rm{s-del}}\,({\tt{'}}{\tt{a2}}, {\rm{sy-b}}\,({\tt{'}}{\tt{z3}}, {\it{x\/}})\index{sy-b})\index{s-del} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z6}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{'}}{\tt{a2}}, {\rm{sy-b}}\,({\tt{'}}{\tt{z3}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z7}}$\;\;${\bf then }{\rm{s-del}}\,({\tt{'}}{\tt{a3}}, {\rm{sy-b}}\,({\tt{'}}{\tt{z6}}, {\it{x\/}})\index{sy-b})\index{s-del} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z8}}$\;\;${\bf then }{\rm{s-plus}}\,({\rm{sy-b}}\,({\tt{'}}{\tt{z5}}, {\it{x\/}})\index{sy-b}, {\rm{sy-b}}\,({\tt{'}}{\tt{z7}}, {\it{x\/}})\index{sy-b})\index{s-plus} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z9}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{2}}, {\rm{sy-b}}\,({\tt{'}}{\tt{z8}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z10}}$\;\;${\bf then }{\rm{s-plus}}\,({\rm{sy-b}}\,({\tt{'}}{\tt{z4}}, {\it{x\/}})\index{sy-b}, {\rm{sy-b}}\,({\tt{'}}{\tt{z9}}, {\it{x\/}})\index{sy-b})\index{s-plus} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{zout}}$\;\;${\bf then }{\rm{s-plus}}\,({\rm{sy-b}}\,({\tt{'}}{\tt{z2}}, {\it{x\/}})\index{sy-b}, {\rm{sy-b}}\,({\tt{'}}{\tt{z10}}, {\it{x\/}})\index{sy-b})\index{s-plus} \\ 
{\bf else }{\rm{sfix}}\,({\it{x\/}})\index{sfix}$\;${\bf  endif}\-\-
\end{tabbing}

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

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

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

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

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

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

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

;;; CORRECTNESS PROOF (hand generated, dreamer!):

; The following works, but is rather inelegant, and painful to 
; scale.
; Note that STR-add1-len-P2 saves an elimination,and hence cuts the
; proof complexity, and run time in 3.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  eq-a-b \\ \index{eq-a-b}
{\rm{stringp}}\,({\it{x\/}})\index{stringp} $\rightarrow$ ({\rm{sy-b}}\,({\tt{'}}{\tt{zout}}, {\it{x\/}})\index{sy-b} $=$ {\rm{sy-a}}\,({\tt{'}}{\tt{yout}}, {\it{x\/}})\index{sy-a})
\end{tabbing}


\begin{verbatim}; The next attempt uses SMARTS instead of strength:
; FIRST we build the equalities which are in some sense 
; syntactically guaranteed to be true, since they relate to the
; "unchanged" part of the circuit:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  eq-z1-y1 \\ \index{eq-z1-y1}
{\rm{stringp}}\,({\it{x\/}})\index{stringp} $\rightarrow$ ({\rm{sy-b}}\,({\tt{'}}{\tt{z1}}, {\it{x\/}})\index{sy-b} $=$ {\rm{sy-a}}\,({\tt{'}}{\tt{y1}}, {\it{x\/}})\index{sy-a})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  eq-z2-y2 \\ \index{eq-z2-y2}
{\rm{stringp}}\,({\it{x\/}})\index{stringp} $\rightarrow$ ({\rm{sy-b}}\,({\tt{'}}{\tt{z2}}, {\it{x\/}})\index{sy-b} $=$ {\rm{sy-a}}\,({\tt{'}}{\tt{y2}}, {\it{x\/}})\index{sy-a})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  eq-z3-y3 \\ \index{eq-z3-y3}
{\rm{stringp}}\,({\it{x\/}})\index{stringp} $\rightarrow$ ({\rm{sy-b}}\,({\tt{'}}{\tt{z3}}, {\it{x\/}})\index{sy-b} $=$ {\rm{sy-a}}\,({\tt{'}}{\tt{y3}}, {\it{x\/}})\index{sy-a})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  eq-z4-y4 \\ \index{eq-z4-y4}
{\rm{stringp}}\,({\it{x\/}})\index{stringp} $\rightarrow$ ({\rm{sy-b}}\,({\tt{'}}{\tt{z4}}, {\it{x\/}})\index{sy-b} $=$ {\rm{sy-a}}\,({\tt{'}}{\tt{y4}}, {\it{x\/}})\index{sy-a})
\end{tabbing}

\begin{verbatim}; SECOND we prove the only tricky fact about the circuit:
\end{verbatim}\begin{tabbing}{\sc Theorem}:  eq-z9-y9 \\ \index{eq-z9-y9}
{\rm{stringp}}\,({\it{x\/}})\index{stringp} $\rightarrow$ ({\rm{sy-b}}\,({\tt{'}}{\tt{z9}}, {\it{x\/}})\index{sy-b} $=$ {\rm{sy-a}}\,({\tt{'}}{\tt{y9}}, {\it{x\/}})\index{sy-a})
\end{tabbing}

\begin{verbatim}; THIRD we complete the list of trivial equalities..
\end{verbatim}\begin{tabbing}{\sc Theorem}:  eq-z10-y10 \\ \index{eq-z10-y10}
{\rm{stringp}}\,({\it{x\/}})\index{stringp} $\rightarrow$ ({\rm{sy-b}}\,({\tt{'}}{\tt{z10}}, {\it{x\/}})\index{sy-b} $=$ {\rm{sy-a}}\,({\tt{'}}{\tt{y10}}, {\it{x\/}})\index{sy-a})
\end{tabbing}

\begin{verbatim}; yielding the desired correctness statement!
\end{verbatim}\begin{tabbing}{\sc Theorem}:  eq-zout-yout \\ \index{eq-zout-yout}
{\rm{stringp}}\,({\it{x\/}})\index{stringp} $\rightarrow$ ({\rm{sy-b}}\,({\tt{'}}{\tt{zout}}, {\it{x\/}})\index{sy-b} $=$ {\rm{sy-a}}\,({\tt{'}}{\tt{yout}}, {\it{x\/}})\index{sy-a})
\end{tabbing}

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