\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}; countstut.bm: a simple clock counter, and a STUTTERING version of it,
;     to test Stutter formalizaton. 
;
; . A2PC blows up on stuttering version, but that's been reduced to a
; a very trivial version (3 lines) which also blows up and on which one
; can see that BM loops without any rule: one of the equality hyp. is used
; in the opposite direction as the definition expansion.  
; We use ADD-AXIOM on A2-PCs which blow.
;

;;; DEFINITION OF CIRCUITs:
#|
(setq A '(sy-A (x)
(Yout R 0 Y1)
(Y1 S Inc Yout)
))

(setq B '(sy-B (x)
(Yout R 0 Y1m)
(Y1m S Mux Yst Yout Y1)
(Y1 S Inc Yout)
(Yst R T Yst1)
(Yst1 S Not Yst)
))

(setq C '(sy-C (xst)
(Yout R 0 Y1m)
(Y1m S Mux xst Yout Y1)
(Y1 S Inc Yout)
))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

; eof:comb_inc.bm


\end{verbatim}\begin{tabbing}{\sc Definition}:\index{topor-sy-a} \\  
\=\+{\rm{topor-sy-a}}\,({\it{ln\/}})\index{topor-sy-a} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{ln\/}} $=$ {\tt{'}}{\tt{yout}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y1}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{sy-a} \\  
\=\+{\rm{sy-a}}\,({\it{ln\/}}, {\it{x\/}})\index{sy-a} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{ln\/}} $=$ {\tt{'}}{\tt{yout}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{0}}, {\rm{sy-a}}\,({\tt{'}}{\tt{y1}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-a})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y1}}$\;\;${\bf then }{\rm{s-inc}}\,({\rm{sy-a}}\,({\tt{'}}{\tt{yout}}, {\it{x\/}})\index{sy-a})\index{s-inc} \\ 
{\bf else }{\rm{sfix}}\,({\it{x\/}})\index{sfix}$\;${\bf  endif}\-\-
\end{tabbing}

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

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

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

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

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

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

\begin{verbatim};; A2-End-SY-A
; BM DEFINITIONS and A2 LEMMAS, generated by BMSYSD:
; 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

;; already loaded in A: (LOAD "Comb/comb_inc.bm")

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{topor-sy-b} \\  
\=\+{\rm{topor-sy-b}}\,({\it{ln\/}})\index{topor-sy-b} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{ln\/}} $=$ {\tt{'}}{\tt{yout}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y1m}}$\;\;${\bf then }{\tt{2}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y1}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yst}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yst1}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{sy-b} \\  
\=\+{\rm{sy-b}}\,({\it{ln\/}}, {\it{x\/}})\index{sy-b} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{ln\/}} $=$ {\tt{'}}{\tt{yout}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{0}}, {\rm{sy-b}}\,({\tt{'}}{\tt{y1m}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y1m}} \\ 
{\bf then }{\rm{s-mux}}\,({\rm{sy-b}}\,({\tt{'}}{\tt{yst}}, {\it{x\/}})\index{sy-b}, {\rm{sy-b}}\,({\tt{'}}{\tt{yout}}, {\it{x\/}})\index{sy-b}, {\rm{sy-b}}\,({\tt{'}}{\tt{y1}}, {\it{x\/}})\index{sy-b})\index{s-mux} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y1}}$\;\;${\bf then }{\rm{s-inc}}\,({\rm{sy-b}}\,({\tt{'}}{\tt{yout}}, {\it{x\/}})\index{sy-b})\index{s-inc} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yst}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\bf{t}}, {\rm{sy-b}}\,({\tt{'}}{\tt{yst1}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yst1}}$\;\;${\bf then }{\rm{s-not}}\,({\rm{sy-b}}\,({\tt{'}}{\tt{yst}}, {\it{x\/}})\index{sy-b})\index{s-not} \\ 
{\bf else }{\rm{sfix}}\,({\it{x\/}})\index{sfix}$\;${\bf  endif}\-\-
\end{tabbing}

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

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

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

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

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

\begin{verbatim}; See note at top of file.
;(PROVE-LEMMA A2-PC-SY-B (REWRITE)
;    (EQUAL (P (SY-B LN X)) (SY-B LN (P X)))
;    ((DISABLE S-MUX S-INC S-NOT A2-IC-S-MUX A2-IC-S-INC A2-IC-S-NOT)))
\end{verbatim}\begin{tabbing}{\sc Axiom}:  a2-pc-sy-b \\ \index{a2-pc-sy-b}
{\rm{p}}\,({\rm{sy-b}}\,({\it{ln\/}}, {\it{xst\/}})\index{sy-b})\index{p} $=$ {\rm{sy-b}}\,({\it{ln\/}}, {\rm{p}}\,({\it{xst\/}})\index{p})\index{sy-b}
\end{tabbing}

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

; BM DEFINITIONS and A2 LEMMAS, generated by BMSYSD:
;; already loaded: (LOAD "Comb/comb_mux.bm")
;; already loaded: (LOAD "Comb/comb_inc.bm")

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{topor-sy-c} \\  
\=\+{\rm{topor-sy-c}}\,({\it{ln\/}})\index{topor-sy-c} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{ln\/}} $=$ {\tt{'}}{\tt{yout}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y1m}}$\;\;${\bf then }{\tt{2}} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y1}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{sy-c} \\  
\=\+{\rm{sy-c}}\,({\it{ln\/}}, {\it{xst\/}})\index{sy-c} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{ln\/}} $=$ {\tt{'}}{\tt{yout}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xst\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{0}}, {\rm{sy-c}}\,({\tt{'}}{\tt{y1m}}, {\rm{p}}\,({\it{xst\/}})\index{p})\index{sy-c})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y1m}}$\;\;${\bf then }{\rm{s-mux}}\,({\it{xst\/}}, {\rm{sy-c}}\,({\tt{'}}{\tt{yout}}, {\it{xst\/}})\index{sy-c}, {\rm{sy-c}}\,({\tt{'}}{\tt{y1}}, {\it{xst\/}})\index{sy-c})\index{s-mux} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{y1}}$\;\;${\bf then }{\rm{s-inc}}\,({\rm{sy-c}}\,({\tt{'}}{\tt{yout}}, {\it{xst\/}})\index{sy-c})\index{s-inc} \\ 
{\bf else }{\rm{sfix}}\,({\it{xst\/}})\index{sfix}$\;${\bf  endif}\-\-
\end{tabbing}

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

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

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

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

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

\begin{verbatim}; blows..
;(PROVE-LEMMA A2-PC-SY-C (REWRITE)
;    (EQUAL (P (SY-C LN XST)) (SY-C LN (P XST)))
;    ((DISABLE S-MUX S-INC A2-IC-S-MUX A2-IC-S-INC)))
; so TEMPORARILY:
\end{verbatim}\begin{tabbing}{\sc Axiom}:  a2-pc-sy-c \\ \index{a2-pc-sy-c}
{\rm{p}}\,({\rm{sy-c}}\,({\it{ln\/}}, {\it{xst\/}})\index{sy-c})\index{p} $=$ {\rm{sy-c}}\,({\it{ln\/}}, {\rm{p}}\,({\it{xst\/}})\index{p})\index{sy-c}
\end{tabbing}

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

;;; BEGIN: Circuit CORRECTNESS modulo Stuttering.

;; BEGIN: new 2nd order properties for combinationals.

;; END: new 2nd order properties for combinationals.

;;; 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


;; BEGIN: ACTUAL Circuit CORRECTNESS modulo Stuttering.

; REVERSAL PROPERTY for sy-a:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  sy-a-reversal \\ \index{sy-a-reversal}
\=\+($\neg$ {\rm{empty}}\,({\rm{bn}}\,({\it{n\/}}, {\rm{sy-a}}\,({\tt{'}}{\tt{yout}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-a})\index{bn})\index{empty}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{h}}\,({\rm{b}}\,({\rm{bn}}\,({\it{n\/}}, {\rm{sy-a}}\,({\tt{'}}{\tt{yout}}, {\it{x\/}})\index{sy-a})\index{bn})\index{b})\index{h} $=$ ($1\;+$ {\rm{h}}\,({\rm{bn}}\,({\it{n\/}}, {\rm{sy-a}}\,({\tt{'}}{\tt{yout}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-a})\index{bn})\index{h}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  count-ac-l \\ \index{count-ac-l}
{\rm{l}}\,({\rm{stut}}\,({\rm{sy-a}}\,({\tt{'}}{\tt{yout}}, {\it{xst\/}})\index{sy-a}, {\it{xst\/}})\index{stut})\index{l} $=$ {\rm{l}}\,({\rm{sy-c}}\,({\tt{'}}{\tt{yout}}, {\it{xst\/}})\index{sy-c})\index{l}
\end{tabbing}


\begin{verbatim}; Now extending to strings.  For some unknow reason, compared to Funacc, we 
; need BOTH splits here... Probably because of some weird non-triggering
; phenomenon in equality hyp usage.

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

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

\begin{verbatim}; and finally:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  count-ac-correct \\ \index{count-ac-correct}
{\rm{stut}}\,({\rm{sy-a}}\,({\tt{'}}{\tt{yout}}, {\it{xst\/}})\index{sy-a}, {\it{xst\/}})\index{stut} $=$ {\rm{sy-c}}\,({\tt{'}}{\tt{yout}}, {\it{xst\/}})\index{sy-c}
\end{tabbing}

\begin{verbatim};; END: ACTUAL Circuit CORRECTNESS modulo Stuttering for A and C.

\end{verbatim}
\noindent{\sc Event}:   Disable count-ac-l.

\addvspace{18pt}

\noindent{\sc Event}:   Disable count-ac-correct.

\addvspace{18pt}

\begin{verbatim}; HCorr properties are the "Hand-Correctness" formulas... They are not
; necessary for the proof of Count-AB-L, but I'm trying to see if they help.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  hcorr-ab-t \\ \index{hcorr-ab-t}
\=\+(($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) $\wedge$ ($\neg$ {\rm{empty}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{empty}) $\wedge$ {\rm{l}}\,({\rm{sy-b}}\,({\tt{'}}{\tt{yst}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b})\index{l}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{l}}\,({\rm{sy-b}}\,({\tt{'}}{\tt{yout}}, {\it{x\/}})\index{sy-b})\index{l} $=$ {\rm{l}}\,({\rm{sy-b}}\,({\tt{'}}{\tt{yout}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b})\index{l})\-
\end{tabbing}

\noindent{\sc Event}:   Disable hcorr-ab-t.

\addvspace{18pt}  \begin{verbatim}; obviously..

\end{verbatim}\begin{tabbing}{\sc Theorem}:  hcorr-ab-f \\ \index{hcorr-ab-f}
\=\+(($\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-b}}\,({\tt{'}}{\tt{yst}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b})\index{l})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{l}}\,({\rm{sy-b}}\,({\tt{'}}{\tt{yout}}, {\it{x\/}})\index{sy-b})\index{l} $=$ ($1\;+$ {\rm{l}}\,({\rm{sy-b}}\,({\tt{'}}{\tt{yout}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-b})\index{l}))\-
\end{tabbing}

\noindent{\sc Event}:   Disable hcorr-ab-f.

\addvspace{18pt}

\begin{verbatim}; Count-AB-L succeeds with either HCorrs enabled, or the expansion hint 
; therein.  The costs (time/clarity) seem equal.  In the future, if the
; effort involved in getting HCorrs is greater, the dichotomy may be useful.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  count-ab-l \\ \index{count-ab-l}
{\rm{l}}\,({\rm{stut}}\,({\rm{sy-a}}\,({\tt{'}}{\tt{yout}}, {\it{x\/}})\index{sy-a}, {\rm{sy-b}}\,({\tt{'}}{\tt{yst}}, {\it{x\/}})\index{sy-b})\index{stut})\index{l} $=$ {\rm{l}}\,({\rm{sy-b}}\,({\tt{'}}{\tt{yout}}, {\it{x\/}})\index{sy-b})\index{l}
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  apl-split-stuta2 \\ \index{apl-split-stuta2}
\=\+($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{stut}}\,({\rm{sy-a}}\,({\tt{'}}{\tt{yout}}, {\it{x\/}})\index{sy-a}, {\rm{sy-b}}\,({\tt{'}}{\tt{yst}}, {\it{x\/}})\index{sy-b})\index{stut} \\ 
$=$$\;\;\;\;${\rm{a}}\,(\=\+{\rm{p}}\,({\rm{stut}}\,({\rm{sy-a}}\,({\tt{'}}{\tt{yout}}, {\it{x\/}})\index{sy-a}, {\rm{sy-b}}\,({\tt{'}}{\tt{yst}}, {\it{x\/}})\index{sy-b})\index{stut})\index{p}, \\ 
{\rm{l}}\,({\rm{stut}}\,({\rm{sy-a}}\,({\tt{'}}{\tt{yout}}, {\it{x\/}})\index{sy-a}, {\rm{sy-b}}\,({\tt{'}}{\tt{yst}}, {\it{x\/}})\index{sy-b})\index{stut})\index{l})\-\index{a})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  count-ab-correct \\ \index{count-ab-correct}
{\rm{stut}}\,({\rm{sy-a}}\,({\tt{'}}{\tt{yout}}, {\it{x\/}})\index{sy-a}, {\rm{sy-b}}\,({\tt{'}}{\tt{yst}}, {\it{x\/}})\index{sy-b})\index{stut} $=$ {\rm{sy-b}}\,({\tt{'}}{\tt{yout}}, {\it{x\/}})\index{sy-b}
\end{tabbing}

\begin{verbatim};; END: ACTUAL Circuit CORRECTNESS modulo Stuttering for A and B.
; eof: countstut.bm
; ))

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