\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}; srccpu.bm is the BIG ONE!
;
; Notes:
; . As in pplfadd, some A2-PCs trigger a BM bug and blow up 
;   (here A2-PC-SY-I) so we declare it as axiom (point that out in
;   Personal Confessions section in thesis).
; . Constants:  Initial PC (pci) has to be declared and axiomatized
;   as a numberp, because we do defined arithmetic (add1) on it.  
;   Others: initial program and initial register file are quoted 
;   constants, because only undefined (dcl) functions act on them.
; . We code "NoAd" (inexistant address) as F, because it makes life
;   easier by avoiding needless equalities around.  As a general 
;   principle (at least in BM), boolean flags should be coded as
;   booleans in the model!  It also means that "small k" and 
;   "big k" in Saxe's picture are now the same thing:
;   (k ctl leftinput) = (if ctl F leftinput).


;;; (Sugared) Circuits:
#|
(setq sy-S '(sy-S (x)
(Ypc R (pci) Ypcn)
(Ypcn S mux Ybc Ybt Ypcp1)
(Ypcp1 S inc Ypc)
(Ybc S eql0 Ywd)

(Ypr R 'pro Ypr)
(Ybt S Umb Ypc Ypr)
(Ywa S Umw Ypc Ypr)
(Yra S Umr Ypc Ypr)
(Yf S Umf Ypc Ypr)

(Ywd S Ualu Yf Yrd)
(Yrd S Ulk Yra Yrf)
(Yrf R 'rfi Yrfn)
(Yrfn S Upd Ywa Ywd Yrf)
))

; pipeline elements are indicated by visual offset (and digits):
; Initial values (originally inspired by Lamport):
;
; The branch target (bt) don't matter, they get 0
; The branch control (bc) DO matter, they must start w/ False: F
; The write address (wa) also matter, they must start w/ "NoAd": F

(setq sy-I '(sy-I (x)
(Ypc R (pci) Ypcn)
(Ypcn S mux Ybc0 Ybt0 Ypcp1)
  (Ybt0 R 0 Ybt1)
  (Ybt1 R 0 Ybt2)
  (Ybt2 R 0 Ybt3)
  (Ybt3 R 0 Ybt4)
  (Ybc0 R F Ybc1k)
  (Ybc1k S k Ybc0 Ybc1)
  (Ybc1 R F Ybc2k)
  (Ybc2k S k Ybc0 Ybc2)
  (Ybc2 R F Ybc3k)
  (Ybc3k S k Ybc0 Ybc3)
  (Ybc3 R F Ybc4k)
  (Ybc4k S k Ybc0 Ybc4)
(Ypcp1 S inc Ypc)
(Ybc4 S eql0 Ywd4)

(Ypr R 'pro Ypr)
(Ybt4 S Umb Ypc Ypr)
(Ywa4 S Umw Ypc Ypr)
(Yra S Umr Ypc Ypr)
(Yf S Umf Ypc Ypr)

(Ywd4 S Ualu Yf Yrd3)
  (Yrd3 S mux Yrb3 Ywd3 Yrd2)
  (Yrd2 S mux Yrb2 Ywd2 Yrd1)
  (Yrd1 S mux Yrb1 Ywd1 Yrd)
  (Yrb3 S equal Yra Ywa3)
  (Yrb2 S equal Yra Ywa2)
  (Yrb1 S equal Yra Ywa1)
  (Ywa3 R F Ywa4k)
  (Ywa2 R F Ywa3k)
  (Ywa1 R F Ywa2k)
  (Ywa4k S k Ybc0 Ywa4)
  (Ywa3k S k Ybc0 Ywa3)
  (Ywa2k S k Ybc0 Ywa2)
  (Ywa1k S k Ybc0 Ywa1)
(Yrd S Ulk Yra Yrf)
(Yrf R 'rfi Yrfn)
(Yrfn S Upd Ywa1k Ywd1 Yrf)
  (Ywd1 R 0 Ywd2)
  (Ywd2 R 0 Ywd3)
  (Ywd3 R 0 Ywd4)

))

(setq srccpu '( |#
; Constants are hand-declared and axiomatized:

\end{verbatim}
\noindent{\sc Event}:   Introduce the function symbol {\it pci\index{pci}\/} of 0 arguments.

\addvspace{18pt}
\begin{tabbing}{\sc Axiom}:  pci-numberp \\ \index{pci-numberp}
{\sc{pci}}\index{pci} $\in\;${\bf{N}}${}$
\end{tabbing}

\begin{verbatim}; BM DEFINITIONS and A2 LEMMAS, generated by BMSYSD:
; comb_mux.bm: Mux combinational element, i.e. "if".
; U7-DONE

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

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

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

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

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


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

\addvspace{18pt}

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

;; A2-Begin-S-MUX

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

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

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

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

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

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

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

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

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

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

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

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

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

;; A2-End-S-MUX

; eof:comb_mux.bm

; 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_eql0.bm: equal to 0 test, without zerop (in contrast to eq0).
; U7-DONE

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{eql0}$\;\;$
{\rm{eql0}}\,({\it{u\/}})\index{eql0} $=$ ({\it{u\/}} $=$ {\tt{0}})
\end{tabbing}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

; eof:comb_eq0.bm

; comb_umb.bm: Umb combinational element (= fun2)
; U7-DONE

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

\addvspace{18pt}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

; eof:comb_umb.bm

; comb_umw.bm: Umw combinational element (= fun2)
; U7-DONE

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

\addvspace{18pt}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

; eof:comb_umw.bm

; comb_umr.bm: Umr combinational element (= fun2)
; U7-DONE

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

\addvspace{18pt}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

; eof:comb_umr.bm

; comb_umf.bm: Umf combinational element (= fun2)
; U7-DONE

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

\addvspace{18pt}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

; eof:comb_umf.bm

; comb_ualu.bm: Ualu combinational element
; U7-DONE

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

\addvspace{18pt}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

; eof:comb_ualu.bm

; comb_ulk.bm: Ulk combinational element
; U7-DONE

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

\addvspace{18pt}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

; eof:comb_ulk.bm

; comb_upd.bm: Upd combinational element
; U7-DONE

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

\addvspace{18pt}

\begin{verbatim}; AXIOM characterising Upd:  (or at least some): see _s .

; Everything below generated by: (bmcomb 'Upd '() '(x1 x2 x3))

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

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

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

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

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

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

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

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

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

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

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

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

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

; eof:comb_upd.bm


\end{verbatim}\begin{tabbing}{\sc Definition}:\index{topor-sy-s} \\  
\=\+{\rm{topor-sy-s}}\,({\it{ln\/}})\index{topor-sy-s} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{ln\/}} $=$ {\tt{'}}{\tt{ypc}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ypcn}}$\;\;${\bf then }{\tt{5}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ypcp1}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ybc}}$\;\;${\bf then }{\tt{4}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ypr}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ybt}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ywa}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yra}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yf}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ywd}}$\;\;${\bf then }{\tt{3}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yrd}}$\;\;${\bf then }{\tt{2}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yrf}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yrfn}}$\;\;${\bf then }{\tt{4}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{sy-s} \\  
\=\+{\rm{sy-s}}\,({\it{ln\/}}, {\it{x\/}})\index{sy-s} \\ 
$=$$\;\;\;\;$\=\+{\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}}\,({\sc{pci}}\index{pci}, {\rm{sy-s}}\,({\tt{'}}{\tt{ypcn}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-s})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ypcn}} \\ 
{\bf then }{\rm{s-mux}}\,({\rm{sy-s}}\,({\tt{'}}{\tt{ybc}}, {\it{x\/}})\index{sy-s}, {\rm{sy-s}}\,({\tt{'}}{\tt{ybt}}, {\it{x\/}})\index{sy-s}, {\rm{sy-s}}\,({\tt{'}}{\tt{ypcp1}}, {\it{x\/}})\index{sy-s})\index{s-mux} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ypcp1}}$\;\;${\bf then }{\rm{s-inc}}\,({\rm{sy-s}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-s})\index{s-inc} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ybc}}$\;\;${\bf then }{\rm{s-eql0}}\,({\rm{sy-s}}\,({\tt{'}}{\tt{ywd}}, {\it{x\/}})\index{sy-s})\index{s-eql0} \\ 
{\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{pro}}, {\rm{sy-s}}\,({\tt{'}}{\tt{ypr}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-s})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ybt}}$\;\;${\bf then }{\rm{s-umb}}\,({\rm{sy-s}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-s}, {\rm{sy-s}}\,({\tt{'}}{\tt{ypr}}, {\it{x\/}})\index{sy-s})\index{s-umb} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ywa}}$\;\;${\bf then }{\rm{s-umw}}\,({\rm{sy-s}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-s}, {\rm{sy-s}}\,({\tt{'}}{\tt{ypr}}, {\it{x\/}})\index{sy-s})\index{s-umw} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yra}}$\;\;${\bf then }{\rm{s-umr}}\,({\rm{sy-s}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-s}, {\rm{sy-s}}\,({\tt{'}}{\tt{ypr}}, {\it{x\/}})\index{sy-s})\index{s-umr} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yf}}$\;\;${\bf then }{\rm{s-umf}}\,({\rm{sy-s}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-s}, {\rm{sy-s}}\,({\tt{'}}{\tt{ypr}}, {\it{x\/}})\index{sy-s})\index{s-umf} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ywd}}$\;\;${\bf then }{\rm{s-ualu}}\,({\rm{sy-s}}\,({\tt{'}}{\tt{yf}}, {\it{x\/}})\index{sy-s}, {\rm{sy-s}}\,({\tt{'}}{\tt{yrd}}, {\it{x\/}})\index{sy-s})\index{s-ualu} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yrd}}$\;\;${\bf then }{\rm{s-ulk}}\,({\rm{sy-s}}\,({\tt{'}}{\tt{yra}}, {\it{x\/}})\index{sy-s}, {\rm{sy-s}}\,({\tt{'}}{\tt{yrf}}, {\it{x\/}})\index{sy-s})\index{s-ulk} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yrf}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{'}}{\tt{rfi}}, {\rm{sy-s}}\,({\tt{'}}{\tt{yrfn}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-s})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yrfn}} \\ 
{\bf then }{\rm{s-upd}}\,({\rm{sy-s}}\,({\tt{'}}{\tt{ywa}}, {\it{x\/}})\index{sy-s}, {\rm{sy-s}}\,({\tt{'}}{\tt{ywd}}, {\it{x\/}})\index{sy-s}, {\rm{sy-s}}\,({\tt{'}}{\tt{yrf}}, {\it{x\/}})\index{sy-s})\index{s-upd} \\ 
{\bf else }{\rm{sfix}}\,({\it{x\/}})\index{sfix}$\;${\bf  endif}\-\-
\end{tabbing}

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

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

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

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

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

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

\begin{verbatim};; A2-End-SY-S
; BM DEFINITIONS and A2 LEMMAS, generated by BMSYSD:
; comb_k.bm: K combinational element. Semantics by Saxe in rn395 Notes 3.
; Our "k" is his "k" (i.e. little k).
; U7-DONE

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{k} \\  
\=\+{\rm{k}}\,({\it{u\/}}, {\it{v\/}})\index{k} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{u\/}}$\;\;${\bf then }{\bf{f}} \\ 
{\bf else }{\it{v\/}}$\;${\bf  endif}\-\-
\end{tabbing}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

; eof:comb_k.bm


\end{verbatim}\begin{tabbing}{\sc Definition}:\index{topor-sy-i} \\  
\=\+{\rm{topor-sy-i}}\,({\it{ln\/}})\index{topor-sy-i} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{ln\/}} $=$ {\tt{'}}{\tt{ypc}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ypcn}}$\;\;${\bf then }{\tt{2}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ybt0}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ybt1}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ybt2}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ybt3}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ybc0}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ybc1k}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ybc1}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ybc2k}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ybc2}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ybc3k}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ybc3}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ybc4k}}$\;\;${\bf then }{\tt{8}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ypcp1}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ybc4}}$\;\;${\bf then }{\tt{7}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ypr}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ybt4}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ywa4}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yra}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yf}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ywd4}}$\;\;${\bf then }{\tt{6}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yrd3}}$\;\;${\bf then }{\tt{5}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yrd2}}$\;\;${\bf then }{\tt{4}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yrd1}}$\;\;${\bf then }{\tt{3}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yrb3}}$\;\;${\bf then }{\tt{2}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yrb2}}$\;\;${\bf then }{\tt{2}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yrb1}}$\;\;${\bf then }{\tt{2}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ywa3}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ywa2}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ywa1}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ywa4k}}$\;\;${\bf then }{\tt{2}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ywa3k}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ywa2k}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ywa1k}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yrd}}$\;\;${\bf then }{\tt{2}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yrf}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yrfn}}$\;\;${\bf then }{\tt{2}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ywd1}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ywd2}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ywd3}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{sy-i} \\  
\=\+{\rm{sy-i}}\,({\it{ln\/}}, {\it{x\/}})\index{sy-i} \\ 
$=$$\;\;\;\;$\=\+{\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}}\,({\sc{pci}}\index{pci}, {\rm{sy-i}}\,({\tt{'}}{\tt{ypcn}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-i})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ypcn}} \\ 
{\bf then }{\rm{s-mux}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ybc0}}, {\it{x\/}})\index{sy-i}, {\rm{sy-i}}\,({\tt{'}}{\tt{ybt0}}, {\it{x\/}})\index{sy-i}, {\rm{sy-i}}\,({\tt{'}}{\tt{ypcp1}}, {\it{x\/}})\index{sy-i})\index{s-mux} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ybt0}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{0}}, {\rm{sy-i}}\,({\tt{'}}{\tt{ybt1}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-i})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ybt1}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{0}}, {\rm{sy-i}}\,({\tt{'}}{\tt{ybt2}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-i})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ybt2}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{0}}, {\rm{sy-i}}\,({\tt{'}}{\tt{ybt3}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-i})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ybt3}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{0}}, {\rm{sy-i}}\,({\tt{'}}{\tt{ybt4}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-i})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ybc0}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\bf{f}}, {\rm{sy-i}}\,({\tt{'}}{\tt{ybc1k}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-i})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ybc1k}}$\;\;${\bf then }{\rm{s-k}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ybc0}}, {\it{x\/}})\index{sy-i}, {\rm{sy-i}}\,({\tt{'}}{\tt{ybc1}}, {\it{x\/}})\index{sy-i})\index{s-k} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ybc1}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\bf{f}}, {\rm{sy-i}}\,({\tt{'}}{\tt{ybc2k}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-i})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ybc2k}}$\;\;${\bf then }{\rm{s-k}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ybc0}}, {\it{x\/}})\index{sy-i}, {\rm{sy-i}}\,({\tt{'}}{\tt{ybc2}}, {\it{x\/}})\index{sy-i})\index{s-k} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ybc2}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\bf{f}}, {\rm{sy-i}}\,({\tt{'}}{\tt{ybc3k}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-i})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ybc3k}}$\;\;${\bf then }{\rm{s-k}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ybc0}}, {\it{x\/}})\index{sy-i}, {\rm{sy-i}}\,({\tt{'}}{\tt{ybc3}}, {\it{x\/}})\index{sy-i})\index{s-k} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ybc3}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\bf{f}}, {\rm{sy-i}}\,({\tt{'}}{\tt{ybc4k}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-i})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ybc4k}}$\;\;${\bf then }{\rm{s-k}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ybc0}}, {\it{x\/}})\index{sy-i}, {\rm{sy-i}}\,({\tt{'}}{\tt{ybc4}}, {\it{x\/}})\index{sy-i})\index{s-k} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ypcp1}}$\;\;${\bf then }{\rm{s-inc}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-i})\index{s-inc} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ybc4}}$\;\;${\bf then }{\rm{s-eql0}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywd4}}, {\it{x\/}})\index{sy-i})\index{s-eql0} \\ 
{\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{pro}}, {\rm{sy-i}}\,({\tt{'}}{\tt{ypr}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-i})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ybt4}}$\;\;${\bf then }{\rm{s-umb}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-i}, {\rm{sy-i}}\,({\tt{'}}{\tt{ypr}}, {\it{x\/}})\index{sy-i})\index{s-umb} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ywa4}}$\;\;${\bf then }{\rm{s-umw}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-i}, {\rm{sy-i}}\,({\tt{'}}{\tt{ypr}}, {\it{x\/}})\index{sy-i})\index{s-umw} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yra}}$\;\;${\bf then }{\rm{s-umr}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-i}, {\rm{sy-i}}\,({\tt{'}}{\tt{ypr}}, {\it{x\/}})\index{sy-i})\index{s-umr} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yf}}$\;\;${\bf then }{\rm{s-umf}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-i}, {\rm{sy-i}}\,({\tt{'}}{\tt{ypr}}, {\it{x\/}})\index{sy-i})\index{s-umf} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ywd4}}$\;\;${\bf then }{\rm{s-ualu}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yf}}, {\it{x\/}})\index{sy-i}, {\rm{sy-i}}\,({\tt{'}}{\tt{yrd3}}, {\it{x\/}})\index{sy-i})\index{s-ualu} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yrd3}} \\ 
{\bf then }{\rm{s-mux}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yrb3}}, {\it{x\/}})\index{sy-i}, {\rm{sy-i}}\,({\tt{'}}{\tt{ywd3}}, {\it{x\/}})\index{sy-i}, {\rm{sy-i}}\,({\tt{'}}{\tt{yrd2}}, {\it{x\/}})\index{sy-i})\index{s-mux} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yrd2}} \\ 
{\bf then }{\rm{s-mux}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yrb2}}, {\it{x\/}})\index{sy-i}, {\rm{sy-i}}\,({\tt{'}}{\tt{ywd2}}, {\it{x\/}})\index{sy-i}, {\rm{sy-i}}\,({\tt{'}}{\tt{yrd1}}, {\it{x\/}})\index{sy-i})\index{s-mux} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yrd1}} \\ 
{\bf then }{\rm{s-mux}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yrb1}}, {\it{x\/}})\index{sy-i}, {\rm{sy-i}}\,({\tt{'}}{\tt{ywd1}}, {\it{x\/}})\index{sy-i}, {\rm{sy-i}}\,({\tt{'}}{\tt{yrd}}, {\it{x\/}})\index{sy-i})\index{s-mux} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yrb3}}$\;\;${\bf then }{\rm{s-equal}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yra}}, {\it{x\/}})\index{sy-i}, {\rm{sy-i}}\,({\tt{'}}{\tt{ywa3}}, {\it{x\/}})\index{sy-i})\index{s-equal} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yrb2}}$\;\;${\bf then }{\rm{s-equal}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yra}}, {\it{x\/}})\index{sy-i}, {\rm{sy-i}}\,({\tt{'}}{\tt{ywa2}}, {\it{x\/}})\index{sy-i})\index{s-equal} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yrb1}}$\;\;${\bf then }{\rm{s-equal}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yra}}, {\it{x\/}})\index{sy-i}, {\rm{sy-i}}\,({\tt{'}}{\tt{ywa1}}, {\it{x\/}})\index{sy-i})\index{s-equal} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ywa3}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\bf{f}}, {\rm{sy-i}}\,({\tt{'}}{\tt{ywa4k}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-i})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ywa2}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\bf{f}}, {\rm{sy-i}}\,({\tt{'}}{\tt{ywa3k}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-i})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ywa1}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\bf{f}}, {\rm{sy-i}}\,({\tt{'}}{\tt{ywa2k}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-i})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ywa4k}}$\;\;${\bf then }{\rm{s-k}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ybc0}}, {\it{x\/}})\index{sy-i}, {\rm{sy-i}}\,({\tt{'}}{\tt{ywa4}}, {\it{x\/}})\index{sy-i})\index{s-k} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ywa3k}}$\;\;${\bf then }{\rm{s-k}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ybc0}}, {\it{x\/}})\index{sy-i}, {\rm{sy-i}}\,({\tt{'}}{\tt{ywa3}}, {\it{x\/}})\index{sy-i})\index{s-k} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ywa2k}}$\;\;${\bf then }{\rm{s-k}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ybc0}}, {\it{x\/}})\index{sy-i}, {\rm{sy-i}}\,({\tt{'}}{\tt{ywa2}}, {\it{x\/}})\index{sy-i})\index{s-k} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ywa1k}}$\;\;${\bf then }{\rm{s-k}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ybc0}}, {\it{x\/}})\index{sy-i}, {\rm{sy-i}}\,({\tt{'}}{\tt{ywa1}}, {\it{x\/}})\index{sy-i})\index{s-k} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yrd}}$\;\;${\bf then }{\rm{s-ulk}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yra}}, {\it{x\/}})\index{sy-i}, {\rm{sy-i}}\,({\tt{'}}{\tt{yrf}}, {\it{x\/}})\index{sy-i})\index{s-ulk} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yrf}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{'}}{\tt{rfi}}, {\rm{sy-i}}\,({\tt{'}}{\tt{yrfn}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-i})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yrfn}} \\ 
{\bf then }{\rm{s-upd}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa1k}}, {\it{x\/}})\index{sy-i}, {\rm{sy-i}}\,({\tt{'}}{\tt{ywd1}}, {\it{x\/}})\index{sy-i}, {\rm{sy-i}}\,({\tt{'}}{\tt{yrf}}, {\it{x\/}})\index{sy-i})\index{s-upd} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ywd1}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{0}}, {\rm{sy-i}}\,({\tt{'}}{\tt{ywd2}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-i})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ywd2}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{0}}, {\rm{sy-i}}\,({\tt{'}}{\tt{ywd3}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-i})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{ywd3}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{0}}, {\rm{sy-i}}\,({\tt{'}}{\tt{ywd4}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-i})\index{i}$\;${\bf  endif}\- \\ 
{\bf else }{\rm{sfix}}\,({\it{x\/}})\index{sfix}$\;${\bf  endif}\-\-
\end{tabbing}

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

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

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

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

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

\begin{verbatim}; blows up, as usual.
;(PROVE-LEMMA A2-PC-SY-I (REWRITE)
;    (EQUAL (P (SY-I LN X)) (SY-I LN (P X)))
;    ((DISABLE S-INC S-EQL0 S-UMB S-UMW S-UMR S-UMF S-UALU S-MUX S-EQUAL
;              S-K S-ULK S-UPD A2-IC-S-INC A2-IC-S-EQL0 A2-IC-S-UMB
;              A2-IC-S-UMW A2-IC-S-UMR A2-IC-S-UMF A2-IC-S-UALU
;              A2-IC-S-MUX A2-IC-S-EQUAL A2-IC-S-K A2-IC-S-ULK
;              A2-IC-S-UPD)))

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

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


; CORRECTNESS PROOF:

;;; Get STUTTER theory:
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; 				TH_STUTTER.BM
;;;
;;; This file contains Stutter theory for BM.  It is supposed to be
;;; loaded directly when needed (i.e. not general enough to be 
;;; stored in Lib/mlp).
;;;

;;; Our current double P-recursive def. of Stutter:
;;; Originally, it came from THETA-PRF-79 (done while babysitting
;;; for Caroline...) followed by MUCH experimentation and fiddling.


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

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

\begin{verbatim}; Stut-Induct inducts like stut, but without the case disjunction 
; on LPx which is useless when we stutter on a line rather than an 
; input. The resulting induction is not very different from a 
; straight P induction, but it takes care of the empty Px case 
; separately, and without bringing an elimination.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{stut-induct} \\  
\=\+{\rm{stut-induct}}\,({\it{x\/}})\index{stut-induct} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\rm{empty}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{empty}$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\rm{stut-induct}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{stut-induct}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};; Properties of Stut:

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

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

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

\begin{verbatim};; Properties of Stut-R:

; Stut-R-E maybe shouldn't be enabled all the time, but when we're 
; doing P inductions on Stut-R, this gives the base case.  The 
; induction step is given by Stut-R-P.  Note that we don't have a 
; full empty x hyp because Stut-R returns x and not sfix x in case
; y is empty...  Maybe we want to fix that at some point.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  stut-r-e \\ \index{stut-r-e}
{\rm{stut-r}}\,({\sc{e}}\index{e}, {\it{y\/}})\index{stut-r} $=$ {\sc{e}}\index{e}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  stut-r-p \\ \index{stut-r-p}
{\rm{p}}\,({\rm{stut-r}}\,({\it{x\/}}, {\it{y\/}})\index{stut-r})\index{p} $=$ {\rm{stut-r}}\,({\rm{p}}\,({\it{x\/}})\index{p}, {\it{y\/}})\index{stut-r}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  stut-r-len \\ \index{stut-r-len}
{\rm{len}}\,({\it{x\/}})\index{len} $<$ ($1\;+$ ({\rm{len}}\,({\it{y\/}})\index{len} $+$ {\rm{len}}\,({\rm{stut-r}}\,({\it{x\/}}, {\it{y\/}})\index{stut-r})\index{len}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  stut-r-not-empty \\ \index{stut-r-not-empty}
({\rm{len}}\,({\it{y\/}})\index{len} $<$ {\rm{len}}\,({\it{x\/}})\index{len}) $\rightarrow$ ($\neg$ {\rm{empty}}\,({\rm{stut-r}}\,({\it{x\/}}, {\it{y\/}})\index{stut-r})\index{empty})
\end{tabbing}

\begin{verbatim}; Stut-Rem removes the trailing Ts of y, but ignores Ly (like R) 
; and leaves one T: this weird def, so it works like Stut-R needs!

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

\begin{tabbing}{\sc Theorem}:  stut-rem-empty \\ \index{stut-rem-empty}
{\rm{empty}}\,({\rm{stut-rem}}\,({\it{x\/}})\index{stut-rem})\index{empty} $=$ {\rm{empty}}\,({\it{x\/}})\index{empty}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  stut-rem-len \\ \index{stut-rem-len}
{\rm{len}}\,({\rm{stut-rem}}\,({\it{x\/}})\index{stut-rem})\index{len} $<$ ($1\;+$ {\rm{len}}\,({\it{x\/}})\index{len})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  stut-rem-len2 \\ \index{stut-rem-len2}
(($\neg$ {\rm{empty}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{empty}) $\wedge$ {\rm{l}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{l}) $\rightarrow$ ({\rm{len}}\,({\rm{stut-rem}}\,({\it{x\/}})\index{stut-rem})\index{len} $<$ {\rm{len}}\,({\it{x\/}})\index{len})
\end{tabbing}


\begin{verbatim}; Stut-Num counts the number of F in y, ignoring Ly, and starts 
; w/ 1, like Stut.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{stut-num} \\  
\=\+{\rm{stut-num}}\,({\it{y\/}})\index{stut-num} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{empty}}\,({\it{y\/}})\index{empty}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\rm{empty}}\,({\rm{p}}\,({\it{y\/}})\index{p})\index{empty}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\rm{l}}\,({\rm{p}}\,({\it{y\/}})\index{p})\index{l}$\;\;${\bf then }{\rm{stut-num}}\,({\rm{p}}\,({\it{y\/}})\index{p})\index{stut-num} \\ 
{\bf else }$1\;+$ {\rm{stut-num}}\,({\rm{p}}\,({\it{y\/}})\index{p})\index{stut-num}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  stut-num-lessp \\ \index{stut-num-lessp}
{\rm{stut-num}}\,({\it{x\/}})\index{stut-num} $<$ ($1\;+$ {\rm{len}}\,({\it{x\/}})\index{len})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  stut-num-eq-0 \\ \index{stut-num-eq-0}
({\rm{stut-num}}\,({\it{x\/}})\index{stut-num} $=$ {\tt{0}}) $=$ {\rm{empty}}\,({\it{x\/}})\index{empty}
\end{tabbing}


\begin{verbatim}; Requires a small induction.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  stut-num-rem-len \\ \index{stut-num-rem-len}
($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) $\rightarrow$ ({\rm{stut-num}}\,({\rm{p}}\,({\rm{stut-rem}}\,({\it{x\/}})\index{stut-rem})\index{p})\index{stut-num} $<$ {\rm{len}}\,({\it{x\/}})\index{len})
\end{tabbing}

\begin{verbatim}; From Stut-Num and Bn we get a CLOSED FORM for Stut-R !!!

\end{verbatim}\begin{tabbing}{\sc Theorem}:  stut-r-closed \\ \index{stut-r-closed}
{\rm{stut-r}}\,({\it{x\/}}, {\it{y\/}})\index{stut-r} $=$ {\rm{bn}}\,({\rm{stut-num}}\,({\it{y\/}})\index{stut-num}, {\it{x\/}})\index{bn}
\end{tabbing}

\begin{verbatim}; Stut-inv is the key invariant property during Stuttering:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  stut-inv \\ \index{stut-inv}
\=\+(($\neg$ {\rm{empty}}\,({\it{y\/}})\index{empty}) $\wedge$ ({\rm{len}}\,({\it{x\/}})\index{len} $\not<$ {\rm{len}}\,({\it{y\/}})\index{len})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{l}}\,({\rm{stut}}\,({\it{x\/}}, {\it{y\/}})\index{stut})\index{l} $=$ {\rm{h}}\,({\rm{stut-r}}\,({\it{x\/}}, {\rm{p}}\,({\rm{stut-rem}}\,({\it{y\/}})\index{stut-rem})\index{p})\index{stut-r})\index{h})\-
\end{tabbing}
\begin{verbatim}; but we only want to use it during the non-stuttering induction 
; step, and not in general so:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  stut-inv0 \\ \index{stut-inv0}
\=\+(($\neg$ {\rm{empty}}\,({\it{y\/}})\index{empty}) $\wedge$ ({\rm{len}}\,({\it{x\/}})\index{len} $\not<$ {\rm{len}}\,({\it{y\/}})\index{len}) $\wedge$ ($\neg$ {\rm{l}}\,({\it{y\/}})\index{l})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{l}}\,({\rm{stut}}\,({\it{x\/}}, {\it{y\/}})\index{stut})\index{l} $=$ {\rm{h}}\,({\rm{stut-r}}\,({\it{x\/}}, {\rm{p}}\,({\rm{stut-rem}}\,({\it{y\/}})\index{stut-rem})\index{p})\index{stut-r})\index{h})\-
\end{tabbing}


\noindent{\sc Event}:   Disable stut-inv.

\addvspace{18pt}

\begin{verbatim}; Now we relate Stut-R for Py and P Rem Py, to get the key to the
; induction step on main Stut inductions, in the non-stuttering 
; case.
;
; It's a BAD rewrite (i.e. expanding, potentially self-applicable),
; and so are the preliminary lemmas needed to build to it.  This
; is not just an unfortunate construction.  It's inherent, because
; we're essentially giving an alternate definition via a Stut-Rem
; recursion.  And definitions are expanding, self-applicable, 
; rewrites.  We get around the problem by lucking out: the
; hypotheses are sufficient to prevent successful self-applic.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  stut-r-indstep-num \\ \index{stut-r-indstep-num}
\=\+(($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) $\wedge$ {\rm{l}}\,({\it{x\/}})\index{l}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{stut-num}}\,({\it{x\/}})\index{stut-num} $=$ ($1\;+$ {\rm{stut-num}}\,({\rm{p}}\,({\rm{stut-rem}}\,({\it{x\/}})\index{stut-rem})\index{p})\index{stut-num}))\-
\end{tabbing}

\noindent{\sc Event}:   Disable stut-r-indstep-num.

\addvspace{18pt}

\begin{verbatim}; OLD induction step prereq: not needed anymore.
;
;(prove-lemma Stut-R-indstep-Num-Rem (rewrite) 
;(implies (and (not (empty y))
;	      (not (empty (P y)))
;	      (not (L (P y)))
;	      )
;	 (equal (Stut-Num (P (Stut-Rem (P y))))
;		(sub1 (Stut-Num (P (Stut-Rem y))))
;		))
;((enable Stut-R-indstep-Num))
;)
;(disable Stut-R-indstep-Num-Rem)

; OLD induction step: not needed anymore.
;
;(prove-lemma Stut-indstep (rewrite)
;(implies (and (not (empty y))
;	      (not (empty (P y)))
;	      (not (L (P y)))
;	      )
;	 (equal (Stut-R x (P y))
;		(B (Stut-R x (P (Stut-Rem (P y)))))
;		))
;((enable Stut-R-indstep-Num-Rem B-Bn-sub1)
; (disable Bn)
; )
;)
;(disable Stut-indstep) ; potentially self-looping... 
;                       ; so we enable explicitely.


; NEW & GENERALIZED induction step hack , note: needs just ONE
; prereq! We're getting cleaner...

\end{verbatim}\begin{tabbing}{\sc Theorem}:  stut-r-indstep \\ \index{stut-r-indstep}
\=\+(($\neg$ {\rm{empty}}\,({\it{y\/}})\index{empty}) $\wedge$ ($\neg$ {\rm{l}}\,({\it{y\/}})\index{l})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{stut-r}}\,({\it{x\/}}, {\it{y\/}})\index{stut-r} $=$ {\rm{b}}\,({\rm{stut-r}}\,({\it{x\/}}, {\rm{p}}\,({\rm{stut-rem}}\,({\it{y\/}})\index{stut-rem})\index{p})\index{stut-r})\index{b})\-
\end{tabbing}

\noindent{\sc Event}:   Disable stut-r-indstep.

\addvspace{18pt}

\begin{verbatim}; all the internal stuff shouldn't be needed outside:

\end{verbatim}
\noindent{\sc Event}:   Disable stut-r.

\addvspace{18pt}

\noindent{\sc Event}:   Disable stut-num.

\addvspace{18pt}

\noindent{\sc Event}:   Disable stut-rem.

\addvspace{18pt}

\begin{verbatim}; Note: by leaving Stut, Stut-inv0, Stut-R-closed enabled, we get
;   the effect of an alternate recursive definition of Stut in the
;   most convenient form.  The remaining uncleanliness is that
;   Stut-R-indstep and Stut-R-closed match the same stuff, and need
;   to be used at different places in the main proof.  So far, we
;   survive by extreme cunning: they are in the right order, and
;   the hypothesis on Stut-R-indstep prevents wrong occurences. 
;   This is neither clear nor robust...

;; eof: th_stutter.bm


;;; ALL DOWN TO HERE IN SRCDEF.{LIB,LISP}

;;; The circuit is mostly undefined.  Here are the axioms which 
;;; give it its meaning:

; Umb-numberp: all branch targets are numbers; necessary since we 
; do Add1 and Sub1 on them, and want that to work out.

\end{verbatim}\begin{tabbing}{\sc Axiom}:  umb-numberp \\ \index{umb-numberp}
{\rm{umb}}\,({\it{x\/}}, {\it{y\/}})\index{umb} $\in\;${\bf{N}}${}$
\end{tabbing}

\begin{verbatim}; NoAd axiomatization:
; Supplying NoAddress (here: F) as the address to Wsel (here: Upd)
; leaves the RFile unchanged.  NoAd is never issued by the memory
; either as a Write or as a Read:

\end{verbatim}\begin{tabbing}{\sc Axiom}:  upd-noad \\ \index{upd-noad}
{\rm{upd}}\,({\bf{f}}, {\it{x\/}}, {\it{y\/}})\index{upd} $=$ {\it{y\/}}
\end{tabbing}
\begin{tabbing}{\sc Axiom}:  umw-noad \\ \index{umw-noad}
{\rm{umw}}\,({\it{x\/}}, {\it{y\/}})\index{umw} $\not=$ {\bf{f}}
\end{tabbing}
\begin{tabbing}{\sc Axiom}:  umr-noad \\ \index{umr-noad}
{\rm{umr}}\,({\it{x\/}}, {\it{y\/}})\index{umr} $\not=$ {\bf{f}}
\end{tabbing}

\begin{verbatim}; axiom to characterize Update and Lookup (with any non-F address 
; valid):
; Note that if we don't use the hypothesis restricting the address,
; we get an inconsistency in the theory!

\end{verbatim}\begin{tabbing}{\sc Axiom}:  ulk-upd \\ \index{ulk-upd}
\=\+({\it{ad1\/}} $\not=$ {\bf{f}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{ulk}}\,({\it{ad1\/}}, {\rm{upd}}\,({\it{ad2\/}}, {\it{dat\/}}, {\it{rf\/}})\index{upd})\index{ulk} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{ad1\/}} $=$ {\it{ad2\/}}$\;\;${\bf then }{\it{dat\/}} \\ 
{\bf else }{\rm{ulk}}\,({\it{ad1\/}}, {\it{rf\/}})\index{ulk}$\;${\bf  endif}\-)\-\-
\end{tabbing}


\begin{verbatim};;; Miscellaneous facts, simplifications, etc... about the 
;;; circuits:

; Corr-S-PR expresses that the program (Ypr) is constant in S:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  corr-s-pr \\ \index{corr-s-pr}
($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) $\rightarrow$ ({\rm{l}}\,({\rm{sy-s}}\,({\tt{'}}{\tt{ypr}}, {\it{x\/}})\index{sy-s})\index{l} $=$ {\tt{'}}{\tt{pro}})
\end{tabbing}

\begin{verbatim}; Corr-I-PR expresses that the program (Ypr) is constant in I:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  corr-i-pr \\ \index{corr-i-pr}
($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) $\rightarrow$ ({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ypr}}, {\it{x\/}})\index{sy-i})\index{l} $=$ {\tt{'}}{\tt{pro}})
\end{tabbing}

\begin{verbatim};;; Stuttering Correctness:

; StutCorr-rf-T expresses correctness WHEN stuttering, and only 
; Upd-NoAd is needed in order to prove it.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  stutcorr-rf-t \\ \index{stutcorr-rf-t}
\=\+(($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) $\wedge$ ($\neg$ {\rm{empty}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{empty}) $\wedge$ ($\neg$ {\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa1k}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-i})\index{l})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yrf}}, {\it{x\/}})\index{sy-i})\index{l} $=$ {\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yrf}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-i})\index{l})\-
\end{tabbing}

\noindent{\sc Event}:   Disable stutcorr-rf-t.

\addvspace{18pt} \begin{verbatim}; self-expanding, enable when needed


;; for PC in sy-I though, there is a fundamental difference. It
;; does NOT stutter sy-S PC, instead, there is a "virtual PC" in
;; sy-I which is a true stuttering of sy-S YPC, and which is
;; derivable from sy-I's global view, and with which sy-I RF is
;; in sync:

; comb_sub1.bm: SUB1 combinational element
; U7-DONE

; no charfun def, already defined in BM.

; Everything below generated by: (bmcomb 'sub1 '() '(x))

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

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

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

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

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

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

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

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

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

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

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

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

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

; eof:comb_sub1.bm
 ; needed for def of ivPC

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{ivpc} \\  
\=\+{\rm{ivpc}}\,({\it{x\/}})\index{ivpc} \\ 
$=$$\;\;\;\;${\rm{s-if}}\,(\=\+{\rm{sy-i}}\,({\tt{'}}{\tt{ybc0}}, {\it{x\/}})\index{sy-i}, \\ 
{\rm{sy-i}}\,({\tt{'}}{\tt{ybt0}}, {\it{x\/}})\index{sy-i}, \\ 
{\rm{s-if}}\,(\=\+{\rm{s-not}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa3}}, {\it{x\/}})\index{sy-i})\index{s-not}, \\ 
{\rm{sy-i}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-i}, \\ 
{\rm{s-if}}\,(\=\+{\rm{s-not}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa2}}, {\it{x\/}})\index{sy-i})\index{s-not}, \\ 
{\rm{s-sub1}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-i})\index{s-sub1}, \\ 
{\rm{s-if}}\,(\=\+{\rm{s-not}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa1}}, {\it{x\/}})\index{sy-i})\index{s-not}, \\ 
{\rm{s-sub1}}\,({\rm{s-sub1}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-i})\index{s-sub1})\index{s-sub1}, \\ 
{\rm{s-sub1}}\,({\rm{s-sub1}}\,({\rm{s-sub1}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-i})\index{s-sub1})\index{s-sub1})\index{s-sub1})\-\index{s-if})\-\index{s-if})\-\index{s-if})\-\index{s-if}\-
\end{tabbing}

\noindent{\sc Event}:   Disable ivpc.

\addvspace{18pt} \begin{verbatim}; we'll enable when needed


; sy-I-PC-numberp is a type lemma about I-PC and the branch targets
; needed for future add1-sub1 manipulation.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  sy-i-pc-numberp \\ \index{sy-i-pc-numberp}
\=\+($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-i})\index{l} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ybt0}}, {\it{x\/}})\index{sy-i})\index{l} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ybt1}}, {\it{x\/}})\index{sy-i})\index{l} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ybt2}}, {\it{x\/}})\index{sy-i})\index{l} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ybt3}}, {\it{x\/}})\index{sy-i})\index{l} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ybt4}}, {\it{x\/}})\index{sy-i})\index{l} $\in\;${\bf{N}}${}$))\-\-
\end{tabbing}

\begin{verbatim}; Useful abbreviations about the semantics of the circuit:

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{res} \\  
{\rm{res}}\,({\it{pc\/}}, {\it{rf\/}})\index{res} $=$ {\rm{ualu}}\,({\rm{umf}}\,({\it{pc\/}}, {\tt{'}}{\tt{pro}})\index{umf}, {\rm{ulk}}\,({\rm{umr}}\,({\it{pc\/}}, {\tt{'}}{\tt{pro}})\index{umr}, {\it{rf\/}})\index{ulk})\index{ualu}
\end{tabbing}

\noindent{\sc Event}:   Disable res.

\addvspace{18pt}

\begin{verbatim}; n-pc is "Next PC"
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{n-pc} \\  
{\rm{n-pc}}\,({\it{pc\/}}, {\it{rf\/}})\index{n-pc} $=$ {\rm{mux}}\,({\rm{eql0}}\,({\rm{res}}\,({\it{pc\/}}, {\it{rf\/}})\index{res})\index{eql0}, {\rm{umb}}\,({\it{pc\/}}, {\tt{'}}{\tt{pro}})\index{umb}, $1\;+$ {\it{pc\/}})\index{mux}
\end{tabbing}

\noindent{\sc Event}:   Disable n-pc.

\addvspace{18pt}

\begin{verbatim}; n-rf is "Next RF"
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{n-rf}$\;\;$
{\rm{n-rf}}\,({\it{pc\/}}, {\it{rf\/}})\index{n-rf} $=$ {\rm{upd}}\,({\rm{umw}}\,({\it{pc\/}}, {\tt{'}}{\tt{pro}})\index{umw}, {\rm{res}}\,({\it{pc\/}}, {\it{rf\/}})\index{res}, {\it{rf\/}})\index{upd}
\end{tabbing}

\noindent{\sc Event}:   Disable n-rf.

\addvspace{18pt}

\begin{verbatim}; Now we prove that they are "correct", with respect to our intent. 
; Even though we don't use the next 3 lemmas anywhere else, they
; are a useful check - and during the development, help raise my
; confidence level! Moreover, they would be useful if we ever
; wanted to prove properties of the specification circuit (sy-S). 

\end{verbatim}\begin{tabbing}{\sc Theorem}:  corr-n-pc \\ \index{corr-n-pc}
\=\+(($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) $\wedge$ ($\neg$ {\rm{empty}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{empty})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{l}}\,({\rm{sy-s}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-s})\index{l} $=$ {\rm{n-pc}}\,({\rm{l}}\,({\rm{sy-s}}\,({\tt{'}}{\tt{ypc}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-s})\index{l}, {\rm{l}}\,({\rm{sy-s}}\,({\tt{'}}{\tt{yrf}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-s})\index{l})\index{n-pc})\-
\end{tabbing}

\noindent{\sc Event}:   Disable corr-n-pc.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  corr-n-rf \\ \index{corr-n-rf}
\=\+(($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) $\wedge$ ($\neg$ {\rm{empty}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{empty})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{l}}\,({\rm{sy-s}}\,({\tt{'}}{\tt{yrf}}, {\it{x\/}})\index{sy-s})\index{l} $=$ {\rm{n-rf}}\,({\rm{l}}\,({\rm{sy-s}}\,({\tt{'}}{\tt{ypc}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-s})\index{l}, {\rm{l}}\,({\rm{sy-s}}\,({\tt{'}}{\tt{yrf}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-s})\index{l})\index{n-rf})\-
\end{tabbing}

\noindent{\sc Event}:   Disable corr-n-rf.

\addvspace{18pt}

\begin{verbatim}; Corr-S-PR-H and Corr-I-PR-H could be earlier, with the rest of 
; the constant treatment for PR, but here is where they were 
; needed & proved.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  corr-s-pr-h \\ \index{corr-s-pr-h}
($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) $\rightarrow$ ({\rm{h}}\,({\rm{sy-s}}\,({\tt{'}}{\tt{ypr}}, {\it{x\/}})\index{sy-s})\index{h} $=$ {\tt{'}}{\tt{pro}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  corr-i-pr-h \\ \index{corr-i-pr-h}
($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) $\rightarrow$ ({\rm{h}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ypr}}, {\it{x\/}})\index{sy-i})\index{h} $=$ {\tt{'}}{\tt{pro}})
\end{tabbing}


\begin{verbatim}; REVERSAL PROPERTies for sy-S:
;  The SAME EXPAND hint as for Corr-n-pc and Corr-n-rf work.

; sy-S-reversal-pr is FUNDAMENTALLY DIFFERENT because we don't want
; to keep PR as part of the global state, so we deduce an equality
; by induction:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  sy-s-reversal-pr \\ \index{sy-s-reversal-pr}
($\neg$ {\rm{empty}}\,({\rm{bn}}\,({\it{n\/}}, {\rm{sy-s}}\,({\tt{'}}{\tt{ypr}}, {\it{x\/}})\index{sy-s})\index{bn})\index{empty}) $\rightarrow$ ({\rm{h}}\,({\rm{bn}}\,({\it{n\/}}, {\rm{sy-s}}\,({\tt{'}}{\tt{ypr}}, {\it{x\/}})\index{sy-s})\index{bn})\index{h} $=$ {\tt{'}}{\tt{pro}})
\end{tabbing}


\begin{verbatim}; we need a few simple props of ivPC for the main induction, 
; because we have to run with ivPC disabled there:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  ivpc-e \\ \index{ivpc-e}
{\rm{empty}}\,({\it{x\/}})\index{empty} $\rightarrow$ ({\rm{ivpc}}\,({\it{x\/}})\index{ivpc} $=$ {\sc{e}}\index{e})
\end{tabbing}

\noindent{\sc Event}:   Disable ivpc-e.

\addvspace{18pt} \begin{verbatim}; enable as needed

\end{verbatim}\begin{tabbing}{\sc Theorem}:  ivpc-1 \\ \index{ivpc-1}
(($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) $\wedge$ {\rm{empty}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{empty}) $\rightarrow$ ({\rm{l}}\,({\rm{ivpc}}\,({\it{x\/}})\index{ivpc})\index{l} $=$ {\sc{pci}}\index{pci})
\end{tabbing}

\noindent{\sc Event}:   Disable ivpc-1.

\addvspace{18pt} \begin{verbatim}; enable as needed


; Junction (hack) lemma between the 2 hyps to get the reversals:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  sy-s-reversal-hyp-hack \\ \index{sy-s-reversal-hyp-hack}
($\neg$ {\rm{empty}}\,({\rm{bn}}\,({\it{n\/}}, {\rm{sy-s}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-s})\index{bn})\index{empty}) $\rightarrow$ ($\neg$ {\rm{empty}}\,({\rm{bn}}\,({\it{n\/}}, {\rm{sy-s}}\,({\tt{'}}{\tt{ypr}}, {\it{x\/}})\index{sy-s})\index{bn})\index{empty})
\end{tabbing}


\noindent{\sc Event}:   Disable sy-s-reversal-hyp-hack.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  sy-s-reversal-pc \\ \index{sy-s-reversal-pc}
\=\+(\=\+($\neg$ {\rm{empty}}\,({\rm{bn}}\,({\it{n\/}}, {\rm{sy-s}}\,({\tt{'}}{\tt{ypc}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-s})\index{bn})\index{empty}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{empty}}\,({\rm{bn}}\,({\it{n\/}}, {\rm{sy-s}}\,({\tt{'}}{\tt{yrf}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-s})\index{bn})\index{empty}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{h}}\,({\rm{b}}\,({\rm{bn}}\,({\it{n\/}}, {\rm{sy-s}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-s})\index{bn})\index{b})\index{h} \\ 
$=$$\;\;\;\;${\rm{n-pc}}\,({\rm{h}}\,({\rm{bn}}\,({\it{n\/}}, {\rm{sy-s}}\,({\tt{'}}{\tt{ypc}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-s})\index{bn})\index{h}, {\rm{h}}\,({\rm{bn}}\,({\it{n\/}}, {\rm{sy-s}}\,({\tt{'}}{\tt{yrf}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-s})\index{bn})\index{h})\index{n-pc})\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  sy-s-reversal-rf \\ \index{sy-s-reversal-rf}
\=\+(\=\+($\neg$ {\rm{empty}}\,({\rm{bn}}\,({\it{n\/}}, {\rm{sy-s}}\,({\tt{'}}{\tt{ypc}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-s})\index{bn})\index{empty}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{empty}}\,({\rm{bn}}\,({\it{n\/}}, {\rm{sy-s}}\,({\tt{'}}{\tt{yrf}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-s})\index{bn})\index{empty}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{h}}\,({\rm{b}}\,({\rm{bn}}\,({\it{n\/}}, {\rm{sy-s}}\,({\tt{'}}{\tt{yrf}}, {\it{x\/}})\index{sy-s})\index{bn})\index{b})\index{h} \\ 
$=$$\;\;\;\;${\rm{n-rf}}\,({\rm{h}}\,({\rm{bn}}\,({\it{n\/}}, {\rm{sy-s}}\,({\tt{'}}{\tt{ypc}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-s})\index{bn})\index{h}, {\rm{h}}\,({\rm{bn}}\,({\it{n\/}}, {\rm{sy-s}}\,({\tt{'}}{\tt{yrf}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-s})\index{bn})\index{h})\index{n-rf})\-\-
\end{tabbing}


\begin{verbatim};; Now we develop the FUNDAMENTAL INVARIANT for sy-I :

; Level is the only one which needs RES enabled, and it's also
; a bit different from the others, because it's never "reset".


; sy-I-Yra-noad tells BM Yra is always an OK address, in a usable 
; way.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  sy-i-yra-noad \\ \index{sy-i-yra-noad}
\=\+($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{ulk}}\,({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yra}}, {\it{x\/}})\index{sy-i})\index{l}, {\rm{upd}}\,({\it{ad\/}}, {\it{dat\/}}, {\it{rf\/}})\index{upd})\index{ulk} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yra}}, {\it{x\/}})\index{sy-i})\index{l} $=$ {\it{ad\/}}$\;\;${\bf then }{\it{dat\/}} \\ 
{\bf else }{\rm{ulk}}\,({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yra}}, {\it{x\/}})\index{sy-i})\index{l}, {\it{rf\/}})\index{ulk}$\;${\bf  endif}\-)\-\-
\end{tabbing}


\begin{verbatim}; We prove the equalities for YRD lines separately, to minimize 
; the mess! 
\end{verbatim}\begin{tabbing}{\sc Theorem}:  sy-i-yrd1 \\ \index{sy-i-yrd1}
\=\+($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yrd1}}, {\it{x\/}})\index{sy-i})\index{l} \\ 
$=$$\;\;\;\;${\rm{ulk}}\,(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yra}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{upd}}\,(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa1}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywd1}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yrf}}, {\it{x\/}})\index{sy-i})\index{l})\-\index{upd})\-\index{ulk})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sy-i-yrd2 \\ \index{sy-i-yrd2}
\=\+($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yrd2}}, {\it{x\/}})\index{sy-i})\index{l} \\ 
$=$$\;\;\;\;${\rm{ulk}}\,(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yra}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{upd}}\,(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa2}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywd2}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{upd}}\,(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa1}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywd1}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yrf}}, {\it{x\/}})\index{sy-i})\index{l})\-\index{upd})\-\index{upd})\-\index{ulk})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sy-i-yrd3 \\ \index{sy-i-yrd3}
\=\+($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yrd3}}, {\it{x\/}})\index{sy-i})\index{l} \\ 
$=$$\;\;\;\;${\rm{ulk}}\,(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yra}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{upd}}\,(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa3}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywd3}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{upd}}\,(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa2}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywd2}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{upd}}\,(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa1}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywd1}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yrf}}, {\it{x\/}})\index{sy-i})\index{l})\-\index{upd})\-\index{upd})\-\index{upd})\-\index{ulk})\-\-
\end{tabbing}

\begin{verbatim}; now we do the invariants, per level:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  sy-i-inv-4 \\ \index{sy-i-inv-4}
\=\+($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ybc4}}, {\it{x\/}})\index{sy-i})\index{l} $=$ {\rm{eql0}}\,({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywd4}}, {\it{x\/}})\index{sy-i})\index{l})\index{eql0}) \\ 
$\wedge$$\;\;\;\;$({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ybt4}}, {\it{x\/}})\index{sy-i})\index{l} $=$ {\rm{umb}}\,({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-i})\index{l}, {\tt{'}}{\tt{pro}})\index{umb}) \\ 
$\wedge$$\;\;\;\;$({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa4}}, {\it{x\/}})\index{sy-i})\index{l} $=$ {\rm{umw}}\,({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-i})\index{l}, {\tt{'}}{\tt{pro}})\index{umw}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywd4}}, {\it{x\/}})\index{sy-i})\index{l} \\ 
$=$$\;\;\;\;${\rm{res}}\,(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{upd}}\,(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa3}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywd3}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{upd}}\,(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa2}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywd2}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{upd}}\,(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa1}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywd1}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yrf}}, {\it{x\/}})\index{sy-i})\index{l})\-\index{upd})\-\index{upd})\-\index{upd})\-\index{res})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yrd3}}, {\it{x\/}})\index{sy-i})\index{l} \\ 
$=$$\;\;\;\;${\rm{ulk}}\,(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yra}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{upd}}\,(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa3}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywd3}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{upd}}\,(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa2}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywd2}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{upd}}\,(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa1}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywd1}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yrf}}, {\it{x\/}})\index{sy-i})\index{l})\-\index{upd})\-\index{upd})\-\index{upd})\-\index{ulk})\-)\-\-
\end{tabbing}



\noindent{\sc Event}:   Disable sy-i-yrd1.

\addvspace{18pt}

\noindent{\sc Event}:   Disable sy-i-yrd2.

\addvspace{18pt}

\noindent{\sc Event}:   Disable sy-i-yrd3.

\addvspace{18pt}

\begin{verbatim}; Note that we repeat sy-I-Yrdn for each n, and this may be costly 
; later. On the other hand, it's nice to have one property which 
; expresses the "complete" correctness of a stage.


\end{verbatim}\begin{tabbing}{\sc Theorem}:  sy-i-inv-3 \\ \index{sy-i-inv-3}
\=\+($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) \\ 
$\rightarrow$$\;\;\;\;$\=\+{\bf if }$\neg$ {\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa3}}, {\it{x\/}})\index{sy-i})\index{l} \\ 
{\bf then }($\neg$ {\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ybc3}}, {\it{x\/}})\index{sy-i})\index{l}) $\wedge$ ($\neg$ {\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa2}}, {\it{x\/}})\index{sy-i})\index{l}) \\ 
{\bf else }\=\+({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ybc3}}, {\it{x\/}})\index{sy-i})\index{l} $=$ {\rm{eql0}}\,({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywd3}}, {\it{x\/}})\index{sy-i})\index{l})\index{eql0}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ybt3}}, {\it{x\/}})\index{sy-i})\index{l} \\ 
$=$$\;\;\;\;${\rm{umb}}\,({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-i})\index{l} $-\;1$, {\tt{'}}{\tt{pro}})\index{umb})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa3}}, {\it{x\/}})\index{sy-i})\index{l} \\ 
$=$$\;\;\;\;${\rm{umw}}\,({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-i})\index{l} $-\;1$, {\tt{'}}{\tt{pro}})\index{umw})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywd3}}, {\it{x\/}})\index{sy-i})\index{l} \\ 
$=$$\;\;\;\;${\rm{res}}\,(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-i})\index{l} $-\;1$, \\ 
{\rm{upd}}\,(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa2}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywd2}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{upd}}\,(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa1}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywd1}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yrf}}, {\it{x\/}})\index{sy-i})\index{l})\-\index{upd})\-\index{upd})\-\index{res})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yrd2}}, {\it{x\/}})\index{sy-i})\index{l} \\ 
$=$$\;\;\;\;${\rm{ulk}}\,(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yra}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{upd}}\,(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa2}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywd2}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{upd}}\,(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa1}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywd1}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yrf}}, {\it{x\/}})\index{sy-i})\index{l})\-\index{upd})\-\index{upd})\-\index{ulk})\-\-$\;${\bf  endif}\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  sy-i-inv-2 \\ \index{sy-i-inv-2}
\=\+($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) \\ 
$\rightarrow$$\;\;\;\;$\=\+{\bf if }$\neg$ {\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa2}}, {\it{x\/}})\index{sy-i})\index{l} \\ 
{\bf then }($\neg$ {\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ybc2}}, {\it{x\/}})\index{sy-i})\index{l}) $\wedge$ ($\neg$ {\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa1}}, {\it{x\/}})\index{sy-i})\index{l}) \\ 
{\bf else }\=\+({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ybc2}}, {\it{x\/}})\index{sy-i})\index{l} $=$ {\rm{eql0}}\,({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywd2}}, {\it{x\/}})\index{sy-i})\index{l})\index{eql0}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ybt2}}, {\it{x\/}})\index{sy-i})\index{l} \\ 
$=$$\;\;\;\;${\rm{umb}}\,(({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-i})\index{l} $-\;1$) $-\;1$, {\tt{'}}{\tt{pro}})\index{umb})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa2}}, {\it{x\/}})\index{sy-i})\index{l} \\ 
$=$$\;\;\;\;${\rm{umw}}\,(({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-i})\index{l} $-\;1$) $-\;1$, {\tt{'}}{\tt{pro}})\index{umw})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywd2}}, {\it{x\/}})\index{sy-i})\index{l} \\ 
$=$$\;\;\;\;${\rm{res}}\,(\=\+({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-i})\index{l} $-\;1$) $-\;1$, \\ 
{\rm{upd}}\,(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa1}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywd1}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yrf}}, {\it{x\/}})\index{sy-i})\index{l})\-\index{upd})\-\index{res})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yrd1}}, {\it{x\/}})\index{sy-i})\index{l} \\ 
$=$$\;\;\;\;${\rm{ulk}}\,(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yra}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{upd}}\,(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa1}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywd1}}, {\it{x\/}})\index{sy-i})\index{l}, \\ 
{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yrf}}, {\it{x\/}})\index{sy-i})\index{l})\-\index{upd})\-\index{ulk})\-\-$\;${\bf  endif}\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  sy-i-inv-1 \\ \index{sy-i-inv-1}
\=\+($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) \\ 
$\rightarrow$$\;\;\;\;$\=\+{\bf if }$\neg$ {\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa1}}, {\it{x\/}})\index{sy-i})\index{l}$\;\;${\bf then }$\neg$ {\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ybc1}}, {\it{x\/}})\index{sy-i})\index{l} \\ 
{\bf else }\=\+({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ybc1}}, {\it{x\/}})\index{sy-i})\index{l} $=$ {\rm{eql0}}\,({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywd1}}, {\it{x\/}})\index{sy-i})\index{l})\index{eql0}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ybt1}}, {\it{x\/}})\index{sy-i})\index{l} \\ 
$=$$\;\;\;\;${\rm{umb}}\,((({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-i})\index{l} $-\;1$) $-\;1$) $-\;1$, {\tt{'}}{\tt{pro}})\index{umb})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa1}}, {\it{x\/}})\index{sy-i})\index{l} \\ 
$=$$\;\;\;\;${\rm{umw}}\,((({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-i})\index{l} $-\;1$) $-\;1$) $-\;1$, {\tt{'}}{\tt{pro}})\index{umw})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywd1}}, {\it{x\/}})\index{sy-i})\index{l} \\ 
$=$$\;\;\;\;${\rm{res}}\,(\=\+(({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-i})\index{l} $-\;1$) $-\;1$) $-\;1$, \\ 
{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yrf}}, {\it{x\/}})\index{sy-i})\index{l})\-\index{res})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yrd}}, {\it{x\/}})\index{sy-i})\index{l} \\ 
$=$$\;\;\;\;${\rm{ulk}}\,({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yra}}, {\it{x\/}})\index{sy-i})\index{l}, {\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yrf}}, {\it{x\/}})\index{sy-i})\index{l})\index{ulk})\-\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; NOTES:
; .  Having the invariants written as above entail the cost of 
; carrying lots of irrelevant information in each proof, and 
; potentially crushing BM.  So instead we'll phrase each needed
; property later as a good rewrite, and prove it by instantiating
; the right invariant(s).
; .  What we did is a hand-induction on the DEPTH of the pipeline.
; Notice that NO explicit induction was necessary, simply proving
; the thms in the right order (4-3-2-1)..


; StutCorr-pc-T expresses correctness of ivPC WHEN stuttering.

; We rewrite just the portions of the invariants we need for 
; StutCorr-pc-T so that BM will get that proof in finite time...

\end{verbatim}\begin{tabbing}{\sc Theorem}:  sc-pc-t-1 \\ \index{sc-pc-t-1}
($\neg$ {\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa1}}, {\it{x\/}})\index{sy-i})\index{l}) $\rightarrow$ ($\neg$ {\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ybc1}}, {\it{x\/}})\index{sy-i})\index{l})
\end{tabbing}

\noindent{\sc Event}:   Disable sc-pc-t-1.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  sc-pc-t-2 \\ \index{sc-pc-t-2}
($\neg$ {\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa2}}, {\it{x\/}})\index{sy-i})\index{l}) $\rightarrow$ ($\neg$ {\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ybc2}}, {\it{x\/}})\index{sy-i})\index{l})
\end{tabbing}

\noindent{\sc Event}:   Disable sc-pc-t-2.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  sc-pc-t-3 \\ \index{sc-pc-t-3}
($\neg$ {\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa3}}, {\it{x\/}})\index{sy-i})\index{l}) $\rightarrow$ ($\neg$ {\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ybc3}}, {\it{x\/}})\index{sy-i})\index{l})
\end{tabbing}

\noindent{\sc Event}:   Disable sc-pc-t-3.

\addvspace{18pt}


\begin{tabbing}{\sc Theorem}:  stutcorr-pc-t \\ \index{stutcorr-pc-t}
\=\+(($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) $\wedge$ ($\neg$ {\rm{empty}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{empty}) $\wedge$ ($\neg$ {\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa1k}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-i})\index{l})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{l}}\,({\rm{ivpc}}\,({\it{x\/}})\index{ivpc})\index{l} $=$ {\rm{l}}\,({\rm{ivpc}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{ivpc})\index{l})\-
\end{tabbing}

\noindent{\sc Event}:   Disable stutcorr-pc-t.

\addvspace{18pt} \begin{verbatim}; self-expanding, enable when needed


; Now we express the "on the right also" invariants in a useful 
; manner...

\end{verbatim}\begin{tabbing}{\sc Theorem}:  sc-pc-f-3 \\ \index{sc-pc-f-3}
($\neg$ {\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa3}}, {\it{x\/}})\index{sy-i})\index{l}) $\rightarrow$ ($\neg$ {\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa2}}, {\it{x\/}})\index{sy-i})\index{l})
\end{tabbing}

\noindent{\sc Event}:   Disable sc-pc-f-3.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  sc-pc-f-2 \\ \index{sc-pc-f-2}
($\neg$ {\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa2}}, {\it{x\/}})\index{sy-i})\index{l}) $\rightarrow$ ($\neg$ {\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa1}}, {\it{x\/}})\index{sy-i})\index{l})
\end{tabbing}

\noindent{\sc Event}:   Disable sc-pc-f-2.

\addvspace{18pt}


\begin{verbatim}; In order to get the arithmetic to work out, we have to prove that
; we never subtract from zero...

\end{verbatim}\begin{tabbing}{\sc Theorem}:  sc-pcn0-0 \\ \index{sc-pcn0-0}
\=\+(($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) $\wedge$ ($\neg$ {\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa2}}, {\it{x\/}})\index{sy-i})\index{l}) $\wedge$ {\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa3}}, {\it{x\/}})\index{sy-i})\index{l}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-i})\index{l} $\not=$ {\tt{0}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sc-pcn0-1 \\ \index{sc-pcn0-1}
\=\+(\=\+($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa1}}, {\it{x\/}})\index{sy-i})\index{l}) \\ 
$\wedge$$\;\;\;\;${\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa2}}, {\it{x\/}})\index{sy-i})\index{l} \\ 
$\wedge$$\;\;\;\;${\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa3}}, {\it{x\/}})\index{sy-i})\index{l})\- \\ 
$\rightarrow$$\;\;\;\;$(({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-i})\index{l} $-\;1$) $\not=$ {\tt{0}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sc-pcn0-2 \\ \index{sc-pcn0-2}
\=\+(\=\+($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) \\ 
$\wedge$$\;\;\;\;${\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa1}}, {\it{x\/}})\index{sy-i})\index{l} \\ 
$\wedge$$\;\;\;\;${\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa3}}, {\it{x\/}})\index{sy-i})\index{l} \\ 
$\wedge$$\;\;\;\;${\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa2}}, {\it{x\/}})\index{sy-i})\index{l})\- \\ 
$\rightarrow$$\;\;\;\;$((({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-i})\index{l} $-\;1$) $-\;1$) $\not=$ {\tt{0}})\-
\end{tabbing}

\begin{verbatim}; Now it goes through:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  stutcorr-pc-f \\ \index{stutcorr-pc-f}
\=\+(($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) $\wedge$ ($\neg$ {\rm{empty}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{empty}) $\wedge$ {\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa1k}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-i})\index{l}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{l}}\,({\rm{ivpc}}\,({\it{x\/}})\index{ivpc})\index{l} $=$ {\rm{n-pc}}\,({\rm{l}}\,({\rm{ivpc}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{ivpc})\index{l}, {\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yrf}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-i})\index{l})\index{n-pc})\-
\end{tabbing}

\noindent{\sc Event}:   Disable stutcorr-pc-f.

\addvspace{18pt}



\begin{tabbing}{\sc Theorem}:  stutcorr-rf-f \\ \index{stutcorr-rf-f}
\=\+(($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) $\wedge$ ($\neg$ {\rm{empty}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{empty}) $\wedge$ {\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa1k}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-i})\index{l}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yrf}}, {\it{x\/}})\index{sy-i})\index{l} $=$ {\rm{n-rf}}\,({\rm{l}}\,({\rm{ivpc}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{ivpc})\index{l}, {\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yrf}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-i})\index{l})\index{n-rf})\-
\end{tabbing}

\noindent{\sc Event}:   Disable stutcorr-rf-f.

\addvspace{18pt}


\begin{verbatim}; We have to simultaneously prove stuttering of RF and ivPC:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  stutcorr-l \\ \index{stutcorr-l}
\=\+({\rm{l}}\,({\rm{stut}}\,({\rm{sy-s}}\,({\tt{'}}{\tt{ypc}}, {\it{x\/}})\index{sy-s}, {\rm{s-not}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa1k}}, {\it{x\/}})\index{sy-i})\index{s-not})\index{stut})\index{l} $=$ {\rm{l}}\,({\rm{ivpc}}\,({\it{x\/}})\index{ivpc})\index{l}) \\ 
$\wedge$$\;\;\;\;$({\rm{l}}\,({\rm{stut}}\,({\rm{sy-s}}\,({\tt{'}}{\tt{yrf}}, {\it{x\/}})\index{sy-s}, {\rm{s-not}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa1k}}, {\it{x\/}})\index{sy-i})\index{s-not})\index{stut})\index{l} $=$ {\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yrf}}, {\it{x\/}})\index{sy-i})\index{l})\-
\end{tabbing}

\begin{verbatim}; Now standard passage to strings:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  apl-split-irf \\ \index{apl-split-irf}
\=\+($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{sy-i}}\,({\tt{'}}{\tt{yrf}}, {\it{x\/}})\index{sy-i} $=$ {\rm{a}}\,({\rm{p}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yrf}}, {\it{x\/}})\index{sy-i})\index{p}, {\rm{l}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{yrf}}, {\it{x\/}})\index{sy-i})\index{l})\index{a})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  apl-split-stut \\ \index{apl-split-stut}
\=\+($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{stut}}\,({\rm{sy-s}}\,({\tt{'}}{\tt{yrf}}, {\it{x\/}})\index{sy-s}, {\rm{s-not}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa1k}}, {\it{x\/}})\index{sy-i})\index{s-not})\index{stut} \\ 
$=$$\;\;\;\;${\rm{a}}\,(\=\+{\rm{p}}\,({\rm{stut}}\,({\rm{sy-s}}\,({\tt{'}}{\tt{yrf}}, {\it{x\/}})\index{sy-s}, {\rm{s-not}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa1k}}, {\it{x\/}})\index{sy-i})\index{s-not})\index{stut})\index{p}, \\ 
{\rm{l}}\,({\rm{stut}}\,({\rm{sy-s}}\,({\tt{'}}{\tt{yrf}}, {\it{x\/}})\index{sy-s}, {\rm{s-not}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa1k}}, {\it{x\/}})\index{sy-i})\index{s-not})\index{stut})\index{l})\-\index{a})\-\-
\end{tabbing}


\begin{verbatim}; YEEEEAHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHH!

\end{verbatim}\begin{tabbing}{\sc Theorem}:  src-cpu-correct \\ \index{src-cpu-correct}
{\rm{stut}}\,({\rm{sy-s}}\,({\tt{'}}{\tt{yrf}}, {\it{x\/}})\index{sy-s}, {\rm{s-not}}\,({\rm{sy-i}}\,({\tt{'}}{\tt{ywa1k}}, {\it{x\/}})\index{sy-i})\index{s-not})\index{stut} $=$ {\rm{sy-i}}\,({\tt{'}}{\tt{yrf}}, {\it{x\/}})\index{sy-i}
\end{tabbing}

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