\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}; ppltcpuM.bm is a variation of ppltcpu which treats ProgMemory like SRC.
;        All it requires is a an additional trivial lemma for the trivial loop.
;
; We use the hands-off PPL proving policies developped there, but
; check both theorems with Explicit and Implicit cork.

;;; (Sugared) Circuits:
#|
(setq sy-A '(SY-A (x)
(Ypc R 0 Ypcn)
(Ypcn S inc Ypc)
(Ypr R 'Ipr Ypr)
(Yin S Ummx Ypc Ypr)
(Yi S Ui Yin)
(Ye S Ue Yi)
(Yout R 0 Ye)
))

(setq sy-B '(SY-B (x)
(Ypc R 0 Ypcn)
(Ypcn S inc Ypc)
(Ypr R 'Ipr Ypr)
(Yin S Ummx Ypc Ypr)
(Yin2 R 0 Yin)
(Yi S Ui Yin2)
(Yi2 R 0 Yi)
(Ye S Ue Yi2)
(Yout R 0 Ye)
))

(setq ppltcpuM '( |#
; BM DEFINITIONS and A2 LEMMAS, generated by BMSYSD:
; comb_inc.bm: INCrement combinational element
; U7-DONE

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{inc}$\;\;$
{\rm{inc}}\,({\it{u\/}})\index{inc} $=$ ($1\;+$ {\it{u\/}})
\end{tabbing}

\begin{verbatim}; Everything below generated by: (bmcomb 'inc '() '(x))

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

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

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

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

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

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

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

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

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

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

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

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

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

; eof:comb_inc.bm

; comb_ummx.bm: Ummx combinational element (= fun2)
; U7-DONE

; arbitrary Char-Fun of arity 2:
\end{verbatim}
\noindent{\sc Event}:   Introduce the function symbol {\it ummx\index{ummx}\/} of 2 arguments.

\addvspace{18pt}

\begin{verbatim}; Everything below generated by: (bmcomb 'Ummx '() '(x y))

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

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

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

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

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

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

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

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

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

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

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

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

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

; eof:comb_ummx.bm

; comb_ui.bm: Ui combinational element (= fun1)
; U7-DONE

; arbitrary Char-Fun of arity 1:
\end{verbatim}
\noindent{\sc Event}:   Introduce the function symbol {\it ui\index{ui}\/} of one argument.

\addvspace{18pt}

\begin{verbatim}; Everything below generated by: (bmcomb 'Ui '() '(x))

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

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

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

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

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

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

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

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

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

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

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

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

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

; eof:comb_ui.bm

; comb_ue.bm: Ue combinational element (= fun1)
; U7-DONE

; arbitrary Char-Fun of arity 1:
\end{verbatim}
\noindent{\sc Event}:   Introduce the function symbol {\it ue\index{ue}\/} of one argument.

\addvspace{18pt}

\begin{verbatim}; Everything below generated by: (bmcomb 'Ue '() '(x))

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

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

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

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

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

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

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

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

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

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

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

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

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

; eof:comb_ue.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{ypc}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ypcn}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ypr}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yin}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yi}}$\;\;${\bf then }{\tt{2}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ye}}$\;\;${\bf then }{\tt{3}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yout}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{sy-a} \\  
\=\+{\rm{sy-a}}\,({\it{ln\/}}, {\it{x\/}})\index{sy-a} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{ln\/}} $=$ {\tt{'}}{\tt{ypc}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{0}}, {\rm{sy-a}}\,({\tt{'}}{\tt{ypcn}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-a})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ypcn}}$\;\;${\bf then }{\rm{s-inc}}\,({\rm{sy-a}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-a})\index{s-inc} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ypr}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{'}}{\tt{ipr}}, {\rm{sy-a}}\,({\tt{'}}{\tt{ypr}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-a})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yin}}$\;\;${\bf then }{\rm{s-ummx}}\,({\rm{sy-a}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-a}, {\rm{sy-a}}\,({\tt{'}}{\tt{ypr}}, {\it{x\/}})\index{sy-a})\index{s-ummx} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yi}}$\;\;${\bf then }{\rm{s-ui}}\,({\rm{sy-a}}\,({\tt{'}}{\tt{yin}}, {\it{x\/}})\index{sy-a})\index{s-ui} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ye}}$\;\;${\bf then }{\rm{s-ue}}\,({\rm{sy-a}}\,({\tt{'}}{\tt{yi}}, {\it{x\/}})\index{sy-a})\index{s-ue} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yout}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{0}}, {\rm{sy-a}}\,({\tt{'}}{\tt{ye}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-a})\index{i}$\;${\bf  endif}\- \\ 
{\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


\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{ypc}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ypcn}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ypr}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yin}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yin2}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yi}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yi2}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ye}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yout}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{sy-b} \\  
\=\+{\rm{sy-b}}\,({\it{ln\/}}, {\it{x\/}})\index{sy-b} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{ln\/}} $=$ {\tt{'}}{\tt{ypc}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{0}}, {\rm{sy-b}}\,({\tt{'}}{\tt{ypcn}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ypcn}}$\;\;${\bf then }{\rm{s-inc}}\,({\rm{sy-b}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-b})\index{s-inc} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ypr}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{'}}{\tt{ipr}}, {\rm{sy-b}}\,({\tt{'}}{\tt{ypr}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yin}}$\;\;${\bf then }{\rm{s-ummx}}\,({\rm{sy-b}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-b}, {\rm{sy-b}}\,({\tt{'}}{\tt{ypr}}, {\it{x\/}})\index{sy-b})\index{s-ummx} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yin2}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{0}}, {\rm{sy-b}}\,({\tt{'}}{\tt{yin}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yi}}$\;\;${\bf then }{\rm{s-ui}}\,({\rm{sy-b}}\,({\tt{'}}{\tt{yin2}}, {\it{x\/}})\index{sy-b})\index{s-ui} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yi2}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{0}}, {\rm{sy-b}}\,({\tt{'}}{\tt{yi}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ye}}$\;\;${\bf then }{\rm{s-ue}}\,({\rm{sy-b}}\,({\tt{'}}{\tt{yi2}}, {\it{x\/}})\index{sy-b})\index{s-ue} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yout}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{0}}, {\rm{sy-b}}\,({\tt{'}}{\tt{ye}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b})\index{i}$\;${\bf  endif}\- \\ 
{\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

; SOME ANIMATION:
; (setq x5T (A (A (A (A (A (e) T) T) T) T) T))
;*(sy-A 'Ye x5t)
; (A (A (A (A (A (E) '(UE (UI (UMMX 0 IPR))))
;             '(UE (UI (UMMX 1 IPR))))
;          '(UE (UI (UMMX 2 IPR))))
;       '(UE (UI (UMMX 3 IPR))))
;    '(UE (UI (UMMX 4 IPR))))
;*(sy-B 'Ye x5t)
; (A (A (A (A (A (E) '(UE 0))
;	     '(UE (UI 0)))
;          '(UE (UI (UMMX 0 IPR))))
;       '(UE (UI (UMMX 1 IPR))))
;    '(UE (UI (UMMX 2 IPR))))
;*

; This takes care of the PC loop:
\end{verbatim}\begin{tabbing}{\sc Theorem}:  eq-pc \\ \index{eq-pc}
{\rm{sy-b}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-b} $=$ {\rm{sy-a}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-a}
\end{tabbing}

\begin{verbatim}; This takes care of the PR loop:
\end{verbatim}\begin{tabbing}{\sc Theorem}:  eq-pr \\ \index{eq-pr}
{\rm{sy-b}}\,({\tt{'}}{\tt{ypr}}, {\it{x\/}})\index{sy-b} $=$ {\rm{sy-a}}\,({\tt{'}}{\tt{ypr}}, {\it{x\/}})\index{sy-a}
\end{tabbing}

\begin{verbatim}; EQ-A-B-exp: explicit cork

\end{verbatim}\begin{tabbing}{\sc Theorem}:  eq-a-b-exp \\ \index{eq-a-b-exp}
\=\+{\rm{sy-b}}\,({\tt{'}}{\tt{ye}}, {\it{x\/}})\index{sy-b} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,(\=\+{\rm{ue}}\,({\tt{0}})\index{ue}, \\ 
\=\+{\bf if }{\rm{empty}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\rm{ue}}\,({\rm{ui}}\,({\tt{0}})\index{ui})\index{ue}, {\rm{sy-a}}\,({\tt{'}}{\tt{ye}}, {\rm{p}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{p})\index{sy-a})\index{i}$\;${\bf  endif}\-)\-\index{i}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; w/ implicit cork:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  eq-a-b-imp \\ \index{eq-a-b-imp}
($\neg$ {\rm{empty}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{empty}) $\rightarrow$ ({\rm{b}}\,({\rm{b}}\,({\rm{sy-b}}\,({\tt{'}}{\tt{ye}}, {\it{x\/}})\index{sy-b})\index{b})\index{b} $=$ {\rm{sy-a}}\,({\tt{'}}{\tt{ye}}, {\rm{p}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{p})\index{sy-a})
\end{tabbing}
\begin{verbatim}; eof: ppltcpuM.bm
;))
\end{verbatim}
%\end{list}
\printindex
\end{document}
