\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 Computational Logic, Inc.  All Rights Reserved.

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

 NO WARRANTY

 Computational Logic, Inc. 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 Computational Logic, Inc. 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};  This file contains examples that illustrate the use
;  of the new events CONSTRAIN and FUNCTIONALLY-INSTANTIATE.

;  Example 1.  Here we simply introduce three new function symbols of
;  1 argument with no constraints on them.

\end{verbatim}\begin{tabbing}{\sc Conservative Axiom}:  p-q-r-intro \\ \index{p-q-r-intro}
{\bf{t}}
\end{tabbing}\noindent Simultaneously, we introduce the new function symbols {\it p\/}, {\it q\/}, and {\it r\/}.



\begin{verbatim};  Example 2.  Here we introduce the function h, which has the strange
;  property we call ``commutativity2'' and show that one can ``map''
;  with such a function in a primitive recursive way (using pr-h) or
;  by using an accumulator (using pr-ac); but either way one gets the
;  same result.  We then can FUNCTIONALLY-INSTANTIATE this result
;  using times instead of h.

\end{verbatim}\begin{tabbing}{\sc Conservative Axiom}:  intro-h \\ \index{intro-h}
{\rm{h}}\,({\it{x\/}}, {\rm{h}}\,({\it{y\/}}, {\it{z\/}})\index{h})\index{h} $=$ {\rm{h}}\,({\it{y\/}}, {\rm{h}}\,({\it{x\/}}, {\it{z\/}})\index{h})\index{h}
\end{tabbing}\noindent Simultaneously, we introduce the new function symbol {\it h\/}.

\begin{tabbing}{\sc Definition}:\index{pr-h} \\  
\=\+{\rm{pr-h}}\,({\it{l\/}}, {\it{z\/}})\index{pr-h} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{l\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\it{z\/}} \\ 
{\bf else }{\rm{h}}\,({\rm{car}}\,({\it{l\/}}), {\rm{pr-h}}\,({\rm{cdr}}\,({\it{l\/}}), {\it{z\/}})\index{pr-h})\index{h}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{ac-h} \\  
\=\+{\rm{ac-h}}\,({\it{l\/}}, {\it{z\/}})\index{ac-h} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{l\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\it{z\/}} \\ 
{\bf else }{\rm{ac-h}}\,({\rm{cdr}}\,({\it{l\/}}), {\rm{h}}\,({\rm{car}}\,({\it{l\/}}), {\it{z\/}})\index{h})\index{ac-h}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  pr-is-ac \\ \index{pr-is-ac}
{\rm{ac-h}}\,({\it{l\/}}, {\it{z\/}})\index{ac-h} $=$ {\rm{pr-h}}\,({\it{l\/}}, {\it{z\/}})\index{pr-h}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{pr-times} \\  
\=\+{\rm{pr-times}}\,({\it{l\/}}, {\it{z\/}})\index{pr-times} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{l\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\it{z\/}} \\ 
{\bf else }{\rm{car}}\,({\it{l\/}}) $*$ {\rm{pr-times}}\,({\rm{cdr}}\,({\it{l\/}}), {\it{z\/}})\index{pr-times}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{ac-times} \\  
\=\+{\rm{ac-times}}\,({\it{l\/}}, {\it{z\/}})\index{ac-times} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{l\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\it{z\/}} \\ 
{\bf else }{\rm{ac-times}}\,({\rm{cdr}}\,({\it{l\/}}), {\rm{car}}\,({\it{l\/}}) $*$ {\it{z\/}})\index{ac-times}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  pr-times-is-ac-times \\ \index{pr-times-is-ac-times}
{\rm{ac-times}}\,({\it{l\/}}, {\it{z\/}})\index{ac-times} $=$ {\rm{pr-times}}\,({\it{l\/}}, {\it{z\/}})\index{pr-times}
\end{tabbing}



\begin{verbatim};  Example 3.  This example is somewhat similar to the last one in
;  spirit.  This time we constrain the function lt to have one of the
;  properties of a simple order, define a sort on top of it, prove the
;  sort correct, and then instantiate the result with lessp for lt.

\end{verbatim}\begin{tabbing}{\sc Conservative Axiom}:  lt-intro \\ \index{lt-intro}
{\rm{lt}}\,({\it{z\/}}, {\it{v\/}})\index{lt} $\rightarrow$ ($\neg$ {\rm{lt}}\,({\it{v\/}}, {\it{z\/}})\index{lt})
\end{tabbing}\noindent Simultaneously, we introduce the new function symbol {\it lt\/}.

\begin{tabbing}{\sc Definition}:\index{ordered-lt} \\  
\=\+{\rm{ordered-lt}}\,({\it{l\/}})\index{ordered-lt} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{l\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{listp}}\,({\rm{cdr}}\,({\it{l\/}})) \\ 
{\bf then }\=\+{\bf if }{\rm{lt}}\,({\rm{cadr}}\,({\it{l\/}}), {\rm{car}}\,({\it{l\/}}))\index{lt}$\;\;${\bf then }{\bf{f}} \\ 
{\bf else }{\rm{ordered-lt}}\,({\rm{cdr}}\,({\it{l\/}}))\index{ordered-lt}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{addtolist-lt} \\  
\=\+{\rm{addtolist-lt}}\,({\it{x\/}}, {\it{l\/}})\index{addtolist-lt} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{l\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{lt}}\,({\it{x\/}}, {\rm{car}}\,({\it{l\/}}))\index{lt}$\;\;${\bf then }{\rm{cons}}\,({\it{x\/}}, {\it{l\/}}) \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\it{l\/}}), {\rm{addtolist-lt}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{l\/}}))\index{addtolist-lt})$\;${\bf  endif}\- \\ 
{\bf else }{\rm{list}}\,({\it{x\/}})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{sort-lt} \\  
\=\+{\rm{sort-lt}}\,({\it{l\/}})\index{sort-lt} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{l\/}})$\;\;${\bf then }{\rm{addtolist-lt}}\,({\rm{car}}\,({\it{l\/}}), {\rm{sort-lt}}\,({\rm{cdr}}\,({\it{l\/}}))\index{sort-lt})\index{addtolist-lt} \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  ordered-sort-lt \\ \index{ordered-sort-lt}
{\rm{ordered-lt}}\,({\rm{sort-lt}}\,({\it{l\/}})\index{sort-lt})\index{ordered-lt}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{ordered-lessp} \\  
\=\+{\rm{ordered-lessp}}\,({\it{l\/}})\index{ordered-lessp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{l\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{listp}}\,({\rm{cdr}}\,({\it{l\/}})) \\ 
{\bf then }\=\+{\bf if }{\rm{cadr}}\,({\it{l\/}}) $<$ {\rm{car}}\,({\it{l\/}})$\;\;${\bf then }{\bf{f}} \\ 
{\bf else }{\rm{ordered-lessp}}\,({\rm{cdr}}\,({\it{l\/}}))\index{ordered-lessp}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{addtolist-lessp} \\  
\=\+{\rm{addtolist-lessp}}\,({\it{x\/}}, {\it{l\/}})\index{addtolist-lessp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{l\/}}) \\ 
{\bf then }\=\+{\bf if }{\it{x\/}} $<$ {\rm{car}}\,({\it{l\/}})$\;\;${\bf then }{\rm{cons}}\,({\it{x\/}}, {\it{l\/}}) \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\it{l\/}}), {\rm{addtolist-lessp}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{l\/}}))\index{addtolist-lessp})$\;${\bf  endif}\- \\ 
{\bf else }{\rm{list}}\,({\it{x\/}})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{sort-lessp} \\  
\=\+{\rm{sort-lessp}}\,({\it{l\/}})\index{sort-lessp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{l\/}})$\;\;${\bf then }{\rm{addtolist-lessp}}\,({\rm{car}}\,({\it{l\/}}), {\rm{sort-lessp}}\,({\rm{cdr}}\,({\it{l\/}}))\index{sort-lessp})\index{addtolist-lessp} \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ordered-sort-lessp \\ \index{ordered-sort-lessp}
{\rm{ordered-lessp}}\,({\rm{sort-lessp}}\,({\it{l\/}})\index{sort-lessp})\index{ordered-lessp}
\end{tabbing}



\begin{verbatim};  Example 4.  We here define the familiar map function, show that it
;  distributes over append, and instantiate the result with a LAMBDA
;  that has a free variable.

\end{verbatim}\begin{tabbing}{\sc Conservative Axiom}:  fn-intro \\ \index{fn-intro}
{\bf{t}}
\end{tabbing}\noindent Simultaneously, we introduce the new function symbol {\it fn\/}.

\begin{tabbing}{\sc Definition}:\index{map-fn} \\  
\=\+{\rm{map-fn}}\,({\it{x\/}})\index{map-fn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,({\rm{fn}}\,({\rm{car}}\,({\it{x\/}}))\index{fn}, {\rm{map-fn}}\,({\rm{cdr}}\,({\it{x\/}}))\index{map-fn})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  map-distributes-over-append \\ \index{map-distributes-over-append}
{\rm{map-fn}}\,({\rm{append}}\,({\it{u\/}}, {\it{v\/}}))\index{map-fn} $=$ {\rm{append}}\,({\rm{map-fn}}\,({\it{u\/}})\index{map-fn}, {\rm{map-fn}}\,({\it{v\/}})\index{map-fn})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{map-plus-y} \\  
\=\+{\rm{map-plus-y}}\,({\it{x\/}}, {\it{y\/}})\index{map-plus-y} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\it{x\/}}) $+$ {\it{y\/}}, {\rm{map-plus-y}}\,({\rm{cdr}}\,({\it{x\/}}), {\it{y\/}})\index{map-plus-y})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  map-plus-y-distributes-over-append \\ \index{map-plus-y-distributes-over-appe!nd}
{\rm{map-plus-y}}\,({\rm{append}}\,({\it{u\/}}, {\it{v\/}}), {\it{z\/}})\index{map-plus-y} $=$ {\rm{append}}\,({\rm{map-plus-y}}\,({\it{u\/}}, {\it{z\/}})\index{map-plus-y}, {\rm{map-plus-y}}\,({\it{v\/}}, {\it{z\/}})\index{map-plus-y})
\end{tabbing}



\begin{verbatim};  Example 5.  Here we follow the lead of Goodstein in his book
;  Primitive Recursive Arithmetic and of McCarthy with his recursion
;  induction.  We show, using FUNCTIONALLY-INSTANTIATE, that the
;  associativity of append can be proved without explicit appeal to
;  induction.  Of course there are inductions hidden all over the
;  place, e.g. in the type-set analysis for true-rec and in the proof
;  of the metatheorem that justifies FUNCTIONALLY-INSTANTIATE.  Still,
;  this is a startling development to those who regard the
;  associativity of append as the first theorem requiring an inductive
;  proof.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{true-rec} \\  
\=\+{\rm{true-rec}}\,({\it{x\/}})\index{true-rec} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{true-rec}}\,({\rm{cdr}}\,({\it{x\/}}))\index{true-rec}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  true-rec-is-true \\ \index{true-rec-is-true}
{\rm{true-rec}}\,({\it{x\/}})\index{true-rec}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{app} \\  
\=\+{\rm{app}}\,({\it{x\/}}, {\it{y\/}})\index{app} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\it{y\/}} \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\it{x\/}}), {\rm{app}}\,({\rm{cdr}}\,({\it{x\/}}), {\it{y\/}})\index{app})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  assoc-of-app \\ \index{assoc-of-app}
{\rm{app}}\,({\rm{app}}\,({\it{x\/}}, {\it{y\/}})\index{app}, {\it{z\/}})\index{app} $=$ {\rm{app}}\,({\it{x\/}}, {\rm{app}}\,({\it{y\/}}, {\it{z\/}})\index{app})\index{app}
\end{tabbing}



\begin{verbatim};  Example 6.  We illustrate that one can prove theorems using
;  CONSTRAIN and FUNCTIONALLY-INSTANTIATE that resemble proofs in
;  first-order predicate calculus with quantifiers.

\end{verbatim}\begin{tabbing}{\sc Conservative Axiom}:  all-x-p-x-intro \\ \index{all-x-p-x-intro}
{\sc{all-x-p-x}}\index{all-x-p-x} $\rightarrow$ {\rm{p}}\,({\it{x\/}})\index{p}
\end{tabbing}\noindent Simultaneously, we introduce the new function symbol {\it all-x-p-x\/}.

\begin{tabbing}{\sc Conservative Axiom}:  all-x-not-p-x-into \\ \index{all-x-not-p-x-into}
{\sc{all-x-not-p-x}}\index{all-x-not-p-x} $\rightarrow$ ($\neg$ {\rm{p}}\,({\it{x\/}})\index{p})
\end{tabbing}\noindent Simultaneously, we introduce the new function symbol {\it all-x-not-p-x\/}.

\begin{tabbing}{\sc Theorem}:  all-x-not-p-x-into-converse \\ \index{all-x-not-p-x-into-converse}
{\rm{p}}\,({\it{x\/}})\index{p} $\rightarrow$ ($\neg$ {\sc{all-x-not-p-x}}\index{all-x-not-p-x})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{some-x-p-x}$\;\;$
{\sc{some-x-p-x}}\index{some-x-p-x} $=$ ($\neg$ {\sc{all-x-not-p-x}}\index{all-x-not-p-x})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-implies-some \\ \index{all-implies-some}
{\sc{all-x-p-x}}\index{all-x-p-x} $\rightarrow$ {\sc{some-x-p-x}}\index{some-x-p-x}
\end{tabbing}

\begin{verbatim};  Example 7.  We illustrate a CONSTRAIN that expresses that a
;  function is ``fair'' in the sense that it is infinitely often true
;  and false.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{even} \\  
\=\+{\rm{even}}\,({\it{x\/}})\index{even} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\it{x\/}} $=$ {\tt{1}}$\;\;${\bf then }{\sc{false}} \\ 
{\bf else }$\neg$ {\rm{even}}\,({\it{x\/}} $-\;1$)\index{even}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Conservative Axiom}:  fair-intro \\ \index{fair-intro}
\=\+{\rm{fair}}\,({\rm{fair-true-witness}}\,({\it{n\/}})\index{fair-true-witness})\index{fair} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{fair}}\,({\rm{fair-false-witness}}\,({\it{n\/}})\index{fair-false-witness})\index{fair}) \\ 
$\wedge$$\;\;\;\;$({\rm{fair-true-witness}}\,({\it{n\/}})\index{fair-true-witness} $\not<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{fair-false-witness}}\,({\it{n\/}})\index{fair-false-witness} $\not<$ {\it{n\/}})\-
\end{tabbing}\noindent Simultaneously, we introduce the new function symbols {\it fair\/}, {\it fair-true-witness\/}, and {\it fair-false-witness\/}.

\begin{verbatim};  Example 8.  We illustrate the idea of ``stubbing'' functions.  We
;  define interp to call an undefined, but constrained, function num.
;  Later we prove a result about instantiation of interp by
;  FUNCTIONALLY-INSTANTIATE.

\end{verbatim}\begin{tabbing}{\sc Conservative Axiom}:  num-intro \\ \index{num-intro}
{\rm{num}}\,({\it{x\/}})\index{num} $\in\;${\bf{N}}${}$
\end{tabbing}\noindent Simultaneously, we introduce the new function symbol {\it num\/}.

\begin{tabbing}{\sc Definition}:\index{interp} \\  
\=\+{\rm{interp}}\,({\it{x\/}})\index{interp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\not\simeq {\tt{0}}$$\;\;${\bf then }{\it{x\/}} $*$ {\it{x\/}} \\ 
{\bf else }{\rm{num}}\,({\it{x\/}})\index{num}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  interp-is-numeric \\ \index{interp-is-numeric}
{\rm{interp}}\,({\it{x\/}})\index{interp} $\in\;${\bf{N}}${}$
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{interp2} \\  
\=\+{\rm{interp2}}\,({\it{x\/}})\index{interp2} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\not\simeq {\tt{0}}$$\;\;${\bf then }{\it{x\/}} $*$ {\it{x\/}} \\ 
{\bf else }{\it{x\/}} $+$ {\it{x\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  interp2-is-numeric \\ \index{interp2-is-numeric}
{\rm{interp2}}\,({\it{x\/}})\index{interp2} $\in\;${\bf{N}}${}$
\end{tabbing}


       
\begin{verbatim};  Example 9.  We here illustrate the fact that add-axioms
;  are correctly tracked.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-alias}$\;\;$
{\rm{p-alias}}\,({\it{x\/}})\index{p-alias} $=$ {\rm{p}}\,({\it{x\/}})\index{p}
\end{tabbing}

\begin{tabbing}{\sc Axiom}:  even-p-alias \\ \index{even-p-alias}
{\rm{even}}\,({\rm{p-alias}}\,({\it{x\/}})\index{p-alias})\index{even}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  even-p \\ \index{even-p}
{\rm{even}}\,({\rm{p}}\,({\it{x\/}})\index{p})\index{even}
\end{tabbing}

\begin{verbatim}#|  

;  Because this step fails, we comment it out.  The failure
;  stems from our having provided a substitution for the
;  apparently irrelevant function q-alias.  However, providing
;  an analogue to q-alias explose the real problem, the necessity
;  of anopther add-axiom.  The key point is that p-alias
;  is not irrelevant when trying to FUNCTIONALLY-INSTANTIATE
;  even-p because p is ancestral in even-p-alias.

(functionally-instantiate even-q nil
  (even (q x))
  even-p
  ((p q)))

|#

;  Example 10.  It is necessary for soundness that we check that
;  the variables in the constraints do not intersect the free variables
;  in the FUNCTIONALLY-INSTANTIATE substitutions.  Otherwise,
;  the following sequence would lead to unsoundness.

\end{verbatim}\begin{tabbing}{\sc Conservative Axiom}:  pp-intro \\ \index{pp-intro}
({\it{y\/}} $=$ {\tt{0}}) $\rightarrow$ ({\sc{pp}}\index{pp} $=$ {\it{y\/}})
\end{tabbing}\noindent Simultaneously, we introduce the new function symbol {\it pp\/}.

\begin{tabbing}{\sc Theorem}:  pp-is-0 \\ \index{pp-is-0}
{\tt{0}} $=$ {\sc{pp}}\index{pp}
\end{tabbing}

\begin{verbatim}#|  

;  Because this last step fails, we comment it out.  Note that if we
;  did not catch this, relieving the constraint would amount to
;  checking merely that (implies (equal y 0) (equal y y)).

(functionally-instantiate anything-is-0 (rewrite)
  (equal 0 y)
  pp-is-0
  ((pp (lambda () y))))

|#

;  Example 11.  Some from ``higher logic.''

\end{verbatim}\begin{tabbing}{\sc Conservative Axiom}:  fn-commutative \\ \index{fn-commutative}
{\rm{fn2}}\,({\it{x\/}}, {\it{y\/}})\index{fn2} $=$ {\rm{fn2}}\,({\it{y\/}}, {\it{x\/}})\index{fn2}
\end{tabbing}\noindent Simultaneously, we introduce the new function symbol {\it fn2\/}.

\begin{tabbing}{\sc Definition}:\index{foldr-fn} \\  
\=\+{\rm{foldr-fn}}\,({\it{lst\/}}, {\it{r\/}})\index{foldr-fn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{lst\/}})$\;\;${\bf then }{\rm{fn2}}\,({\rm{car}}\,({\it{lst\/}}), {\rm{foldr-fn}}\,({\rm{cdr}}\,({\it{lst\/}}), {\it{r\/}})\index{foldr-fn})\index{fn2} \\ 
{\bf else }{\it{r\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{foldl-fn} \\  
\=\+{\rm{foldl-fn}}\,({\it{lst\/}}, {\it{r\/}})\index{foldl-fn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{lst\/}})$\;\;${\bf then }{\rm{foldl-fn}}\,({\rm{cdr}}\,({\it{lst\/}}), {\rm{fn2}}\,({\it{r\/}}, {\rm{car}}\,({\it{lst\/}}))\index{fn2})\index{foldl-fn} \\ 
{\bf else }{\it{r\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{reverse} \\  
\=\+{\rm{reverse}}\,({\it{x\/}})\index{reverse} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}})$\;\;${\bf then }{\rm{append}}\,({\rm{reverse}}\,({\rm{cdr}}\,({\it{x\/}}))\index{reverse}, {\rm{list}}\,({\rm{car}}\,({\it{x\/}}))) \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  foldl-is-foldr \\ \index{foldl-is-foldr}
{\rm{foldr-fn}}\,({\it{lst\/}}, {\it{r\/}})\index{foldr-fn} $=$ {\rm{foldl-fn}}\,({\rm{reverse}}\,({\it{lst\/}})\index{reverse}, {\it{r\/}})\index{foldl-fn}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  times-add1 \\ \index{times-add1}
({\it{x\/}} $*$ ($1\;+$ {\it{y\/}})) $=$ ({\it{x\/}} $+$ ({\it{x\/}} $*$ {\it{y\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  times-comm \\ \index{times-comm}
({\it{x\/}} $*$ {\it{y\/}}) $=$ ({\it{y\/}} $*$ {\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{foldr-times} \\  
\=\+{\rm{foldr-times}}\,({\it{lst\/}}, {\it{r\/}})\index{foldr-times} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{lst\/}})$\;\;${\bf then }{\rm{car}}\,({\it{lst\/}}) $*$ {\rm{foldr-times}}\,({\rm{cdr}}\,({\it{lst\/}}), {\it{r\/}})\index{foldr-times} \\ 
{\bf else }{\it{r\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{foldl-times} \\  
\=\+{\rm{foldl-times}}\,({\it{lst\/}}, {\it{r\/}})\index{foldl-times} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{lst\/}})$\;\;${\bf then }{\rm{foldl-times}}\,({\rm{cdr}}\,({\it{lst\/}}), {\it{r\/}} $*$ {\rm{car}}\,({\it{lst\/}}))\index{foldl-times} \\ 
{\bf else }{\it{r\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  foldl-times-is-foldr-times \\ \index{foldl-times-is-foldr-times}
{\rm{foldr-times}}\,({\it{lst\/}}, {\it{r\/}})\index{foldr-times} $=$ {\rm{foldl-times}}\,({\rm{reverse}}\,({\it{lst\/}})\index{reverse}, {\it{r\/}})\index{foldl-times}
\end{tabbing}


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