\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}; funacc.bm
;   Circuit is similar to acc, but uses ARBITRARY CHAR-FUN (arity 2) instead of
; addition. It's expressed in CSXA form.  Proving it guarantees (at the BM
; level) that the theorems stated in bm_syds_2ndorder.txt are indeed true
; in general, although of course, BM can not instantiate them.
;

;;; DEFINITION OF CIRCUIT:
#|
(setq sysd '(sy-funacc (x)
(Yfun S Fun2 x Yreg)
(Yreg R 'finit Yfun)
))

(setq funacc '(
|#
; BM DEFINITIONS and A2 LEMMAS, generated by BMSYSD:
; comb_fun2.bm: Fun2 combinational element
; U7-DONE

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

\addvspace{18pt}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

; eof:comb_fun2.bm


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

\begin{tabbing}{\sc Definition}:\index{sy-funacc} \\  
\=\+{\rm{sy-funacc}}\,({\it{ln\/}}, {\it{x\/}})\index{sy-funacc} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{ln\/}} $=$ {\tt{'}}{\tt{yfun}}$\;\;${\bf then }{\rm{s-fun2}}\,({\it{x\/}}, {\rm{sy-funacc}}\,({\tt{'}}{\tt{yreg}}, {\it{x\/}})\index{sy-funacc})\index{s-fun2} \\ 
{\bf elseif }{\it{ln\/}} $=$ {\tt{'}}{\tt{yreg}} \\ 
{\bf then }\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{i}}\,({\tt{'}}{\tt{finit}}, {\rm{sy-funacc}}\,({\tt{'}}{\tt{yfun}}, {\rm{p}}\,({\it{x\/}})\index{p})\index{sy-funacc})\index{i}$\;${\bf  endif}\- \\ 
{\bf else }{\rm{sfix}}\,({\it{x\/}})\index{sfix}$\;${\bf  endif}\-\-
\end{tabbing}

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

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

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

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

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

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

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

;;; SPEC definition:

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{numer-funacc} \\  
\=\+{\rm{numer-funacc}}\,({\it{x\/}})\index{numer-funacc} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\tt{'}}{\tt{finit}} \\ 
{\bf else }{\rm{fun2}}\,({\rm{numer-funacc}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{numer-funacc}, {\rm{l}}\,({\it{x\/}})\index{l})\index{fun2}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; this is the standard extension from last-char-fun to MLP-string-fun.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{spec-funacc} \\  
\=\+{\rm{spec-funacc}}\,({\it{x\/}})\index{spec-funacc} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{empty}}\,({\it{x\/}})\index{empty}$\;\;${\bf then }{\sc{e}}\index{e} \\ 
{\bf else }{\rm{a}}\,({\rm{spec-funacc}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{spec-funacc}, {\rm{numer-funacc}}\,({\it{x\/}})\index{numer-funacc})\index{a}$\;${\bf  endif}\-\-
\end{tabbing}


\begin{verbatim};;; Circuit CORRECTNESS:

; We now declare Fun2 to be COMMUTATIVE because the definition of NUMER-FUNACC
; funs the 2 arguments in the opposite order than the sysd, and hence
; commutativity is required.  Alternatively, we could change NUMER-FUNACC's
; definition.  (This has been tested and runs.)
\end{verbatim}\begin{tabbing}{\sc Axiom}:  fun2-comm \\ \index{fun2-comm}
{\rm{fun2}}\,({\it{u\/}}, {\it{v\/}})\index{fun2} $=$ {\rm{fun2}}\,({\it{v\/}}, {\it{u\/}})\index{fun2}
\end{tabbing}

\begin{verbatim}; Funacc-correct-ax is a "predicative correctness statement",i.e. what we would
; do if we didn't have functional equality as a specification method, but 
; instead used a purely axiomatic approach.
; NOTE: the simplicity of the proof should imply that disabling the 
; char-function in specific instances of accumulator syds should help...

\end{verbatim}\begin{tabbing}{\sc Theorem}:  funacc-correct-ax \\ \index{funacc-correct-ax}
($\neg$ {\rm{empty}}\,({\it{x\/}})\index{empty}) $\rightarrow$ ({\rm{l}}\,({\rm{sy-funacc}}\,({\tt{'}}{\tt{yfun}}, {\it{x\/}})\index{sy-funacc})\index{l} $=$ {\rm{numer-funacc}}\,({\it{x\/}})\index{numer-funacc})
\end{tabbing}

\begin{verbatim}; to go to a functional equality once we have the "last" (ax) statement is
; a trivial induction, if we start out with an P-L split which is unnatural
; for BM, so we force it w/ a USE hint of A-p-l-split .  See also THETA.BM .

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

\begin{tabbing}{\sc Theorem}:  funacc-correct \\ \index{funacc-correct}
{\rm{sy-funacc}}\,({\tt{'}}{\tt{yfun}}, {\it{x\/}})\index{sy-funacc} $=$ {\rm{spec-funacc}}\,({\it{x\/}})\index{spec-funacc}
\end{tabbing}

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