\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}; counterR.bm: a resetable clock counter, i.e. Paillet example 1.
;
; This is our first circuit w/ 2 inputs, yet to my amazement, 
; extra EQLEN hypotheses were NEVER required, neither in the A2
; lemmas, nor in the actual specifications (Paillet, or mine)!  Of 
; course, when they became required (in Paillet #7) and put in
; Sugar, they were installed here.
;
; NOTE (w/ EMPTY enabled) : Attempts to speed up A2-PC failed 
; miserably: disabling the combinationals fails because of the 
; uneven cases, and the fact that BM can't derive (empty y) from
; (empty x) and equal (len x) (len y).
; A problem we have had for a long time, and which will probably 
; persist until we solve EQLEN.
; Giving the induction hint ahead of time made things worse, as 
; usual. Twiddling with STR-P-I2 improved nothing.



;;; CIRCUIT in SUGARED form:
#|
(setq sysd '(sy-COUNT (Xc Xe)
(Ymux  S Mux Xc Xe Yinc)
(Yreg  R 0 YMux)
(Yinc  S Incn Yreg)
))

(setq counterR '( |#
; 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_incn.bm: Inc modulo N combinational element, a minor modification
;               of comb_inc which shouldn't cause any difference, unless
;               the loop-around property is used in a critical way, which is
;               rare.  
; Note that N is treated as a global constant, but not as an individual 
; parameter, so we don't have to carry it around everywhere.  This is just
; an experiment, to see what's more convenient.
; U7-DONE

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

\addvspace{18pt}
\begin{verbatim}; we may want to add an axiom saying that it's a number, not needed so far..

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

; eof:comb_incn.bm


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

\begin{tabbing}{\sc Definition}:\index{sy-count} \\  
\=\+{\rm{sy-count}}\,({\it{ln\/}}, {\it{xc\/}}, {\it{xe\/}})\index{sy-count} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{ln\/}} $=$ {\tt{'}}{\tt{ymux}}$\;\;${\bf then }{\rm{s-mux}}\,({\it{xc\/}}, {\it{xe\/}}, {\rm{sy-count}}\,({\tt{'}}{\tt{yinc}}, {\it{xc\/}}, {\it{xe\/}})\index{sy-count})\index{s-mux} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yreg}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{xc\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{0}}, {\rm{sy-count}}\,({\tt{'}}{\tt{ymux}}, {\rm{p}}\,({\it{xc\/}})\index{p}, {\rm{p}}\,({\it{xe\/}})\index{p})\index{sy-count})\index{i}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yinc}}$\;\;${\bf then }{\rm{s-incn}}\,({\rm{sy-count}}\,({\tt{'}}{\tt{yreg}}, {\it{xc\/}}, {\it{xe\/}})\index{sy-count})\index{s-incn} \\ 
{\bf else }{\rm{sfix}}\,({\it{xc\/}})\index{sfix}$\;${\bf  endif}\-\-
\end{tabbing}

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

\end{verbatim}\begin{tabbing}{\sc Theorem}:  a2-empty-sy-count \\ \index{a2-empty-sy-count}
({\rm{len}}\,({\it{xc\/}})\index{len} $=$ {\rm{len}}\,({\it{xe\/}})\index{len}) $\rightarrow$ ({\rm{empty}}\,({\rm{sy-count}}\,({\it{ln\/}}, {\it{xc\/}}, {\it{xe\/}})\index{sy-count})\index{empty} $=$ {\rm{empty}}\,({\it{xc\/}})\index{empty})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-e-sy-count \\ \index{a2-e-sy-count}
({\rm{len}}\,({\it{xc\/}})\index{len} $=$ {\rm{len}}\,({\it{xe\/}})\index{len}) $\rightarrow$ (({\rm{sy-count}}\,({\it{ln\/}}, {\it{xc\/}}, {\it{xe\/}})\index{sy-count} $=$ {\sc{e}}\index{e}) $=$ {\rm{empty}}\,({\it{xc\/}})\index{empty})
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  a2-lpe-sy-count \\ \index{a2-lpe-sy-count}
({\rm{len}}\,({\it{xc\/}})\index{len} $=$ {\rm{len}}\,({\it{xe\/}})\index{len}) $\rightarrow$ {\rm{eqlen}}\,({\rm{sy-count}}\,({\it{ln\/}}, {\it{xc\/}}, {\it{xe\/}})\index{sy-count}, {\it{xc\/}})\index{eqlen}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a2-pc-sy-count \\ \index{a2-pc-sy-count}
\=\+({\rm{len}}\,({\it{xc\/}})\index{len} $=$ {\rm{len}}\,({\it{xe\/}})\index{len}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{p}}\,({\rm{sy-count}}\,({\it{ln\/}}, {\it{xc\/}}, {\it{xe\/}})\index{sy-count})\index{p} $=$ {\rm{sy-count}}\,({\it{ln\/}}, {\rm{p}}\,({\it{xc\/}})\index{p}, {\rm{p}}\,({\it{xe\/}})\index{p})\index{sy-count})\-
\end{tabbing}

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

;;; Circuit CORRECTNESS /Paillet:

; Note that as originally stated in Paillet, with the P outside of 
; sy-count makes for a looping (unfolding) which would have to be 
; proved kludgeily, and would be useless.  The following rule can
; be used as a rewrite.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  count-paillet-correct \\ \index{count-paillet-correct}
\=\+(($\neg$ {\rm{empty}}\,({\it{xc\/}})\index{empty}) $\wedge$ ($\neg$ {\rm{empty}}\,({\it{xe\/}})\index{empty})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{sy-count}}\,({\tt{'}}{\tt{yreg}}, {\it{xc\/}}, {\it{xe\/}})\index{sy-count} \\ 
$=$$\;\;\;\;${\rm{i}}\,({\tt{0}}, {\rm{s-if}}\,({\rm{p}}\,({\it{xc\/}})\index{p}, {\rm{p}}\,({\it{xe\/}})\index{p}, {\rm{s-incn}}\,({\rm{sy-count}}\,({\tt{'}}{\tt{yreg}}, {\rm{p}}\,({\it{xc\/}})\index{p}, {\rm{p}}\,({\it{xe\/}})\index{p})\index{sy-count})\index{s-incn})\index{s-if})\index{i})\-\-
\end{tabbing}

\begin{verbatim}; The "last-char" reading of the spec yields:
; NOTE: we can prove it by repeating the same hint and disabling 
; CORRECT, i.e. independently.  Trying to use CORRECT fails 
; miserably because it also triggers on:
; (sy-count 'Yreg (P Xc) (P Xe)).  Note also that we need the
; EQ-LEN hyp because we need A2-EMPTY-SY-COUNT.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  count-paillet-correct-l \\ \index{count-paillet-correct-l}
\=\+(($\neg$ {\rm{empty}}\,({\rm{p}}\,({\it{xc\/}})\index{p})\index{empty}) $\wedge$ ($\neg$ {\rm{empty}}\,({\rm{p}}\,({\it{xe\/}})\index{p})\index{empty}) $\wedge$ ({\rm{len}}\,({\it{xc\/}})\index{len} $=$ {\rm{len}}\,({\it{xe\/}})\index{len})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{l}}\,({\rm{sy-count}}\,({\tt{'}}{\tt{yreg}}, {\it{xc\/}}, {\it{xe\/}})\index{sy-count})\index{l} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{l}}\,({\rm{p}}\,({\it{xc\/}})\index{p})\index{l}$\;\;${\bf then }{\rm{l}}\,({\rm{p}}\,({\it{xe\/}})\index{p})\index{l} \\ 
{\bf else }{\rm{incn}}\,({\rm{l}}\,({\rm{sy-count}}\,({\tt{'}}{\tt{yreg}}, {\rm{p}}\,({\it{xc\/}})\index{p}, {\rm{p}}\,({\it{xe\/}})\index{p})\index{sy-count})\index{l})\index{incn}$\;${\bf  endif}\-)\-\-
\end{tabbing}

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