\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 John Cowles.  All Rights Reserved.

 This script is hereby placed in the public domain, and therefore unlimited
 editing and redistribution is permitted.

 NO WARRANTY

 John Cowles PROVIDES 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 John Cowles 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 initial {\bf nqthm} theory.

\addvspace{18pt} 



\begin{verbatim};                          A NOTE ON SHELLS
;                                 by
;                             John Cowles
;                     Department of Computer Science
;                         University of Wyoming

; The following is intended to give the reader some insight into SHELLS.

; Intuitively a nonempty SEQUENCE is an ordered list, possibly with
;  duplicates, of objects, ( Obj1 Obj2 ... ObjN ).

; There are two ways to recursively decompose sequences.
; 
;  1. A SEQUENCE is either the EMPTY-SEQUENCE or a pair < Obj,Seq >.
;  
;  2. A SEQUENCE is either the EMPTY-SEQUENCE or a pair [ Seq,Obj ].
;
;  Here Obj is an object, Seq is a sequence, and EMPTY-SEQUENCE is 
;  the unique sequence which contains no objects.  Different pairing
;  brackets, < > and [ ], are used to enphasize which of the 
;  decompositions is being used.

; Here the Shell Principle is used with decomposition 1 above to
;  add sequences as a "new" data type. 

\end{verbatim}
\noindent{\sc Event}:   Add the shell {\it{cons-seq-first\/}}\index{cons-seq-first}, with bottom object function symbol {\it{empty-seq\/}}, with recognizer function symbol {\it{seq-p\/}}, and 2 accessors: {\it{first\/}}, with type restriction (none-of) and default value empty-seq; {\it{final\/}}, with type restriction (one-of seq-p) and default value empty-seq.

\addvspace{18pt} \begin{verbatim}; default value

; ( CONS-SEQ-FIRST Obj Seq )     returns < Obj,Seq >.
; ( CONS-SEQ-FIRST Obj Non-Seq ) returns < Obj,EMPTY-SEQUENCE >.

; ( EMPTY-SEQ ) returns the EMPTY-SEQUENCE.

; ( SEQ-P Seq )     returns T.
; ( SEQ-P Non-Seq ) reTurns F.

; ( FIRST < Obj,Seq > ) returns Obj.
; ( FIRST (EMPTY-SEQ) ) returns (EMPTY-SEQ).
; ( FIRST Non-Seq )     returns (EMPTY-SEQ).

; ( FINAL < Obj,Seq > ) returns Seq.
; ( FINAL (EMPTY-SEQ) ) returns (EMPTY-SEQ).
; ( FINAL Non-Seq )     returns (EMPTY-SEQ).
; ==================
; The next two functions "coerce" non-sequences into
;  behaving like the EMPTY-SEQUENCE.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{empty-seq-p} \\  
{\rm{empty-seq-p}}\,({\it{s\/}})\index{empty-seq-p} $=$ (({\it{s\/}} $=$ {\sc{empty-seq}}\index{empty-seq}) $\vee$ ($\neg$ {\rm{seq-p}}\,({\it{s\/}})\index{seq-p}))
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{coerce-seq} \\  
\=\+{\rm{coerce-seq}}\,({\it{s\/}})\index{coerce-seq} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{seq-p}}\,({\it{s\/}})\index{seq-p}$\;\;${\bf then }{\it{s\/}} \\ 
{\bf else }{\sc{empty-seq}}\index{empty-seq}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; The next three functions implement sequence decomposion 2 above. 

; ( CONS-SEQ-LAST Seq Obj )     returns [ Seq,Obj ].
; ( CONS-SEQ-LAST Non-Seq Obj ) returns [ (EMPTY-SEQ),Obj ].
;     Here [ (EMPTY-SEQ),Obj ] is identified with < Obj,(EMPTY-SEQ) >.

; ( INITIAL [ Seq,Obj ] ) returns Seq.
; ( INITIAL (EMPTY-SEQ) ) returns (EMPTY-SEQ).
; ( INITIAL Non-Seq )     returns (EMPTY-SEQ).

; ( LAST [ Seq,Obj ] ) returns Obj.
; ( LAST (EMPTY-SEQ) ) returns (EMPTY-SEQ).
; ( LAST Non-Seq )     returns (EMPTY-SEQ).

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{cons-seq-last} \\  
\=\+{\rm{cons-seq-last}}\,({\it{s\/}}, {\it{c\/}})\index{cons-seq-last} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{empty-seq-p}}\,({\it{s\/}})\index{empty-seq-p}$\;\;${\bf then }{\rm{cons-seq-first}}\,({\it{c\/}}, {\it{s\/}})\index{cons-seq-first} \\ 
{\bf else }{\rm{cons-seq-first}}\,({\rm{first}}\,({\it{s\/}})\index{first}, {\rm{cons-seq-last}}\,({\rm{final}}\,({\it{s\/}})\index{final}, {\it{c\/}})\index{cons-seq-last})\index{cons-seq-first}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{initial} \\  
\=\+{\rm{initial}}\,({\it{s\/}})\index{initial} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{empty-seq-p}}\,({\it{s\/}})\index{empty-seq-p}$\;\;${\bf then }{\sc{empty-seq}}\index{empty-seq} \\ 
{\bf elseif }{\rm{final}}\,({\it{s\/}})\index{final} $=$ {\sc{empty-seq}}\index{empty-seq}$\;\;${\bf then }{\sc{empty-seq}}\index{empty-seq} \\ 
{\bf else }{\rm{cons-seq-first}}\,({\rm{first}}\,({\it{s\/}})\index{first}, {\rm{initial}}\,({\rm{final}}\,({\it{s\/}})\index{final})\index{initial})\index{cons-seq-first}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{last} \\  
\=\+{\rm{last}}\,({\it{s\/}})\index{last} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{empty-seq-p}}\,({\it{s\/}})\index{empty-seq-p}$\;\;${\bf then }{\sc{empty-seq}}\index{empty-seq} \\ 
{\bf elseif }{\rm{final}}\,({\it{s\/}})\index{final} $=$ {\sc{empty-seq}}\index{empty-seq}$\;\;${\bf then }{\rm{first}}\,({\it{s\/}})\index{first} \\ 
{\bf else }{\rm{last}}\,({\rm{final}}\,({\it{s\/}})\index{final})\index{last}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; The next 12 rewrite rules and 1 elimination rule would have been
;  explicitly added as axioms to the data base by the shell principle 
;  if sequence decomposition 2 had been used, in place of decomposition 1,
;  as the basis for the shell which added sequences as a new type.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  initial-cons-seq-last \\ \index{initial-cons-seq-last}
\=\+{\rm{initial}}\,({\rm{cons-seq-last}}\,({\it{s\/}}, {\it{c\/}})\index{cons-seq-last})\index{initial} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{seq-p}}\,({\it{s\/}})\index{seq-p}$\;\;${\bf then }{\it{s\/}} \\ 
{\bf else }{\sc{empty-seq}}\index{empty-seq}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  initial-nseq-p \\ \index{initial-nseq-p}
($\neg$ {\rm{seq-p}}\,({\it{s\/}})\index{seq-p}) $\rightarrow$ ({\rm{initial}}\,({\it{s\/}})\index{initial} $=$ {\sc{empty-seq}}\index{empty-seq})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  initial-type-restriction \\ \index{initial-type-restriction}
($\neg$ {\rm{seq-p}}\,({\it{s\/}})\index{seq-p}) $\rightarrow$ ({\rm{cons-seq-last}}\,({\it{s\/}}, {\it{c\/}})\index{cons-seq-last} $=$ {\rm{cons-seq-last}}\,({\sc{empty-seq}}\index{empty-seq}, {\it{c\/}})\index{cons-seq-last})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  initial-lessp \\ \index{initial-lessp}
({\rm{seq-p}}\,({\it{s\/}})\index{seq-p} $\wedge$ ({\it{s\/}} $\not=$ {\sc{empty-seq}}\index{empty-seq})) $\rightarrow$ ({\rm{count}}\,({\rm{initial}}\,({\it{s\/}})\index{initial}) $<$ {\rm{count}}\,({\it{s\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  initial-lesseqp \\ \index{initial-lesseqp}
{\rm{count}}\,({\it{s\/}}) $\not<$ {\rm{count}}\,({\rm{initial}}\,({\it{s\/}})\index{initial})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  last-cons-seq-last \\ \index{last-cons-seq-last}
{\rm{last}}\,({\rm{cons-seq-last}}\,({\it{s\/}}, {\it{c\/}})\index{cons-seq-last})\index{last} $=$ {\it{c\/}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  last-nseq-p \\ \index{last-nseq-p}
($\neg$ {\rm{seq-p}}\,({\it{s\/}})\index{seq-p}) $\rightarrow$ ({\rm{last}}\,({\it{s\/}})\index{last} $=$ {\sc{empty-seq}}\index{empty-seq})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  last-lessp \\ \index{last-lessp}
({\rm{seq-p}}\,({\it{s\/}})\index{seq-p} $\wedge$ ({\it{s\/}} $\not=$ {\sc{empty-seq}}\index{empty-seq})) $\rightarrow$ ({\rm{count}}\,({\rm{last}}\,({\it{s\/}})\index{last}) $<$ {\rm{count}}\,({\it{s\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  last-lesseqp \\ \index{last-lesseqp}
{\rm{count}}\,({\it{s\/}}) $\not<$ {\rm{count}}\,({\rm{last}}\,({\it{s\/}})\index{last})
\end{tabbing}

\begin{verbatim}; The next two lemmas are obvious facts used only as 
; hints for the proof of the lemma CONS-SEQ-LAST-EQUAL.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  initial-apply-equals \\ \index{initial-apply-equals}
({\it{x\/}} $=$ {\it{y\/}}) $\rightarrow$ ({\rm{initial}}\,({\it{x\/}})\index{initial} $=$ {\rm{initial}}\,({\it{y\/}})\index{initial})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  last-apply-equals \\ \index{last-apply-equals}
({\it{x\/}} $=$ {\it{y\/}}) $\rightarrow$ ({\rm{last}}\,({\it{x\/}})\index{last} $=$ {\rm{last}}\,({\it{y\/}})\index{last})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  cons-seq-last-equal \\ \index{cons-seq-last-equal}
\=\+({\rm{cons-seq-last}}\,({\it{s1\/}}, {\it{c1\/}})\index{cons-seq-last} $=$ {\rm{cons-seq-last}}\,({\it{s2\/}}, {\it{c2\/}})\index{cons-seq-last}) \\ 
$=$$\;\;\;\;$(\=\+\=\+{\bf if }{\rm{seq-p}}\,({\it{s1\/}})\index{seq-p} \\ 
{\bf then }\=\+{\bf if }{\rm{seq-p}}\,({\it{s2\/}})\index{seq-p}$\;\;${\bf then }{\it{s1\/}} $=$ {\it{s2\/}} \\ 
{\bf else }{\it{s1\/}} $=$ {\sc{empty-seq}}\index{empty-seq}$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{seq-p}}\,({\it{s2\/}})\index{seq-p}$\;\;${\bf then }{\sc{empty-seq}}\index{empty-seq} $=$ {\it{s2\/}} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\- \\ 
$\wedge$$\;\;\;\;$({\it{c1\/}} $=$ {\it{c2\/}}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  cons-seq-last-initial-last \\ \index{cons-seq-last-initial-last}
\=\+{\rm{cons-seq-last}}\,({\rm{initial}}\,({\it{s\/}})\index{initial}, {\rm{last}}\,({\it{s\/}})\index{last})\index{cons-seq-last} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{seq-p}}\,({\it{s\/}})\index{seq-p} $\wedge$ ({\it{s\/}} $\not=$ {\sc{empty-seq}}\index{empty-seq})$\;\;${\bf then }{\it{s\/}} \\ 
{\bf else }{\rm{cons-seq-last}}\,({\sc{empty-seq}}\index{empty-seq}, {\sc{empty-seq}}\index{empty-seq})\index{cons-seq-last}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  initial-last-elim \\ \index{initial-last-elim}
\=\+({\rm{seq-p}}\,({\it{s\/}})\index{seq-p} $\wedge$ ({\it{s\/}} $\not=$ {\sc{empty-seq}}\index{empty-seq})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{cons-seq-last}}\,({\rm{initial}}\,({\it{s\/}})\index{initial}, {\rm{last}}\,({\it{s\/}})\index{last})\index{cons-seq-last} $=$ {\it{s\/}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  count-cons-seq-last \\ \index{count-cons-seq-last}
\=\+{\rm{count}}\,({\rm{cons-seq-last}}\,({\it{s\/}}, {\it{c\/}})\index{cons-seq-last}) \\ 
$=$$\;\;\;\;$($1\;+$ (\=\+\=\+{\bf if }{\rm{seq-p}}\,({\it{s\/}})\index{seq-p}$\;\;${\bf then }{\rm{count}}\,({\it{s\/}}) \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\- \\ 
$+$$\;\;\;\;${\rm{count}}\,({\it{c\/}}))\-)\-
\end{tabbing}

\begin{verbatim}; The next rewrite rule would, in effect, have been implicitly added
;  as an axiom to the data base by the shell principle if sequence 
;  decomposition 2 had been used, in place of decomposition 1, as the 
;  basis for the shell which added sequences as a new type.   

\end{verbatim}\begin{tabbing}{\sc Theorem}:  cons-seq-last-not-empty-seq \\ \index{cons-seq-last-not-empty-seq}
{\rm{cons-seq-last}}\,({\it{s\/}}, {\it{c\/}})\index{cons-seq-last} $\not=$ {\sc{empty-seq}}\index{empty-seq}
\end{tabbing}
\begin{verbatim};====================================================================

; The next two functions give different versions of REVERSE.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{reverse1} \\  
\=\+{\rm{reverse1}}\,({\it{s\/}})\index{reverse1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{empty-seq-p}}\,({\it{s\/}})\index{empty-seq-p}$\;\;${\bf then }{\it{s\/}} \\ 
{\bf else }{\rm{cons-seq-last}}\,({\rm{reverse1}}\,({\rm{final}}\,({\it{s\/}})\index{final})\index{reverse1}, {\rm{first}}\,({\it{s\/}})\index{first})\index{cons-seq-last}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{reverse2} \\  
\=\+{\rm{reverse2}}\,({\it{s\/}})\index{reverse2} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{empty-seq-p}}\,({\it{s\/}})\index{empty-seq-p}$\;\;${\bf then }{\it{s\/}} \\ 
{\bf else }{\rm{cons-seq-first}}\,({\rm{last}}\,({\it{s\/}})\index{last}, {\rm{reverse2}}\,({\rm{initial}}\,({\it{s\/}})\index{initial})\index{reverse2})\index{cons-seq-first}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; Use the Theorem Prover to verify the following proposed theorems.
;
; 1. For i=1 and i=2, ( EQUAL (REVERSEi (REVERSEi S)) S )
;
; 2. ( EQUAL (REVERSE1 S) (REVERSE2 S) )
; ==================================================================

; The next four functions give different versions of CONCATENATION.    

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{concat1} \\  
\=\+{\rm{concat1}}\,({\it{s1\/}}, {\it{s2\/}})\index{concat1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{empty-seq-p}}\,({\it{s1\/}})\index{empty-seq-p}$\;\;${\bf then }{\rm{coerce-seq}}\,({\it{s2\/}})\index{coerce-seq} \\ 
{\bf else }{\rm{cons-seq-first}}\,({\rm{first}}\,({\it{s1\/}})\index{first}, {\rm{concat1}}\,({\rm{final}}\,({\it{s1\/}})\index{final}, {\it{s2\/}})\index{concat1})\index{cons-seq-first}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{concat2} \\  
\=\+{\rm{concat2}}\,({\it{s1\/}}, {\it{s2\/}})\index{concat2} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{empty-seq-p}}\,({\it{s2\/}})\index{empty-seq-p}$\;\;${\bf then }{\rm{coerce-seq}}\,({\it{s1\/}})\index{coerce-seq} \\ 
{\bf else }{\rm{concat2}}\,({\rm{cons-seq-last}}\,({\it{s1\/}}, {\rm{first}}\,({\it{s2\/}})\index{first})\index{cons-seq-last}, {\rm{final}}\,({\it{s2\/}})\index{final})\index{concat2}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{concat3} \\  
\=\+{\rm{concat3}}\,({\it{s1\/}}, {\it{s2\/}})\index{concat3} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{empty-seq-p}}\,({\it{s2\/}})\index{empty-seq-p}$\;\;${\bf then }{\rm{coerce-seq}}\,({\it{s1\/}})\index{coerce-seq} \\ 
{\bf else }{\rm{cons-seq-last}}\,({\rm{concat3}}\,({\it{s1\/}}, {\rm{initial}}\,({\it{s2\/}})\index{initial})\index{concat3}, {\rm{last}}\,({\it{s2\/}})\index{last})\index{cons-seq-last}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{concat4} \\  
\=\+{\rm{concat4}}\,({\it{s1\/}}, {\it{s2\/}})\index{concat4} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{empty-seq-p}}\,({\it{s1\/}})\index{empty-seq-p}$\;\;${\bf then }{\rm{coerce-seq}}\,({\it{s2\/}})\index{coerce-seq} \\ 
{\bf else }{\rm{concat4}}\,({\rm{initial}}\,({\it{s1\/}})\index{initial}, {\rm{cons-seq-first}}\,({\rm{last}}\,({\it{s1\/}})\index{last}, {\it{s2\/}})\index{cons-seq-first})\index{concat4}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; Use the Theorem Prover to verify the following proposed theorems.
;
; 1. For i=1, i=2, i=3, and i=4, CONCATi is associative.
;
; 2. For i=1 and i=2; and for j=1, j=2, j=3, and j=4;
;      ( EQUAL (REVERSEi (CONCATj S1 S2))
;              (CONCATj (REVERSEi S2) (REVERSEi S1)) )
;
; 3. For i and j such that 1 <= i < j <= 4,
;      ( EQUAL (CONCATi S1 S2) (CONCATj S1 S2) )

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