\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}; pplfadd.bm: first realistic PPL: Ripple Adder vs. PPL Adder
; 
; RIGHT NOW: Fadd is defined (made sysd animation/debugging/corking
; easier).
; 
; NOTE w/ bad chip: A2-PC-A fails because BM gets hopelessly lost
; in the EQ-LEN hyps...
; Now we bypass all SYSD A2's and get the expansion directly...
;
; We test both the Corked and Uncorked (B-P) thms.

;;; (Sugared) Circuits:
#|
(setq sy-A '(SY-A (Xx2 Xx1 Xx0 Xy2 Xy1 Xy0)
(Yf S Const F Xx2)
(Yo0 S fa-S Xx0 Xy0 Yf)
(Y00 S fa-C Xx0 Xy0 Yf)
(Yo1 S fa-S Xx1 Xy1 Y00)
(Y01 S fa-C Xx1 Xy1 Y00)
(Yo2 S fa-S Xx2 Xy2 Y01)
(Yo3 S fa-C Xx2 Xy2 Y01)

; and the corks (one for each output line), here it's easy: all F
(Yo0c2 R F Yo0)
(Yo0c1 R F Yo0c2)
(Yo0c R F Yo0c1)

(Yo1c2 R F Yo1)
(Yo1c1 R F Yo1c2)
(Yo1c R F Yo1c1)

(Yo2c2 R F Yo2)
(Yo2c1 R F Yo2c2)
(Yo2c R F Yo2c1)

(Yo3c2 R F Yo3)
(Yo3c1 R F Yo3c2)
(Yo3c R F Yo3c1)
))

(setq sy-B '(SY-B (Xx2 Xx1 Xx0 Xy2 Xy1 Xy0)
; 1st stage:
(Zf S Const F Xx2)
(Z00P S fa-S Xx0 Xy0 Zf)
(Z00 R F Z00P)
(Z01P S fa-C Xx0 Xy0 Zf)
(Z01 R F Z01P)
(Z02 R F Xx1)
(Z03 R F Xy1)
(Z04 R F Xx2)
(Z05 R F Xy2)
; 2nd stage:
(Z10 R F Z00)
(Z11P S fa-S Z02 Z03 Z01)
(Z11 R F Z11P)
(Z12P S fa-C Z02 Z03 Z01)
(Z12 R F Z12P)
(Z13 R F Z04)
(Z14 R F Z05)
; 3rd stage:
(Zo0 R F Z10)
(Zo1 R F Z11)
(Zo2P S fa-S Z13 Z14 Z12)
(Zo2 R F Zo2P)
(Zo3P S fa-C Z13 Z14 Z12)
(Zo3 R F Zo3P)
))

; Note: we can animate the sysds in r-loop with:
; for fadd: x = 3 0 0 0 , y = 4 0 0 0 
; (result should be: 7 0 0 0 or 0 0 0 7)
; FUNDAMENTALLY: note that this simulation did NOT fail even with
; our first -- buggy -- circuit...
;(setq xx0 (A (A (A (A (e) T) F) F) F))
;(setq xx1 (A (A (A (A (e) T) F) F) F))
;(setq xx2 (A (A (A (A (e) F) F) F) F))
;(setq xy0 (A (A (A (A (e) F) F) F) F))
;(setq xy1 (A (A (A (A (e) F) F) F) F))
;(setq xy2 (A (A (A (A (e) T) F) F) F))
;
;(sy-a 'Yo0 XX2 XX1 XX0 XY2 XY1 XY0) 
;(sy-a 'Yo1 XX2 XX1 XX0 XY2 XY1 XY0) 
;(sy-a 'Yo2 XX2 XX1 XX0 XY2 XY1 XY0) 
;(sy-a 'Yo3 XX2 XX1 XX0 XY2 XY1 XY0) 
;
;(sy-a 'Yo0c XX2 XX1 XX0 XY2 XY1 XY0) 
;(sy-a 'Yo1c XX2 XX1 XX0 XY2 XY1 XY0) 
;(sy-a 'Yo2c XX2 XX1 XX0 XY2 XY1 XY0) 
;(sy-a 'Yo3c XX2 XX1 XX0 XY2 XY1 XY0) 
;
;(sy-b 'Zo0 XX2 XX1 XX0 XY2 XY1 XY0) 
;(sy-b 'Zo1 XX2 XX1 XX0 XY2 XY1 XY0) 
;(sy-b 'Zo2 XX2 XX1 XX0 XY2 XY1 XY0) 
;(sy-b 'Zo3 XX2 XX1 XX0 XY2 XY1 XY0) 
;
; end r-loop data

(setq pplfadd '( |#
; BM DEFINITIONS and A2 LEMMAS, generated by BMSYSD:
; comb_fa-S.bm: Fa-S , Full Adder, Sum output.
; currently: char function defined
; U7-DONE

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{fa-s} \\  
\=\+{\rm{fa-s}}\,({\it{u\/}}, {\it{v\/}}, {\it{w\/}})\index{fa-s} \\ 
$=$$\;\;\;\;$(\=\+(($\neg$ {\it{u\/}}) $\wedge$ ($\neg$ {\it{v\/}}) $\wedge$ {\it{w\/}}) \\ 
$\vee$$\;\;\;\;$(($\neg$ {\it{u\/}}) $\wedge$ {\it{v\/}} $\wedge$ ($\neg$ {\it{w\/}})) \\ 
$\vee$$\;\;\;\;$({\it{u\/}} $\wedge$ ($\neg$ {\it{v\/}}) $\wedge$ ($\neg$ {\it{w\/}})) \\ 
$\vee$$\;\;\;\;$({\it{u\/}} $\wedge$ {\it{v\/}} $\wedge$ {\it{w\/}}))\-\-
\end{tabbing}

\begin{verbatim}; Everything below generated by: (bmcomb 'Fa-S '() '(x y z))

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

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

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

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

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

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

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

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

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

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

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

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

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

; eof:comb_fa-S.bm

; comb_fa-C.bm: fa-C , Full Adder, Carry output.
; currently: character function is defined 
; U7-DONE

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{fa-c} \\  
{\rm{fa-c}}\,({\it{u\/}}, {\it{v\/}}, {\it{w\/}})\index{fa-c} $=$ (({\it{u\/}} $\wedge$ {\it{v\/}}) $\vee$ ({\it{v\/}} $\wedge$ {\it{w\/}}) $\vee$ ({\it{w\/}} $\wedge$ {\it{u\/}}))
\end{tabbing}

\begin{verbatim}; Everything below generated by: (bmcomb 'fa-C '() '(x y z))

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

\begin{verbatim};; A2-Begin-S-FA-C

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

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

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

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

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

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

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

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

\begin{tabbing}{\sc Theorem}:  a2-bc-s-fa-c \\ \index{a2-bc-s-fa-c}
\=\+(({\rm{len}}\,({\it{x\/}})\index{len} $=$ {\rm{len}}\,({\it{y\/}})\index{len}) $\wedge$ ({\rm{len}}\,({\it{y\/}})\index{len} $=$ {\rm{len}}\,({\it{z\/}})\index{len})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{b}}\,({\rm{s-fa-c}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{s-fa-c})\index{b} $=$ {\rm{s-fa-c}}\,({\rm{b}}\,({\it{x\/}})\index{b}, {\rm{b}}\,({\it{y\/}})\index{b}, {\rm{b}}\,({\it{z\/}})\index{b})\index{s-fa-c})\-
\end{tabbing}

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

\begin{verbatim};; A2-End-S-FA-C

; eof:comb_fa-C.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{yf}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yo0}}$\;\;${\bf then }{\tt{2}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y00}}$\;\;${\bf then }{\tt{2}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yo1}}$\;\;${\bf then }{\tt{3}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y01}}$\;\;${\bf then }{\tt{3}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yo2}}$\;\;${\bf then }{\tt{4}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yo3}}$\;\;${\bf then }{\tt{4}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yo0c2}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yo0c1}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yo0c}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yo1c2}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yo1c1}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yo1c}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yo2c2}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yo2c1}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yo2c}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yo3c2}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yo3c1}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yo3c}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};Parameter found: F in: (YF S CONST F XX2)
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{sy-a} \\  
\=\+{\rm{sy-a}}\,({\it{ln\/}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-a} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{ln\/}} $=$ {\tt{'}}{\tt{yf}}$\;\;${\bf then }{\rm{s-const}}\,({\bf{f}}, {\it{xx2\/}})\index{s-const} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yo0}} \\ 
{\bf then }{\rm{s-fa-s}}\,({\it{xx0\/}}, {\it{xy0\/}}, {\rm{sy-a}}\,({\tt{'}}{\tt{yf}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-a})\index{s-fa-s} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y00}} \\ 
{\bf then }{\rm{s-fa-c}}\,({\it{xx0\/}}, {\it{xy0\/}}, {\rm{sy-a}}\,({\tt{'}}{\tt{yf}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-a})\index{s-fa-c} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yo1}} \\ 
{\bf then }{\rm{s-fa-s}}\,({\it{xx1\/}}, {\it{xy1\/}}, {\rm{sy-a}}\,({\tt{'}}{\tt{y00}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-a})\index{s-fa-s} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y01}} \\ 
{\bf then }{\rm{s-fa-c}}\,({\it{xx1\/}}, {\it{xy1\/}}, {\rm{sy-a}}\,({\tt{'}}{\tt{y00}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-a})\index{s-fa-c} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yo2}} \\ 
{\bf then }{\rm{s-fa-s}}\,({\it{xx2\/}}, {\it{xy2\/}}, {\rm{sy-a}}\,({\tt{'}}{\tt{y01}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-a})\index{s-fa-s} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yo3}} \\ 
{\bf then }{\rm{s-fa-c}}\,({\it{xx2\/}}, {\it{xy2\/}}, {\rm{sy-a}}\,({\tt{'}}{\tt{y01}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-a})\index{s-fa-c} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yo0c2}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xx2\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,(\=\+{\bf{f}}, \\ 
{\rm{sy-a}}\,(\=\+{\tt{'}}{\tt{yo0}}, \\ 
{\rm{p}}\,({\it{xx2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx0\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy0\/}})\index{p})\-\index{sy-a})\-\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yo0c1}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xx2\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,(\=\+{\bf{f}}, \\ 
{\rm{sy-a}}\,(\=\+{\tt{'}}{\tt{yo0c2}}, \\ 
{\rm{p}}\,({\it{xx2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx0\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy0\/}})\index{p})\-\index{sy-a})\-\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yo0c}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xx2\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,(\=\+{\bf{f}}, \\ 
{\rm{sy-a}}\,(\=\+{\tt{'}}{\tt{yo0c1}}, \\ 
{\rm{p}}\,({\it{xx2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx0\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy0\/}})\index{p})\-\index{sy-a})\-\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yo1c2}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xx2\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,(\=\+{\bf{f}}, \\ 
{\rm{sy-a}}\,(\=\+{\tt{'}}{\tt{yo1}}, \\ 
{\rm{p}}\,({\it{xx2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx0\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy0\/}})\index{p})\-\index{sy-a})\-\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yo1c1}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xx2\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,(\=\+{\bf{f}}, \\ 
{\rm{sy-a}}\,(\=\+{\tt{'}}{\tt{yo1c2}}, \\ 
{\rm{p}}\,({\it{xx2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx0\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy0\/}})\index{p})\-\index{sy-a})\-\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yo1c}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xx2\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,(\=\+{\bf{f}}, \\ 
{\rm{sy-a}}\,(\=\+{\tt{'}}{\tt{yo1c1}}, \\ 
{\rm{p}}\,({\it{xx2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx0\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy0\/}})\index{p})\-\index{sy-a})\-\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yo2c2}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xx2\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,(\=\+{\bf{f}}, \\ 
{\rm{sy-a}}\,(\=\+{\tt{'}}{\tt{yo2}}, \\ 
{\rm{p}}\,({\it{xx2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx0\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy0\/}})\index{p})\-\index{sy-a})\-\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yo2c1}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xx2\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,(\=\+{\bf{f}}, \\ 
{\rm{sy-a}}\,(\=\+{\tt{'}}{\tt{yo2c2}}, \\ 
{\rm{p}}\,({\it{xx2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx0\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy0\/}})\index{p})\-\index{sy-a})\-\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yo2c}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xx2\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,(\=\+{\bf{f}}, \\ 
{\rm{sy-a}}\,(\=\+{\tt{'}}{\tt{yo2c1}}, \\ 
{\rm{p}}\,({\it{xx2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx0\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy0\/}})\index{p})\-\index{sy-a})\-\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yo3c2}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xx2\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,(\=\+{\bf{f}}, \\ 
{\rm{sy-a}}\,(\=\+{\tt{'}}{\tt{yo3}}, \\ 
{\rm{p}}\,({\it{xx2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx0\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy0\/}})\index{p})\-\index{sy-a})\-\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yo3c1}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xx2\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,(\=\+{\bf{f}}, \\ 
{\rm{sy-a}}\,(\=\+{\tt{'}}{\tt{yo3c2}}, \\ 
{\rm{p}}\,({\it{xx2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx0\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy0\/}})\index{p})\-\index{sy-a})\-\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yo3c}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xx2\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,(\=\+{\bf{f}}, \\ 
{\rm{sy-a}}\,(\=\+{\tt{'}}{\tt{yo3c1}}, \\ 
{\rm{p}}\,({\it{xx2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx0\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy0\/}})\index{p})\-\index{sy-a})\-\index{i}$\;${\bf  endif}\- \\ 
{\bf else }{\rm{sfix}}\,({\it{xx2\/}})\index{sfix}$\;${\bf  endif}\-\-
\end{tabbing}


\begin{tabbing}{\sc Definition}:\index{topor-sy-b} \\  
\=\+{\rm{topor-sy-b}}\,({\it{ln\/}})\index{topor-sy-b} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{ln\/}} $=$ {\tt{'}}{\tt{zf}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z00p}}$\;\;${\bf then }{\tt{2}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z00}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z01p}}$\;\;${\bf then }{\tt{2}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z01}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z02}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z03}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z04}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z05}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z10}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z11p}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z11}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z12p}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z12}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z13}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z14}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{zo0}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{zo1}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{zo2p}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{zo2}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{zo3p}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{zo3}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};Parameter found: F in: (ZF S CONST F XX2)
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{sy-b} \\  
\=\+{\rm{sy-b}}\,({\it{ln\/}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-b} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{ln\/}} $=$ {\tt{'}}{\tt{zf}}$\;\;${\bf then }{\rm{s-const}}\,({\bf{f}}, {\it{xx2\/}})\index{s-const} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z00p}} \\ 
{\bf then }{\rm{s-fa-s}}\,({\it{xx0\/}}, {\it{xy0\/}}, {\rm{sy-b}}\,({\tt{'}}{\tt{zf}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-b})\index{s-fa-s} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z00}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xx2\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,(\=\+{\bf{f}}, \\ 
{\rm{sy-b}}\,(\=\+{\tt{'}}{\tt{z00p}}, \\ 
{\rm{p}}\,({\it{xx2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx0\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy0\/}})\index{p})\-\index{sy-b})\-\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z01p}} \\ 
{\bf then }{\rm{s-fa-c}}\,({\it{xx0\/}}, {\it{xy0\/}}, {\rm{sy-b}}\,({\tt{'}}{\tt{zf}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-b})\index{s-fa-c} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z01}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xx2\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,(\=\+{\bf{f}}, \\ 
{\rm{sy-b}}\,(\=\+{\tt{'}}{\tt{z01p}}, \\ 
{\rm{p}}\,({\it{xx2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx0\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy0\/}})\index{p})\-\index{sy-b})\-\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z02}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xx2\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\bf{f}}, {\rm{p}}\,({\it{xx1\/}})\index{p})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z03}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xx2\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\bf{f}}, {\rm{p}}\,({\it{xy1\/}})\index{p})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z04}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xx2\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\bf{f}}, {\rm{p}}\,({\it{xx2\/}})\index{p})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z05}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xx2\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\bf{f}}, {\rm{p}}\,({\it{xy2\/}})\index{p})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z10}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xx2\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,(\=\+{\bf{f}}, \\ 
{\rm{sy-b}}\,(\=\+{\tt{'}}{\tt{z00}}, \\ 
{\rm{p}}\,({\it{xx2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx0\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy0\/}})\index{p})\-\index{sy-b})\-\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z11p}} \\ 
{\bf then }{\rm{s-fa-s}}\,(\=\+{\rm{sy-b}}\,({\tt{'}}{\tt{z02}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-b}, \\ 
{\rm{sy-b}}\,({\tt{'}}{\tt{z03}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-b}, \\ 
{\rm{sy-b}}\,({\tt{'}}{\tt{z01}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-b})\-\index{s-fa-s} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z11}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xx2\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,(\=\+{\bf{f}}, \\ 
{\rm{sy-b}}\,(\=\+{\tt{'}}{\tt{z11p}}, \\ 
{\rm{p}}\,({\it{xx2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx0\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy0\/}})\index{p})\-\index{sy-b})\-\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z12p}} \\ 
{\bf then }{\rm{s-fa-c}}\,(\=\+{\rm{sy-b}}\,({\tt{'}}{\tt{z02}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-b}, \\ 
{\rm{sy-b}}\,({\tt{'}}{\tt{z03}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-b}, \\ 
{\rm{sy-b}}\,({\tt{'}}{\tt{z01}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-b})\-\index{s-fa-c} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z12}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xx2\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,(\=\+{\bf{f}}, \\ 
{\rm{sy-b}}\,(\=\+{\tt{'}}{\tt{z12p}}, \\ 
{\rm{p}}\,({\it{xx2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx0\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy0\/}})\index{p})\-\index{sy-b})\-\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z13}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xx2\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,(\=\+{\bf{f}}, \\ 
{\rm{sy-b}}\,(\=\+{\tt{'}}{\tt{z04}}, \\ 
{\rm{p}}\,({\it{xx2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx0\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy0\/}})\index{p})\-\index{sy-b})\-\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{z14}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xx2\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,(\=\+{\bf{f}}, \\ 
{\rm{sy-b}}\,(\=\+{\tt{'}}{\tt{z05}}, \\ 
{\rm{p}}\,({\it{xx2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx0\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy0\/}})\index{p})\-\index{sy-b})\-\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{zo0}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xx2\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,(\=\+{\bf{f}}, \\ 
{\rm{sy-b}}\,(\=\+{\tt{'}}{\tt{z10}}, \\ 
{\rm{p}}\,({\it{xx2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx0\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy0\/}})\index{p})\-\index{sy-b})\-\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{zo1}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xx2\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,(\=\+{\bf{f}}, \\ 
{\rm{sy-b}}\,(\=\+{\tt{'}}{\tt{z11}}, \\ 
{\rm{p}}\,({\it{xx2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx0\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy0\/}})\index{p})\-\index{sy-b})\-\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{zo2p}} \\ 
{\bf then }{\rm{s-fa-s}}\,(\=\+{\rm{sy-b}}\,({\tt{'}}{\tt{z13}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-b}, \\ 
{\rm{sy-b}}\,({\tt{'}}{\tt{z14}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-b}, \\ 
{\rm{sy-b}}\,({\tt{'}}{\tt{z12}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-b})\-\index{s-fa-s} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{zo2}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xx2\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,(\=\+{\bf{f}}, \\ 
{\rm{sy-b}}\,(\=\+{\tt{'}}{\tt{zo2p}}, \\ 
{\rm{p}}\,({\it{xx2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx0\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy0\/}})\index{p})\-\index{sy-b})\-\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{zo3p}} \\ 
{\bf then }{\rm{s-fa-c}}\,(\=\+{\rm{sy-b}}\,({\tt{'}}{\tt{z13}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-b}, \\ 
{\rm{sy-b}}\,({\tt{'}}{\tt{z14}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-b}, \\ 
{\rm{sy-b}}\,({\tt{'}}{\tt{z12}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-b})\-\index{s-fa-c} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{zo3}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xx2\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,(\=\+{\bf{f}}, \\ 
{\rm{sy-b}}\,(\=\+{\tt{'}}{\tt{zo3p}}, \\ 
{\rm{p}}\,({\it{xx2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xx0\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy2\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy1\/}})\index{p}, \\ 
{\rm{p}}\,({\it{xy0\/}})\index{p})\-\index{sy-b})\-\index{i}$\;${\bf  endif}\- \\ 
{\bf else }{\rm{sfix}}\,({\it{xx2\/}})\index{sfix}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; Note: One way to get the EXPAND-ALWAYS effect is to get a rewrite 
; lemma for each def.  (suggestion from Boyer):
;
;(prove-lemma SY-A-lemma (rewrite) 
; (equal (SY-A LN XX2 XX1 XX0 XY2 XY1 XY0)
;(IF (EQUAL LN 'YF) (S-CONST F XX2) 
;...
;(SFIX XX2)))))))))))))))))))))
;)
;
;(prove-lemma SY-B-lemma (rewrite)
; (equal (SY-B LN XX2 XX1 XX0 XY2 XY1 XY0) 
;(IF (EQUAL LN 'ZF) (S-CONST F XX2) 
;...(SFIX XX2))))))))))))))))))))))))
;)
;
; Tested: works.


;;; CORRECTNESS PROOF, hand generated, although full expansion is 
;;; obvious:

; EQ-A-B:  Corked thms:


; let's try it first one pair at a time:  EQ-A-B-0:
; with Boyer's patch, we can do:
; (push 'sy-a always-open-up) (push 'sy-b always-open-up)
; and skip the expand hint, and it WORKS (no hint at all)!
; (pop always-open-up) (pop always-open-up)

\end{verbatim}\begin{tabbing}{\sc Theorem}:  eq-a-b-0 \\ \index{eq-a-b-0}
\=\+{\rm{sy-b}}\,({\tt{'}}{\tt{zo0}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-b} \\ 
$=$$\;\;\;\;${\rm{sy-a}}\,({\tt{'}}{\tt{yo0c}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-a}\-
\end{tabbing}

\begin{verbatim}; EQ-A-B-1 now succeeds!
; seems to require some EQ-LEN hyps so IC's can trigger on inputs 
; different from Xx2.  We try to put just the ones we need to
; minimize confusion:
; (and (equal (len Xx1) (len Xy1))
;      (equal (len Xy1) (len Xx0))
;      (equal (len Xx0) (len Xy0))
;      (equal (len Xy0) (len Xx2))
;      )
; IT WORKS!!!  A bit ad-hoc, but it works!!!
; And with the Sugar generated EQ-LEN hyp:
;(AND (EQUAL (LEN XX2) (LEN XX1))
;     (EQUAL (LEN XX1) (LEN XX0))
;     (EQUAL (LEN XX0) (LEN XY2))
;     (EQUAL (LEN XY2) (LEN XY1))
;     (EQUAL (LEN XY1) (LEN XY0)))
; it works too!  (a couple seconds more but who cares...)
; and with new&improved systemized EQ-LEN hyp, it works too! (Same
; time, but no need to call linear arithmetic.)
;
; W/ Boyer's patch, replacing the expand hint by above PUSHs works 
; fine!
 
\end{verbatim}\begin{tabbing}{\sc Theorem}:  eq-a-b-1 \\ \index{eq-a-b-1}
\=\+(\=\+({\rm{len}}\,({\it{xx1\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xx2\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xy0\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xy1\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xy2\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{sy-b}}\,({\tt{'}}{\tt{zo1}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-b} \\ 
$=$$\;\;\;\;${\rm{sy-a}}\,({\tt{'}}{\tt{yo1c}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-a})\-\-
\end{tabbing}

\begin{verbatim}; EQ-A-B-2:
; BM fails to get some LEN equalities at the right time in EQ-A-B-2
; hence failing the firings of A2-IC-S-FA-S which would complete 
; the proof.  So we prove these facts separately:
; Again, this is a symptom that we have not succeeeded in making BM
; use the fundamental EQ-LEN hyp right...
;
; W/ Boyer's patch, replacing the expand hint by above PUSHs works
; fine!

\end{verbatim}\begin{tabbing}{\sc Theorem}:  eq-a-b-2-bridge1 \\ \index{eq-a-b-2-bridge1}
\=\+(\=\+($\neg$ {\rm{empty}}\,({\rm{p}}\,({\rm{p}}\,({\it{xx2\/}})\index{p})\index{p})\index{empty}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{empty}}\,({\rm{p}}\,({\it{xx2\/}})\index{p})\index{empty}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{empty}}\,({\it{xx2\/}})\index{empty}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xy2\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xy1\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xy0\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xx2\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xx1\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{len}}\,({\rm{p}}\,({\rm{p}}\,({\it{xx2\/}})\index{p})\index{p})\index{len} $=$ ($1\;+$ {\rm{len}}\,({\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xy2\/}})\index{p})\index{p})\index{p})\index{len}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  eq-a-b-2-bridge2 \\ \index{eq-a-b-2-bridge2}
\=\+(\=\+($\neg$ {\rm{empty}}\,({\rm{p}}\,({\rm{p}}\,({\it{xx2\/}})\index{p})\index{p})\index{empty}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{empty}}\,({\rm{p}}\,({\it{xx2\/}})\index{p})\index{empty}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{empty}}\,({\it{xx2\/}})\index{empty}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xy2\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xy1\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xy0\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xx2\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xx1\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{len}}\,({\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xx2\/}})\index{p})\index{p})\index{p})\index{len} $=$ {\rm{len}}\,({\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xy2\/}})\index{p})\index{p})\index{p})\index{len})\-
\end{tabbing}
 
\begin{tabbing}{\sc Theorem}:  eq-a-b-2 \\ \index{eq-a-b-2}
\=\+(\=\+({\rm{len}}\,({\it{xx1\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xx2\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xy0\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xy1\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xy2\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{sy-b}}\,({\tt{'}}{\tt{zo2}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-b} \\ 
$=$$\;\;\;\;${\rm{sy-a}}\,({\tt{'}}{\tt{yo2c}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-a})\-\-
\end{tabbing}

\begin{verbatim}; EQ-A-B-3:
; W/ Boyer's patch, replacing the expand hint by above PUSHs works 
; fine!

\end{verbatim}\begin{tabbing}{\sc Theorem}:  eq-a-b-3 \\ \index{eq-a-b-3}
\=\+(\=\+({\rm{len}}\,({\it{xx1\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xx2\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xy0\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xy1\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xy2\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{sy-b}}\,({\tt{'}}{\tt{zo3}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-b} \\ 
$=$$\;\;\;\;${\rm{sy-a}}\,({\tt{'}}{\tt{yo3c}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-a})\-\-
\end{tabbing}

\begin{verbatim}; EQ2-A-B:  UNCorked thms:
; Boyer's always-open-up patch does wonders here too...

; interestingly enough, EQ-A-B-0 did not require EQ-LEN hyp, but 
; EQ2 does not go through without it.. and the 3 bridges:  This is
; GRUESOMELY AD-HOC...

; Note about the bridge: the first hyp in the AND clause is the one 
; used during the existential instantiation...  Also, additional 
; eq-len clauses confuse the application even more.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  eq2-a-b-0-bridge1 \\ \index{eq2-a-b-0-bridge1}
({\rm{empty}}\,({\rm{p}}\,({\it{xx2\/}})\index{p})\index{empty} $\wedge$ ({\rm{len}}\,({\it{xx2\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len})) $\rightarrow$ {\rm{empty}}\,({\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xx0\/}})\index{p})\index{p})\index{p})\index{empty}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  eq2-a-b-0-bridge2 \\ \index{eq2-a-b-0-bridge2}
({\rm{empty}}\,({\rm{p}}\,({\rm{p}}\,({\it{xx2\/}})\index{p})\index{p})\index{empty} $\wedge$ ({\rm{len}}\,({\it{xx2\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len})) $\rightarrow$ {\rm{empty}}\,({\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xx0\/}})\index{p})\index{p})\index{p})\index{empty}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  eq2-a-b-0-bridge3 \\ \index{eq2-a-b-0-bridge3}
({\rm{empty}}\,({\it{xx2\/}})\index{empty} $\wedge$ ({\rm{len}}\,({\it{xx2\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len})) $\rightarrow$ {\rm{empty}}\,({\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xx0\/}})\index{p})\index{p})\index{p})\index{empty}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  eq2-a-b-0 \\ \index{eq2-a-b-0}
\=\+(\=\+({\rm{len}}\,({\it{xx1\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xx2\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xy0\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xy1\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xy2\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{b}}\,({\rm{b}}\,({\rm{b}}\,({\rm{sy-b}}\,({\tt{'}}{\tt{zo0}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-b})\index{b})\index{b})\index{b} \\ 
$=$$\;\;\;\;${\rm{sy-a}}\,(\=\+{\tt{'}}{\tt{yo0}}, \\ 
{\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xx2\/}})\index{p})\index{p})\index{p}, \\ 
{\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xx1\/}})\index{p})\index{p})\index{p}, \\ 
{\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xx0\/}})\index{p})\index{p})\index{p}, \\ 
{\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xy2\/}})\index{p})\index{p})\index{p}, \\ 
{\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xy1\/}})\index{p})\index{p})\index{p}, \\ 
{\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xy0\/}})\index{p})\index{p})\index{p})\-\index{sy-a})\-\-
\end{tabbing}

\begin{verbatim}; EQ2-A-B-1 ALSO uses the bridges...

\end{verbatim}\begin{tabbing}{\sc Theorem}:  eq2-a-b-1 \\ \index{eq2-a-b-1}
\=\+(\=\+({\rm{len}}\,({\it{xx1\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xx2\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xy0\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xy1\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xy2\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{b}}\,({\rm{b}}\,({\rm{b}}\,({\rm{sy-b}}\,({\tt{'}}{\tt{zo1}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-b})\index{b})\index{b})\index{b} \\ 
$=$$\;\;\;\;${\rm{sy-a}}\,(\=\+{\tt{'}}{\tt{yo1}}, \\ 
{\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xx2\/}})\index{p})\index{p})\index{p}, \\ 
{\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xx1\/}})\index{p})\index{p})\index{p}, \\ 
{\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xx0\/}})\index{p})\index{p})\index{p}, \\ 
{\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xy2\/}})\index{p})\index{p})\index{p}, \\ 
{\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xy1\/}})\index{p})\index{p})\index{p}, \\ 
{\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xy0\/}})\index{p})\index{p})\index{p})\-\index{sy-a})\-\-
\end{tabbing}

\begin{verbatim}; uses both the old and new bridges...

\end{verbatim}\begin{tabbing}{\sc Theorem}:  eq2-a-b-2 \\ \index{eq2-a-b-2}
\=\+(\=\+({\rm{len}}\,({\it{xx1\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xx2\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xy0\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xy1\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xy2\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{b}}\,({\rm{b}}\,({\rm{b}}\,({\rm{sy-b}}\,({\tt{'}}{\tt{zo2}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-b})\index{b})\index{b})\index{b} \\ 
$=$$\;\;\;\;${\rm{sy-a}}\,(\=\+{\tt{'}}{\tt{yo2}}, \\ 
{\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xx2\/}})\index{p})\index{p})\index{p}, \\ 
{\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xx1\/}})\index{p})\index{p})\index{p}, \\ 
{\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xx0\/}})\index{p})\index{p})\index{p}, \\ 
{\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xy2\/}})\index{p})\index{p})\index{p}, \\ 
{\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xy1\/}})\index{p})\index{p})\index{p}, \\ 
{\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xy0\/}})\index{p})\index{p})\index{p})\-\index{sy-a})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  eq2-a-b-3 \\ \index{eq2-a-b-3}
\=\+(\=\+({\rm{len}}\,({\it{xx1\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xx2\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xy0\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xy1\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}) \\ 
$\wedge$$\;\;\;\;$({\rm{len}}\,({\it{xy2\/}})\index{len} $=$ {\rm{len}}\,({\it{xx0\/}})\index{len}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{b}}\,({\rm{b}}\,({\rm{b}}\,({\rm{sy-b}}\,({\tt{'}}{\tt{zo3}}, {\it{xx2\/}}, {\it{xx1\/}}, {\it{xx0\/}}, {\it{xy2\/}}, {\it{xy1\/}}, {\it{xy0\/}})\index{sy-b})\index{b})\index{b})\index{b} \\ 
$=$$\;\;\;\;${\rm{sy-a}}\,(\=\+{\tt{'}}{\tt{yo3}}, \\ 
{\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xx2\/}})\index{p})\index{p})\index{p}, \\ 
{\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xx1\/}})\index{p})\index{p})\index{p}, \\ 
{\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xx0\/}})\index{p})\index{p})\index{p}, \\ 
{\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xy2\/}})\index{p})\index{p})\index{p}, \\ 
{\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xy1\/}})\index{p})\index{p})\index{p}, \\ 
{\rm{p}}\,({\rm{p}}\,({\rm{p}}\,({\it{xy0\/}})\index{p})\index{p})\index{p})\-\index{sy-a})\-\-
\end{tabbing}

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