\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 Natarajan Shankar.  All Rights Reserved.

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

 NO WARRANTY

 Natarajan Shankar 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 Natarajan Shankar 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 thm} theory.

\addvspace{18pt}

\begin{verbatim};Annotated script for mechanical proof of the Tautology theorem.
;Proof involves - 
;Definition of proof-checker for Schoenfield's FOL.
;Proof of several derived inference rules, primarily the
;subset lemma.
;Definition of tautology-checker.
;Every tautology has a proof.
;Correctness of tautology-checker - every tautology is
;always logically-true, and all logical-truths are tautologies.
;First, functions, variables and predicate symbols.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{function} \\  
\=\+{\rm{function}}\,({\it{fn\/}})\index{function} \\ 
$=$$\;\;\;\;$(\=\+({\it{fn\/}} $=$ {\rm{list}}\,({\tt{'}}{\tt{f}}, {\rm{cadr}}\,({\it{fn\/}}), {\rm{caddr}}\,({\it{fn\/}}))) \\ 
$\wedge$$\;\;\;\;$({\rm{cadr}}\,({\it{fn\/}}) $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{caddr}}\,({\it{fn\/}}) $\in\;${\bf{N}}${}$))\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{variable} \\  
{\rm{variable}}\,({\it{x\/}})\index{variable} $=$ (({\it{x\/}} $=$ {\rm{list}}\,({\tt{'}}{\tt{x}}, {\rm{cadr}}\,({\it{x\/}}))) $\wedge$ ({\rm{cadr}}\,({\it{x\/}}) $\in\;${\bf{N}}${}$))
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{predicate} \\  
\=\+{\rm{predicate}}\,({\it{p\/}})\index{predicate} \\ 
$=$$\;\;\;\;$(\=\+(\=\+({\it{p\/}} $=$ {\rm{list}}\,({\tt{'}}{\tt{p}}, {\rm{cadr}}\,({\it{p\/}}), {\rm{caddr}}\,({\it{p\/}}))) \\ 
$\wedge$$\;\;\;\;$({\rm{cadr}}\,({\it{p\/}}) $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{caddr}}\,({\it{p\/}}) $\in\;${\bf{N}}${}$))\- \\ 
$\vee$$\;\;\;\;$({\it{p\/}} $=$ {\tt{'}}{\tt{equal}}))\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{degree} \\  
\=\+{\rm{degree}}\,({\it{fn\/}})\index{degree} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{fn\/}} $=$ {\tt{'}}{\tt{equal}}$\;\;${\bf then }{\tt{2}} \\ 
{\bf else }{\rm{caddr}}\,({\it{fn\/}})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{index}$\;\;$
{\rm{index}}\,({\it{fn\/}})\index{index} $=$ {\rm{cadr}}\,({\it{fn\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{func-pred}$\;\;$
{\rm{func-pred}}\,({\it{x\/}})\index{func-pred} $=$ ({\rm{function}}\,({\it{x\/}})\index{function} $\vee$ {\rm{predicate}}\,({\it{x\/}})\index{predicate})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{v}$\;\;$
{\rm{v}}\,({\it{x\/}})\index{v} $=$ {\rm{list}}\,({\tt{'}}{\tt{x}}, {\rm{fix}}\,({\it{x\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  numberp-fix \\ \index{numberp-fix}
{\rm{fix}}\,({\it{x\/}}) $\in\;${\bf{N}}${}$
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  variable-v \\ \index{variable-v}
{\rm{variable}}\,({\rm{v}}\,({\it{x\/}})\index{v})\index{variable}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{fn}$\;\;$
{\rm{fn}}\,({\it{x\/}}, {\it{y\/}})\index{fn} $=$ {\rm{list}}\,({\tt{'}}{\tt{f}}, {\rm{fix}}\,({\it{x\/}}), {\rm{fix}}\,({\it{y\/}}))
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{p}$\;\;$
{\rm{p}}\,({\it{x\/}}, {\it{y\/}})\index{p} $=$ {\rm{list}}\,({\tt{'}}{\tt{p}}, {\rm{fix}}\,({\it{x\/}}), {\rm{fix}}\,({\it{y\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  function-fn \\ \index{function-fn}
{\rm{function}}\,({\rm{fn}}\,({\it{x\/}}, {\it{y\/}})\index{fn})\index{function}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  predicate-p \\ \index{predicate-p}
{\rm{predicate}}\,({\rm{p}}\,({\it{x\/}}, {\it{y\/}})\index{p})\index{predicate}
\end{tabbing}
\begin{verbatim};quantifer, there exists.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{quantifier}$\;\;$
{\rm{quantifier}}\,({\it{x\/}})\index{quantifier} $=$ ({\it{x\/}} $=$ {\tt{'}}{\tt{forsome}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{union} \\  
\=\+({\it{x\/}} $\cup$ {\it{y\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{car}}\,({\it{x\/}}) $\in$ {\it{y\/}}$\;\;${\bf then }{\rm{cdr}}\,({\it{x\/}}) $\cup$ {\it{y\/}} \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\it{x\/}}), {\rm{cdr}}\,({\it{x\/}}) $\cup$ {\it{y\/}})$\;${\bf  endif}\- \\ 
{\bf else }{\it{y\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\noindent{\sc Event}:   Enable variable; name this event `g0223'.\index{g0223}

\addvspace{18pt}

\noindent{\sc Event}:   Enable quantifier; name this event `g0224'.\index{g0224}

\addvspace{18pt}
\begin{tabbing}{\sc Theorem}:  predicate-f-equal \\ \index{predicate-f-equal}
{\rm{predicate}}\,({\tt{'}}{\tt{equal}})\index{predicate}
\end{tabbing}

\noindent{\sc Event}:   Enable function; name this event `g0225'.\index{g0225}

\addvspace{18pt}

\noindent{\sc Event}:   Enable predicate; name this event `g0226'.\index{g0226}

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{append} \\  
\=\+{\rm{append}}\,({\it{x\/}}, {\it{y\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}})$\;\;${\bf then }{\rm{cons}}\,({\rm{car}}\,({\it{x\/}}), {\rm{append}}\,({\rm{cdr}}\,({\it{x\/}}), {\it{y\/}})) \\ 
{\bf else }{\it{y\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{delete} \\  
\=\+{\rm{delete}}\,({\it{x\/}}, {\it{y\/}})\index{delete} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{y\/}}) \\ 
{\bf then }\=\+{\bf if }{\it{x\/}} $=$ {\rm{car}}\,({\it{y\/}})$\;\;${\bf then }{\rm{delete}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{y\/}}))\index{delete} \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\it{y\/}}), {\rm{delete}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{y\/}}))\index{delete})$\;${\bf  endif}\- \\ 
{\bf else }{\it{y\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  not-member-delete \\ \index{not-member-delete}
{\it{x\/}} $\not\in$ {\rm{delete}}\,({\it{x\/}}, {\it{y\/}})\index{delete}
\end{tabbing}
\begin{verbatim};returns list of free variables in EXP.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{collect-free} \\  
\=\+{\rm{collect-free}}\,({\it{exp\/}}, {\it{flg\/}})\index{collect-free} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{exp\/}}) \\ 
{\bf then }\=\+{\bf if }{\it{flg\/}} $=$ {\bf{t}} \\ 
{\bf then }\=\+{\bf if }{\rm{variable}}\,({\it{exp\/}})\index{variable}$\;\;${\bf then }{\rm{cons}}\,({\it{exp\/}}, {\bf{nil}}) \\ 
{\bf elseif }{\rm{quantifier}}\,({\rm{car}}\,({\it{exp\/}}))\index{quantifier} $\wedge$ {\rm{listp}}\,({\rm{cdr}}\,({\it{exp\/}})) \\ 
{\bf then }{\rm{delete}}\,({\rm{cadr}}\,({\it{exp\/}}), {\rm{collect-free}}\,({\rm{cddr}}\,({\it{exp\/}}), {\tt{'}}{\tt{list}})\index{collect-free})\index{delete} \\ 
{\bf elseif }\=\+{\rm{func-pred}}\,({\rm{car}}\,({\it{exp\/}}))\index{func-pred} \\ 
$\vee$$\;\;\;\;$({\rm{car}}\,({\it{exp\/}}) $=$ {\tt{'}}{\tt{not}}) \\ 
$\vee$$\;\;\;\;$({\rm{car}}\,({\it{exp\/}}) $=$ {\tt{'}}{\tt{or}})\- \\ 
{\bf then }{\rm{collect-free}}\,({\rm{cdr}}\,({\it{exp\/}}), {\tt{'}}{\tt{list}})\index{collect-free} \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\- \\ 
{\bf else }{\rm{append}}\,(\=\+{\rm{collect-free}}\,({\rm{car}}\,({\it{exp\/}}), {\bf{t}})\index{collect-free}, \\ 
{\rm{collect-free}}\,({\rm{cdr}}\,({\it{exp\/}}), {\tt{'}}{\tt{list}})\index{collect-free})\-$\;${\bf  endif}\- \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{sentence}$\;\;$
{\rm{sentence}}\,({\it{exp\/}})\index{sentence} $=$ ({\rm{collect-free}}\,({\it{exp\/}}, {\bf{t}})\index{collect-free} $=$ {\bf{nil}})
\end{tabbing}
\begin{verbatim};returns bound variables in EXP that surround free occurrences of VAR.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{covering} \\  
\=\+{\rm{covering}}\,({\it{exp\/}}, {\it{var\/}}, {\it{flg\/}})\index{covering} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{exp\/}}) \\ 
{\bf then }\=\+{\bf if }{\it{flg\/}} $=$ {\bf{t}} \\ 
{\bf then }\=\+{\bf if }{\rm{variable}}\,({\it{exp\/}})\index{variable}$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }{\rm{quantifier}}\,({\rm{car}}\,({\it{exp\/}}))\index{quantifier} $\wedge$ {\rm{listp}}\,({\rm{cdr}}\,({\it{exp\/}})) \\ 
{\bf then }\=\+{\bf if }{\rm{cadr}}\,({\it{exp\/}}) $=$ {\it{var\/}}$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }{\it{var\/}} $\in$ {\rm{collect-free}}\,({\rm{cddr}}\,({\it{exp\/}}), {\tt{'}}{\tt{list}})\index{collect-free} \\ 
{\bf then }{\rm{cons}}\,({\rm{cadr}}\,({\it{exp\/}}), {\rm{covering}}\,({\rm{cddr}}\,({\it{exp\/}}), {\it{var\/}}, {\tt{'}}{\tt{list}})\index{covering}) \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\- \\ 
{\bf elseif }\=\+{\rm{func-pred}}\,({\rm{car}}\,({\it{exp\/}}))\index{func-pred} \\ 
$\vee$$\;\;\;\;$({\rm{car}}\,({\it{exp\/}}) $=$ {\tt{'}}{\tt{not}}) \\ 
$\vee$$\;\;\;\;$({\rm{car}}\,({\it{exp\/}}) $=$ {\tt{'}}{\tt{or}})\- \\ 
{\bf then }{\rm{covering}}\,({\rm{cdr}}\,({\it{exp\/}}), {\it{var\/}}, {\tt{'}}{\tt{list}})\index{covering} \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\- \\ 
{\bf else }{\rm{append}}\,(\=\+{\rm{covering}}\,({\rm{car}}\,({\it{exp\/}}), {\it{var\/}}, {\bf{t}})\index{covering}, \\ 
{\rm{covering}}\,({\rm{cdr}}\,({\it{exp\/}}), {\it{var\/}}, {\tt{'}}{\tt{list}})\index{covering})\-$\;${\bf  endif}\- \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim};X and Y are disjoint.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{nil-intersect} \\  
\=\+{\rm{nil-intersect}}\,({\it{x\/}}, {\it{y\/}})\index{nil-intersect} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}})$\;\;${\bf then }({\rm{car}}\,({\it{x\/}}) $\not\in$ {\it{y\/}}) $\wedge$ {\rm{nil-intersect}}\,({\rm{cdr}}\,({\it{x\/}}), {\it{y\/}})\index{nil-intersect} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim};TERM is free for VAR in EXP.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{free-for} \\  
\=\+{\rm{free-for}}\,({\it{exp\/}}, {\it{var\/}}, {\it{term\/}}, {\it{flg\/}})\index{free-for} \\ 
$=$$\;\;\;\;${\rm{nil-intersect}}\,({\rm{covering}}\,({\it{exp\/}}, {\it{var\/}}, {\it{flg\/}})\index{covering}, {\rm{collect-free}}\,({\it{term\/}}, {\bf{t}})\index{collect-free})\index{nil-intersect}\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{f-equal}$\;\;$
{\rm{f-equal}}\,({\it{x\/}}, {\it{y\/}})\index{f-equal} $=$ {\rm{list}}\,({\tt{'}}{\tt{equal}}, {\it{x\/}}, {\it{y\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{f-not}$\;\;$
{\rm{f-not}}\,({\it{x\/}})\index{f-not} $=$ {\rm{list}}\,({\tt{'}}{\tt{not}}, {\it{x\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{f-or}$\;\;$
{\rm{f-or}}\,({\it{x\/}}, {\it{y\/}})\index{f-or} $=$ {\rm{list}}\,({\tt{'}}{\tt{or}}, {\it{x\/}}, {\it{y\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{forsome}$\;\;$
{\rm{forsome}}\,({\it{x\/}}, {\it{y\/}})\index{forsome} $=$ {\rm{list}}\,({\tt{'}}{\tt{forsome}}, {\it{x\/}}, {\it{y\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{f-and}$\;\;$
{\rm{f-and}}\,({\it{x\/}}, {\it{y\/}})\index{f-and} $=$ {\rm{f-not}}\,({\rm{f-or}}\,({\rm{f-not}}\,({\it{x\/}})\index{f-not}, {\rm{f-not}}\,({\it{y\/}})\index{f-not})\index{f-or})\index{f-not}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{f-implies}$\;\;$
{\rm{f-implies}}\,({\it{x\/}}, {\it{y\/}})\index{f-implies} $=$ {\rm{f-or}}\,({\rm{f-not}}\,({\it{x\/}})\index{f-not}, {\it{y\/}})\index{f-or}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{forall}$\;\;$
$\forall\;${\it{var\/}}$\;${\it{exp\/}}\index{forall} $=$ {\rm{f-not}}\,({\rm{forsome}}\,({\it{var\/}}, {\rm{f-not}}\,({\it{exp\/}})\index{f-not})\index{forsome})\index{f-not}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{f-iff}$\;\;$
{\rm{f-iff}}\,({\it{x\/}}, {\it{y\/}})\index{f-iff} $=$ {\rm{f-and}}\,({\rm{f-implies}}\,({\it{x\/}}, {\it{y\/}})\index{f-implies}, {\rm{f-implies}}\,({\it{y\/}}, {\it{x\/}})\index{f-implies})\index{f-and}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{var-list} \\  
\=\+{\rm{var-list}}\,({\it{list\/}}, {\it{n\/}})\index{var-list} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\it{list\/}} $=$ {\bf{nil}} \\ 
{\bf else }{\rm{variable}}\,({\rm{car}}\,({\it{list\/}}))\index{variable} $\wedge$ {\rm{var-list}}\,({\rm{cdr}}\,({\it{list\/}}), {\it{n\/}} $-\;1$)\index{var-list}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{var-set} \\  
\=\+{\rm{var-set}}\,({\it{list\/}}, {\it{n\/}})\index{var-set} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\it{list\/}} $=$ {\bf{nil}} \\ 
{\bf else }\=\+{\rm{variable}}\,({\rm{car}}\,({\it{list\/}}))\index{variable} \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{list\/}}) $\not\in$ {\rm{cdr}}\,({\it{list\/}})) \\ 
$\wedge$$\;\;\;\;${\rm{var-set}}\,({\rm{cdr}}\,({\it{list\/}}), {\it{n\/}} $-\;1$)\index{var-set}\-$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim};Recognizer for terms.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{termp} \\  
\=\+{\rm{termp}}\,({\it{exp\/}}, {\it{flg\/}}, {\it{count\/}})\index{termp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{flg\/}} $=$ {\bf{t}} \\ 
{\bf then }\=\+{\bf if }{\it{exp\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{f}} \\ 
{\bf else }\=\+{\rm{variable}}\,({\it{exp\/}})\index{variable} \\ 
$\vee$$\;\;\;\;$(\=\+{\rm{function}}\,({\rm{car}}\,({\it{exp\/}}))\index{function} \\ 
$\wedge$$\;\;\;\;${\rm{termp}}\,(\=\+{\rm{cdr}}\,({\it{exp\/}}), \\ 
{\tt{'}}{\tt{list}}, \\ 
{\rm{degree}}\,({\rm{car}}\,({\it{exp\/}}))\index{degree})\-\index{termp})\-\-$\;${\bf  endif}\- \\ 
{\bf elseif }({\it{exp\/}} $\simeq\;${{\bf{nil}}}${}$) $\vee$ ({\it{count\/}} $\simeq {\tt{0}}$)$\;\;${\bf then }({\it{exp\/}} $=$ {\bf{nil}}) $\wedge$ ({\it{count\/}} $\simeq {\tt{0}}$) \\ 
{\bf else }{\rm{termp}}\,({\rm{car}}\,({\it{exp\/}}), {\bf{t}}, {\tt{0}})\index{termp} $\wedge$ {\rm{termp}}\,({\rm{cdr}}\,({\it{exp\/}}), {\tt{'}}{\tt{list}}, {\it{count\/}} $-\;1$)\index{termp}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{arg1}$\;\;$
{\rm{arg1}}\,({\it{x\/}})\index{arg1} $=$ {\rm{cadr}}\,({\it{x\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{arg2}$\;\;$
{\rm{arg2}}\,({\it{x\/}})\index{arg2} $=$ {\rm{caddr}}\,({\it{x\/}})
\end{tabbing}
\begin{verbatim};EXP is an atom, pred. symbol followed by list of terms.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{atomp} \\  
\=\+{\rm{atomp}}\,({\it{exp\/}})\index{atomp} \\ 
$=$$\;\;\;\;$({\rm{predicate}}\,({\rm{car}}\,({\it{exp\/}}))\index{predicate} $\wedge$ {\rm{termp}}\,({\rm{cdr}}\,({\it{exp\/}}), {\tt{'}}{\tt{list}}, {\rm{degree}}\,({\rm{car}}\,({\it{exp\/}}))\index{degree})\index{termp})\-
\end{tabbing}

\noindent{\sc Event}:   Enable atomp; name this event `g0253'.\index{g0253}

\addvspace{18pt}
\begin{verbatim};EXP is a formula
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{formula} \\  
\=\+{\rm{formula}}\,({\it{exp\/}}, {\it{flg\/}}, {\it{count\/}})\index{formula} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{flg\/}} $=$ {\bf{t}} \\ 
{\bf then }\=\+{\bf if }{\it{exp\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{f}} \\ 
{\bf else }\=\+{\rm{atomp}}\,({\it{exp\/}})\index{atomp} \\ 
$\vee$$\;\;\;\;$(\=\+({\rm{car}}\,({\it{exp\/}}) $=$ {\tt{'}}{\tt{not}}) \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\rm{cdr}}\,({\it{exp\/}}), {\tt{'}}{\tt{list}}, {\tt{1}})\index{formula})\- \\ 
$\vee$$\;\;\;\;$(\=\+({\rm{car}}\,({\it{exp\/}}) $=$ {\tt{'}}{\tt{or}}) \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\rm{cdr}}\,({\it{exp\/}}), {\tt{'}}{\tt{list}}, {\tt{2}})\index{formula})\- \\ 
$\vee$$\;\;\;\;$(\=\+({\rm{car}}\,({\it{exp\/}}) $=$ {\tt{'}}{\tt{forsome}}) \\ 
$\wedge$$\;\;\;\;${\rm{variable}}\,({\rm{cadr}}\,({\it{exp\/}}))\index{variable} \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\rm{cddr}}\,({\it{exp\/}}), {\tt{'}}{\tt{list}}, {\tt{1}})\index{formula})\-\-$\;${\bf  endif}\- \\ 
{\bf elseif }({\it{exp\/}} $\simeq\;${{\bf{nil}}}${}$) $\vee$ ({\it{count\/}} $\simeq {\tt{0}}$)$\;\;${\bf then }({\it{exp\/}} $=$ {\bf{nil}}) $\wedge$ ({\it{count\/}} $\simeq {\tt{0}}$) \\ 
{\bf else }\=\+{\rm{formula}}\,({\rm{car}}\,({\it{exp\/}}), {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\rm{cdr}}\,({\it{exp\/}}), {\tt{'}}{\tt{list}}, {\it{count\/}} $-\;1$)\index{formula}\-$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim};Result of substituting TERM for VAR in EXP.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{subst} \\  
\=\+{\rm{subst}}\,({\it{exp\/}}, {\it{var\/}}, {\it{term\/}}, {\it{flg\/}})\index{subst} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{exp\/}}) \\ 
{\bf then }\=\+{\bf if }{\it{flg\/}} $=$ {\bf{t}} \\ 
{\bf then }\=\+{\bf if }{\rm{variable}}\,({\it{exp\/}})\index{variable} \\ 
{\bf then }\=\+{\bf if }{\it{exp\/}} $=$ {\it{var\/}}$\;\;${\bf then }{\it{term\/}} \\ 
{\bf else }{\it{exp\/}}$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{quantifier}}\,({\rm{car}}\,({\it{exp\/}}))\index{quantifier} $\wedge$ {\rm{listp}}\,({\rm{cdr}}\,({\it{exp\/}})) \\ 
{\bf then }\=\+{\bf if }{\rm{cadr}}\,({\it{exp\/}}) $=$ {\it{var\/}}$\;\;${\bf then }{\it{exp\/}} \\ 
{\bf else }{\rm{cons}}\,(\=\+{\rm{car}}\,({\it{exp\/}}), \\ 
{\rm{cons}}\,(\=\+{\rm{cadr}}\,({\it{exp\/}}), \\ 
{\rm{subst}}\,({\rm{cddr}}\,({\it{exp\/}}), {\it{var\/}}, {\it{term\/}}, {\tt{'}}{\tt{list}})\index{subst})\-)\-$\;${\bf  endif}\- \\ 
{\bf elseif }\=\+{\rm{func-pred}}\,({\rm{car}}\,({\it{exp\/}}))\index{func-pred} \\ 
$\vee$$\;\;\;\;$({\rm{car}}\,({\it{exp\/}}) $=$ {\tt{'}}{\tt{not}}) \\ 
$\vee$$\;\;\;\;$({\rm{car}}\,({\it{exp\/}}) $=$ {\tt{'}}{\tt{or}})\- \\ 
{\bf then }{\rm{cons}}\,({\rm{car}}\,({\it{exp\/}}), {\rm{subst}}\,({\rm{cdr}}\,({\it{exp\/}}), {\it{var\/}}, {\it{term\/}}, {\tt{'}}{\tt{list}})\index{subst}) \\ 
{\bf else }{\it{exp\/}}$\;${\bf  endif}\- \\ 
{\bf else }{\rm{cons}}\,(\=\+{\rm{subst}}\,({\rm{car}}\,({\it{exp\/}}), {\it{var\/}}, {\it{term\/}}, {\bf{t}})\index{subst}, \\ 
{\rm{subst}}\,({\rm{cdr}}\,({\it{exp\/}}), {\it{var\/}}, {\it{term\/}}, {\tt{'}}{\tt{list}})\index{subst})\-$\;${\bf  endif}\- \\ 
{\bf else }{\it{exp\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{neg} \\  
{\rm{neg}}\,({\it{exp1\/}}, {\it{exp2\/}})\index{neg} $=$ (({\it{exp1\/}} $=$ {\rm{f-not}}\,({\it{exp2\/}})\index{f-not}) $\vee$ ({\it{exp2\/}} $=$ {\rm{f-not}}\,({\it{exp1\/}})\index{f-not}))
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{conc} \\  
\=\+{\rm{conc}}\,({\it{pf\/}}, {\it{flg\/}})\index{conc} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{pf\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }{\it{flg\/}} $=$ {\bf{t}}$\;\;${\bf then }{\rm{caddr}}\,({\it{pf\/}}) \\ 
{\bf else }{\rm{cons}}\,({\rm{conc}}\,({\rm{car}}\,({\it{pf\/}}), {\bf{t}})\index{conc}, {\rm{conc}}\,({\rm{cdr}}\,({\it{pf\/}}), {\tt{'}}{\tt{list}})\index{conc})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{subset} \\  
\=\+{\rm{subset}}\,({\it{x\/}}, {\it{y\/}})\index{subset} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}})$\;\;${\bf then }({\rm{car}}\,({\it{x\/}}) $\in$ {\it{y\/}}) $\wedge$ {\rm{subset}}\,({\rm{cdr}}\,({\it{x\/}}), {\it{y\/}})\index{subset} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{set-equal}$\;\;$
{\rm{set-equal}}\,({\it{x\/}}, {\it{y\/}})\index{set-equal} $=$ ({\rm{subset}}\,({\it{x\/}}, {\it{y\/}})\index{subset} $\wedge$ {\rm{subset}}\,({\it{y\/}}, {\it{x\/}})\index{subset})
\end{tabbing}
\begin{verbatim};The axioms: propositional, substitution, identity, equality for functions and predicates.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{prop-axiom}$\;\;$
{\rm{prop-axiom}}\,({\it{exp\/}})\index{prop-axiom} $=$ {\rm{f-or}}\,({\rm{f-not}}\,({\it{exp\/}})\index{f-not}, {\it{exp\/}})\index{f-or}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{subst-axiom} \\  
\=\+{\rm{subst-axiom}}\,({\it{exp\/}}, {\it{var\/}}, {\it{term\/}})\index{subst-axiom} \\ 
$=$$\;\;\;\;${\rm{f-implies}}\,({\rm{subst}}\,({\it{exp\/}}, {\it{var\/}}, {\it{term\/}}, {\bf{t}})\index{subst}, {\rm{forsome}}\,({\it{var\/}}, {\it{exp\/}})\index{forsome})\index{f-implies}\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{ident-axiom}$\;\;$
{\rm{ident-axiom}}\,({\it{var\/}})\index{ident-axiom} $=$ {\rm{f-equal}}\,({\it{var\/}}, {\it{var\/}})\index{f-equal}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{pairequals} \\  
\=\+{\rm{pairequals}}\,({\it{vars1\/}}, {\it{vars2\/}}, {\it{exp\/}})\index{pairequals} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{vars1\/}}) \\ 
{\bf then }{\rm{f-implies}}\,(\=\+{\rm{f-equal}}\,({\rm{car}}\,({\it{vars1\/}}), {\rm{car}}\,({\it{vars2\/}}))\index{f-equal}, \\ 
{\rm{pairequals}}\,({\rm{cdr}}\,({\it{vars1\/}}), {\rm{cdr}}\,({\it{vars2\/}}), {\it{exp\/}})\index{pairequals})\-\index{f-implies} \\ 
{\bf else }{\it{exp\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{equal-axiom2} \\  
\=\+{\rm{equal-axiom2}}\,({\it{vars1\/}}, {\it{vars2\/}}, {\it{pr\/}})\index{equal-axiom2} \\ 
$=$$\;\;\;\;${\rm{pairequals}}\,({\it{vars1\/}}, {\it{vars2\/}}, {\rm{f-implies}}\,({\rm{cons}}\,({\it{pr\/}}, {\it{vars1\/}}), {\rm{cons}}\,({\it{pr\/}}, {\it{vars2\/}}))\index{f-implies})\index{pairequals}\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{assume} \\  
\=\+{\rm{assume}}\,({\it{exp\/}}, {\it{list\/}}, {\it{flg\/}})\index{assume} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{list\/}}) \\ 
{\bf then }\=\+{\bf if }({\rm{caaar}}\,({\it{list\/}}) $=$ {\it{flg\/}}) $\wedge$ ({\it{exp\/}} $=$ {\rm{cadar}}\,({\it{list\/}})) \\ 
{\bf then }{\rm{cdr}}\,({\it{list\/}}) \\ 
{\bf else }{\rm{assume}}\,({\it{exp\/}}, {\rm{cdr}}\,({\it{list\/}}), {\it{flg\/}})\index{assume}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim};Proof-constructors
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{prop-axiom-proof} \\  
\=\+{\rm{prop-axiom-proof}}\,({\it{exp\/}})\index{prop-axiom-proof} \\ 
$=$$\;\;\;\;${\rm{list}}\,({\tt{'}}{\tt{axiom}}, {\rm{list}}\,({\tt{'}}{\tt{prop-axiom}}, {\it{exp\/}}), {\rm{prop-axiom}}\,({\it{exp\/}})\index{prop-axiom})\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{subst-axiom-proof} \\  
\=\+{\rm{subst-axiom-proof}}\,({\it{exp\/}}, {\it{var\/}}, {\it{term\/}})\index{subst-axiom-proof} \\ 
$=$$\;\;\;\;${\rm{list}}\,(\=\+{\tt{'}}{\tt{axiom}}, \\ 
{\rm{list}}\,({\tt{'}}{\tt{subst-axiom}}, {\it{exp\/}}, {\it{var\/}}, {\it{term\/}}), \\ 
{\rm{subst-axiom}}\,({\it{exp\/}}, {\it{var\/}}, {\it{term\/}})\index{subst-axiom})\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{ident-axiom-proof} \\  
\=\+{\rm{ident-axiom-proof}}\,({\it{var\/}})\index{ident-axiom-proof} \\ 
$=$$\;\;\;\;${\rm{list}}\,({\tt{'}}{\tt{axiom}}, {\rm{list}}\,({\tt{'}}{\tt{ident-axiom}}, {\it{var\/}}), {\rm{f-equal}}\,({\it{var\/}}, {\it{var\/}})\index{f-equal})\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{equal-axiom1} \\  
\=\+{\rm{equal-axiom1}}\,({\it{vars1\/}}, {\it{vars2\/}}, {\it{fn\/}})\index{equal-axiom1} \\ 
$=$$\;\;\;\;${\rm{pairequals}}\,({\it{vars1\/}}, {\it{vars2\/}}, {\rm{f-equal}}\,({\rm{cons}}\,({\it{fn\/}}, {\it{vars1\/}}), {\rm{cons}}\,({\it{fn\/}}, {\it{vars2\/}}))\index{f-equal})\index{pairequals}\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{equal-axiom1-proof} \\  
\=\+{\rm{equal-axiom1-proof}}\,({\it{fn\/}}, {\it{vars1\/}}, {\it{vars2\/}})\index{equal-axiom1-proof} \\ 
$=$$\;\;\;\;${\rm{list}}\,(\=\+{\tt{'}}{\tt{axiom}}, \\ 
{\rm{list}}\,({\tt{'}}{\tt{equal-axiom1}}, {\it{fn\/}}, {\it{vars1\/}}, {\it{vars2\/}}), \\ 
{\rm{equal-axiom1}}\,({\it{vars1\/}}, {\it{vars2\/}}, {\it{fn\/}})\index{equal-axiom1})\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{equal-axiom2-proof} \\  
\=\+{\rm{equal-axiom2-proof}}\,({\it{pr\/}}, {\it{vars1\/}}, {\it{vars2\/}})\index{equal-axiom2-proof} \\ 
$=$$\;\;\;\;${\rm{list}}\,(\=\+{\tt{'}}{\tt{axiom}}, \\ 
{\rm{list}}\,({\tt{'}}{\tt{equal-axiom2}}, {\it{pr\/}}, {\it{vars1\/}}, {\it{vars2\/}}), \\ 
{\rm{equal-axiom2}}\,({\it{vars1\/}}, {\it{vars2\/}}, {\it{pr\/}})\index{equal-axiom2})\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{expan-proof} \\  
{\rm{expan-proof}}\,({\it{a\/}}, {\it{b\/}}, {\it{pf\/}})\index{expan-proof} $=$ {\rm{list}}\,({\tt{'}}{\tt{rule}}, {\rm{list}}\,({\tt{'}}{\tt{expan}}, {\it{a\/}}, {\it{b\/}}), {\rm{f-or}}\,({\it{a\/}}, {\it{b\/}})\index{f-or}, {\it{pf\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{contrac-proof} \\  
{\rm{contrac-proof}}\,({\it{a\/}}, {\it{pf\/}})\index{contrac-proof} $=$ {\rm{list}}\,({\tt{'}}{\tt{rule}}, {\rm{list}}\,({\tt{'}}{\tt{contrac}}, {\it{a\/}}), {\it{a\/}}, {\it{pf\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{assoc-proof} \\  
\=\+{\rm{assoc-proof}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}}, {\it{pf\/}})\index{assoc-proof} \\ 
$=$$\;\;\;\;${\rm{list}}\,({\tt{'}}{\tt{rule}}, {\rm{list}}\,({\tt{'}}{\tt{assoc}}, {\it{a\/}}, {\it{b\/}}, {\it{c\/}}), {\rm{f-or}}\,({\rm{f-or}}\,({\it{a\/}}, {\it{b\/}})\index{f-or}, {\it{c\/}})\index{f-or}, {\it{pf\/}})\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{cut-proof} \\  
\=\+{\rm{cut-proof}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}}, {\it{pf1\/}}, {\it{pf2\/}})\index{cut-proof} \\ 
$=$$\;\;\;\;${\rm{list}}\,({\tt{'}}{\tt{rule}}, {\rm{list}}\,({\tt{'}}{\tt{cut}}, {\it{a\/}}, {\it{b\/}}, {\it{c\/}}), {\rm{f-or}}\,({\it{b\/}}, {\it{c\/}})\index{f-or}, {\rm{list}}\,({\it{pf1\/}}, {\it{pf2\/}}))\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{forsome-intro-proof} \\  
\=\+{\rm{forsome-intro-proof}}\,({\it{var\/}}, {\it{a\/}}, {\it{b\/}}, {\it{pf\/}})\index{forsome-intro-proof} \\ 
$=$$\;\;\;\;${\rm{list}}\,({\tt{'}}{\tt{rule}}, {\rm{list}}\,({\tt{'}}{\tt{e-intro}}, {\it{var\/}}, {\it{a\/}}, {\it{b\/}}), {\rm{f-implies}}\,({\rm{forsome}}\,({\it{var\/}}, {\it{a\/}})\index{forsome}, {\it{b\/}})\index{f-implies}, {\it{pf\/}})\-
\end{tabbing}

\noindent{\sc Event}:   Disable atomp; name this event `g2737'.\index{g2737}

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{hint1}$\;\;$
{\rm{hint1}}\,({\it{pf\/}})\index{hint1} $=$ {\rm{caadr}}\,({\it{pf\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{hint2}$\;\;$
{\rm{hint2}}\,({\it{pf\/}})\index{hint2} $=$ {\rm{cadadr}}\,({\it{pf\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{hint3}$\;\;$
{\rm{hint3}}\,({\it{pf\/}})\index{hint3} $=$ {\rm{caddadr}}\,({\it{pf\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{hint4}$\;\;$
{\rm{hint4}}\,({\it{pf\/}})\index{hint4} $=$ {\rm{cadddadr}}\,({\it{pf\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{sub-proof}$\;\;$
{\rm{sub-proof}}\,({\it{pf\/}})\index{sub-proof} $=$ {\rm{cadddr}}\,({\it{pf\/}})
\end{tabbing}
\begin{verbatim};The proof-checker, PF is a proof.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{prf} \\  
\=\+{\rm{prf}}\,({\it{pf\/}})\index{prf} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{pf\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{f}} \\ 
{\bf elseif }{\rm{car}}\,({\it{pf\/}}) $=$ {\tt{'}}{\tt{axiom}} \\ 
{\bf then }\=\+{\bf if }{\rm{hint1}}\,({\it{pf\/}})\index{hint1} $=$ {\tt{'}}{\tt{prop-axiom}} \\ 
{\bf then }\=\+{\rm{formula}}\,({\rm{hint2}}\,({\it{pf\/}})\index{hint2}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;$({\it{pf\/}} $=$ {\rm{prop-axiom-proof}}\,({\rm{hint2}}\,({\it{pf\/}})\index{hint2})\index{prop-axiom-proof})\- \\ 
{\bf elseif }{\rm{hint1}}\,({\it{pf\/}})\index{hint1} $=$ {\tt{'}}{\tt{subst-axiom}} \\ 
{\bf then }\=\+{\rm{formula}}\,({\rm{hint2}}\,({\it{pf\/}})\index{hint2}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{variable}}\,({\rm{hint3}}\,({\it{pf\/}})\index{hint3})\index{variable} \\ 
$\wedge$$\;\;\;\;${\rm{termp}}\,({\rm{hint4}}\,({\it{pf\/}})\index{hint4}, {\bf{t}}, {\tt{0}})\index{termp} \\ 
$\wedge$$\;\;\;\;${\rm{free-for}}\,({\rm{hint2}}\,({\it{pf\/}})\index{hint2}, {\rm{hint3}}\,({\it{pf\/}})\index{hint3}, {\rm{hint4}}\,({\it{pf\/}})\index{hint4}, {\bf{t}})\index{free-for} \\ 
$\wedge$$\;\;\;\;$({\it{pf\/}} $=$ {\rm{subst-axiom-proof}}\,(\=\+{\rm{hint2}}\,({\it{pf\/}})\index{hint2}, \\ 
{\rm{hint3}}\,({\it{pf\/}})\index{hint3}, \\ 
{\rm{hint4}}\,({\it{pf\/}})\index{hint4})\-\index{subst-axiom-proof})\- \\ 
{\bf elseif }{\rm{hint1}}\,({\it{pf\/}})\index{hint1} $=$ {\tt{'}}{\tt{ident-axiom}} \\ 
{\bf then }\=\+{\rm{variable}}\,({\rm{hint2}}\,({\it{pf\/}})\index{hint2})\index{variable} \\ 
$\wedge$$\;\;\;\;$({\it{pf\/}} $=$ {\rm{ident-axiom-proof}}\,({\rm{hint2}}\,({\it{pf\/}})\index{hint2})\index{ident-axiom-proof})\- \\ 
{\bf elseif }{\rm{hint1}}\,({\it{pf\/}})\index{hint1} $=$ {\tt{'}}{\tt{equal-axiom1}} \\ 
{\bf then }\=\+{\rm{function}}\,({\rm{hint2}}\,({\it{pf\/}})\index{hint2})\index{function} \\ 
$\wedge$$\;\;\;\;${\rm{var-list}}\,({\rm{hint3}}\,({\it{pf\/}})\index{hint3}, {\rm{degree}}\,({\rm{hint2}}\,({\it{pf\/}})\index{hint2})\index{degree})\index{var-list} \\ 
$\wedge$$\;\;\;\;${\rm{var-list}}\,({\rm{hint4}}\,({\it{pf\/}})\index{hint4}, {\rm{degree}}\,({\rm{hint2}}\,({\it{pf\/}})\index{hint2})\index{degree})\index{var-list} \\ 
$\wedge$$\;\;\;\;$({\it{pf\/}} $=$ {\rm{equal-axiom1-proof}}\,(\=\+{\rm{hint2}}\,({\it{pf\/}})\index{hint2}, \\ 
{\rm{hint3}}\,({\it{pf\/}})\index{hint3}, \\ 
{\rm{hint4}}\,({\it{pf\/}})\index{hint4})\-\index{equal-axiom1-proof})\- \\ 
{\bf elseif }{\rm{hint1}}\,({\it{pf\/}})\index{hint1} $=$ {\tt{'}}{\tt{equal-axiom2}} \\ 
{\bf then }\=\+{\rm{predicate}}\,({\rm{hint2}}\,({\it{pf\/}})\index{hint2})\index{predicate} \\ 
$\wedge$$\;\;\;\;${\rm{var-list}}\,({\rm{hint3}}\,({\it{pf\/}})\index{hint3}, {\rm{degree}}\,({\rm{hint2}}\,({\it{pf\/}})\index{hint2})\index{degree})\index{var-list} \\ 
$\wedge$$\;\;\;\;${\rm{var-list}}\,({\rm{hint4}}\,({\it{pf\/}})\index{hint4}, {\rm{degree}}\,({\rm{hint2}}\,({\it{pf\/}})\index{hint2})\index{degree})\index{var-list} \\ 
$\wedge$$\;\;\;\;$({\it{pf\/}} $=$ {\rm{equal-axiom2-proof}}\,(\=\+{\rm{hint2}}\,({\it{pf\/}})\index{hint2}, \\ 
{\rm{hint3}}\,({\it{pf\/}})\index{hint3}, \\ 
{\rm{hint4}}\,({\it{pf\/}})\index{hint4})\-\index{equal-axiom2-proof})\- \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{car}}\,({\it{pf\/}}) $=$ {\tt{'}}{\tt{rule}} \\ 
{\bf then }\=\+{\bf if }{\rm{hint1}}\,({\it{pf\/}})\index{hint1} $=$ {\tt{'}}{\tt{expan}} \\ 
{\bf then }\=\+{\rm{formula}}\,({\rm{hint2}}\,({\it{pf\/}})\index{hint2}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;$({\it{pf\/}} $=$ {\rm{expan-proof}}\,(\=\+{\rm{hint2}}\,({\it{pf\/}})\index{hint2}, \\ 
{\rm{hint3}}\,({\it{pf\/}})\index{hint3}, \\ 
{\rm{sub-proof}}\,({\it{pf\/}})\index{sub-proof})\-\index{expan-proof}) \\ 
$\wedge$$\;\;\;\;$({\rm{conc}}\,({\rm{sub-proof}}\,({\it{pf\/}})\index{sub-proof}, {\bf{t}})\index{conc} $=$ {\rm{hint3}}\,({\it{pf\/}})\index{hint3}) \\ 
$\wedge$$\;\;\;\;${\rm{prf}}\,({\rm{sub-proof}}\,({\it{pf\/}})\index{sub-proof})\index{prf}\- \\ 
{\bf elseif }{\rm{hint1}}\,({\it{pf\/}})\index{hint1} $=$ {\tt{'}}{\tt{contrac}} \\ 
{\bf then }\=\+({\it{pf\/}} $=$ {\rm{contrac-proof}}\,({\rm{hint2}}\,({\it{pf\/}})\index{hint2}, {\rm{sub-proof}}\,({\it{pf\/}})\index{sub-proof})\index{contrac-proof}) \\ 
$\wedge$$\;\;\;\;$({\rm{conc}}\,({\rm{sub-proof}}\,({\it{pf\/}})\index{sub-proof}, {\bf{t}})\index{conc} $=$ {\rm{f-or}}\,({\rm{hint2}}\,({\it{pf\/}})\index{hint2}, {\rm{hint2}}\,({\it{pf\/}})\index{hint2})\index{f-or}) \\ 
$\wedge$$\;\;\;\;${\rm{prf}}\,({\rm{sub-proof}}\,({\it{pf\/}})\index{sub-proof})\index{prf}\- \\ 
{\bf elseif }{\rm{hint1}}\,({\it{pf\/}})\index{hint1} $=$ {\tt{'}}{\tt{assoc}} \\ 
{\bf then }\=\+({\it{pf\/}} $=$ {\rm{assoc-proof}}\,(\=\+{\rm{hint2}}\,({\it{pf\/}})\index{hint2}, \\ 
{\rm{hint3}}\,({\it{pf\/}})\index{hint3}, \\ 
{\rm{hint4}}\,({\it{pf\/}})\index{hint4}, \\ 
{\rm{sub-proof}}\,({\it{pf\/}})\index{sub-proof})\-\index{assoc-proof}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{conc}}\,({\rm{sub-proof}}\,({\it{pf\/}})\index{sub-proof}, {\bf{t}})\index{conc} \\ 
$=$$\;\;\;\;${\rm{f-or}}\,({\rm{hint2}}\,({\it{pf\/}})\index{hint2}, {\rm{f-or}}\,({\rm{hint3}}\,({\it{pf\/}})\index{hint3}, {\rm{hint4}}\,({\it{pf\/}})\index{hint4})\index{f-or})\index{f-or})\- \\ 
$\wedge$$\;\;\;\;${\rm{prf}}\,({\rm{sub-proof}}\,({\it{pf\/}})\index{sub-proof})\index{prf}\- \\ 
{\bf elseif }{\rm{hint1}}\,({\it{pf\/}})\index{hint1} $=$ {\tt{'}}{\tt{cut}} \\ 
{\bf then }\=\+({\it{pf\/}} $=$ {\rm{cut-proof}}\,(\=\+{\rm{hint2}}\,({\it{pf\/}})\index{hint2}, \\ 
{\rm{hint3}}\,({\it{pf\/}})\index{hint3}, \\ 
{\rm{hint4}}\,({\it{pf\/}})\index{hint4}, \\ 
{\rm{car}}\,({\rm{sub-proof}}\,({\it{pf\/}})\index{sub-proof}), \\ 
{\rm{cadr}}\,({\rm{sub-proof}}\,({\it{pf\/}})\index{sub-proof}))\-\index{cut-proof}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{conc}}\,({\rm{sub-proof}}\,({\it{pf\/}})\index{sub-proof}, {\tt{'}}{\tt{list}})\index{conc} \\ 
$=$$\;\;\;\;${\rm{list}}\,(\=\+{\rm{f-or}}\,({\rm{hint2}}\,({\it{pf\/}})\index{hint2}, {\rm{hint3}}\,({\it{pf\/}})\index{hint3})\index{f-or}, \\ 
{\rm{f-or}}\,({\rm{f-not}}\,({\rm{hint2}}\,({\it{pf\/}})\index{hint2})\index{f-not}, {\rm{hint4}}\,({\it{pf\/}})\index{hint4})\index{f-or})\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{prf}}\,({\rm{car}}\,({\rm{sub-proof}}\,({\it{pf\/}})\index{sub-proof}))\index{prf} \\ 
$\wedge$$\;\;\;\;${\rm{prf}}\,({\rm{cadr}}\,({\rm{sub-proof}}\,({\it{pf\/}})\index{sub-proof}))\index{prf}\- \\ 
{\bf elseif }{\rm{hint1}}\,({\it{pf\/}})\index{hint1} $=$ {\tt{'}}{\tt{e-intro}} \\ 
{\bf then }\=\+{\rm{variable}}\,({\rm{hint2}}\,({\it{pf\/}})\index{hint2})\index{variable} \\ 
$\wedge$$\;\;\;\;$({\it{pf\/}} $=$ {\rm{forsome-intro-proof}}\,(\=\+{\rm{hint2}}\,({\it{pf\/}})\index{hint2}, \\ 
{\rm{hint3}}\,({\it{pf\/}})\index{hint3}, \\ 
{\rm{hint4}}\,({\it{pf\/}})\index{hint4}, \\ 
{\rm{sub-proof}}\,({\it{pf\/}})\index{sub-proof})\-\index{forsome-intro-proof}) \\ 
$\wedge$$\;\;\;\;$({\rm{hint2}}\,({\it{pf\/}})\index{hint2} $\not\in$ {\rm{collect-free}}\,({\rm{hint4}}\,({\it{pf\/}})\index{hint4}, {\bf{t}})\index{collect-free}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{conc}}\,({\rm{sub-proof}}\,({\it{pf\/}})\index{sub-proof}, {\bf{t}})\index{conc} \\ 
$=$$\;\;\;\;${\rm{f-implies}}\,({\rm{hint3}}\,({\it{pf\/}})\index{hint3}, {\rm{hint4}}\,({\it{pf\/}})\index{hint4})\index{f-implies})\- \\ 
$\wedge$$\;\;\;\;${\rm{prf}}\,({\rm{sub-proof}}\,({\it{pf\/}})\index{sub-proof})\index{prf}\- \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  formula-or-reduc \\ \index{formula-or-reduc}
{\rm{formula}}\,({\rm{list}}\,({\tt{'}}{\tt{or}}, {\it{a\/}}, {\it{b\/}}), {\bf{t}}, {\tt{0}})\index{formula} $=$ ({\rm{formula}}\,({\it{a\/}}, {\bf{t}}, {\tt{0}})\index{formula} $\wedge$ {\rm{formula}}\,({\it{b\/}}, {\bf{t}}, {\tt{0}})\index{formula})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  formula-not-reduc \\ \index{formula-not-reduc}
{\rm{formula}}\,({\rm{list}}\,({\tt{'}}{\tt{not}}, {\it{a\/}}), {\bf{t}}, {\tt{0}})\index{formula} $=$ {\rm{formula}}\,({\it{a\/}}, {\bf{t}}, {\tt{0}})\index{formula}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  formula-forsome-reduc \\ \index{formula-forsome-reduc}
{\rm{formula}}\,({\rm{list}}\,({\tt{'}}{\tt{forsome}}, {\it{x\/}}, {\it{a\/}}), {\bf{t}}, {\tt{0}})\index{formula} $=$ ({\rm{variable}}\,({\it{x\/}})\index{variable} $\wedge$ {\rm{formula}}\,({\it{a\/}}, {\bf{t}}, {\tt{0}})\index{formula})
\end{tabbing}
\begin{verbatim};PF is a valid proof of EXP.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{proves} \\  
{\rm{proves}}\,({\it{pf\/}}, {\it{exp\/}})\index{proves} $=$ (({\rm{conc}}\,({\it{pf\/}}, {\bf{t}})\index{conc} $=$ {\it{exp\/}}) $\wedge$ {\rm{formula}}\,({\it{exp\/}}, {\bf{t}}, {\tt{0}})\index{formula} $\wedge$ {\rm{prf}}\,({\it{pf\/}})\index{prf})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  proves-is-formula \\ \index{proves-is-formula}
{\rm{proves}}\,({\it{pf\/}}, {\it{exp\/}})\index{proves} $\rightarrow$ {\rm{formula}}\,({\it{exp\/}}, {\bf{t}}, {\tt{0}})\index{formula}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  proves-is-formula-again \\ \index{proves-is-formula-again}
($\neg$ {\rm{formula}}\,({\it{exp\/}}, {\bf{t}}, {\tt{0}})\index{formula}) $\rightarrow$ ($\neg$ {\rm{proves}}\,({\it{pf\/}}, {\it{exp\/}})\index{proves})
\end{tabbing}
\begin{verbatim};Getting rid of PRF by lemmas.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  prop-axiom-proves \\ \index{prop-axiom-proves}
\=\+({\rm{formula}}\,({\it{exp\/}}, {\bf{t}}, {\tt{0}})\index{formula} $\wedge$ ({\it{concl\/}} $=$ {\rm{f-or}}\,({\rm{f-not}}\,({\it{exp\/}})\index{f-not}, {\it{exp\/}})\index{f-or})) \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{prop-axiom-proof}}\,({\it{exp\/}})\index{prop-axiom-proof}, {\it{concl\/}})\index{proves}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  subst-axiom-proves \\ \index{subst-axiom-proves}
\=\+(\=\+{\rm{formula}}\,({\it{concl\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{variable}}\,({\it{var\/}})\index{variable} \\ 
$\wedge$$\;\;\;\;${\rm{termp}}\,({\it{term\/}}, {\bf{t}}, {\tt{0}})\index{termp} \\ 
$\wedge$$\;\;\;\;${\rm{free-for}}\,({\it{exp\/}}, {\it{var\/}}, {\it{term\/}}, {\bf{t}})\index{free-for} \\ 
$\wedge$$\;\;\;\;$({\it{concl\/}} $=$ {\rm{subst-axiom}}\,({\it{exp\/}}, {\it{var\/}}, {\it{term\/}})\index{subst-axiom}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{subst-axiom-proof}}\,({\it{exp\/}}, {\it{var\/}}, {\it{term\/}})\index{subst-axiom-proof}, {\it{concl\/}})\index{proves}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  equal-axiom1-proves \\ \index{equal-axiom1-proves}
\=\+(\=\+{\rm{function}}\,({\it{fn\/}})\index{function} \\ 
$\wedge$$\;\;\;\;${\rm{var-list}}\,({\it{vars1\/}}, {\rm{degree}}\,({\it{fn\/}})\index{degree})\index{var-list} \\ 
$\wedge$$\;\;\;\;${\rm{var-list}}\,({\it{vars2\/}}, {\rm{degree}}\,({\it{fn\/}})\index{degree})\index{var-list} \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\it{concl\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;$({\it{concl\/}} $=$ {\rm{equal-axiom1}}\,({\it{vars1\/}}, {\it{vars2\/}}, {\it{fn\/}})\index{equal-axiom1}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{equal-axiom1-proof}}\,({\it{fn\/}}, {\it{vars1\/}}, {\it{vars2\/}})\index{equal-axiom1-proof}, {\it{concl\/}})\index{proves}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  equal-axiom2-proves \\ \index{equal-axiom2-proves}
\=\+(\=\+{\rm{predicate}}\,({\it{pr\/}})\index{predicate} \\ 
$\wedge$$\;\;\;\;${\rm{var-list}}\,({\it{vars1\/}}, {\rm{degree}}\,({\it{pr\/}})\index{degree})\index{var-list} \\ 
$\wedge$$\;\;\;\;${\rm{var-list}}\,({\it{vars2\/}}, {\rm{degree}}\,({\it{pr\/}})\index{degree})\index{var-list} \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\it{concl\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;$({\it{concl\/}} $=$ {\rm{equal-axiom2}}\,({\it{vars1\/}}, {\it{vars2\/}}, {\it{pr\/}})\index{equal-axiom2}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{equal-axiom2-proof}}\,({\it{pr\/}}, {\it{vars1\/}}, {\it{vars2\/}})\index{equal-axiom2-proof}, {\it{concl\/}})\index{proves}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  ident-axiom-proves \\ \index{ident-axiom-proves}
\=\+({\rm{variable}}\,({\it{var\/}})\index{variable} $\wedge$ ({\it{concl\/}} $=$ {\rm{ident-axiom}}\,({\it{var\/}})\index{ident-axiom}) $\wedge$ {\rm{formula}}\,({\it{concl\/}}, {\bf{t}}, {\tt{0}})\index{formula}) \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{ident-axiom-proof}}\,({\it{var\/}})\index{ident-axiom-proof}, {\it{concl\/}})\index{proves}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  expan-proof-proves \\ \index{expan-proof-proves}
\=\+({\rm{formula}}\,({\it{a\/}}, {\bf{t}}, {\tt{0}})\index{formula} $\wedge$ {\rm{proves}}\,({\it{pf\/}}, {\it{b\/}})\index{proves} $\wedge$ ({\it{concl\/}} $=$ {\rm{f-or}}\,({\it{a\/}}, {\it{b\/}})\index{f-or})) \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{expan-proof}}\,({\it{a\/}}, {\it{b\/}}, {\it{pf\/}})\index{expan-proof}, {\it{concl\/}})\index{proves}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  contrac-proof-proves \\ \index{contrac-proof-proves}
{\rm{proves}}\,({\it{pf\/}}, {\rm{f-or}}\,({\it{a\/}}, {\it{a\/}})\index{f-or})\index{proves} $\rightarrow$ {\rm{proves}}\,({\rm{contrac-proof}}\,({\it{a\/}}, {\it{pf\/}})\index{contrac-proof}, {\it{a\/}})\index{proves}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  assoc-proof-proves \\ \index{assoc-proof-proves}
\=\+({\rm{proves}}\,({\it{pf\/}}, {\rm{f-or}}\,({\it{a\/}}, {\rm{f-or}}\,({\it{b\/}}, {\it{c\/}})\index{f-or})\index{f-or})\index{proves} $\wedge$ ({\it{concl\/}} $=$ {\rm{f-or}}\,({\rm{f-or}}\,({\it{a\/}}, {\it{b\/}})\index{f-or}, {\it{c\/}})\index{f-or})) \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{assoc-proof}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}}, {\it{pf\/}})\index{assoc-proof}, {\it{concl\/}})\index{proves}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  cut-proof-proves \\ \index{cut-proof-proves}
\=\+(\=\+{\rm{proves}}\,({\it{pf1\/}}, {\rm{f-or}}\,({\it{a\/}}, {\it{b\/}})\index{f-or})\index{proves} \\ 
$\wedge$$\;\;\;\;${\rm{proves}}\,({\it{pf2\/}}, {\rm{f-or}}\,({\rm{f-not}}\,({\it{a\/}})\index{f-not}, {\it{c\/}})\index{f-or})\index{proves} \\ 
$\wedge$$\;\;\;\;$({\it{concl\/}} $=$ {\rm{f-or}}\,({\it{b\/}}, {\it{c\/}})\index{f-or}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{cut-proof}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}}, {\it{pf1\/}}, {\it{pf2\/}})\index{cut-proof}, {\it{concl\/}})\index{proves}\-
\end{tabbing}
\begin{verbatim};disabling the proof-constructors since the lemmas above show they work.
\end{verbatim}
\noindent{\sc Event}:   Enable prop-axiom-proof; name this event `g2752'.\index{g2752}

\addvspace{18pt}

\noindent{\sc Event}:   Enable subst-axiom-proof; name this event `g2753'.\index{g2753}

\addvspace{18pt}

\noindent{\sc Event}:   Enable equal-axiom1-proof; name this event `g2754'.\index{g2754}

\addvspace{18pt}

\noindent{\sc Event}:   Enable equal-axiom2-proof; name this event `g2755'.\index{g2755}

\addvspace{18pt}

\noindent{\sc Event}:   Enable ident-axiom-proof; name this event `g2756'.\index{g2756}

\addvspace{18pt}

\noindent{\sc Event}:   Enable expan-proof; name this event `g2759'.\index{g2759}

\addvspace{18pt}

\noindent{\sc Event}:   Enable contrac-proof; name this event `g2760'.\index{g2760}

\addvspace{18pt}

\noindent{\sc Event}:   Enable assoc-proof; name this event `g2761'.\index{g2761}

\addvspace{18pt}

\noindent{\sc Event}:   Enable cut-proof; name this event `g2762'.\index{g2762}

\addvspace{18pt}
\begin{tabbing}{\sc Theorem}:  forsome-intro-proves \\ \index{forsome-intro-proves}
\=\+(\=\+{\rm{proves}}\,({\it{pf\/}}, {\rm{f-implies}}\,({\it{a\/}}, {\it{b\/}})\index{f-implies})\index{proves} \\ 
$\wedge$$\;\;\;\;$({\it{var\/}} $\not\in$ {\rm{collect-free}}\,({\it{b\/}}, {\bf{t}})\index{collect-free}) \\ 
$\wedge$$\;\;\;\;${\rm{variable}}\,({\it{var\/}})\index{variable} \\ 
$\wedge$$\;\;\;\;$({\it{a-prime\/}} $=$ {\rm{f-implies}}\,({\rm{forsome}}\,({\it{var\/}}, {\it{a\/}})\index{forsome}, {\it{b\/}})\index{f-implies}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{forsome-intro-proof}}\,({\it{var\/}}, {\it{a\/}}, {\it{b\/}}, {\it{pf\/}})\index{forsome-intro-proof}, {\it{a-prime\/}})\index{proves}\-
\end{tabbing}

\noindent{\sc Event}:   Enable forsome-intro-proof; name this event `g2763'.\index{g2763}

\addvspace{18pt}

\noindent{\sc Event}:   Enable prf; name this event `g2764'.\index{g2764}

\addvspace{18pt}

\noindent{\sc Event}:   Enable proves; name this event `g2765'.\index{g2765}

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{commut-proof} \\  
{\rm{commut-proof}}\,({\it{a\/}}, {\it{b\/}}, {\it{pf\/}})\index{commut-proof} $=$ {\rm{cut-proof}}\,({\it{a\/}}, {\it{b\/}}, {\it{a\/}}, {\it{pf\/}}, {\rm{prop-axiom-proof}}\,({\it{a\/}})\index{prop-axiom-proof})\index{cut-proof}
\end{tabbing}
\begin{verbatim};The first derived inference rule - commutativity of disjunction.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  commut-proof-proves \\ \index{commut-proof-proves}
\=\+({\rm{proves}}\,({\it{pf\/}}, {\rm{f-or}}\,({\it{a\/}}, {\it{b\/}})\index{f-or})\index{proves} $\wedge$ {\rm{formula}}\,({\rm{f-or}}\,({\it{a\/}}, {\it{b\/}})\index{f-or}, {\bf{t}}, {\tt{0}})\index{formula} $\wedge$ ({\it{concl\/}} $=$ {\rm{f-or}}\,({\it{b\/}}, {\it{a\/}})\index{f-or})) \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{commut-proof}}\,({\it{a\/}}, {\it{b\/}}, {\it{pf\/}})\index{commut-proof}, {\it{concl\/}})\index{proves}\-
\end{tabbing}

\noindent{\sc Event}:   Enable commut-proof; name this event `g2766'.\index{g2766}

\addvspace{18pt}
\begin{verbatim};Modus Ponens.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{detach-proof} \\  
\=\+{\rm{detach-proof}}\,({\it{a\/}}, {\it{b\/}}, {\it{pf1\/}}, {\it{pf2\/}})\index{detach-proof} \\ 
$=$$\;\;\;\;${\rm{contrac-proof}}\,(\=\+{\it{b\/}}, \\ 
{\rm{cut-proof}}\,(\=\+{\it{a\/}}, \\ 
{\it{b\/}}, \\ 
{\it{b\/}}, \\ 
{\rm{commut-proof}}\,({\it{b\/}}, {\it{a\/}}, {\rm{expan-proof}}\,({\it{b\/}}, {\it{a\/}}, {\it{pf1\/}})\index{expan-proof})\index{commut-proof}, \\ 
{\it{pf2\/}})\-\index{cut-proof})\-\index{contrac-proof}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  detach-proof-proves1 \\ \index{detach-proof-proves1}
\=\+({\rm{proves}}\,({\it{pf1\/}}, {\it{a\/}})\index{proves} $\wedge$ {\rm{proves}}\,({\it{pf2\/}}, {\rm{f-implies}}\,({\it{a\/}}, {\it{b\/}})\index{f-implies})\index{proves} $\wedge$ {\rm{formula}}\,({\it{b\/}}, {\bf{t}}, {\tt{0}})\index{formula}) \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{detach-proof}}\,({\it{a\/}}, {\it{b\/}}, {\it{pf1\/}}, {\it{pf2\/}})\index{detach-proof}, {\it{b\/}})\index{proves}\-
\end{tabbing}

\noindent{\sc Event}:   Enable detach-proof; name this event `g2767'.\index{g2767}

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{proves-list} \\  
\=\+{\rm{proves-list}}\,({\it{pflist\/}}, {\it{explist\/}})\index{proves-list} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{explist\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\it{pflist\/}} $=$ {\bf{nil}} \\ 
{\bf else }\=\+{\rm{proves}}\,({\rm{car}}\,({\it{pflist\/}}), {\rm{car}}\,({\it{explist\/}}))\index{proves} \\ 
$\wedge$$\;\;\;\;${\rm{proves-list}}\,({\rm{cdr}}\,({\it{pflist\/}}), {\rm{cdr}}\,({\it{explist\/}}))\index{proves-list}\-$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{list-implies} \\  
\=\+{\rm{list-implies}}\,({\it{list\/}}, {\it{conc\/}})\index{list-implies} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{list\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\it{conc\/}} \\ 
{\bf elseif }{\rm{cdr}}\,({\it{list\/}}) $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\rm{f-implies}}\,({\rm{car}}\,({\it{list\/}}), {\it{conc\/}})\index{f-implies} \\ 
{\bf else }{\rm{f-implies}}\,({\rm{car}}\,({\it{list\/}}), {\rm{list-implies}}\,({\rm{cdr}}\,({\it{list\/}}), {\it{conc\/}})\index{list-implies})\index{f-implies}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{list-detach-proof} \\  
\=\+{\rm{list-detach-proof}}\,({\it{alist\/}}, {\it{b\/}}, {\it{pflist\/}}, {\it{pf2\/}})\index{list-detach-proof} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{alist\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\it{pf2\/}} \\ 
{\bf elseif }{\rm{cdr}}\,({\it{alist\/}}) $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\rm{detach-proof}}\,({\rm{car}}\,({\it{alist\/}}), {\it{b\/}}, {\rm{car}}\,({\it{pflist\/}}), {\it{pf2\/}})\index{detach-proof} \\ 
{\bf else }{\rm{list-detach-proof}}\,(\=\+{\rm{cdr}}\,({\it{alist\/}}), \\ 
{\it{b\/}}, \\ 
{\rm{cdr}}\,({\it{pflist\/}}), \\ 
{\rm{detach-proof}}\,(\=\+{\rm{car}}\,({\it{alist\/}}), \\ 
{\rm{list-implies}}\,({\rm{cdr}}\,({\it{alist\/}}), {\it{b\/}})\index{list-implies}, \\ 
{\rm{car}}\,({\it{pflist\/}}), \\ 
{\it{pf2\/}})\-\index{detach-proof})\-\index{list-detach-proof}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim};Chained Modus Ponens.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  detach-list-implies \\ \index{detach-list-implies}
\=\+(\=\+{\rm{list}}\,({\it{c\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{proves}}\,({\it{pf\/}}, {\it{a\/}})\index{proves} \\ 
$\wedge$$\;\;\;\;${\rm{proves}}\,({\it{pf2\/}}, {\rm{list-implies}}\,({\rm{cons}}\,({\it{a\/}}, {\it{c\/}}), {\it{b\/}})\index{list-implies})\index{proves} \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\it{a\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\rm{list-implies}}\,({\it{c\/}}, {\it{b\/}})\index{list-implies}, {\bf{t}}, {\tt{0}})\index{formula})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{detach-proof}}\,({\it{a\/}}, {\rm{list-implies}}\,({\it{c\/}}, {\it{b\/}})\index{list-implies}, {\it{pf\/}}, {\it{pf2\/}})\index{detach-proof}, {\rm{list-implies}}\,({\it{c\/}}, {\it{b\/}})\index{list-implies})\index{proves}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  formula-list-implies \\ \index{formula-list-implies}
\=\+({\rm{formula}}\,({\rm{list-implies}}\,({\it{alist\/}}, {\it{b\/}})\index{list-implies}, {\bf{t}}, {\tt{0}})\index{formula} $\wedge$ {\rm{listp}}\,({\it{alist\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{formula}}\,({\rm{list-implies}}\,({\rm{cdr}}\,({\it{alist\/}}), {\it{b\/}})\index{list-implies}, {\bf{t}}, {\tt{0}})\index{formula}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  detach-rule-corr \\ \index{detach-rule-corr}
\=\+(\=\+{\rm{proves-list}}\,({\it{pflist\/}}, {\it{alist\/}})\index{proves-list} \\ 
$\wedge$$\;\;\;\;${\rm{proves}}\,({\it{pf2\/}}, {\rm{list-implies}}\,({\it{alist\/}}, {\it{b\/}})\index{list-implies})\index{proves} \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\it{b\/}}, {\bf{t}}, {\tt{0}})\index{formula})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{list-detach-proof}}\,({\it{alist\/}}, {\it{b\/}}, {\it{pflist\/}}, {\it{pf2\/}})\index{list-detach-proof}, {\it{b\/}})\index{proves}\-
\end{tabbing}

\noindent{\sc Event}:   Enable list-detach-proof; name this event `g0220'.\index{g0220}

\addvspace{18pt}

\noindent{\sc Event}:   Enable detach-list-implies; name this event `g0221'.\index{g0221}

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{rt-expan-proof} \\  
{\rm{rt-expan-proof}}\,({\it{a\/}}, {\it{b\/}}, {\it{pf\/}})\index{rt-expan-proof} $=$ {\rm{commut-proof}}\,({\it{b\/}}, {\it{a\/}}, {\rm{expan-proof}}\,({\it{b\/}}, {\it{a\/}}, {\it{pf\/}})\index{expan-proof})\index{commut-proof}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  rt-expan-proof-proves \\ \index{rt-expan-proof-proves}
\=\+({\rm{proves}}\,({\it{pf\/}}, {\it{a\/}})\index{proves} $\wedge$ {\rm{formula}}\,({\it{b\/}}, {\bf{t}}, {\tt{0}})\index{formula} $\wedge$ ({\it{concl\/}} $=$ {\rm{f-or}}\,({\it{a\/}}, {\it{b\/}})\index{f-or})) \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{rt-expan-proof}}\,({\it{a\/}}, {\it{b\/}}, {\it{pf\/}})\index{rt-expan-proof}, {\it{concl\/}})\index{proves}\-
\end{tabbing}

\noindent{\sc Event}:   Enable rt-expan-proof; name this event `g0227'.\index{g0227}

\addvspace{18pt}
\begin{verbatim};Takes list of formulas and returns disjunction.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{make-disjunct} \\  
\=\+{\rm{make-disjunct}}\,({\it{flist\/}})\index{make-disjunct} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{flist\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }{\rm{cdr}}\,({\it{flist\/}}) $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\rm{car}}\,({\it{flist\/}}) \\ 
{\bf else }{\rm{f-or}}\,({\rm{car}}\,({\it{flist\/}}), {\rm{make-disjunct}}\,({\rm{cdr}}\,({\it{flist\/}}))\index{make-disjunct})\index{f-or}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{m1-proof} \\  
\=\+{\rm{m1-proof}}\,({\it{exp\/}}, {\it{flist\/}}, {\it{pf\/}})\index{m1-proof} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{flist\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }{\rm{cdr}}\,({\it{flist\/}}) $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\it{pf\/}} \\ 
{\bf elseif }{\it{exp\/}} $=$ {\rm{car}}\,({\it{flist\/}}) \\ 
{\bf then }{\rm{rt-expan-proof}}\,({\rm{car}}\,({\it{flist\/}}), {\rm{make-disjunct}}\,({\rm{cdr}}\,({\it{flist\/}}))\index{make-disjunct}, {\it{pf\/}})\index{rt-expan-proof} \\ 
{\bf else }{\rm{expan-proof}}\,(\=\+{\rm{car}}\,({\it{flist\/}}), \\ 
{\rm{make-disjunct}}\,({\rm{cdr}}\,({\it{flist\/}}))\index{make-disjunct}, \\ 
{\rm{m1-proof}}\,({\it{exp\/}}, {\rm{cdr}}\,({\it{flist\/}}), {\it{pf\/}})\index{m1-proof})\-\index{expan-proof}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  m1-proof-proves1 \\ \index{m1-proof-proves1}
\=\+({\rm{formula}}\,({\rm{make-disjunct}}\,({\it{flist\/}})\index{make-disjunct}, {\bf{t}}, {\tt{0}})\index{formula} $\wedge$ ({\it{exp\/}} $\in$ {\it{flist\/}}) $\wedge$ {\rm{proves}}\,({\it{pf\/}}, {\it{exp\/}})\index{proves}) \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{m1-proof}}\,({\it{exp\/}}, {\it{flist\/}}, {\it{pf\/}})\index{m1-proof}, {\rm{make-disjunct}}\,({\it{flist\/}})\index{make-disjunct})\index{proves}\-
\end{tabbing}

\noindent{\sc Event}:   Enable m1-proof; name this event `g0228'.\index{g0228}

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{rt-assoc-proof} \\  
\=\+{\rm{rt-assoc-proof}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}}, {\it{pf\/}})\index{rt-assoc-proof} \\ 
$=$$\;\;\;\;${\rm{commut-proof}}\,(\=\+{\rm{f-or}}\,({\it{b\/}}, {\it{c\/}})\index{f-or}, \\ 
{\it{a\/}}, \\ 
{\rm{assoc-proof}}\,(\=\+{\it{b\/}}, \\ 
{\it{c\/}}, \\ 
{\it{a\/}}, \\ 
{\rm{commut-proof}}\,(\=\+{\rm{f-or}}\,({\it{c\/}}, {\it{a\/}})\index{f-or}, \\ 
{\it{b\/}}, \\ 
{\rm{assoc-proof}}\,(\=\+{\it{c\/}}, \\ 
{\it{a\/}}, \\ 
{\it{b\/}}, \\ 
{\rm{commut-proof}}\,(\=\+{\rm{f-or}}\,(\=\+{\it{a\/}}, \\ 
{\it{b\/}})\-\index{f-or}, \\ 
{\it{c\/}}, \\ 
{\it{pf\/}})\-\index{commut-proof})\-\index{assoc-proof})\-\index{commut-proof})\-\index{assoc-proof})\-\index{commut-proof}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  rt-assoc-proof-proves \\ \index{rt-assoc-proof-proves}
\=\+(\=\+{\rm{proves}}\,({\it{pf\/}}, {\rm{f-or}}\,({\rm{f-or}}\,({\it{a\/}}, {\it{b\/}})\index{f-or}, {\it{c\/}})\index{f-or})\index{proves} \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\it{a\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\it{b\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\it{c\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;$({\it{concl\/}} $=$ {\rm{f-or}}\,({\it{a\/}}, {\rm{f-or}}\,({\it{b\/}}, {\it{c\/}})\index{f-or})\index{f-or}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{rt-assoc-proof}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}}, {\it{pf\/}})\index{rt-assoc-proof}, {\it{concl\/}})\index{proves}\-
\end{tabbing}

\noindent{\sc Event}:   Enable rt-assoc-proof; name this event `g0231'.\index{g0231}

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{insert-proof} \\  
\=\+{\rm{insert-proof}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}}, {\it{pf\/}})\index{insert-proof} \\ 
$=$$\;\;\;\;${\rm{commut-proof}}\,(\=\+{\rm{f-or}}\,({\it{a\/}}, {\it{c\/}})\index{f-or}, \\ 
{\it{b\/}}, \\ 
{\rm{assoc-proof}}\,(\=\+{\it{a\/}}, \\ 
{\it{c\/}}, \\ 
{\it{b\/}}, \\ 
{\rm{expan-proof}}\,({\it{a\/}}, {\rm{f-or}}\,({\it{c\/}}, {\it{b\/}})\index{f-or}, {\rm{commut-proof}}\,({\it{b\/}}, {\it{c\/}}, {\it{pf\/}})\index{commut-proof})\index{expan-proof})\-\index{assoc-proof})\-\index{commut-proof}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  insert-proof-proves \\ \index{insert-proof-proves}
\=\+(\=\+{\rm{proves}}\,({\it{pf\/}}, {\rm{f-or}}\,({\it{b\/}}, {\it{c\/}})\index{f-or})\index{proves} \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\it{a\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\it{b\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\it{c\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;$({\it{concl\/}} $=$ {\rm{f-or}}\,({\it{b\/}}, {\rm{f-or}}\,({\it{a\/}}, {\it{c\/}})\index{f-or})\index{f-or}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{insert-proof}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}}, {\it{pf\/}})\index{insert-proof}, {\it{concl\/}})\index{proves}\-
\end{tabbing}

\noindent{\sc Event}:   Enable insert-proof; name this event `g0232'.\index{g0232}

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{m2-proof-step} \\  
\=\+{\rm{m2-proof-step}}\,({\it{exp1\/}}, {\it{exp2\/}}, {\it{flist\/}}, {\it{pf\/}})\index{m2-proof-step} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{flist\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }{\rm{cdr}}\,({\it{flist\/}}) $\simeq\;${{\bf{nil}}}${}$ \\ 
{\bf then }\=\+{\bf if }{\it{exp2\/}} $=$ {\rm{car}}\,({\it{flist\/}})$\;\;${\bf then }{\it{pf\/}} \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{exp2\/}} $=$ {\rm{car}}\,({\it{flist\/}}) \\ 
{\bf then }{\rm{rt-assoc-proof}}\,(\=\+{\it{exp1\/}}, \\ 
{\it{exp2\/}}, \\ 
{\rm{make-disjunct}}\,({\rm{cdr}}\,({\it{flist\/}}))\index{make-disjunct}, \\ 
{\rm{rt-expan-proof}}\,(\=\+{\rm{f-or}}\,({\it{exp1\/}}, {\it{exp2\/}})\index{f-or}, \\ 
{\rm{make-disjunct}}\,({\rm{cdr}}\,({\it{flist\/}}))\index{make-disjunct}, \\ 
{\it{pf\/}})\-\index{rt-expan-proof})\-\index{rt-assoc-proof} \\ 
{\bf else }{\rm{insert-proof}}\,(\=\+{\rm{car}}\,({\it{flist\/}}), \\ 
{\it{exp1\/}}, \\ 
{\rm{make-disjunct}}\,({\rm{cdr}}\,({\it{flist\/}}))\index{make-disjunct}, \\ 
{\rm{m2-proof-step}}\,({\it{exp1\/}}, {\it{exp2\/}}, {\rm{cdr}}\,({\it{flist\/}}), {\it{pf\/}})\index{m2-proof-step})\-\index{insert-proof}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  m2-proof-step-proves \\ \index{m2-proof-step-proves}
\=\+(\=\+{\rm{formula}}\,({\rm{make-disjunct}}\,({\it{flist\/}})\index{make-disjunct}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;$({\it{exp2\/}} $\in$ {\it{flist\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\it{exp1\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\it{exp2\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{proves}}\,({\it{pf\/}}, {\rm{f-or}}\,({\it{exp1\/}}, {\it{exp2\/}})\index{f-or})\index{proves})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,(\=\+{\rm{m2-proof-step}}\,({\it{exp1\/}}, {\it{exp2\/}}, {\it{flist\/}}, {\it{pf\/}})\index{m2-proof-step}, \\ 
{\rm{f-or}}\,({\it{exp1\/}}, {\rm{make-disjunct}}\,({\it{flist\/}})\index{make-disjunct})\index{f-or})\-\index{proves}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  m2-proof-step-proves1 \\ \index{m2-proof-step-proves1}
\=\+(\=\+{\rm{formula}}\,({\rm{make-disjunct}}\,({\it{flist\/}})\index{make-disjunct}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;$({\it{exp2\/}} $\in$ {\it{flist\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\it{exp1\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\it{exp2\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{proves}}\,({\it{pf\/}}, {\rm{f-or}}\,({\it{exp1\/}}, {\it{exp2\/}})\index{f-or})\index{proves} \\ 
$\wedge$$\;\;\;\;$({\it{concl\/}} $=$ {\rm{f-or}}\,({\it{exp1\/}}, {\rm{make-disjunct}}\,({\it{flist\/}})\index{make-disjunct})\index{f-or}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{m2-proof-step}}\,({\it{exp1\/}}, {\it{exp2\/}}, {\it{flist\/}}, {\it{pf\/}})\index{m2-proof-step}, {\it{concl\/}})\index{proves}\-
\end{tabbing}

\noindent{\sc Event}:   Enable m2-proof-step; name this event `g0233'.\index{g0233}

\addvspace{18pt}

\noindent{\sc Event}:   Enable m2-proof-step-proves; name this event `g0234'.\index{g0234}

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{m2-proof} \\  
\=\+{\rm{m2-proof}}\,({\it{exp1\/}}, {\it{exp2\/}}, {\it{flist\/}}, {\it{pf\/}})\index{m2-proof} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{flist\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }{\it{exp1\/}} $=$ {\it{exp2\/}}$\;\;${\bf then }{\rm{m1-proof}}\,({\it{exp1\/}}, {\it{flist\/}}, {\rm{contrac-proof}}\,({\it{exp1\/}}, {\it{pf\/}})\index{contrac-proof})\index{m1-proof} \\ 
{\bf elseif }{\it{exp1\/}} $=$ {\rm{car}}\,({\it{flist\/}}) \\ 
{\bf then }{\rm{m2-proof-step}}\,({\it{exp1\/}}, {\it{exp2\/}}, {\rm{cdr}}\,({\it{flist\/}}), {\it{pf\/}})\index{m2-proof-step} \\ 
{\bf elseif }{\it{exp2\/}} $=$ {\rm{car}}\,({\it{flist\/}}) \\ 
{\bf then }{\rm{m2-proof-step}}\,({\it{exp2\/}}, {\it{exp1\/}}, {\rm{cdr}}\,({\it{flist\/}}), {\rm{commut-proof}}\,({\it{exp1\/}}, {\it{exp2\/}}, {\it{pf\/}})\index{commut-proof})\index{m2-proof-step} \\ 
{\bf else }{\rm{expan-proof}}\,(\=\+{\rm{car}}\,({\it{flist\/}}), \\ 
{\rm{make-disjunct}}\,({\rm{cdr}}\,({\it{flist\/}}))\index{make-disjunct}, \\ 
{\rm{m2-proof}}\,({\it{exp1\/}}, {\it{exp2\/}}, {\rm{cdr}}\,({\it{flist\/}}), {\it{pf\/}})\index{m2-proof})\-\index{expan-proof}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  m1-proof-proves \\ \index{m1-proof-proves}
\=\+(\=\+{\rm{formula}}\,({\rm{make-disjunct}}\,({\it{flist\/}})\index{make-disjunct}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;$({\it{exp\/}} $\in$ {\it{flist\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{proves}}\,({\it{pf\/}}, {\it{exp\/}})\index{proves} \\ 
$\wedge$$\;\;\;\;$({\it{concl\/}} $=$ {\rm{make-disjunct}}\,({\it{flist\/}})\index{make-disjunct}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{m1-proof}}\,({\it{exp\/}}, {\it{flist\/}}, {\it{pf\/}})\index{m1-proof}, {\it{concl\/}})\index{proves}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  m2-proof-proves \\ \index{m2-proof-proves}
\=\+(\=\+{\rm{formula}}\,({\rm{make-disjunct}}\,({\it{flist\/}})\index{make-disjunct}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\it{exp1\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\it{exp2\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;$({\it{exp1\/}} $\in$ {\it{flist\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{exp2\/}} $\in$ {\it{flist\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{proves}}\,({\it{pf\/}}, {\rm{f-or}}\,({\it{exp1\/}}, {\it{exp2\/}})\index{f-or})\index{proves})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{m2-proof}}\,({\it{exp1\/}}, {\it{exp2\/}}, {\it{flist\/}}, {\it{pf\/}})\index{m2-proof}, {\rm{make-disjunct}}\,({\it{flist\/}})\index{make-disjunct})\index{proves}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  m2-proof-proves1 \\ \index{m2-proof-proves1}
\=\+(\=\+{\rm{formula}}\,({\rm{make-disjunct}}\,({\it{flist\/}})\index{make-disjunct}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\it{exp1\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\it{exp2\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;$({\it{exp1\/}} $\in$ {\it{flist\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{exp2\/}} $\in$ {\it{flist\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{proves}}\,({\it{pf\/}}, {\rm{f-or}}\,({\it{exp1\/}}, {\it{exp2\/}})\index{f-or})\index{proves} \\ 
$\wedge$$\;\;\;\;$({\it{concl\/}} $=$ {\rm{make-disjunct}}\,({\it{flist\/}})\index{make-disjunct}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{m2-proof}}\,({\it{exp1\/}}, {\it{exp2\/}}, {\it{flist\/}}, {\it{pf\/}})\index{m2-proof}, {\it{concl\/}})\index{proves}\-
\end{tabbing}

\noindent{\sc Event}:   Enable m2-proof; name this event `g0235'.\index{g0235}

\addvspace{18pt}

\noindent{\sc Event}:   Enable m2-proof-proves; name this event `g0236'.\index{g0236}

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{m3-proof} \\  
\=\+{\rm{m3-proof}}\,({\it{exp1\/}}, {\it{exp2\/}}, {\it{flist2\/}}, {\it{pf\/}})\index{m3-proof} \\ 
$=$$\;\;\;\;${\rm{contrac-proof}}\,(\=\+{\rm{make-disjunct}}\,({\it{flist2\/}})\index{make-disjunct}, \\ 
{\rm{contrac-proof}}\,(\=\+{\rm{f-or}}\,(\=\+{\rm{make-disjunct}}\,({\it{flist2\/}})\index{make-disjunct}, \\ 
{\rm{make-disjunct}}\,({\it{flist2\/}})\index{make-disjunct})\-\index{f-or}, \\ 
{\rm{m2-proof}}\,(\=\+{\rm{f-or}}\,(\=\+{\rm{make-disjunct}}\,({\it{flist2\/}})\index{make-disjunct}, \\ 
{\rm{make-disjunct}}\,({\it{flist2\/}})\index{make-disjunct})\-\index{f-or}, \\ 
{\it{exp1\/}}, \\ 
{\rm{cons}}\,(\=\+{\rm{f-or}}\,(\=\+{\rm{make-disjunct}}\,({\it{flist2\/}})\index{make-disjunct}, \\ 
{\rm{make-disjunct}}\,({\it{flist2\/}})\index{make-disjunct})\-\index{f-or}, \\ 
{\rm{cons}}\,(\=\+{\rm{make-disjunct}}\,({\it{flist2\/}})\index{make-disjunct}, \\ 
{\it{flist2\/}})\-)\-, \\ 
{\rm{assoc-proof}}\,(\=\+{\rm{make-disjunct}}\,({\it{flist2\/}})\index{make-disjunct}, \\ 
{\rm{make-disjunct}}\,({\it{flist2\/}})\index{make-disjunct}, \\ 
{\it{exp1\/}}, \\ 
{\rm{commut-proof}}\,(\=\+{\rm{f-or}}\,(\=\+{\rm{make-disjunct}}\,({\it{flist2\/}})\index{make-disjunct}, \\ 
{\it{exp1\/}})\-\index{f-or}, \\ 
{\rm{make-disjunct}}\,({\it{flist2\/}})\index{make-disjunct}, \\ 
{\rm{m2-proof}}\,(\=\+{\rm{f-or}}\,(\=\+{\rm{make-disjunct}}\,({\it{flist2\/}})\index{make-disjunct}, \\ 
{\it{exp1\/}})\-\index{f-or}, \\ 
{\it{exp2\/}}, \\ 
{\rm{cons}}\,(\=\+{\rm{f-or}}\,(\=\+{\rm{make-disjunct}}\,({\it{flist2\/}})\index{make-disjunct}, \\ 
{\it{exp1\/}})\-\index{f-or}, \\ 
{\it{flist2\/}})\-, \\ 
{\rm{assoc-proof}}\,(\=\+{\rm{make-disjunct}}\,({\it{flist2\/}})\index{make-disjunct}, \\ 
{\it{exp1\/}}, \\ 
{\it{exp2\/}}, \\ 
{\rm{commut-proof}}\,(\=\+{\rm{f-or}}\,(\=\+{\it{exp1\/}}, \\ 
{\it{exp2\/}})\-\index{f-or}, \\ 
{\rm{make-disjunct}}\,({\it{flist2\/}})\index{make-disjunct}, \\ 
{\it{pf\/}})\-\index{commut-proof})\-\index{assoc-proof})\-\index{m2-proof})\-\index{commut-proof})\-\index{assoc-proof})\-\index{m2-proof})\-\index{contrac-proof})\-\index{contrac-proof}\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{m-proof} \\  
\=\+{\rm{m-proof}}\,({\it{flist1\/}}, {\it{flist2\/}}, {\it{pf\/}})\index{m-proof} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{flist1\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }{\rm{cdr}}\,({\it{flist1\/}}) $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\rm{m1-proof}}\,({\rm{car}}\,({\it{flist1\/}}), {\it{flist2\/}}, {\it{pf\/}})\index{m1-proof} \\ 
{\bf elseif }{\rm{cddr}}\,({\it{flist1\/}}) $\simeq\;${{\bf{nil}}}${}$ \\ 
{\bf then }{\rm{m2-proof}}\,({\rm{car}}\,({\it{flist1\/}}), {\rm{cadr}}\,({\it{flist1\/}}), {\it{flist2\/}}, {\it{pf\/}})\index{m2-proof} \\ 
{\bf else }{\rm{m3-proof}}\,(\=\+{\rm{car}}\,({\it{flist1\/}}), \\ 
{\rm{cadr}}\,({\it{flist1\/}}), \\ 
{\it{flist2\/}}, \\ 
{\rm{m-proof}}\,(\=\+{\rm{cons}}\,(\=\+{\rm{f-or}}\,({\rm{car}}\,({\it{flist1\/}}), {\rm{cadr}}\,({\it{flist1\/}}))\index{f-or}, \\ 
{\rm{cddr}}\,({\it{flist1\/}}))\-, \\ 
{\rm{cons}}\,(\=\+{\rm{f-or}}\,({\rm{car}}\,({\it{flist1\/}}), {\rm{cadr}}\,({\it{flist1\/}}))\index{f-or}, \\ 
{\it{flist2\/}})\-, \\ 
{\rm{assoc-proof}}\,(\=\+{\rm{car}}\,({\it{flist1\/}}), \\ 
{\rm{cadr}}\,({\it{flist1\/}}), \\ 
{\rm{make-disjunct}}\,({\rm{cddr}}\,({\it{flist1\/}}))\index{make-disjunct}, \\ 
{\it{pf\/}})\-\index{assoc-proof})\-\index{m-proof})\-\index{m3-proof}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  subset-cons \\ \index{subset-cons}
{\rm{subset}}\,({\it{x\/}}, {\it{y\/}})\index{subset} $\rightarrow$ {\rm{subset}}\,({\it{x\/}}, {\rm{cons}}\,({\it{z\/}}, {\it{y\/}}))\index{subset}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{form-list} \\  
\=\+{\rm{form-list}}\,({\it{flist\/}})\index{form-list} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{flist\/}}) \\ 
{\bf then }{\rm{formula}}\,({\rm{car}}\,({\it{flist\/}}), {\bf{t}}, {\tt{0}})\index{formula} $\wedge$ {\rm{form-list}}\,({\rm{cdr}}\,({\it{flist\/}}))\index{form-list} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  formlist-formula-make-disj \\ \index{formlist-formula-make-disj}
({\rm{form-list}}\,({\it{flist\/}})\index{form-list} $\wedge$ {\rm{listp}}\,({\it{flist\/}})) $\rightarrow$ {\rm{formula}}\,({\rm{make-disjunct}}\,({\it{flist\/}})\index{make-disjunct}, {\bf{t}}, {\tt{0}})\index{formula}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  m3-proof-proves \\ \index{m3-proof-proves}
\=\+(\=\+{\rm{formula}}\,({\it{exp1\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\it{exp2\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{form-list}}\,({\it{flist2\/}})\index{form-list} \\ 
$\wedge$$\;\;\;\;${\rm{proves}}\,({\it{pf\/}}, {\rm{make-disjunct}}\,({\rm{cons}}\,({\rm{f-or}}\,({\it{exp1\/}}, {\it{exp2\/}})\index{f-or}, {\it{flist2\/}}))\index{make-disjunct})\index{proves} \\ 
$\wedge$$\;\;\;\;$({\it{exp1\/}} $\in$ {\it{flist2\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{exp2\/}} $\in$ {\it{flist2\/}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{m3-proof}}\,({\it{exp1\/}}, {\it{exp2\/}}, {\it{flist2\/}}, {\it{pf\/}})\index{m3-proof}, {\rm{make-disjunct}}\,({\it{flist2\/}})\index{make-disjunct})\index{proves}\-
\end{tabbing}

\noindent{\sc Event}:   Enable m3-proof; name this event `g0222'.\index{g0222}

\addvspace{18pt}
\begin{tabbing}{\sc Theorem}:  m3-proof-proves1 \\ \index{m3-proof-proves1}
\=\+(\=\+{\rm{formula}}\,({\it{exp1\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\it{exp2\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{form-list}}\,({\it{flist2\/}})\index{form-list} \\ 
$\wedge$$\;\;\;\;${\rm{proves}}\,({\it{pf\/}}, {\rm{make-disjunct}}\,({\rm{cons}}\,({\rm{f-or}}\,({\it{exp1\/}}, {\it{exp2\/}})\index{f-or}, {\it{flist2\/}}))\index{make-disjunct})\index{proves} \\ 
$\wedge$$\;\;\;\;$({\it{exp1\/}} $\in$ {\it{flist2\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{exp2\/}} $\in$ {\it{flist2\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{concl\/}} $=$ {\rm{make-disjunct}}\,({\it{flist2\/}})\index{make-disjunct}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{m3-proof}}\,({\it{exp1\/}}, {\it{exp2\/}}, {\it{flist2\/}}, {\it{pf\/}})\index{m3-proof}, {\it{concl\/}})\index{proves}\-
\end{tabbing}

\noindent{\sc Event}:   Enable m3-proof-proves; name this event `g0229'.\index{g0229}

\addvspace{18pt}
\begin{verbatim};The subset lemma
\end{verbatim}\begin{tabbing}{\sc Theorem}:  m-proof-proves \\ \index{m-proof-proves}
\=\+(\=\+{\rm{form-list}}\,({\it{flist1\/}})\index{form-list} \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{flist1\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{form-list}}\,({\it{flist2\/}})\index{form-list} \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{flist2\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{subset}}\,({\it{flist1\/}}, {\it{flist2\/}})\index{subset} \\ 
$\wedge$$\;\;\;\;${\rm{proves}}\,({\it{pf\/}}, {\rm{make-disjunct}}\,({\it{flist1\/}})\index{make-disjunct})\index{proves})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{m-proof}}\,({\it{flist1\/}}, {\it{flist2\/}}, {\it{pf\/}})\index{m-proof}, {\rm{make-disjunct}}\,({\it{flist2\/}})\index{make-disjunct})\index{proves}\-
\end{tabbing}

\noindent{\sc Event}:   Enable m-proof; name this event `g0247'.\index{g0247}

\addvspace{18pt}
\begin{tabbing}{\sc Theorem}:  m-proof-proves1 \\ \index{m-proof-proves1}
\=\+(\=\+{\rm{form-list}}\,({\it{flist1\/}})\index{form-list} \\ 
$\wedge$$\;\;\;\;${\rm{form-list}}\,({\it{flist2\/}})\index{form-list} \\ 
$\wedge$$\;\;\;\;${\rm{subset}}\,({\it{flist1\/}}, {\it{flist2\/}})\index{subset} \\ 
$\wedge$$\;\;\;\;${\rm{proves}}\,({\it{pf\/}}, {\rm{make-disjunct}}\,({\it{flist1\/}})\index{make-disjunct})\index{proves} \\ 
$\wedge$$\;\;\;\;$({\it{concl\/}} $=$ {\rm{make-disjunct}}\,({\it{flist2\/}})\index{make-disjunct}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{m-proof}}\,({\it{flist1\/}}, {\it{flist2\/}}, {\it{pf\/}})\index{m-proof}, {\it{concl\/}})\index{proves}\-
\end{tabbing}
\begin{verbatim};Disjunctions.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{or-type}$\;\;$
{\rm{or-type}}\,({\it{exp\/}})\index{or-type} $=$ ({\it{exp\/}} $=$ {\rm{f-or}}\,({\rm{cadr}}\,({\it{exp\/}}), {\rm{caddr}}\,({\it{exp\/}}))\index{f-or})
\end{tabbing}
\begin{verbatim};Negation of disjunctions.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{nor-type} \\  
{\rm{nor-type}}\,({\it{exp\/}})\index{nor-type} $=$ ({\it{exp\/}} $=$ {\rm{f-not}}\,({\rm{f-or}}\,({\rm{cadadr}}\,({\it{exp\/}}), {\rm{caddadr}}\,({\it{exp\/}}))\index{f-or})\index{f-not})
\end{tabbing}

\noindent{\sc Event}:   Enable atomp; name this event `g0250'.\index{g0250}

\addvspace{18pt}
\begin{verbatim};Elementary and negation of elementary formulas
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{elem-form} \\  
{\rm{elem-form}}\,({\it{exp\/}})\index{elem-form} $=$ ({\rm{atomp}}\,({\it{exp\/}})\index{atomp} $\vee$ ({\it{exp\/}} $=$ {\rm{forsome}}\,({\rm{cadr}}\,({\it{exp\/}}), {\rm{caddr}}\,({\it{exp\/}}))\index{forsome}))
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{neg-elem-form} \\  
\=\+{\rm{neg-elem-form}}\,({\it{exp\/}})\index{neg-elem-form} \\ 
$=$$\;\;\;\;$(({\it{exp\/}} $=$ {\rm{f-not}}\,({\rm{cadr}}\,({\it{exp\/}}))\index{f-not}) $\wedge$ {\rm{elem-form}}\,({\rm{arg1}}\,({\it{exp\/}})\index{arg1})\index{elem-form})\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{prop-atomp} \\  
{\rm{prop-atomp}}\,({\it{exp\/}})\index{prop-atomp} $=$ ({\rm{elem-form}}\,({\it{exp\/}})\index{elem-form} $\vee$ {\rm{neg-elem-form}}\,({\it{exp\/}})\index{neg-elem-form})
\end{tabbing}
\begin{verbatim};Double-negations
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{dble-neg-type} \\  
{\rm{dble-neg-type}}\,({\it{exp\/}})\index{dble-neg-type} $=$ ({\it{exp\/}} $=$ {\rm{f-not}}\,({\rm{f-not}}\,({\rm{cadadr}}\,({\it{exp\/}}))\index{f-not})\index{f-not})
\end{tabbing}

\noindent{\sc Event}:   Disable atomp; name this event `g0251'.\index{g0251}

\addvspace{18pt}
\begin{tabbing}{\sc Theorem}:  dble-neg-not-prop-atomp \\ \index{dble-neg-not-prop-atomp}
{\rm{dble-neg-type}}\,({\it{exp\/}})\index{dble-neg-type} $\rightarrow$ ($\neg$ {\rm{prop-atomp}}\,({\it{exp\/}})\index{prop-atomp})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  or-type-not-prop-atomp \\ \index{or-type-not-prop-atomp}
{\rm{or-type}}\,({\it{exp\/}})\index{or-type} $\rightarrow$ ($\neg$ {\rm{prop-atomp}}\,({\it{exp\/}})\index{prop-atomp})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  nor-type-not-prop-atomp \\ \index{nor-type-not-prop-atomp}
{\rm{nor-type}}\,({\it{exp\/}})\index{nor-type} $\rightarrow$ ($\neg$ {\rm{prop-atomp}}\,({\it{exp\/}})\index{prop-atomp})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{list-count} \\  
\=\+{\rm{list-count}}\,({\it{list\/}})\index{list-count} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{list\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }($1\;+$ {\rm{count}}\,({\rm{car}}\,({\it{list\/}}))) $+$ {\rm{list-count}}\,({\rm{cdr}}\,({\it{list\/}}))\index{list-count}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{neg-list} \\  
\=\+{\rm{neg-list}}\,({\it{exp\/}}, {\it{list\/}})\index{neg-list} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{list\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{f}} \\ 
{\bf else }{\rm{neg}}\,({\it{exp\/}}, {\rm{car}}\,({\it{list\/}}))\index{neg} $\vee$ {\rm{neg-list}}\,({\it{exp\/}}, {\rm{cdr}}\,({\it{list\/}}))\index{neg-list}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  lessp-list-count \\ \index{lessp-list-count}
{\rm{listp}}\,({\it{flist\/}}) $\rightarrow$ ({\rm{list-count}}\,({\rm{cdr}}\,({\it{flist\/}}))\index{list-count} $<$ {\rm{list-count}}\,({\it{flist\/}})\index{list-count})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  or-type-list-count \\ \index{or-type-list-count}
\=\+({\rm{or-type}}\,({\rm{car}}\,({\it{flist\/}}))\index{or-type} $\wedge$ {\rm{listp}}\,({\it{flist\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{list-count}}\,({\rm{cons}}\,({\rm{cadar}}\,({\it{flist\/}}), {\rm{cons}}\,({\rm{caddar}}\,({\it{flist\/}}), {\rm{cdr}}\,({\it{flist\/}}))))\index{list-count} \\ 
$<$$\;\;\;\;${\rm{list-count}}\,({\it{flist\/}})\index{list-count})\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  nor-type-list-count1 \\ \index{nor-type-list-count1}
\=\+({\rm{listp}}\,({\it{flist\/}}) $\wedge$ {\rm{nor-type}}\,({\rm{car}}\,({\it{flist\/}}))\index{nor-type}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{list-count}}\,({\rm{cons}}\,({\rm{list}}\,({\tt{'}}{\tt{not}}, {\rm{cadadar}}\,({\it{flist\/}})), {\rm{cdr}}\,({\it{flist\/}})))\index{list-count} \\ 
$<$$\;\;\;\;${\rm{list-count}}\,({\it{flist\/}})\index{list-count})\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  nor-type-list-count2 \\ \index{nor-type-list-count2}
\=\+({\rm{listp}}\,({\it{flist\/}}) $\wedge$ {\rm{nor-type}}\,({\rm{car}}\,({\it{flist\/}}))\index{nor-type}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{list-count}}\,({\rm{cons}}\,({\rm{list}}\,({\tt{'}}{\tt{not}}, {\rm{caddadar}}\,({\it{flist\/}})), {\rm{cdr}}\,({\it{flist\/}})))\index{list-count} \\ 
$<$$\;\;\;\;${\rm{list-count}}\,({\it{flist\/}})\index{list-count})\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  dble-neg-list-count \\ \index{dble-neg-list-count}
\=\+({\rm{listp}}\,({\it{flist\/}}) $\wedge$ {\rm{dble-neg-type}}\,({\rm{car}}\,({\it{flist\/}}))\index{dble-neg-type}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{list-count}}\,({\rm{cons}}\,({\rm{cadadar}}\,({\it{flist\/}}), {\rm{cdr}}\,({\it{flist\/}})))\index{list-count} $<$ {\rm{list-count}}\,({\it{flist\/}})\index{list-count})\-
\end{tabbing}

\noindent{\sc Event}:   Enable prop-atomp; name this event `g0230'.\index{g0230}

\addvspace{18pt}

\noindent{\sc Event}:   Enable or-type; name this event `g0237'.\index{g0237}

\addvspace{18pt}

\noindent{\sc Event}:   Enable nor-type; name this event `g0238'.\index{g0238}

\addvspace{18pt}

\noindent{\sc Event}:   Enable dble-neg-type; name this event `g0239'.\index{g0239}

\addvspace{18pt}

\noindent{\sc Event}:   Enable list-count; name this event `g0240'.\index{g0240}

\addvspace{18pt}
\begin{verbatim};The tautology-checker.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{tautologyp1} \\  
\=\+{\rm{tautologyp1}}\,({\it{flist\/}}, {\it{auxlist\/}})\index{tautologyp1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{flist\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{f}} \\ 
{\bf elseif }{\rm{prop-atomp}}\,({\rm{car}}\,({\it{flist\/}}))\index{prop-atomp} \\ 
{\bf then }\=\+{\rm{neg-list}}\,({\rm{car}}\,({\it{flist\/}}), {\it{auxlist\/}})\index{neg-list} \\ 
$\vee$$\;\;\;\;${\rm{tautologyp1}}\,({\rm{cdr}}\,({\it{flist\/}}), {\rm{cons}}\,({\rm{car}}\,({\it{flist\/}}), {\it{auxlist\/}}))\index{tautologyp1}\- \\ 
{\bf elseif }{\rm{or-type}}\,({\rm{car}}\,({\it{flist\/}}))\index{or-type} \\ 
{\bf then }{\rm{tautologyp1}}\,(\=\+{\rm{cons}}\,(\=\+{\rm{arg1}}\,({\rm{car}}\,({\it{flist\/}}))\index{arg1}, \\ 
{\rm{cons}}\,({\rm{arg2}}\,({\rm{car}}\,({\it{flist\/}}))\index{arg2}, {\rm{cdr}}\,({\it{flist\/}})))\-, \\ 
{\it{auxlist\/}})\-\index{tautologyp1} \\ 
{\bf elseif }{\rm{nor-type}}\,({\rm{car}}\,({\it{flist\/}}))\index{nor-type} \\ 
{\bf then }\=\+{\rm{tautologyp1}}\,(\=\+{\rm{cons}}\,({\rm{f-not}}\,({\rm{arg1}}\,({\rm{arg1}}\,({\rm{car}}\,({\it{flist\/}}))\index{arg1})\index{arg1})\index{f-not}, {\rm{cdr}}\,({\it{flist\/}})), \\ 
{\it{auxlist\/}})\-\index{tautologyp1} \\ 
$\wedge$$\;\;\;\;${\rm{tautologyp1}}\,(\=\+{\rm{cons}}\,({\rm{f-not}}\,({\rm{arg2}}\,({\rm{arg1}}\,({\rm{car}}\,({\it{flist\/}}))\index{arg1})\index{arg2})\index{f-not}, {\rm{cdr}}\,({\it{flist\/}})), \\ 
{\it{auxlist\/}})\-\index{tautologyp1}\- \\ 
{\bf elseif }{\rm{dble-neg-type}}\,({\rm{car}}\,({\it{flist\/}}))\index{dble-neg-type} \\ 
{\bf then }{\rm{tautologyp1}}\,({\rm{cons}}\,({\rm{arg1}}\,({\rm{arg1}}\,({\rm{car}}\,({\it{flist\/}}))\index{arg1})\index{arg1}, {\rm{cdr}}\,({\it{flist\/}})), {\it{auxlist\/}})\index{tautologyp1} \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  form-list-append \\ \index{form-list-append}
({\rm{form-list}}\,({\it{x\/}})\index{form-list} $\wedge$ {\rm{form-list}}\,({\it{y\/}})\index{form-list}) $\rightarrow$ {\rm{form-list}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}))\index{form-list}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{neg-proof} \\  
\=\+{\rm{neg-proof}}\,({\it{exp1\/}}, {\it{exp2\/}})\index{neg-proof} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{exp1\/}} $=$ {\rm{f-not}}\,({\it{exp2\/}})\index{f-not}$\;\;${\bf then }{\rm{prop-axiom-proof}}\,({\it{exp2\/}})\index{prop-axiom-proof} \\ 
{\bf else }{\rm{commut-proof}}\,({\it{exp2\/}}, {\it{exp1\/}}, {\rm{prop-axiom-proof}}\,({\it{exp1\/}})\index{prop-axiom-proof})\index{commut-proof}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  neg-proof-proves \\ \index{neg-proof-proves}
\=\+(\=\+{\rm{formula}}\,({\it{exp1\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\it{exp2\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{neg}}\,({\it{exp1\/}}, {\it{exp2\/}})\index{neg} \\ 
$\wedge$$\;\;\;\;$({\it{concl\/}} $=$ {\rm{f-or}}\,({\it{exp1\/}}, {\it{exp2\/}})\index{f-or}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{neg-proof}}\,({\it{exp1\/}}, {\it{exp2\/}})\index{neg-proof}, {\it{concl\/}})\index{proves}\-
\end{tabbing}

\noindent{\sc Event}:   Enable neg-proof; name this event `g0245'.\index{g0245}

\addvspace{18pt}
\begin{tabbing}{\sc Theorem}:  neg-list-reduc \\ \index{neg-list-reduc}
\=\+{\rm{neg-list}}\,({\it{exp\/}}, {\it{flist\/}})\index{neg-list} \\ 
$=$$\;\;\;\;$(\=\+({\rm{f-not}}\,({\it{exp\/}})\index{f-not} $\in$ {\it{flist\/}}) \\ 
$\vee$$\;\;\;\;$(({\it{exp\/}} $=$ {\rm{f-not}}\,({\rm{cadr}}\,({\it{exp\/}}))\index{f-not}) $\wedge$ ({\rm{cadr}}\,({\it{exp\/}}) $\in$ {\it{flist\/}})))\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{neg-list-proof} \\  
\=\+{\rm{neg-list-proof}}\,({\it{exp\/}}, {\it{flist\/}})\index{neg-list-proof} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{f-not}}\,({\it{exp\/}})\index{f-not} $\in$ {\it{flist\/}} \\ 
{\bf then }{\rm{m2-proof}}\,(\=\+{\it{exp\/}}, \\ 
{\rm{f-not}}\,({\it{exp\/}})\index{f-not}, \\ 
{\rm{cons}}\,({\it{exp\/}}, {\it{flist\/}}), \\ 
{\rm{neg-proof}}\,({\it{exp\/}}, {\rm{f-not}}\,({\it{exp\/}})\index{f-not})\index{neg-proof})\-\index{m2-proof} \\ 
{\bf else }{\rm{m2-proof}}\,(\=\+{\it{exp\/}}, \\ 
{\rm{cadr}}\,({\it{exp\/}}), \\ 
{\rm{cons}}\,({\it{exp\/}}, {\it{flist\/}}), \\ 
{\rm{neg-proof}}\,({\it{exp\/}}, {\rm{cadr}}\,({\it{exp\/}}))\index{neg-proof})\-\index{m2-proof}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  neg-list-proof-proves \\ \index{neg-list-proof-proves}
\=\+(\=\+{\rm{formula}}\,({\it{exp\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{form-list}}\,({\it{flist\/}})\index{form-list} \\ 
$\wedge$$\;\;\;\;${\rm{neg-list}}\,({\it{exp\/}}, {\it{flist\/}})\index{neg-list} \\ 
$\wedge$$\;\;\;\;$({\it{concl\/}} $=$ {\rm{make-disjunct}}\,({\rm{cons}}\,({\it{exp\/}}, {\it{flist\/}}))\index{make-disjunct}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{neg-list-proof}}\,({\it{exp\/}}, {\it{flist\/}})\index{neg-list-proof}, {\it{concl\/}})\index{proves}\-
\end{tabbing}

\noindent{\sc Event}:   Enable neg-list-proof; name this event `g0256'.\index{g0256}

\addvspace{18pt}
\begin{tabbing}{\sc Theorem}:  subset-ident \\ \index{subset-ident}
{\rm{subset}}\,({\it{x\/}}, {\it{x\/}})\index{subset}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  subset-car \\ \index{subset-car}
{\rm{subset}}\,({\it{x\/}}, {\rm{cons}}\,({\it{y\/}}, {\it{x\/}}))\index{subset}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  subset-append \\ \index{subset-append}
{\rm{subset}}\,({\rm{cons}}\,({\it{exp\/}}, {\it{list2\/}}), {\rm{append}}\,({\rm{cons}}\,({\it{exp\/}}, {\it{list1\/}}), {\it{list2\/}}))\index{subset}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  nlistp-neg-list \\ \index{nlistp-neg-list}
({\it{list\/}} $\simeq\;${{\bf{nil}}}${}$) $\rightarrow$ ($\neg$ {\rm{neg-list}}\,({\it{exp\/}}, {\it{list\/}})\index{neg-list})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{prop-atom-proof1} \\  
\=\+{\rm{prop-atom-proof1}}\,({\it{flist1\/}}, {\it{flist2\/}})\index{prop-atom-proof1} \\ 
$=$$\;\;\;\;${\rm{m-proof}}\,(\=\+{\rm{cons}}\,({\rm{car}}\,({\it{flist1\/}}), {\it{flist2\/}}), \\ 
{\rm{append}}\,({\it{flist1\/}}, {\it{flist2\/}}), \\ 
{\rm{neg-list-proof}}\,({\rm{car}}\,({\it{flist1\/}}), {\it{flist2\/}})\index{neg-list-proof})\-\index{m-proof}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  prop-atom-proof1-proves \\ \index{prop-atom-proof1-proves}
\=\+(\=\+{\rm{form-list}}\,({\it{flist1\/}})\index{form-list} \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{flist1\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{form-list}}\,({\it{flist2\/}})\index{form-list} \\ 
$\wedge$$\;\;\;\;${\rm{neg-list}}\,({\rm{car}}\,({\it{flist1\/}}), {\it{flist2\/}})\index{neg-list} \\ 
$\wedge$$\;\;\;\;$({\it{concl\/}} $=$ {\rm{make-disjunct}}\,({\rm{append}}\,({\it{flist1\/}}, {\it{flist2\/}}))\index{make-disjunct}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{prop-atom-proof1}}\,({\it{flist1\/}}, {\it{flist2\/}})\index{prop-atom-proof1}, {\it{concl\/}})\index{proves}\-
\end{tabbing}

\noindent{\sc Event}:   Enable prop-atom-proof1; name this event `g0259'.\index{g0259}

\addvspace{18pt}
\begin{tabbing}{\sc Theorem}:  subset-append-car \\ \index{subset-append-car}
{\rm{subset}}\,({\rm{append}}\,({\it{list1\/}}, {\rm{cons}}\,({\it{exp\/}}, {\it{list2\/}})), {\rm{append}}\,({\rm{cons}}\,({\it{exp\/}}, {\it{list1\/}}), {\it{list2\/}}))\index{subset}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  form-list-append-car \\ \index{form-list-append-car}
\=\+({\rm{form-list}}\,({\rm{cons}}\,({\it{exp\/}}, {\it{list1\/}}))\index{form-list} $\wedge$ {\rm{form-list}}\,({\it{list2\/}})\index{form-list}) \\ 
$\rightarrow$$\;\;\;\;${\rm{form-list}}\,({\rm{append}}\,({\it{list1\/}}, {\rm{cons}}\,({\it{exp\/}}, {\it{list2\/}})))\index{form-list}\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{prop-atom-proof2} \\  
\=\+{\rm{prop-atom-proof2}}\,({\it{flist1\/}}, {\it{flist2\/}}, {\it{pf\/}})\index{prop-atom-proof2} \\ 
$=$$\;\;\;\;${\rm{m-proof}}\,(\=\+{\rm{append}}\,({\rm{cdr}}\,({\it{flist1\/}}), {\rm{cons}}\,({\rm{car}}\,({\it{flist1\/}}), {\it{flist2\/}})), \\ 
{\rm{append}}\,({\it{flist1\/}}, {\it{flist2\/}}), \\ 
{\it{pf\/}})\-\index{m-proof}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  prop-atom-proof2-proves \\ \index{prop-atom-proof2-proves}
\=\+(\=\+{\rm{form-list}}\,({\it{flist1\/}})\index{form-list} \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{flist1\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{form-list}}\,({\it{flist2\/}})\index{form-list} \\ 
$\wedge$$\;\;\;\;${\rm{proves}}\,(\=\+{\it{pf\/}}, \\ 
{\rm{make-disjunct}}\,({\rm{append}}\,({\rm{cdr}}\,({\it{flist1\/}}), {\rm{cons}}\,({\rm{car}}\,({\it{flist1\/}}), {\it{flist2\/}})))\index{make-disjunct})\-\index{proves} \\ 
$\wedge$$\;\;\;\;$({\it{concl\/}} $=$ {\rm{make-disjunct}}\,({\rm{append}}\,({\it{flist1\/}}, {\it{flist2\/}}))\index{make-disjunct}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{prop-atom-proof2}}\,({\it{flist1\/}}, {\it{flist2\/}}, {\it{pf\/}})\index{prop-atom-proof2}, {\it{concl\/}})\index{proves}\-
\end{tabbing}

\noindent{\sc Event}:   Enable prop-atom-proof2; name this event `g0258'.\index{g0258}

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{cancel-proof} \\  
\=\+{\rm{cancel-proof}}\,({\it{a\/}}, {\it{b\/}}, {\it{pf1\/}}, {\it{pf2\/}})\index{cancel-proof} \\ 
$=$$\;\;\;\;${\rm{contrac-proof}}\,({\it{b\/}}, {\rm{cut-proof}}\,({\it{a\/}}, {\it{b\/}}, {\it{b\/}}, {\it{pf2\/}}, {\rm{rt-expan-proof}}\,({\rm{f-not}}\,({\it{a\/}})\index{f-not}, {\it{b\/}}, {\it{pf1\/}})\index{rt-expan-proof})\index{cut-proof})\index{contrac-proof}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  cancel-proof-proves \\ \index{cancel-proof-proves}
\=\+(\=\+{\rm{proves}}\,({\it{pf1\/}}, {\rm{f-not}}\,({\it{a\/}})\index{f-not})\index{proves} \\ 
$\wedge$$\;\;\;\;${\rm{proves}}\,({\it{pf2\/}}, {\rm{f-or}}\,({\it{a\/}}, {\it{b\/}})\index{f-or})\index{proves} \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\it{a\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\it{b\/}}, {\bf{t}}, {\tt{0}})\index{formula})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{cancel-proof}}\,({\it{a\/}}, {\it{b\/}}, {\it{pf1\/}}, {\it{pf2\/}})\index{cancel-proof}, {\it{b\/}})\index{proves}\-
\end{tabbing}

\noindent{\sc Event}:   Enable cancel-proof; name this event `g0255'.\index{g0255}

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{nlistp-nor-type-proof} \\  
\=\+{\rm{nlistp-nor-type-proof}}\,({\it{a\/}}, {\it{b\/}}, {\it{pf1\/}}, {\it{pf2\/}})\index{nlistp-nor-type-proof} \\ 
$=$$\;\;\;\;${\rm{cancel-proof}}\,(\=\+{\it{b\/}}, \\ 
{\rm{f-not}}\,({\rm{f-or}}\,({\it{a\/}}, {\it{b\/}})\index{f-or})\index{f-not}, \\ 
{\it{pf2\/}}, \\ 
{\rm{cancel-proof}}\,(\=\+{\it{a\/}}, \\ 
{\rm{f-or}}\,({\it{b\/}}, {\rm{f-not}}\,({\rm{f-or}}\,({\it{a\/}}, {\it{b\/}})\index{f-or})\index{f-not})\index{f-or}, \\ 
{\it{pf1\/}}, \\ 
{\rm{m-proof}}\,(\=\+{\rm{list}}\,({\rm{f-not}}\,({\rm{f-or}}\,({\it{a\/}}, {\it{b\/}})\index{f-or})\index{f-not}, {\it{a\/}}, {\it{b\/}}), \\ 
{\rm{list}}\,({\it{a\/}}, {\it{b\/}}, {\rm{f-not}}\,({\rm{f-or}}\,({\it{a\/}}, {\it{b\/}})\index{f-or})\index{f-not}), \\ 
{\rm{prop-axiom-proof}}\,({\rm{f-or}}\,({\it{a\/}}, {\it{b\/}})\index{f-or})\index{prop-axiom-proof})\-\index{m-proof})\-\index{cancel-proof})\-\index{cancel-proof}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  nlistp-nor-type-proof-proves \\ \index{nlistp-nor-type-proof-proves}
\=\+(\=\+{\rm{formula}}\,({\it{a\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\it{b\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{proves}}\,({\it{pf1\/}}, {\rm{f-not}}\,({\it{a\/}})\index{f-not})\index{proves} \\ 
$\wedge$$\;\;\;\;${\rm{proves}}\,({\it{pf2\/}}, {\rm{f-not}}\,({\it{b\/}})\index{f-not})\index{proves} \\ 
$\wedge$$\;\;\;\;$({\it{concl\/}} $=$ {\rm{f-not}}\,({\rm{f-or}}\,({\it{a\/}}, {\it{b\/}})\index{f-or})\index{f-not}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{nlistp-nor-type-proof}}\,({\it{a\/}}, {\it{b\/}}, {\it{pf1\/}}, {\it{pf2\/}})\index{nlistp-nor-type-proof}, {\it{concl\/}})\index{proves}\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{listp-nor-type-proof} \\  
\=\+{\rm{listp-nor-type-proof}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}}, {\it{pf1\/}}, {\it{pf2\/}})\index{listp-nor-type-proof} \\ 
$=$$\;\;\;\;${\rm{m-proof}}\,(\=\+{\rm{list}}\,({\rm{f-not}}\,({\rm{f-or}}\,({\it{a\/}}, {\it{b\/}})\index{f-or})\index{f-not}, {\it{c\/}}, {\it{c\/}}), \\ 
{\rm{list}}\,({\rm{f-not}}\,({\rm{f-or}}\,({\it{a\/}}, {\it{b\/}})\index{f-or})\index{f-not}, {\it{c\/}}), \\ 
{\rm{rt-assoc-proof}}\,(\=\+{\rm{f-not}}\,({\rm{f-or}}\,({\it{a\/}}, {\it{b\/}})\index{f-or})\index{f-not}, \\ 
{\it{c\/}}, \\ 
{\it{c\/}}, \\ 
{\rm{cut-proof}}\,(\=\+{\it{b\/}}, \\ 
{\rm{f-or}}\,({\rm{f-not}}\,({\rm{f-or}}\,({\it{a\/}}, {\it{b\/}})\index{f-or})\index{f-not}, {\it{c\/}})\index{f-or}, \\ 
{\it{c\/}}, \\ 
{\rm{rt-assoc-proof}}\,(\=\+{\it{b\/}}, \\ 
{\rm{f-not}}\,({\rm{f-or}}\,({\it{a\/}}, {\it{b\/}})\index{f-or})\index{f-not}, \\ 
{\it{c\/}}, \\ 
{\rm{cut-proof}}\,(\=\+{\it{a\/}}, \\ 
{\rm{f-or}}\,(\=\+{\it{b\/}}, \\ 
{\rm{f-not}}\,({\rm{f-or}}\,(\=\+{\it{a\/}}, \\ 
{\it{b\/}})\-\index{f-or})\index{f-not})\-\index{f-or}, \\ 
{\it{c\/}}, \\ 
{\rm{m-proof}}\,(\=\+{\rm{list}}\,(\=\+{\rm{f-not}}\,({\rm{f-or}}\,(\=\+{\it{a\/}}, \\ 
{\it{b\/}})\-\index{f-or})\index{f-not}, \\ 
{\it{a\/}}, \\ 
{\it{b\/}})\-, \\ 
{\rm{list}}\,(\=\+{\it{a\/}}, \\ 
{\it{b\/}}, \\ 
{\rm{f-not}}\,({\rm{f-or}}\,(\=\+{\it{a\/}}, \\ 
{\it{b\/}})\-\index{f-or})\index{f-not})\-, \\ 
{\rm{prop-axiom-proof}}\,({\rm{f-or}}\,(\=\+{\it{a\/}}, \\ 
{\it{b\/}})\-\index{f-or})\index{prop-axiom-proof})\-\index{m-proof}, \\ 
{\it{pf1\/}})\-\index{cut-proof})\-\index{rt-assoc-proof}, \\ 
{\it{pf2\/}})\-\index{cut-proof})\-\index{rt-assoc-proof})\-\index{m-proof}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  listp-nor-type-proof-proves \\ \index{listp-nor-type-proof-proves}
\=\+(\=\+{\rm{formula}}\,({\it{a\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\it{b\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\it{c\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{proves}}\,({\it{pf1\/}}, {\rm{f-or}}\,({\rm{f-not}}\,({\it{a\/}})\index{f-not}, {\it{c\/}})\index{f-or})\index{proves} \\ 
$\wedge$$\;\;\;\;${\rm{proves}}\,({\it{pf2\/}}, {\rm{f-or}}\,({\rm{f-not}}\,({\it{b\/}})\index{f-not}, {\it{c\/}})\index{f-or})\index{proves} \\ 
$\wedge$$\;\;\;\;$({\it{concl\/}} $=$ {\rm{f-or}}\,({\rm{f-not}}\,({\rm{f-or}}\,({\it{a\/}}, {\it{b\/}})\index{f-or})\index{f-not}, {\it{c\/}})\index{f-or}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{listp-nor-type-proof}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}}, {\it{pf1\/}}, {\it{pf2\/}})\index{listp-nor-type-proof}, {\it{concl\/}})\index{proves}\-
\end{tabbing}

\noindent{\sc Event}:   Enable m-proof-proves; name this event `g0242'.\index{g0242}

\addvspace{18pt}

\noindent{\sc Event}:   Enable nlistp-nor-type-proof; name this event `g0243'.\index{g0243}

\addvspace{18pt}

\noindent{\sc Event}:   Enable listp-nor-type-proof; name this event `g0244'.\index{g0244}

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{nor-type-proof} \\  
\=\+{\rm{nor-type-proof}}\,({\it{a\/}}, {\it{b\/}}, {\it{clist\/}}, {\it{pf1\/}}, {\it{pf2\/}})\index{nor-type-proof} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{clist\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\rm{nlistp-nor-type-proof}}\,({\it{a\/}}, {\it{b\/}}, {\it{pf1\/}}, {\it{pf2\/}})\index{nlistp-nor-type-proof} \\ 
{\bf else }{\rm{listp-nor-type-proof}}\,({\it{a\/}}, {\it{b\/}}, {\rm{make-disjunct}}\,({\it{clist\/}})\index{make-disjunct}, {\it{pf1\/}}, {\it{pf2\/}})\index{listp-nor-type-proof}$\;${\bf  endif}\-\-
\end{tabbing}

\noindent{\sc Event}:   Disable nor-type; name this event `g0292'.\index{g0292}

\addvspace{18pt}
\begin{tabbing}{\sc Theorem}:  nor-type-proof-proves \\ \index{nor-type-proof-proves}
\=\+(\=\+{\rm{nor-type}}\,({\it{exp\/}})\index{nor-type} \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\it{exp\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{form-list}}\,({\it{clist\/}})\index{form-list} \\ 
$\wedge$$\;\;\;\;${\rm{proves}}\,({\it{pf1\/}}, {\rm{make-disjunct}}\,({\rm{cons}}\,({\rm{f-not}}\,({\rm{cadadr}}\,({\it{exp\/}}))\index{f-not}, {\it{clist\/}}))\index{make-disjunct})\index{proves} \\ 
$\wedge$$\;\;\;\;${\rm{proves}}\,({\it{pf2\/}}, {\rm{make-disjunct}}\,({\rm{cons}}\,({\rm{f-not}}\,({\rm{caddadr}}\,({\it{exp\/}}))\index{f-not}, {\it{clist\/}}))\index{make-disjunct})\index{proves} \\ 
$\wedge$$\;\;\;\;$({\it{concl\/}} $=$ {\rm{make-disjunct}}\,({\rm{cons}}\,({\it{exp\/}}, {\it{clist\/}}))\index{make-disjunct}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{nor-type-proof}}\,({\rm{cadadr}}\,({\it{exp\/}}), {\rm{caddadr}}\,({\it{exp\/}}), {\it{clist\/}}, {\it{pf1\/}}, {\it{pf2\/}})\index{nor-type-proof}, {\it{concl\/}})\index{proves}\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{nlistp-dble-neg-proof} \\  
\=\+{\rm{nlistp-dble-neg-proof}}\,({\it{a\/}}, {\it{pf\/}})\index{nlistp-dble-neg-proof} \\ 
$=$$\;\;\;\;${\rm{contrac-proof}}\,(\=\+{\rm{f-not}}\,({\rm{f-not}}\,({\it{a\/}})\index{f-not})\index{f-not}, \\ 
{\rm{cut-proof}}\,(\=\+{\it{a\/}}, \\ 
{\rm{f-not}}\,({\rm{f-not}}\,({\it{a\/}})\index{f-not})\index{f-not}, \\ 
{\rm{f-not}}\,({\rm{f-not}}\,({\it{a\/}})\index{f-not})\index{f-not}, \\ 
{\rm{rt-expan-proof}}\,({\it{a\/}}, {\rm{f-not}}\,({\rm{f-not}}\,({\it{a\/}})\index{f-not})\index{f-not}, {\it{pf\/}})\index{rt-expan-proof}, \\ 
{\rm{commut-proof}}\,(\=\+{\rm{f-not}}\,({\rm{f-not}}\,({\it{a\/}})\index{f-not})\index{f-not}, \\ 
{\rm{f-not}}\,({\it{a\/}})\index{f-not}, \\ 
{\rm{prop-axiom-proof}}\,({\rm{f-not}}\,({\it{a\/}})\index{f-not})\index{prop-axiom-proof})\-\index{commut-proof})\-\index{cut-proof})\-\index{contrac-proof}\-
\end{tabbing}

\noindent{\sc Event}:   Enable nor-type-proof; name this event `g0248'.\index{g0248}

\addvspace{18pt}
\begin{tabbing}{\sc Theorem}:  nlistp-dble-neg-proof-proves \\ \index{nlistp-dble-neg-proof-proves}
\=\+({\rm{formula}}\,({\it{a\/}}, {\bf{t}}, {\tt{0}})\index{formula} $\wedge$ {\rm{proves}}\,({\it{pf\/}}, {\it{a\/}})\index{proves} $\wedge$ ({\it{concl\/}} $=$ {\rm{f-not}}\,({\rm{f-not}}\,({\it{a\/}})\index{f-not})\index{f-not})) \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{nlistp-dble-neg-proof}}\,({\it{a\/}}, {\it{pf\/}})\index{nlistp-dble-neg-proof}, {\it{concl\/}})\index{proves}\-
\end{tabbing}

\noindent{\sc Event}:   Enable nlistp-dble-neg-proof; name this event `g0249'.\index{g0249}

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{listp-dble-neg-proof} \\  
\=\+{\rm{listp-dble-neg-proof}}\,({\it{a\/}}, {\it{c\/}}, {\it{pf\/}})\index{listp-dble-neg-proof} \\ 
$=$$\;\;\;\;${\rm{commut-proof}}\,(\=\+{\it{c\/}}, \\ 
{\rm{f-not}}\,({\rm{f-not}}\,({\it{a\/}})\index{f-not})\index{f-not}, \\ 
{\rm{cut-proof}}\,(\=\+{\it{a\/}}, \\ 
{\it{c\/}}, \\ 
{\rm{f-not}}\,({\rm{f-not}}\,({\it{a\/}})\index{f-not})\index{f-not}, \\ 
{\it{pf\/}}, \\ 
{\rm{commut-proof}}\,(\=\+{\rm{f-not}}\,({\rm{f-not}}\,({\it{a\/}})\index{f-not})\index{f-not}, \\ 
{\rm{f-not}}\,({\it{a\/}})\index{f-not}, \\ 
{\rm{prop-axiom-proof}}\,({\rm{f-not}}\,({\it{a\/}})\index{f-not})\index{prop-axiom-proof})\-\index{commut-proof})\-\index{cut-proof})\-\index{commut-proof}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  listp-dble-neg-proof-proves \\ \index{listp-dble-neg-proof-proves}
\=\+(\=\+{\rm{formula}}\,({\it{a\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\it{c\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{proves}}\,({\it{pf\/}}, {\rm{f-or}}\,({\it{a\/}}, {\it{c\/}})\index{f-or})\index{proves} \\ 
$\wedge$$\;\;\;\;$({\it{concl\/}} $=$ {\rm{f-or}}\,({\rm{f-not}}\,({\rm{f-not}}\,({\it{a\/}})\index{f-not})\index{f-not}, {\it{c\/}})\index{f-or}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{listp-dble-neg-proof}}\,({\it{a\/}}, {\it{c\/}}, {\it{pf\/}})\index{listp-dble-neg-proof}, {\it{concl\/}})\index{proves}\-
\end{tabbing}

\noindent{\sc Event}:   Enable listp-dble-neg-proof; name this event `g0203'.\index{g0203}

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{dble-neg-type-proof} \\  
\=\+{\rm{dble-neg-type-proof}}\,({\it{a\/}}, {\it{clist\/}}, {\it{pf\/}})\index{dble-neg-type-proof} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{clist\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\rm{nlistp-dble-neg-proof}}\,({\it{a\/}}, {\it{pf\/}})\index{nlistp-dble-neg-proof} \\ 
{\bf else }{\rm{listp-dble-neg-proof}}\,({\it{a\/}}, {\rm{make-disjunct}}\,({\it{clist\/}})\index{make-disjunct}, {\it{pf\/}})\index{listp-dble-neg-proof}$\;${\bf  endif}\-\-
\end{tabbing}

\noindent{\sc Event}:   Disable dble-neg-type; name this event `g0252'.\index{g0252}

\addvspace{18pt}
\begin{tabbing}{\sc Theorem}:  dble-neg-type-proof-proves \\ \index{dble-neg-type-proof-proves}
\=\+(\=\+{\rm{dble-neg-type}}\,({\it{exp\/}})\index{dble-neg-type} \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\it{exp\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{form-list}}\,({\it{clist\/}})\index{form-list} \\ 
$\wedge$$\;\;\;\;${\rm{proves}}\,({\it{pf\/}}, {\rm{make-disjunct}}\,({\rm{cons}}\,({\rm{cadadr}}\,({\it{exp\/}}), {\it{clist\/}}))\index{make-disjunct})\index{proves} \\ 
$\wedge$$\;\;\;\;$({\it{concl\/}} $=$ {\rm{make-disjunct}}\,({\rm{cons}}\,({\it{exp\/}}, {\it{clist\/}}))\index{make-disjunct}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{dble-neg-type-proof}}\,({\rm{cadadr}}\,({\it{exp\/}}), {\it{clist\/}}, {\it{pf\/}})\index{dble-neg-type-proof}, {\it{concl\/}})\index{proves}\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{or-type-proof} \\  
\=\+{\rm{or-type-proof}}\,({\it{a\/}}, {\it{b\/}}, {\it{clist\/}}, {\it{pf\/}})\index{or-type-proof} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{clist\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\it{pf\/}} \\ 
{\bf else }{\rm{assoc-proof}}\,({\it{a\/}}, {\it{b\/}}, {\rm{make-disjunct}}\,({\it{clist\/}})\index{make-disjunct}, {\it{pf\/}})\index{assoc-proof}$\;${\bf  endif}\-\-
\end{tabbing}

\noindent{\sc Event}:   Disable or-type; name this event `g0260'.\index{g0260}

\addvspace{18pt}
\begin{tabbing}{\sc Theorem}:  or-type-proof-proves \\ \index{or-type-proof-proves}
\=\+(\=\+{\rm{or-type}}\,({\rm{car}}\,({\it{flist1\/}}))\index{or-type} \\ 
$\wedge$$\;\;\;\;${\rm{form-list}}\,({\it{flist1\/}})\index{form-list} \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{flist1\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{form-list}}\,({\it{flist2\/}})\index{form-list} \\ 
$\wedge$$\;\;\;\;${\rm{proves}}\,(\=\+{\it{pf\/}}, \\ 
{\rm{make-disjunct}}\,({\rm{append}}\,(\=\+{\rm{cons}}\,(\=\+{\rm{cadar}}\,({\it{flist1\/}}), \\ 
{\rm{cons}}\,({\rm{caddar}}\,({\it{flist1\/}}), {\rm{cdr}}\,({\it{flist1\/}})))\-, \\ 
{\it{flist2\/}})\-)\index{make-disjunct})\-\index{proves} \\ 
$\wedge$$\;\;\;\;$({\it{concl\/}} $=$ {\rm{make-disjunct}}\,({\rm{append}}\,({\it{flist1\/}}, {\it{flist2\/}}))\index{make-disjunct}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,(\=\+{\rm{or-type-proof}}\,(\=\+{\rm{cadar}}\,({\it{flist1\/}}), \\ 
{\rm{caddar}}\,({\it{flist1\/}}), \\ 
{\rm{append}}\,({\rm{cdr}}\,({\it{flist1\/}}), {\it{flist2\/}}), \\ 
{\it{pf\/}})\-\index{or-type-proof}, \\ 
{\it{concl\/}})\-\index{proves}\-
\end{tabbing}

\noindent{\sc Event}:   Enable or-type-proof; name this event `g0271'.\index{g0271}

\addvspace{18pt}
\begin{tabbing}{\sc Theorem}:  or-type-form-list \\ \index{or-type-form-list}
\=\+({\rm{or-type}}\,({\rm{car}}\,({\it{flist\/}}))\index{or-type} $\wedge$ {\rm{form-list}}\,({\it{flist\/}})\index{form-list} $\wedge$ {\rm{listp}}\,({\it{flist\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{form-list}}\,({\rm{cons}}\,({\rm{cadar}}\,({\it{flist\/}}), {\rm{cons}}\,({\rm{caddar}}\,({\it{flist\/}}), {\rm{cdr}}\,({\it{flist\/}}))))\index{form-list}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  nor-type-form-list \\ \index{nor-type-form-list}
\=\+({\rm{nor-type}}\,({\rm{car}}\,({\it{flist\/}}))\index{nor-type} $\wedge$ {\rm{form-list}}\,({\it{flist\/}})\index{form-list} $\wedge$ {\rm{listp}}\,({\it{flist\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{form-list}}\,({\rm{cons}}\,({\rm{list}}\,({\tt{'}}{\tt{not}}, {\rm{cadadar}}\,({\it{flist\/}})), {\rm{cdr}}\,({\it{flist\/}})))\index{form-list}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  nor-type-form-list2 \\ \index{nor-type-form-list2}
\=\+({\rm{nor-type}}\,({\rm{car}}\,({\it{flist\/}}))\index{nor-type} $\wedge$ {\rm{form-list}}\,({\it{flist\/}})\index{form-list} $\wedge$ {\rm{listp}}\,({\it{flist\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{form-list}}\,({\rm{cons}}\,({\rm{list}}\,({\tt{'}}{\tt{not}}, {\rm{caddadar}}\,({\it{flist\/}})), {\rm{cdr}}\,({\it{flist\/}})))\index{form-list}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  dble-neg-type-form-list \\ \index{dble-neg-type-form-list}
\=\+({\rm{dble-neg-type}}\,({\rm{car}}\,({\it{flist\/}}))\index{dble-neg-type} $\wedge$ {\rm{form-list}}\,({\it{flist\/}})\index{form-list} $\wedge$ {\rm{listp}}\,({\it{flist\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{form-list}}\,({\rm{cons}}\,({\rm{cadadar}}\,({\it{flist\/}}), {\rm{cdr}}\,({\it{flist\/}})))\index{form-list}\-
\end{tabbing}

\noindent{\sc Event}:   Enable or-type; name this event `g0272'.\index{g0272}

\addvspace{18pt}

\noindent{\sc Event}:   Enable nor-type; name this event `g0273'.\index{g0273}

\addvspace{18pt}

\noindent{\sc Event}:   Enable dble-neg-type; name this event `g0274'.\index{g0274}

\addvspace{18pt}

\noindent{\sc Event}:   Enable dble-neg-type-proof; name this event `g0254'.\index{g0254}

\addvspace{18pt}
\begin{verbatim};The proof-constructor for tautologies.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{taut-proof1} \\  
\=\+{\rm{taut-proof1}}\,({\it{flist\/}}, {\it{auxlist\/}})\index{taut-proof1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{flist\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }{\rm{prop-atomp}}\,({\rm{car}}\,({\it{flist\/}}))\index{prop-atomp} \\ 
{\bf then }\=\+{\bf if }{\rm{neg-list}}\,({\rm{car}}\,({\it{flist\/}}), {\it{auxlist\/}})\index{neg-list} \\ 
{\bf then }{\rm{prop-atom-proof1}}\,({\it{flist\/}}, {\it{auxlist\/}})\index{prop-atom-proof1} \\ 
{\bf else }{\rm{prop-atom-proof2}}\,(\=\+{\it{flist\/}}, \\ 
{\it{auxlist\/}}, \\ 
{\rm{taut-proof1}}\,(\=\+{\rm{cdr}}\,({\it{flist\/}}), \\ 
{\rm{cons}}\,({\rm{car}}\,({\it{flist\/}}), {\it{auxlist\/}}))\-\index{taut-proof1})\-\index{prop-atom-proof2}$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{or-type}}\,({\rm{car}}\,({\it{flist\/}}))\index{or-type} \\ 
{\bf then }{\rm{or-type-proof}}\,(\=\+{\rm{arg1}}\,({\rm{car}}\,({\it{flist\/}}))\index{arg1}, \\ 
{\rm{arg2}}\,({\rm{car}}\,({\it{flist\/}}))\index{arg2}, \\ 
{\rm{append}}\,({\rm{cdr}}\,({\it{flist\/}}), {\it{auxlist\/}}), \\ 
{\rm{taut-proof1}}\,(\=\+{\rm{cons}}\,(\=\+{\rm{arg1}}\,({\rm{car}}\,({\it{flist\/}}))\index{arg1}, \\ 
{\rm{cons}}\,({\rm{arg2}}\,({\rm{car}}\,({\it{flist\/}}))\index{arg2}, {\rm{cdr}}\,({\it{flist\/}})))\-, \\ 
{\it{auxlist\/}})\-\index{taut-proof1})\-\index{or-type-proof} \\ 
{\bf elseif }{\rm{nor-type}}\,({\rm{car}}\,({\it{flist\/}}))\index{nor-type} \\ 
{\bf then }{\rm{nor-type-proof}}\,(\=\+{\rm{arg1}}\,({\rm{arg1}}\,({\rm{car}}\,({\it{flist\/}}))\index{arg1})\index{arg1}, \\ 
{\rm{arg2}}\,({\rm{arg1}}\,({\rm{car}}\,({\it{flist\/}}))\index{arg1})\index{arg2}, \\ 
{\rm{append}}\,({\rm{cdr}}\,({\it{flist\/}}), {\it{auxlist\/}}), \\ 
{\rm{taut-proof1}}\,(\=\+{\rm{cons}}\,(\=\+{\rm{f-not}}\,({\rm{arg1}}\,({\rm{arg1}}\,({\rm{car}}\,({\it{flist\/}}))\index{arg1})\index{arg1})\index{f-not}, \\ 
{\rm{cdr}}\,({\it{flist\/}}))\-, \\ 
{\it{auxlist\/}})\-\index{taut-proof1}, \\ 
{\rm{taut-proof1}}\,(\=\+{\rm{cons}}\,(\=\+{\rm{f-not}}\,({\rm{arg2}}\,({\rm{arg1}}\,({\rm{car}}\,({\it{flist\/}}))\index{arg1})\index{arg2})\index{f-not}, \\ 
{\rm{cdr}}\,({\it{flist\/}}))\-, \\ 
{\it{auxlist\/}})\-\index{taut-proof1})\-\index{nor-type-proof} \\ 
{\bf elseif }{\rm{dble-neg-type}}\,({\rm{car}}\,({\it{flist\/}}))\index{dble-neg-type} \\ 
{\bf then }{\rm{dble-neg-type-proof}}\,(\=\+{\rm{arg1}}\,({\rm{arg1}}\,({\rm{car}}\,({\it{flist\/}}))\index{arg1})\index{arg1}, \\ 
{\rm{append}}\,({\rm{cdr}}\,({\it{flist\/}}), {\it{auxlist\/}}), \\ 
{\rm{taut-proof1}}\,(\=\+{\rm{cons}}\,(\=\+{\rm{arg1}}\,({\rm{arg1}}\,({\rm{car}}\,({\it{flist\/}}))\index{arg1})\index{arg1}, \\ 
{\rm{cdr}}\,({\it{flist\/}}))\-, \\ 
{\it{auxlist\/}})\-\index{taut-proof1})\-\index{dble-neg-type-proof} \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim};Every tautology has a proof (when AUXLIST is NIL)
\end{verbatim}\begin{tabbing}{\sc Theorem}:  taut-thm1 \\ \index{taut-thm1}
\=\+({\rm{form-list}}\,({\it{flist\/}})\index{form-list} $\wedge$ {\rm{form-list}}\,({\it{auxlist\/}})\index{form-list} $\wedge$ {\rm{tautologyp1}}\,({\it{flist\/}}, {\it{auxlist\/}})\index{tautologyp1}) \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,(\=\+{\rm{taut-proof1}}\,({\it{flist\/}}, {\it{auxlist\/}})\index{taut-proof1}, \\ 
{\rm{make-disjunct}}\,({\rm{append}}\,({\it{flist\/}}, {\it{auxlist\/}}))\index{make-disjunct})\-\index{proves}\-
\end{tabbing}

\noindent{\sc Event}:   Enable taut-proof1; name this event `g0275'.\index{g0275}

\addvspace{18pt}
\begin{tabbing}{\sc Theorem}:  taut-thm2 \\ \index{taut-thm2}
\=\+(\=\+{\rm{form-list}}\,({\it{flist\/}})\index{form-list} \\ 
$\wedge$$\;\;\;\;${\rm{form-list}}\,({\it{auxlist\/}})\index{form-list} \\ 
$\wedge$$\;\;\;\;${\rm{tautologyp1}}\,({\it{flist\/}}, {\it{auxlist\/}})\index{tautologyp1} \\ 
$\wedge$$\;\;\;\;$({\it{concl\/}} $=$ {\rm{make-disjunct}}\,({\rm{append}}\,({\it{flist\/}}, {\it{auxlist\/}}))\index{make-disjunct}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{taut-proof1}}\,({\it{flist\/}}, {\it{auxlist\/}})\index{taut-proof1}, {\it{concl\/}})\index{proves}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  listp-elem-form \\ \index{listp-elem-form}
({\it{exp\/}} $\simeq\;${{\bf{nil}}}${}$) $\rightarrow$ ($\neg$ {\rm{elem-form}}\,({\it{exp\/}})\index{elem-form})
\end{tabbing}
\begin{verbatim};Truth value evaluator.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{eval} \\  
\=\+{\rm{eval}}\,({\it{exp\/}}, {\it{alist\/}})\index{eval} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{exp\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{f}} \\ 
{\bf elseif }{\rm{elem-form}}\,({\it{exp\/}})\index{elem-form}$\;\;${\bf then }{\it{exp\/}} $\in$ {\it{alist\/}} \\ 
{\bf elseif }{\rm{car}}\,({\it{exp\/}}) $=$ {\tt{'}}{\tt{not}}$\;\;${\bf then }$\neg$ {\rm{eval}}\,({\rm{cadr}}\,({\it{exp\/}}), {\it{alist\/}})\index{eval} \\ 
{\bf elseif }{\rm{car}}\,({\it{exp\/}}) $=$ {\tt{'}}{\tt{or}} \\ 
{\bf then }{\rm{eval}}\,({\rm{cadr}}\,({\it{exp\/}}), {\it{alist\/}})\index{eval} $\vee$ {\rm{eval}}\,({\rm{caddr}}\,({\it{exp\/}}), {\it{alist\/}})\index{eval} \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  elem-form-eval \\ \index{elem-form-eval}
{\rm{elem-form}}\,({\it{exp\/}})\index{elem-form} $\rightarrow$ ({\rm{eval}}\,({\it{exp\/}}, {\it{alist\/}})\index{eval} $=$ ({\it{exp\/}} $\in$ {\it{alist\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  nlistp-eval \\ \index{nlistp-eval}
({\it{exp\/}} $\simeq\;${{\bf{nil}}}${}$) $\rightarrow$ ($\neg$ {\rm{eval}}\,({\it{exp\/}}, {\it{alist\/}})\index{eval})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  not-eval \\ \index{not-eval}
\=\+({\rm{listp}}\,({\it{exp\/}}) $\wedge$ ({\rm{car}}\,({\it{exp\/}}) $=$ {\tt{'}}{\tt{not}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{eval}}\,({\it{exp\/}}, {\it{alist\/}})\index{eval} $=$ ($\neg$ {\rm{eval}}\,({\rm{cadr}}\,({\it{exp\/}}), {\it{alist\/}})\index{eval}))\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  or-eval \\ \index{or-eval}
\=\+({\rm{listp}}\,({\it{exp\/}}) $\wedge$ ({\rm{car}}\,({\it{exp\/}}) $=$ {\tt{'}}{\tt{or}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{eval}}\,({\it{exp\/}}, {\it{alist\/}})\index{eval} \\ 
$=$$\;\;\;\;$({\rm{eval}}\,({\rm{cadr}}\,({\it{exp\/}}), {\it{alist\/}})\index{eval} $\vee$ {\rm{eval}}\,({\rm{caddr}}\,({\it{exp\/}}), {\it{alist\/}})\index{eval}))\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  member-eval \\ \index{member-eval}
(({\it{exp\/}} $\in$ {\it{flist\/}}) $\wedge$ {\rm{eval}}\,({\it{exp\/}}, {\it{alist\/}})\index{eval}) $\rightarrow$ {\rm{eval}}\,({\rm{make-disjunct}}\,({\it{flist\/}})\index{make-disjunct}, {\it{alist\/}})\index{eval}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  eval-elem-form \\ \index{eval-elem-form}
\=\+(\=\+{\rm{elem-form}}\,({\it{exp\/}})\index{elem-form} \\ 
$\wedge$$\;\;\;\;$({\it{exp\/}} $\in$ {\it{list\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{exp\/}} $\in$ {\it{alist\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{concl\/}} $=$ {\rm{make-disjunct}}\,({\it{list\/}})\index{make-disjunct}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\it{concl\/}}, {\it{alist\/}})\index{eval}\-
\end{tabbing}

\noindent{\sc Event}:   Disable or-type; name this event `g0278'.\index{g0278}

\addvspace{18pt}

\noindent{\sc Event}:   Disable nor-type; name this event `g0279'.\index{g0279}

\addvspace{18pt}

\noindent{\sc Event}:   Disable dble-neg-type; name this event `g0280'.\index{g0280}

\addvspace{18pt}

\noindent{\sc Event}:   Disable prop-atomp; name this event `g0281'.\index{g0281}

\addvspace{18pt}
\begin{tabbing}{\sc Theorem}:  member-append \\ \index{member-append}
({\it{exp\/}} $\in$ {\rm{append}}\,({\it{flist1\/}}, {\it{flist2\/}})) $=$ (({\it{exp\/}} $\in$ {\it{flist1\/}}) $\vee$ ({\it{exp\/}} $\in$ {\it{flist2\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  eval-neg-elem-form \\ \index{eval-neg-elem-form}
\=\+(\=\+({\it{exp\/}} $\in$ {\it{list\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{f-not}}\,({\it{exp\/}})\index{f-not} $\in$ {\it{list\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{concl\/}} $=$ {\rm{make-disjunct}}\,({\it{list\/}})\index{make-disjunct}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\it{concl\/}}, {\it{alist\/}})\index{eval}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  eval-make-disjunct \\ \index{eval-make-disjunct}
\=\+{\rm{eval}}\,({\rm{make-disjunct}}\,({\rm{append}}\,({\it{list1\/}}, {\it{list2\/}}))\index{make-disjunct}, {\it{alist\/}})\index{eval} \\ 
$=$$\;\;\;\;$(\=\+{\rm{eval}}\,({\rm{make-disjunct}}\,({\it{list1\/}})\index{make-disjunct}, {\it{alist\/}})\index{eval} \\ 
$\vee$$\;\;\;\;${\rm{eval}}\,({\rm{make-disjunct}}\,({\it{list2\/}})\index{make-disjunct}, {\it{alist\/}})\index{eval})\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  neg-list-eval \\ \index{neg-list-eval}
\=\+(\=\+{\rm{listp}}\,({\it{flist1\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{neg-list}}\,({\rm{car}}\,({\it{flist1\/}}), {\it{flist2\/}})\index{neg-list} \\ 
$\wedge$$\;\;\;\;$({\it{concl\/}} $=$ {\rm{make-disjunct}}\,({\rm{append}}\,({\it{flist1\/}}, {\it{flist2\/}}))\index{make-disjunct}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\it{concl\/}}, {\it{alist\/}})\index{eval}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  eval-prop-atomp \\ \index{eval-prop-atomp}
\=\+(\=\+{\rm{listp}}\,({\it{flist1\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{eval}}\,(\=\+{\rm{make-disjunct}}\,({\rm{append}}\,({\rm{cdr}}\,({\it{flist1\/}}), {\rm{cons}}\,({\rm{car}}\,({\it{flist1\/}}), {\it{flist2\/}})))\index{make-disjunct}, \\ 
{\it{alist\/}})\-\index{eval})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\rm{make-disjunct}}\,({\rm{append}}\,({\it{flist1\/}}, {\it{flist2\/}}))\index{make-disjunct}, {\it{alist\/}})\index{eval}\-
\end{tabbing}

\noindent{\sc Event}:   Enable eval; name this event `g1253'.\index{g1253}

\addvspace{18pt}
\begin{tabbing}{\sc Theorem}:  eval-or-type \\ \index{eval-or-type}
\=\+({\rm{listp}}\,({\it{flist1\/}}) $\wedge$ {\rm{or-type}}\,({\rm{car}}\,({\it{flist1\/}}))\index{or-type}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{eval}}\,({\rm{make-disjunct}}\,({\rm{append}}\,({\it{flist1\/}}, {\it{flist2\/}}))\index{make-disjunct}, {\it{alist\/}})\index{eval} \\ 
$=$$\;\;\;\;${\rm{eval}}\,(\=\+{\rm{make-disjunct}}\,({\rm{append}}\,(\=\+{\rm{cons}}\,(\=\+{\rm{cadar}}\,({\it{flist1\/}}), \\ 
{\rm{cons}}\,(\=\+{\rm{caddar}}\,({\it{flist1\/}}), \\ 
{\rm{cdr}}\,({\it{flist1\/}}))\-)\-, \\ 
{\it{flist2\/}})\-)\index{make-disjunct}, \\ 
{\it{alist\/}})\-\index{eval})\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  eval-nor-type \\ \index{eval-nor-type}
\=\+({\rm{listp}}\,({\it{flist1\/}}) $\wedge$ {\rm{nor-type}}\,({\rm{car}}\,({\it{flist1\/}}))\index{nor-type}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{eval}}\,({\rm{make-disjunct}}\,({\rm{append}}\,({\it{flist1\/}}, {\it{flist2\/}}))\index{make-disjunct}, {\it{alist\/}})\index{eval} \\ 
$=$$\;\;\;\;$(\=\+{\rm{eval}}\,(\=\+{\rm{make-disjunct}}\,({\rm{append}}\,(\=\+{\rm{cons}}\,(\=\+{\rm{f-not}}\,({\rm{cadadar}}\,({\it{flist1\/}}))\index{f-not}, \\ 
{\rm{cdr}}\,({\it{flist1\/}}))\-, \\ 
{\it{flist2\/}})\-)\index{make-disjunct}, \\ 
{\it{alist\/}})\-\index{eval} \\ 
$\wedge$$\;\;\;\;${\rm{eval}}\,(\=\+{\rm{make-disjunct}}\,({\rm{append}}\,(\=\+{\rm{cons}}\,(\=\+{\rm{f-not}}\,({\rm{caddadar}}\,({\it{flist1\/}}))\index{f-not}, \\ 
{\rm{cdr}}\,({\it{flist1\/}}))\-, \\ 
{\it{flist2\/}})\-)\index{make-disjunct}, \\ 
{\it{alist\/}})\-\index{eval})\-)\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  eval-dble-neg-type \\ \index{eval-dble-neg-type}
\=\+({\rm{listp}}\,({\it{flist1\/}}) $\wedge$ {\rm{dble-neg-type}}\,({\rm{car}}\,({\it{flist1\/}}))\index{dble-neg-type}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{eval}}\,({\rm{make-disjunct}}\,({\rm{append}}\,({\it{flist1\/}}, {\it{flist2\/}}))\index{make-disjunct}, {\it{alist\/}})\index{eval} \\ 
$=$$\;\;\;\;${\rm{eval}}\,(\=\+{\rm{make-disjunct}}\,({\rm{append}}\,(\=\+{\rm{cons}}\,({\rm{cadadar}}\,({\it{flist1\/}}), {\rm{cdr}}\,({\it{flist1\/}})), \\ 
{\it{flist2\/}})\-)\index{make-disjunct}, \\ 
{\it{alist\/}})\-\index{eval})\-\-
\end{tabbing}
\begin{verbatim};All tautologies are logically-true.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  taut-eval \\ \index{taut-eval}
\=\+{\rm{tautologyp1}}\,({\it{flist\/}}, {\it{auxlist\/}})\index{tautologyp1} \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\rm{make-disjunct}}\,({\rm{append}}\,({\it{flist\/}}, {\it{auxlist\/}}))\index{make-disjunct}, {\it{alist\/}})\index{eval}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  not-eval-prop-atomp \\ \index{not-eval-prop-atomp}
\=\+(\=\+{\rm{listp}}\,({\it{flist1\/}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{eval}}\,(\=\+{\rm{make-disjunct}}\,({\rm{append}}\,({\rm{cdr}}\,({\it{flist1\/}}), {\rm{cons}}\,({\rm{car}}\,({\it{flist1\/}}), {\it{flist2\/}})))\index{make-disjunct}, \\ 
{\it{alist\/}})\-\index{eval}))\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{eval}}\,({\rm{make-disjunct}}\,({\rm{append}}\,({\it{flist1\/}}, {\it{flist2\/}}))\index{make-disjunct}, {\it{alist\/}})\index{eval})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  prop-atomp-reduc \\ \index{prop-atomp-reduc}
\=\+{\rm{prop-atomp}}\,({\it{exp\/}})\index{prop-atomp} \\ 
$=$$\;\;\;\;$(\=\+{\rm{elem-form}}\,({\it{exp\/}})\index{elem-form} \\ 
$\vee$$\;\;\;\;$(({\it{exp\/}} $=$ {\rm{f-not}}\,({\rm{cadr}}\,({\it{exp\/}}))\index{f-not}) $\wedge$ {\rm{elem-form}}\,({\rm{cadr}}\,({\it{exp\/}}))\index{elem-form}))\-\-
\end{tabbing}

\noindent{\sc Event}:   Enable elem-form; name this event `g0263'.\index{g0263}

\addvspace{18pt}

\noindent{\sc Event}:   Enable prop-atomp; name this event `g0264'.\index{g0264}

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{prop-atomp-list} \\  
\=\+{\rm{prop-atomp-list}}\,({\it{list\/}})\index{prop-atomp-list} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{list\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{prop-atomp}}\,({\rm{car}}\,({\it{list\/}}))\index{prop-atomp} $\wedge$ {\rm{prop-atomp-list}}\,({\rm{cdr}}\,({\it{list\/}}))\index{prop-atomp-list}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{falsify} \\  
\=\+{\rm{falsify}}\,({\it{list\/}})\index{falsify} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{list\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }{\rm{car}}\,({\it{list\/}}) $=$ {\rm{f-not}}\,({\rm{cadar}}\,({\it{list\/}}))\index{f-not} \\ 
{\bf then }{\rm{cons}}\,({\rm{cadar}}\,({\it{list\/}}), {\rm{falsify}}\,({\rm{cdr}}\,({\it{list\/}}))\index{falsify}) \\ 
{\bf else }{\rm{falsify}}\,({\rm{cdr}}\,({\it{list\/}}))\index{falsify}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  falsify-step \\ \index{falsify-step}
({\rm{f-not}}\,({\it{exp\/}})\index{f-not} $\not\in$ {\it{auxlist\/}}) $\rightarrow$ ({\it{exp\/}} $\not\in$ {\rm{falsify}}\,({\it{auxlist\/}})\index{falsify})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  prop-atomp-auxlist \\ \index{prop-atomp-auxlist}
\=\+(\=\+{\rm{prop-atomp}}\,({\it{exp\/}})\index{prop-atomp} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{neg-list}}\,({\it{exp\/}}, {\it{auxlist\/}})\index{neg-list}) \\ 
$\wedge$$\;\;\;\;${\rm{prop-atomp-list}}\,({\it{auxlist\/}})\index{prop-atomp-list})\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{eval}}\,({\it{exp\/}}, {\rm{falsify}}\,({\rm{cons}}\,({\it{exp\/}}, {\it{auxlist\/}}))\index{falsify})\index{eval})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  prop-atomp-auxlist2 \\ \index{prop-atomp-auxlist2}
\=\+(\=\+($\neg$ {\rm{neg-list}}\,({\it{exp\/}}, {\it{auxlist\/}})\index{neg-list}) \\ 
$\wedge$$\;\;\;\;${\rm{prop-atomp-list}}\,({\it{auxlist\/}})\index{prop-atomp-list} \\ 
$\wedge$$\;\;\;\;${\rm{prop-atomp}}\,({\it{exp\/}})\index{prop-atomp} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{eval}}\,({\rm{make-disjunct}}\,({\it{auxlist\/}})\index{make-disjunct}, {\rm{falsify}}\,({\it{alist\/}})\index{falsify})\index{eval}))\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{eval}}\,({\rm{make-disjunct}}\,({\it{auxlist\/}})\index{make-disjunct}, {\rm{falsify}}\,({\rm{cons}}\,({\it{exp\/}}, {\it{alist\/}}))\index{falsify})\index{eval})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  prop-atomp-falsify \\ \index{prop-atomp-falsify}
\=\+(\=\+{\rm{prop-atomp}}\,({\it{exp\/}})\index{prop-atomp} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{neg-list}}\,({\it{exp\/}}, {\it{auxlist\/}})\index{neg-list}) \\ 
$\wedge$$\;\;\;\;${\rm{prop-atomp-list}}\,({\it{auxlist\/}})\index{prop-atomp-list} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{eval}}\,({\rm{make-disjunct}}\,({\it{auxlist\/}})\index{make-disjunct}, {\rm{falsify}}\,({\it{auxlist\/}})\index{falsify})\index{eval}))\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{eval}}\,({\rm{make-disjunct}}\,({\rm{cons}}\,({\it{exp\/}}, {\it{auxlist\/}}))\index{make-disjunct}, {\rm{falsify}}\,({\rm{cons}}\,({\it{exp\/}}, {\it{auxlist\/}}))\index{falsify})\index{eval})\-
\end{tabbing}

\noindent{\sc Event}:   Disable prop-atomp; name this event `g0268'.\index{g0268}

\addvspace{18pt}

\noindent{\sc Event}:   Disable elem-form; name this event `g0269'.\index{g0269}

\addvspace{18pt}

\noindent{\sc Event}:   Enable atomp; name this event `g0204'.\index{g0204}

\addvspace{18pt}
\begin{tabbing}{\sc Theorem}:  formula-cases1 \\ \index{formula-cases1}
\=\+{\rm{formula}}\,({\it{exp\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{prop-atomp}}\,({\it{exp\/}})\index{prop-atomp} \\ 
$\vee$$\;\;\;\;${\rm{or-type}}\,({\it{exp\/}})\index{or-type} \\ 
$\vee$$\;\;\;\;${\rm{nor-type}}\,({\it{exp\/}})\index{nor-type} \\ 
$\vee$$\;\;\;\;${\rm{dble-neg-type}}\,({\it{exp\/}})\index{dble-neg-type})\-\-
\end{tabbing}

\noindent{\sc Event}:   Disable atomp; name this event `g0205'.\index{g0205}

\addvspace{18pt}

\noindent{\sc Event}:   Enable prop-atomp; name this event `g0296'.\index{g0296}

\addvspace{18pt}

\noindent{\sc Event}:   Enable or-type; name this event `g0297'.\index{g0297}

\addvspace{18pt}

\noindent{\sc Event}:   Enable nor-type; name this event `g0298'.\index{g0298}

\addvspace{18pt}

\noindent{\sc Event}:   Enable dble-neg-type; name this event `g0299'.\index{g0299}

\addvspace{18pt}
\begin{tabbing}{\sc Theorem}:  formula-cases \\ \index{formula-cases}
\=\+(\=\+($\neg$ {\rm{dble-neg-type}}\,({\it{exp\/}})\index{dble-neg-type}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{nor-type}}\,({\it{exp\/}})\index{nor-type}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{or-type}}\,({\it{exp\/}})\index{or-type}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{prop-atomp}}\,({\it{exp\/}})\index{prop-atomp}))\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{formula}}\,({\it{exp\/}}, {\bf{t}}, {\tt{0}})\index{formula})\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{falsify-taut} \\  
\=\+{\rm{falsify-taut}}\,({\it{flist\/}}, {\it{auxlist\/}})\index{falsify-taut} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{flist\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\rm{falsify}}\,({\it{auxlist\/}})\index{falsify} \\ 
{\bf elseif }{\rm{prop-atomp}}\,({\rm{car}}\,({\it{flist\/}}))\index{prop-atomp} \\ 
{\bf then }\=\+{\bf if }{\rm{neg-list}}\,({\rm{car}}\,({\it{flist\/}}), {\it{auxlist\/}})\index{neg-list}$\;\;${\bf then }{\bf{f}} \\ 
{\bf else }{\rm{falsify-taut}}\,({\rm{cdr}}\,({\it{flist\/}}), {\rm{cons}}\,({\rm{car}}\,({\it{flist\/}}), {\it{auxlist\/}}))\index{falsify-taut}$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{or-type}}\,({\rm{car}}\,({\it{flist\/}}))\index{or-type} \\ 
{\bf then }{\rm{falsify-taut}}\,(\=\+{\rm{cons}}\,({\rm{cadar}}\,({\it{flist\/}}), {\rm{cons}}\,({\rm{caddar}}\,({\it{flist\/}}), {\rm{cdr}}\,({\it{flist\/}}))), \\ 
{\it{auxlist\/}})\-\index{falsify-taut} \\ 
{\bf elseif }{\rm{nor-type}}\,({\rm{car}}\,({\it{flist\/}}))\index{nor-type} \\ 
{\bf then }\=\+{\bf if }{\rm{falsify-taut}}\,({\rm{cons}}\,({\rm{f-not}}\,({\rm{caddadar}}\,({\it{flist\/}}))\index{f-not}, {\rm{cdr}}\,({\it{flist\/}})), {\it{auxlist\/}})\index{falsify-taut} \\ 
{\bf then }{\rm{falsify-taut}}\,(\=\+{\rm{cons}}\,({\rm{f-not}}\,({\rm{caddadar}}\,({\it{flist\/}}))\index{f-not}, {\rm{cdr}}\,({\it{flist\/}})), \\ 
{\it{auxlist\/}})\-\index{falsify-taut} \\ 
{\bf else }{\rm{falsify-taut}}\,(\=\+{\rm{cons}}\,({\rm{f-not}}\,({\rm{cadadar}}\,({\it{flist\/}}))\index{f-not}, {\rm{cdr}}\,({\it{flist\/}})), \\ 
{\it{auxlist\/}})\-\index{falsify-taut}$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{dble-neg-type}}\,({\rm{car}}\,({\it{flist\/}}))\index{dble-neg-type} \\ 
{\bf then }{\rm{falsify-taut}}\,({\rm{cons}}\,({\rm{cadadar}}\,({\it{flist\/}}), {\rm{cdr}}\,({\it{flist\/}})), {\it{auxlist\/}})\index{falsify-taut} \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  append-nlistp \\ \index{append-nlistp}
({\it{x\/}} $\simeq\;${{\bf{nil}}}${}$) $\rightarrow$ ({\rm{append}}\,({\it{x\/}}, {\it{y\/}}) $=$ {\it{y\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  not-falsify-taut \\ \index{not-falsify-taut}
{\rm{tautologyp1}}\,({\it{flist\/}}, {\it{auxlist\/}})\index{tautologyp1} $=$ ($\neg$ {\rm{falsify-taut}}\,({\it{flist\/}}, {\it{auxlist\/}})\index{falsify-taut})
\end{tabbing}
\begin{verbatim};Non-tautologies are falsifiable.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  not-taut-false \\ \index{not-taut-false}
\=\+(\=\+{\rm{form-list}}\,({\it{flist\/}})\index{form-list} \\ 
$\wedge$$\;\;\;\;${\rm{prop-atomp-list}}\,({\it{auxlist\/}})\index{prop-atomp-list} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{eval}}\,({\rm{make-disjunct}}\,({\it{auxlist\/}})\index{make-disjunct}, {\rm{falsify}}\,({\it{auxlist\/}})\index{falsify})\index{eval}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{tautologyp1}}\,({\it{flist\/}}, {\it{auxlist\/}})\index{tautologyp1}))\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{eval}}\,(\=\+{\rm{make-disjunct}}\,({\rm{append}}\,({\it{flist\/}}, {\it{auxlist\/}}))\index{make-disjunct}, \\ 
{\rm{falsify-taut}}\,({\it{flist\/}}, {\it{auxlist\/}})\index{falsify-taut})\-\index{eval})\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{tautologyp}$\;\;$
{\rm{tautologyp}}\,({\it{flist\/}})\index{tautologyp} $=$ {\rm{tautologyp1}}\,({\it{flist\/}}, {\bf{nil}})\index{tautologyp1}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{taut-proof}$\;\;$
{\rm{taut-proof}}\,({\it{flist\/}})\index{taut-proof} $=$ {\rm{taut-proof1}}\,({\it{flist\/}}, {\bf{nil}})\index{taut-proof1}
\end{tabbing}

\noindent{\sc Event}:   Disable append; name this event `g0300'.\index{g0300}

\addvspace{18pt}
\begin{tabbing}{\sc Theorem}:  form-list-append-nil \\ \index{form-list-append-nil}
{\rm{make-disjunct}}\,({\rm{append}}\,({\it{flist\/}}, {\bf{nil}}))\index{make-disjunct} $=$ {\rm{make-disjunct}}\,({\it{flist\/}})\index{make-disjunct}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  tautology-theorem \\ \index{tautology-theorem}
\=\+({\rm{form-list}}\,({\it{flist\/}})\index{form-list} $\wedge$ {\rm{tautologyp}}\,({\it{flist\/}})\index{tautologyp} $\wedge$ ({\it{concl\/}} $=$ {\rm{make-disjunct}}\,({\it{flist\/}})\index{make-disjunct})) \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{taut-proof}}\,({\it{flist\/}})\index{taut-proof}, {\it{concl\/}})\index{proves}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  taut-eval2 \\ \index{taut-eval2}
\=\+(\=\+{\rm{tautologyp1}}\,({\it{flist\/}}, {\it{auxlist\/}})\index{tautologyp1} \\ 
$\wedge$$\;\;\;\;$({\it{concl\/}} $=$ {\rm{make-disjunct}}\,({\rm{append}}\,({\it{flist\/}}, {\it{auxlist\/}}))\index{make-disjunct}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\it{concl\/}}, {\it{alist\/}})\index{eval}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  tautologies-are-true \\ \index{tautologies-are-true}
\=\+({\rm{form-list}}\,({\it{flist\/}})\index{form-list} $\wedge$ {\rm{tautologyp}}\,({\it{flist\/}})\index{tautologyp}) \\ 
$\rightarrow$$\;\;\;\;${\rm{eval}}\,({\rm{make-disjunct}}\,({\it{flist\/}})\index{make-disjunct}, {\it{alist\/}})\index{eval}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  not-taut-falsify2 \\ \index{not-taut-falsify2}
\=\+(\=\+{\rm{form-list}}\,({\it{flist\/}})\index{form-list} \\ 
$\wedge$$\;\;\;\;${\rm{prop-atomp-list}}\,({\it{auxlist\/}})\index{prop-atomp-list} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{eval}}\,({\rm{make-disjunct}}\,({\it{auxlist\/}})\index{make-disjunct}, {\rm{falsify}}\,({\it{auxlist\/}})\index{falsify})\index{eval}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{tautologyp1}}\,({\it{flist\/}}, {\it{auxlist\/}})\index{tautologyp1}) \\ 
$\wedge$$\;\;\;\;$({\it{concl\/}} $=$ {\rm{make-disjunct}}\,({\rm{append}}\,({\it{flist\/}}, {\it{auxlist\/}}))\index{make-disjunct}))\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{eval}}\,({\it{concl\/}}, {\rm{falsify-taut}}\,({\it{flist\/}}, {\it{auxlist\/}})\index{falsify-taut})\index{eval})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  truths-are-tautologies \\ \index{truths-are-tautologies}
\=\+({\rm{form-list}}\,({\it{flist\/}})\index{form-list} $\wedge$ ($\neg$ {\rm{tautologyp}}\,({\it{flist\/}})\index{tautologyp})) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{eval}}\,({\rm{make-disjunct}}\,({\it{flist\/}})\index{make-disjunct}, {\rm{falsify-taut}}\,({\it{flist\/}}, {\bf{nil}})\index{falsify-taut})\index{eval})\-
\end{tabbing}

\noindent{\sc Event}:   Enable truths-are-tautologies; name this event `g2439'.\index{g2439}

\addvspace{18pt}

\noindent{\sc Event}:   Enable not-taut-falsify2; name this event `g2440'.\index{g2440}

\addvspace{18pt}

\noindent{\sc Event}:   Enable tautologies-are-true; name this event `g2441'.\index{g2441}

\addvspace{18pt}

\noindent{\sc Event}:   Enable taut-eval2; name this event `g2442'.\index{g2442}

\addvspace{18pt}

\noindent{\sc Event}:   Enable form-list-append-nil; name this event `g2443'.\index{g2443}

\addvspace{18pt}

\noindent{\sc Event}:   Enable taut-proof; name this event `g2444'.\index{g2444}

\addvspace{18pt}

\noindent{\sc Event}:   Enable not-taut-false; name this event `g2445'.\index{g2445}

\addvspace{18pt}

\noindent{\sc Event}:   Enable not-falsify-taut; name this event `g2446'.\index{g2446}

\addvspace{18pt}

\noindent{\sc Event}:   Enable append-nlistp; name this event `g2447'.\index{g2447}

\addvspace{18pt}

\noindent{\sc Event}:   Enable falsify-taut; name this event `g2448'.\index{g2448}

\addvspace{18pt}

\noindent{\sc Event}:   Enable formula-cases; name this event `g2449'.\index{g2449}

\addvspace{18pt}

\noindent{\sc Event}:   Enable formula-cases1; name this event `g2450'.\index{g2450}

\addvspace{18pt}

\noindent{\sc Event}:   Enable prop-atomp-falsify; name this event `g2451'.\index{g2451}

\addvspace{18pt}

\noindent{\sc Event}:   Enable prop-atomp-auxlist; name this event `g2453'.\index{g2453}

\addvspace{18pt}

\noindent{\sc Event}:   Enable prop-atomp-list; name this event `g2454'.\index{g2454}

\addvspace{18pt}

\noindent{\sc Event}:   Enable falsify-step; name this event `g2455'.\index{g2455}

\addvspace{18pt}

\noindent{\sc Event}:   Enable falsify; name this event `g2456'.\index{g2456}

\addvspace{18pt}

\noindent{\sc Event}:   Enable not-eval-prop-atomp; name this event `g2457'.\index{g2457}

\addvspace{18pt}

\noindent{\sc Event}:   Enable taut-eval; name this event `g2458'.\index{g2458}

\addvspace{18pt}

\noindent{\sc Event}:   Enable eval-dble-neg-type; name this event `g2459'.\index{g2459}

\addvspace{18pt}

\noindent{\sc Event}:   Enable eval-nor-type; name this event `g2460'.\index{g2460}

\addvspace{18pt}

\noindent{\sc Event}:   Enable eval-or-type; name this event `g2461'.\index{g2461}

\addvspace{18pt}

\noindent{\sc Event}:   Enable eval-prop-atomp; name this event `g2463'.\index{g2463}

\addvspace{18pt}

\noindent{\sc Event}:   Enable neg-list-eval; name this event `g2464'.\index{g2464}

\addvspace{18pt}

\noindent{\sc Event}:   Enable eval-neg-elem-form; name this event `g2465'.\index{g2465}

\addvspace{18pt}

\noindent{\sc Event}:   Enable elem-form-eval; name this event `g2471'.\index{g2471}

\addvspace{18pt}

\noindent{\sc Event}:   Enable eval; name this event `g2472'.\index{g2472}

\addvspace{18pt}
\begin{tabbing}{\sc Theorem}:  eval-tautologyp \\ \index{eval-tautologyp}
\=\+({\rm{form-list}}\,({\it{flist\/}})\index{form-list} $\wedge$ {\rm{eval}}\,({\rm{make-disjunct}}\,({\it{flist\/}})\index{make-disjunct}, {\rm{falsify-taut}}\,({\it{flist\/}}, {\bf{nil}})\index{falsify-taut})\index{eval}) \\ 
$\rightarrow$$\;\;\;\;${\rm{tautologyp}}\,({\it{flist\/}})\index{tautologyp}\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{lis-not} \\  
\=\+{\rm{lis-not}}\,({\it{flist\/}})\index{lis-not} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{flist\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,({\rm{f-not}}\,({\rm{car}}\,({\it{flist\/}}))\index{f-not}, {\rm{lis-not}}\,({\rm{cdr}}\,({\it{flist\/}}))\index{lis-not})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{taut-conseq} \\  
{\rm{taut-conseq}}\,({\it{flist\/}}, {\it{exp\/}})\index{taut-conseq} $=$ {\rm{tautologyp}}\,({\rm{append}}\,({\rm{lis-not}}\,({\it{flist\/}})\index{lis-not}, {\rm{cons}}\,({\it{exp\/}}, {\bf{nil}})))\index{tautologyp}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{tautconseq-proof} \\  
\=\+{\rm{tautconseq-proof}}\,({\it{flist\/}}, {\it{exp\/}}, {\it{pflist\/}})\index{tautconseq-proof} \\ 
$=$$\;\;\;\;${\rm{list-detach-proof}}\,(\=\+{\it{flist\/}}, \\ 
{\it{exp\/}}, \\ 
{\it{pflist\/}}, \\ 
{\rm{taut-proof}}\,({\rm{append}}\,({\rm{lis-not}}\,({\it{flist\/}})\index{lis-not}, {\rm{cons}}\,({\it{exp\/}}, {\bf{nil}})))\index{taut-proof})\-\index{list-detach-proof}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  list-implies-reduc \\ \index{list-implies-reduc}
\=\+{\rm{list-implies}}\,({\it{flist\/}}, {\it{exp\/}})\index{list-implies} \\ 
$=$$\;\;\;\;${\rm{make-disjunct}}\,({\rm{append}}\,({\rm{lis-not}}\,({\it{flist\/}})\index{lis-not}, {\rm{cons}}\,({\it{exp\/}}, {\bf{nil}})))\index{make-disjunct}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  append-exp-form-list \\ \index{append-exp-form-list}
\=\+({\rm{form-list}}\,({\it{flist\/}})\index{form-list} $\wedge$ {\rm{formula}}\,({\it{exp\/}}, {\bf{t}}, {\tt{0}})\index{formula}) \\ 
$\rightarrow$$\;\;\;\;${\rm{form-list}}\,({\rm{append}}\,({\rm{lis-not}}\,({\it{flist\/}})\index{lis-not}, {\rm{cons}}\,({\it{exp\/}}, {\bf{nil}})))\index{form-list}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  taut-conseq-proves \\ \index{taut-conseq-proves}
\=\+(\=\+{\rm{form-list}}\,({\it{flist\/}})\index{form-list} \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\it{exp\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{taut-conseq}}\,({\it{flist\/}}, {\it{exp\/}})\index{taut-conseq} \\ 
$\wedge$$\;\;\;\;${\rm{proves-list}}\,({\it{pflist\/}}, {\it{flist\/}})\index{proves-list})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{tautconseq-proof}}\,({\it{flist\/}}, {\it{exp\/}}, {\it{pflist\/}})\index{tautconseq-proof}, {\it{exp\/}})\index{proves}\-
\end{tabbing}

\noindent{\sc Event}:   Enable tautconseq-proof; name this event `g0276'.\index{g0276}

\addvspace{18pt}
\begin{tabbing}{\sc Theorem}:  eval-tautconseq \\ \index{eval-tautconseq}
\=\+(\=\+{\rm{form-list}}\,({\it{flist\/}})\index{form-list} \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\it{exp\/}}, {\bf{t}}, {\tt{0}})\index{formula} \\ 
$\wedge$$\;\;\;\;${\rm{eval}}\,(\=\+{\rm{make-disjunct}}\,({\rm{append}}\,({\rm{lis-not}}\,({\it{flist\/}})\index{lis-not}, {\rm{cons}}\,({\it{exp\/}}, {\bf{nil}})))\index{make-disjunct}, \\ 
{\rm{falsify-taut}}\,({\rm{append}}\,({\rm{lis-not}}\,({\it{flist\/}})\index{lis-not}, {\rm{cons}}\,({\it{exp\/}}, {\bf{nil}})), {\bf{nil}})\index{falsify-taut})\-\index{eval})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{taut-conseq}}\,({\it{flist\/}}, {\it{exp\/}})\index{taut-conseq}\-
\end{tabbing}

\noindent{\sc Event}:   Enable taut-conseq; name this event `g0277'.\index{g0277}

\addvspace{18pt}

\noindent{\sc Event}:   Enable falsify-taut; name this event `g0282'.\index{g0282}

\addvspace{18pt}

\noindent{\sc Event}:   Enable formula; name this event `g0295'.\index{g0295}

\addvspace{18pt}
\begin{tabbing}{\sc Theorem}:  eval-tautconseq-proof-proves \\ \index{eval-tautconseq-proof-proves}
\=\+(\=\+{\rm{eval}}\,(\=\+{\rm{make-disjunct}}\,({\rm{append}}\,({\rm{lis-not}}\,({\it{flist\/}})\index{lis-not}, {\rm{cons}}\,({\it{exp\/}}, {\bf{nil}})))\index{make-disjunct}, \\ 
{\rm{falsify-taut}}\,({\rm{append}}\,({\rm{lis-not}}\,({\it{flist\/}})\index{lis-not}, {\rm{cons}}\,({\it{exp\/}}, {\bf{nil}})), {\bf{nil}})\index{falsify-taut})\-\index{eval} \\ 
$\wedge$$\;\;\;\;${\rm{proves-list}}\,({\it{pflist\/}}, {\it{flist\/}})\index{proves-list} \\ 
$\wedge$$\;\;\;\;${\rm{form-list}}\,({\it{flist\/}})\index{form-list} \\ 
$\wedge$$\;\;\;\;${\rm{formula}}\,({\it{exp\/}}, {\bf{t}}, {\tt{0}})\index{formula})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proves}}\,({\rm{tautconseq-proof}}\,({\it{flist\/}}, {\it{exp\/}}, {\it{pflist\/}})\index{tautconseq-proof}, {\it{exp\/}})\index{proves}\-
\end{tabbing}

\noindent{\sc Event}:   Enable taut-conseq-proves; name this event `g0283'.\index{g0283}

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{f-iff-reduc-proof} \\  
\=\+{\rm{f-iff-reduc-proof}}\,({\it{a\/}}, {\it{b\/}}, {\it{pf1\/}}, {\it{pf2\/}})\index{f-iff-reduc-proof} \\ 
$=$$\;\;\;\;${\rm{tautconseq-proof}}\,({\rm{list}}\,({\rm{f-iff}}\,({\it{a\/}}, {\it{b\/}})\index{f-iff}, {\it{a\/}}), {\it{b\/}}, {\rm{list}}\,({\it{pf1\/}}, {\it{pf2\/}}))\index{tautconseq-proof}\-
\end{tabbing}



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