\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};; Requires sets, alists, and terms, which currently contain a number
;; of rules that aren't really needed here, even indirectly.

;; This is a proof soundness of a slight abstraction of the GENERALIZE
;; command of PC-NQTHM.

\end{verbatim}
\noindent{\sc Event}:   Start with the library {\tt{"terms"}}.

\addvspace{18pt}

\begin{verbatim}#| Here's what I want to prove.

(implies (and (generalize-okp sg state)
	      (valid-state (generalize sg state)))
	 (valid-state state))

I also prove the much simpler fact, GENERALIZE-STATEP:

(implies (generalize-okp sg state)
	 (statep (generalize sg state)))

|#

;; << 1 >>
\end{verbatim}\begin{tabbing}{\sc Conservative Axiom}:  theorem-intro \\ \index{theorem-intro}
\=\+(({\rm{theorem}}\,({\it{x\/}})\index{theorem} $\wedge$ {\it{flg\/}}) $\rightarrow$ {\rm{termp}}\,({\it{flg\/}}, {\it{x\/}})\index{termp}) \\ 
$\wedge$$\;\;\;\;$(({\rm{theorem}}\,({\it{x\/}})\index{theorem} $\wedge$ {\it{flg\/}} $\wedge$ {\rm{var-substp}}\,({\it{s\/}})\index{var-substp}) $\rightarrow$ {\rm{theorem}}\,({\rm{subst}}\,({\it{flg\/}}, {\it{s\/}}, {\it{x\/}})\index{subst})\index{theorem})\-
\end{tabbing}\noindent Simultaneously, we introduce the new function symbol {\it theorem\/}.

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

\begin{verbatim};; << 3 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  theorem-list-properties \\ \index{theorem-list-properties}
\=\+({\rm{theorem-list}}\,({\it{x\/}})\index{theorem-list} $\rightarrow$ {\rm{termp}}\,({\bf{f}}, {\it{x\/}})\index{termp}) \\ 
$\wedge$$\;\;\;\;$(({\rm{theorem-list}}\,({\it{x\/}})\index{theorem-list} $\wedge$ {\rm{var-substp}}\,({\it{s\/}})\index{var-substp}) $\rightarrow$ {\rm{theorem-list}}\,({\rm{subst}}\,({\bf{f}}, {\it{s\/}}, {\it{x\/}})\index{subst})\index{theorem-list})\-
\end{tabbing}

\begin{verbatim};; << 4 >>
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{statep} \\  
\=\+{\rm{statep}}\,({\it{state\/}})\index{statep} \\ 
$=$$\;\;\;\;$({\rm{listp}}\,({\it{state\/}}) $\wedge$ {\rm{termp}}\,({\bf{f}}, {\rm{car}}\,({\it{state\/}}))\index{termp} $\wedge$ {\rm{variable-listp}}\,({\rm{cdr}}\,({\it{state\/}}))\index{variable-listp})\-
\end{tabbing}

\begin{verbatim};; << 5 >>
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{valid-state} \\  
\=\+{\rm{valid-state}}\,({\it{state\/}})\index{valid-state} \\ 
$\leftrightarrow$$\;\;\;\;$(\=\+{\rm{statep}}\,({\it{state\/}})\index{statep} \\ 
$\wedge$$\;\;\;\;$$\exists\;${\it{witnessing-instantiation\/}}$\;$(\=\+{\rm{var-substp}}\,({\it{witnessing-instantiation\/}})\index{var-substp} \\ 
$\wedge$$\;\;\;\;${\rm{subsetp}}\,(\=\+{\rm{domain}}\,({\it{witnessing-instantiation\/}})\index{domain}, \\ 
{\rm{cdr}}\,({\it{state\/}}))\-\index{subsetp} \\ 
$\wedge$$\;\;\;\;${\rm{theorem-list}}\,({\rm{subst}}\,(\=\+{\bf{f}}, \\ 
{\it{witnessing-instantiation\/}}, \\ 
{\rm{car}}\,({\it{state\/}}))\-\index{subst})\index{theorem-list})\-\index{exists})\-\-
\end{tabbing}

\begin{verbatim};; << 6 >>
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{new-gen-vars} \\  
\=\+{\rm{new-gen-vars}}\,({\it{goals\/}}, {\it{free\/}}, {\it{vars\/}})\index{new-gen-vars} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{goals\/}}) \\ 
{\bf then }\=\+{\bf let }\=\+{\it{current-free-vars\/}}{\bf $\;$ be$\;\;$}{\rm{intersection}}\,(\=\+{\it{free\/}}, \\ 
{\rm{all-vars}}\,({\bf{t}}, {\rm{car}}\,({\it{goals\/}}))\index{all-vars})\-\index{intersection}\- \\ 
{\bf in} \\ 
\=\+{\bf if }{\rm{disjoint}}\,({\it{current-free-vars\/}}, {\it{vars\/}})\index{disjoint} \\ 
{\bf then }{\rm{new-gen-vars}}\,({\rm{cdr}}\,({\it{goals\/}}), {\it{free\/}}, {\it{vars\/}})\index{new-gen-vars} \\ 
{\bf else }{\rm{append}}\,(\=\+{\it{current-free-vars\/}}, \\ 
{\rm{new-gen-vars}}\,({\rm{cdr}}\,({\it{goals\/}}), {\it{free\/}}, {\it{vars\/}})\index{new-gen-vars})\-$\;${\bf  endif}\-$\;${\bf  endlet}\- \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};; << 7 >>
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{cardinality}$\;\;$
{\rm{cardinality}}\,({\it{x\/}})\index{cardinality} $=$ {\rm{length}}\,({\rm{make-set}}\,({\it{x\/}})\index{make-set})\index{length}
\end{tabbing}

\begin{verbatim};; Next goal:  get the definition of GEN-CLOSURE accepted.  In fact,
;; the lemma GEN-CLOSURE-ACCEPT below suffices, taking NEW to be
;; (NEW-GEN-VARS GOALS FREE FREE-VARS-SO-FAR), as long as we prove the
;; following lemma, NEW-GEN-VARS-SUBSET.

;; << 8 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  new-gen-vars-subset \\ \index{new-gen-vars-subset}
{\rm{subsetp}}\,({\rm{new-gen-vars}}\,({\it{goals\/}}, {\it{free\/}}, {\it{vars\/}})\index{new-gen-vars}, {\it{free\/}})\index{subsetp}
\end{tabbing}

\begin{verbatim};; It is interesting to note that the exact form of the following
;; lemma changed while polishing the proof, since rewrite rules
;; applied to the old version so as to make it irrelevant.

;; << 9 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  gen-closure-accept \\ \index{gen-closure-accept}
\=\+(($\neg$ {\rm{subsetp}}\,({\it{new\/}}, {\it{free-vars-so-far\/}})\index{subsetp}) $\wedge$ {\rm{subsetp}}\,({\it{new\/}}, {\it{free\/}})\index{subsetp}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+(\=\+{\rm{length}}\,({\rm{make-set}}\,({\it{free\/}})\index{make-set})\index{length} \\ 
$-$$\;\;\;\;${\rm{length}}\,({\rm{intersection}}\,({\rm{make-set}}\,({\it{free\/}})\index{make-set}, {\it{free-vars-so-far\/}})\index{intersection})\index{length})\- \\ 
$-$$\;\;\;\;${\rm{length}}\,({\rm{intersection}}\,(\=\+{\rm{set-diff}}\,({\rm{make-set}}\,({\it{free\/}})\index{make-set}, {\it{free-vars-so-far\/}})\index{set-diff}, \\ 
{\it{new\/}})\-\index{intersection})\index{length})\- \\ 
$<$$\;\;\;\;$(\=\+{\rm{length}}\,({\rm{make-set}}\,({\it{free\/}})\index{make-set})\index{length} \\ 
$-$$\;\;\;\;${\rm{length}}\,({\rm{intersection}}\,({\rm{make-set}}\,({\it{free\/}})\index{make-set}, {\it{free-vars-so-far\/}})\index{intersection})\index{length})\-)\-\-
\end{tabbing}

\begin{verbatim};; Here I have a choice:  I could intersect the accumulator with free
;; at the end, or I could assume that it's intersected with free
;; before it's input.  I'll choose the former approach, so that I'll
;; have a simpler rewrite rule and so that I can call gen-closure more
;; simply.  I may wish to commute the arguments to intersection in the
;; exit below, but probably that won't matter because I'll only be
;; talking about membership.

;; << 10 >>
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{gen-closure} \\  
\=\+{\rm{gen-closure}}\,({\it{goals\/}}, {\it{free\/}}, {\it{free-vars-so-far\/}})\index{gen-closure} \\ 
$=$$\;\;\;\;$\=\+{\bf let }\=\+{\it{new-free-vars\/}}{\bf $\;$ be$\;\;$}{\rm{new-gen-vars}}\,({\it{goals\/}}, {\it{free\/}}, {\it{free-vars-so-far\/}})\index{new-gen-vars}\- \\ 
{\bf in} \\ 
\=\+{\bf if }{\rm{subsetp}}\,({\it{new-free-vars\/}}, {\it{free-vars-so-far\/}})\index{subsetp} \\ 
{\bf then }{\rm{intersection}}\,({\it{free-vars-so-far\/}}, {\it{free\/}})\index{intersection} \\ 
{\bf else }{\rm{gen-closure}}\,(\=\+{\it{goals\/}}, \\ 
{\it{free\/}}, \\ 
{\rm{append}}\,({\it{new-free-vars\/}}, {\it{free-vars-so-far\/}}))\-\index{gen-closure}$\;${\bf  endif}\-$\;${\bf  endlet}\-\-
\end{tabbing}

\begin{verbatim};; << 11 >>
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{generalize-okp} \\  
\=\+{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} \\ 
$=$$\;\;\;\;$(\=\+{\rm{var-substp}}\,({\it{sg\/}})\index{var-substp} \\ 
$\wedge$$\;\;\;\;${\rm{statep}}\,({\it{state\/}})\index{statep} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{domain}}\,({\it{sg\/}})\index{domain}, {\rm{all-vars}}\,({\bf{f}}, {\rm{car}}\,({\it{state\/}}))\index{all-vars})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\rm{car}}\,({\it{state\/}})) \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{domain}}\,({\it{sg\/}})\index{domain}, {\rm{cdr}}\,({\it{state\/}}))\index{disjoint})\-\-
\end{tabbing}

\begin{verbatim};; << 12 >>
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{generalize} \\  
\=\+{\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize} \\ 
$=$$\;\;\;\;$\=\+{\bf let }\=\+{\it{g\/}}{\bf $\;$ be$\;\;$}{\rm{caar}}\,({\it{state\/}}), \\ 
{\it{p\/}}{\bf $\;$ be$\;\;$}{\rm{cdar}}\,({\it{state\/}}), \\ 
{\it{free\/}}{\bf $\;$ be$\;\;$}{\rm{cdr}}\,({\it{state\/}}), \\ 
{\it{sg-vars\/}}{\bf $\;$ be$\;\;$}{\rm{all-vars}}\,({\bf{f}}, {\rm{range}}\,({\it{sg\/}})\index{range})\index{all-vars}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{new-g\/}}{\bf $\;$ be$\;\;$}{\rm{subst}}\,({\bf{t}}, {\rm{invert}}\,({\it{sg\/}})\index{invert}, {\it{g\/}})\index{subst}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{new-free\/}}{\bf $\;$ be$\;\;$}{\rm{set-diff}}\,(\=\+{\it{free\/}}, \\ 
{\rm{intersection}}\,(\=\+{\rm{gen-closure}}\,(\=\+{\rm{cons}}\,(\=\+{\it{new-g\/}}, \\ 
{\it{p\/}})\-, \\ 
{\it{free\/}}, \\ 
{\rm{all-vars}}\,(\=\+{\bf{t}}, \\ 
{\it{new-g\/}})\-\index{all-vars})\-\index{gen-closure}, \\ 
{\rm{all-vars}}\,(\=\+{\bf{f}}, \\ 
{\rm{range}}\,({\it{sg\/}})\index{range})\-\index{all-vars})\-\index{intersection})\-\index{set-diff}\- \\ 
{\bf in} \\ 
{\rm{cons}}\,({\rm{cons}}\,({\it{new-g\/}}, {\it{p\/}}), {\it{new-free\/}})$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-\-
\end{tabbing}

\begin{verbatim};; Here is a fact, not needed elsewhere, that is worth noticing, in
;; case we wish to extend the current theorem to a sequence of commands.

;; << 13 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  generalize-statep \\ \index{generalize-statep}
{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} $\rightarrow$ {\rm{statep}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{statep}
\end{tabbing}

\begin{verbatim};; << 14 >>
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{gen-inst} \\  
\=\+{\rm{gen-inst}}\,({\it{sg\/}}, {\it{state\/}})\index{gen-inst} \\ 
$=$$\;\;\;\;$\=\+{\bf let }\=\+{\it{s\/}}{\bf $\;$ be$\;\;$}{\rm{witnessing-instantiation}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{witnessing-instantiation}, \\ 
{\it{domain-1\/}}{\bf $\;$ be$\;\;$}{\rm{gen-closure}}\,(\=\+{\rm{cons}}\,(\=\+{\rm{subst}}\,({\bf{t}}, {\rm{invert}}\,({\it{sg\/}})\index{invert}, {\rm{caar}}\,({\it{state\/}}))\index{subst}, \\ 
{\rm{cdar}}\,({\it{state\/}}))\-, \\ 
{\rm{cdr}}\,({\it{state\/}}), \\ 
{\rm{all-vars}}\,(\=\+{\bf{t}}, \\ 
{\rm{subst}}\,(\=\+{\bf{t}}, \\ 
{\rm{invert}}\,({\it{sg\/}})\index{invert}, \\ 
{\rm{caar}}\,({\it{state\/}}))\-\index{subst})\-\index{all-vars})\-\index{gen-closure}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{restrict}, \\ 
{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{apply-to-subst}}\,(\=\+{\rm{nullify-subst}}\,({\it{sg\/}})\index{nullify-subst}, \\ 
{\rm{co-restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{co-restrict})\-\index{apply-to-subst}\- \\ 
{\bf in} \\ 
{\rm{apply-to-subst}}\,({\rm{apply-to-subst}}\,({\it{s2\/}}, {\it{sg\/}})\index{apply-to-subst}, {\rm{append}}\,({\it{s1\/}}, {\it{s2\/}}))\index{apply-to-subst}$\;${\bf  endlet}\-$\;${\bf  endlet}\-\-
\end{tabbing}

\begin{verbatim};; Let's see that it suffices to prove the result of opening up the
;; conclusion of the main theorem with a particular witness.

#|

(add-axiom main-theorem-1 (rewrite)
  (let ((wit (gen-inst sg state)))
    (implies (and (generalize-okp sg state)
		  (valid-state (generalize sg state)))
	     (and (statep state)
		  (var-substp wit)
		  (subsetp (domain wit) (cdr state))
		  (theorem-list (subst f wit (car state)))))))

(prove-lemma generalize-is-correct (rewrite)
  (implies (and (generalize-okp sg state)
		(valid-state (generalize sg state)))
	   (valid-state state))
  ((disable-theory t)
   (enable-theory ground-zero)
   (enable main-theorem-1)
   (use (valid-state
	 (witnessing-instantiation (gen-inst sg state))))))

|#

;; So, it suffices to prove main-theorem-1.  The first three conjuncts
;; of the conclusion are quite trivial.

;; << 15 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-theorem-1-case-1 \\ \index{main-theorem-1-case-1}
{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} $\rightarrow$ {\rm{statep}}\,({\it{state\/}})\index{statep}
\end{tabbing}

\begin{verbatim};; We put one direction of the definition of valid-state here, for
;; efficiency in proofs.

;; << 16 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  valid-state-opener \\ \index{valid-state-opener}
\=\+{\rm{valid-state}}\,({\it{state\/}})\index{valid-state} \\ 
$=$$\;\;\;\;$(\=\+{\rm{statep}}\,({\it{state\/}})\index{statep} \\ 
$\wedge$$\;\;\;\;$\=\+{\bf let }\=\+{\it{witnessing-instantiation\/}}{\bf $\;$ be$\;\;$}{\rm{witnessing-instantiation}}\,({\it{state\/}})\index{witnessing-instantiation}\- \\ 
{\bf in} \\ 
\=\+{\rm{var-substp}}\,({\it{witnessing-instantiation\/}})\index{var-substp} \\ 
$\wedge$$\;\;\;\;${\rm{subsetp}}\,(\=\+{\rm{domain}}\,({\it{witnessing-instantiation\/}})\index{domain}, \\ 
{\rm{cdr}}\,({\it{state\/}}))\-\index{subsetp} \\ 
$\wedge$$\;\;\;\;${\rm{theorem-list}}\,({\rm{subst}}\,(\=\+{\bf{f}}, \\ 
{\it{witnessing-instantiation\/}}, \\ 
{\rm{car}}\,({\it{state\/}}))\-\index{subst})\index{theorem-list}\-$\;${\bf  endlet}\-)\-\-
\end{tabbing}

\begin{verbatim};; << 17 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-theorem-1-case-2 \\ \index{main-theorem-1-case-2}
\=\+{\bf let }\=\+{\it{wit\/}}{\bf $\;$ be$\;\;$}{\rm{gen-inst}}\,({\it{sg\/}}, {\it{state\/}})\index{gen-inst}\- \\ 
{\bf in} \\ 
\=\+({\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} $\wedge$ {\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state}) \\ 
$\rightarrow$$\;\;\;\;${\rm{var-substp}}\,({\it{wit\/}})\index{var-substp}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; << 18 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  subsetp-cdr-generalize \\ \index{subsetp-cdr-generalize}
{\rm{subsetp}}\,({\rm{cdr}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize}), {\rm{cdr}}\,({\it{state\/}}))\index{subsetp}
\end{tabbing}

\begin{verbatim};; At this point I had to prove SUBSETP-SET-DIFF-SUFFICIENCY because
;; of some lemma that was created during the polishing process
;; (perhaps DOMAIN-RESTRICT).

;; << 19 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-theorem-1-case-3 \\ \index{main-theorem-1-case-3}
\=\+{\bf let }\=\+{\it{wit\/}}{\bf $\;$ be$\;\;$}{\rm{gen-inst}}\,({\it{sg\/}}, {\it{state\/}})\index{gen-inst}\- \\ 
{\bf in} \\ 
\=\+{\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state} \\ 
$\rightarrow$$\;\;\;\;${\rm{subsetp}}\,({\rm{domain}}\,({\it{wit\/}})\index{domain}, {\rm{cdr}}\,({\it{state\/}}))\index{subsetp}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; So now we only have to prove MAIN-THEOREM-1-CASE-4 (written here
;; without use of LET):

#|

(add-axiom main-theorem-1-case-4 (rewrite)
  (implies (and (generalize-okp sg state)
		(valid-state (generalize sg state)))
	   (theorem-list (subst f (gen-inst sg state) (car state)))))

(prove-lemma main-theorem-1 (rewrite)
  (let ((wit (gen-inst sg state)))
    (implies (and (generalize-okp sg state)
		  (valid-state (generalize sg state)))
	     (and (statep state)
		  (var-substp wit)
		  (subsetp (domain wit) (cdr state))
		  (theorem-list (subst f wit (car state))))))
  ((disable-theory t)
   (enable-theory ground-zero)
   (enable main-theorem-1-case-1 main-theorem-1-case-2
	   main-theorem-1-case-3 main-theorem-1-case-4)))

|#

;; << 20 >>
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{gen-setting-substitutions} \\  
\=\+{\rm{gen-setting-substitutions}}\,({\it{s1\/}}, {\it{s2\/}}, {\it{sg\/}})\index{gen-setting-substitutions} \\ 
$=$$\;\;\;\;$(\=\+{\rm{var-substp}}\,({\it{s1\/}})\index{var-substp} \\ 
$\wedge$$\;\;\;\;${\rm{var-substp}}\,({\it{s2\/}})\index{var-substp} \\ 
$\wedge$$\;\;\;\;${\rm{var-substp}}\,({\it{sg\/}})\index{var-substp} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{domain}}\,({\it{s1\/}})\index{domain}, {\rm{domain}}\,({\it{s2\/}})\index{domain})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{domain}}\,({\it{s1\/}})\index{domain}, {\rm{domain}}\,({\it{sg\/}})\index{domain})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{domain}}\,({\it{s2\/}})\index{domain}, {\rm{domain}}\,({\it{sg\/}})\index{domain})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{all-vars}}\,({\bf{f}}, {\rm{range}}\,({\it{sg\/}})\index{range})\index{all-vars}, {\rm{domain}}\,({\it{s1\/}})\index{domain})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{all-vars}}\,({\bf{f}}, {\rm{range}}\,({\it{s2\/}})\index{range})\index{all-vars}, {\rm{domain}}\,({\it{sg\/}})\index{domain})\index{disjoint})\-\-
\end{tabbing}

\begin{verbatim};; << 21 >>
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{main-hyps} \\  
\=\+{\rm{main-hyps}}\,({\it{s1\/}}, {\it{s2\/}}, {\it{sg\/}}, {\it{g\/}}, {\it{p\/}})\index{main-hyps} \\ 
$=$$\;\;\;\;$(\=\+{\rm{termp}}\,({\bf{t}}, {\it{g\/}})\index{termp} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{all-vars}}\,({\bf{t}}, {\it{g\/}})\index{all-vars}, {\rm{domain}}\,({\it{sg\/}})\index{domain})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{termp}}\,({\bf{f}}, {\it{p\/}})\index{termp} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{all-vars}}\,({\bf{f}}, {\it{p\/}})\index{all-vars}, {\rm{domain}}\,({\it{sg\/}})\index{domain})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{gen-setting-substitutions}}\,({\it{s1\/}}, {\it{s2\/}}, {\it{sg\/}})\index{gen-setting-substitutions} \\ 
$\wedge$$\;\;\;\;${\rm{theorem-list}}\,({\rm{subst}}\,(\=\+{\bf{f}}, \\ 
{\rm{append}}\,({\it{s1\/}}, {\it{s2\/}}), \\ 
{\rm{cons}}\,({\rm{subst}}\,({\bf{t}}, {\rm{invert}}\,({\it{sg\/}})\index{invert}, {\it{g\/}})\index{subst}, {\it{p\/}}))\-\index{subst})\index{theorem-list})\-\-
\end{tabbing}

\begin{verbatim};; The goal above, MAIN-THEOREM-1-CASE-4, should follow from the
;; following two lemmas.

#|

(add-axiom main-hyps-suffice (rewrite)
  (implies (and (listp goals)
		(main-hyps s1 s2 sg (car goals) (cdr goals)))
	   (theorem-list (subst f
				(apply-to-subst (apply-to-subst s2 sg)
						(append s1 s2))
				goals))))

(add-axiom main-hyps-relieved (rewrite)
  (let ((g (caar state))
	(p (cdar state))
	(free (cdr state))
	(s (witnessing-instantiation (generalize sg state))))
    (let ((new-g (subst t (invert sg) g)))
      (let ((domain-1
	     (gen-closure (cons new-g p) free (all-vars t new-g))))
	(let ((s1 (restrict s domain-1))
	      (s2 (apply-to-subst (nullify-subst sg)
				  (co-restrict s domain-1))))
	  (implies (and (generalize-okp sg state)
			(valid-state (generalize sg state)))
		   (main-hyps s1 s2 sg g p)))))))

(prove-lemma main-theorem-1-case-4 (rewrite)
  (implies (and (generalize-okp sg state)
		(valid-state (generalize sg state)))
	   (theorem-list (subst f (gen-inst sg state) (car state))))
  ((disable-theory t)
   (enable-theory ground-zero)
   (enable gen-inst main-hyps-suffice generalize-okp main-hyps-relieved)))

|#

;; So, now let us start with MAIN-HYPS-SUFFICE.  It should follow from
;; two subgoals, as shown:

#|

(add-axiom main-hyps-suffice-first (rewrite)
  (implies (main-hyps s1 s2 sg g p)
	   (theorem (subst t
			   (apply-to-subst (apply-to-subst s2 sg)
					   (append s1 s2))
			   g))))

(add-axiom main-hyps-suffice-rest (rewrite)
  (implies (main-hyps s1 s2 sg g p)
	   (theorem-list (subst f
				(apply-to-subst (apply-to-subst s2 sg)
						(append s1 s2))
				p))))

(prove-lemma main-hyps-suffice (rewrite)
  (implies (and (listp goals)
		(main-hyps s1 s2 sg (car goals) (cdr goals)))
	   (theorem-list (subst f
				(apply-to-subst (apply-to-subst s2 sg)
						(append s1 s2))
				goals)))
  ((disable-theory t)
   (enable-theory ground-zero)
   (enable theorem-list subst main-hyps-suffice-first main-hyps-suffice-rest)))

|#

;; Consider the first of these.  Although COMPOSE-PROPERTY-REVERSED is
;; used in the proof (because it's enabled), it's actually not
;; necessary.  A proof took slightly over 10 minutes with the rule
;; enabled, and roughly 9 minutes without.

;; << 22 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-suffice-first-lemma-general \\ \index{main-hyps-suffice-first-lemma-ge!neral}
\=\+(\=\+{\rm{termp}}\,({\it{flg\/}}, {\it{g\/}})\index{termp} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{all-vars}}\,({\it{flg\/}}, {\it{g\/}})\index{all-vars}, {\rm{domain}}\,({\it{sg\/}})\index{domain})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{gen-setting-substitutions}}\,({\it{s1\/}}, {\it{s2\/}}, {\it{sg\/}})\index{gen-setting-substitutions} \\ 
$\wedge$$\;\;\;\;$({\it{sg-1\/}} $=$ {\rm{invert}}\,({\it{sg\/}})\index{invert}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{subst}}\,({\it{flg\/}}, {\rm{apply-to-subst}}\,({\rm{apply-to-subst}}\,({\it{s2\/}}, {\it{sg\/}})\index{apply-to-subst}, {\rm{append}}\,({\it{s1\/}}, {\it{s2\/}}))\index{apply-to-subst}, {\it{g\/}})\index{subst} \\ 
$=$$\;\;\;\;${\rm{subst}}\,(\=\+{\it{flg\/}}, \\ 
{\rm{apply-to-subst}}\,({\it{s2\/}}, {\it{sg\/}})\index{apply-to-subst}, \\ 
{\rm{subst}}\,({\it{flg\/}}, {\rm{append}}\,({\it{s1\/}}, {\it{s2\/}}), {\rm{subst}}\,({\it{flg\/}}, {\it{sg-1\/}}, {\it{g\/}})\index{subst})\index{subst})\-\index{subst})\-\-
\end{tabbing}

\begin{verbatim};; << 23 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-suffice-first-lemma \\ \index{main-hyps-suffice-first-lemma}
\=\+(\=\+{\rm{termp}}\,({\bf{t}}, {\it{g\/}})\index{termp} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{all-vars}}\,({\bf{t}}, {\it{g\/}})\index{all-vars}, {\rm{domain}}\,({\it{sg\/}})\index{domain})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{gen-setting-substitutions}}\,({\it{s1\/}}, {\it{s2\/}}, {\it{sg\/}})\index{gen-setting-substitutions})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{subst}}\,({\bf{t}}, {\rm{apply-to-subst}}\,({\rm{apply-to-subst}}\,({\it{s2\/}}, {\it{sg\/}})\index{apply-to-subst}, {\rm{append}}\,({\it{s1\/}}, {\it{s2\/}}))\index{apply-to-subst}, {\it{g\/}})\index{subst} \\ 
$=$$\;\;\;\;${\rm{subst}}\,(\=\+{\bf{t}}, \\ 
{\rm{apply-to-subst}}\,({\it{s2\/}}, {\it{sg\/}})\index{apply-to-subst}, \\ 
{\rm{subst}}\,({\bf{t}}, {\rm{append}}\,({\it{s1\/}}, {\it{s2\/}}), {\rm{subst}}\,({\bf{t}}, {\rm{invert}}\,({\it{sg\/}})\index{invert}, {\it{g\/}})\index{subst})\index{subst})\-\index{subst})\-\-
\end{tabbing}

\begin{verbatim};; << 24 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-suffice-first \\ \index{main-hyps-suffice-first}
\=\+{\rm{main-hyps}}\,({\it{s1\/}}, {\it{s2\/}}, {\it{sg\/}}, {\it{g\/}}, {\it{p\/}})\index{main-hyps} \\ 
$\rightarrow$$\;\;\;\;${\rm{theorem}}\,({\rm{subst}}\,({\bf{t}}, {\rm{apply-to-subst}}\,({\rm{apply-to-subst}}\,({\it{s2\/}}, {\it{sg\/}})\index{apply-to-subst}, {\rm{append}}\,({\it{s1\/}}, {\it{s2\/}}))\index{apply-to-subst}, {\it{g\/}})\index{subst})\index{theorem}\-
\end{tabbing}

\begin{verbatim};; The following is useful with s = (append s1 s2).

;; << 25 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-suffice-rest-lemma \\ \index{main-hyps-suffice-rest-lemma}
\=\+(\=\+{\rm{termp}}\,({\it{flg\/}}, {\it{p\/}})\index{termp} \\ 
$\wedge$$\;\;\;\;${\rm{variable-listp}}\,({\rm{domain}}\,({\it{sg\/}})\index{domain})\index{variable-listp} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{all-vars}}\,({\it{flg\/}}, {\it{p\/}})\index{all-vars}, {\rm{domain}}\,({\it{sg\/}})\index{domain})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{subst}}\,({\it{flg\/}}, {\rm{apply-to-subst}}\,({\rm{apply-to-subst}}\,({\it{s2\/}}, {\it{sg\/}})\index{apply-to-subst}, {\it{s\/}})\index{apply-to-subst}, {\it{p\/}})\index{subst} \\ 
$=$$\;\;\;\;${\rm{subst}}\,({\it{flg\/}}, {\rm{apply-to-subst}}\,({\it{s2\/}}, {\it{sg\/}})\index{apply-to-subst}, {\rm{subst}}\,({\it{flg\/}}, {\it{s\/}}, {\it{p\/}})\index{subst})\index{subst})\-\-
\end{tabbing}

\begin{verbatim};; << 26 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-suffice-rest \\ \index{main-hyps-suffice-rest}
\=\+{\rm{main-hyps}}\,({\it{s1\/}}, {\it{s2\/}}, {\it{sg\/}}, {\it{g\/}}, {\it{p\/}})\index{main-hyps} \\ 
$\rightarrow$$\;\;\;\;${\rm{theorem-list}}\,({\rm{subst}}\,(\=\+{\bf{f}}, \\ 
{\rm{apply-to-subst}}\,({\rm{apply-to-subst}}\,({\it{s2\/}}, {\it{sg\/}})\index{apply-to-subst}, {\rm{append}}\,({\it{s1\/}}, {\it{s2\/}}))\index{apply-to-subst}, \\ 
{\it{p\/}})\-\index{subst})\index{theorem-list}\-
\end{tabbing}

\begin{verbatim};; << 27 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-suffice \\ \index{main-hyps-suffice}
\=\+({\rm{listp}}\,({\it{goals\/}}) $\wedge$ {\rm{main-hyps}}\,({\it{s1\/}}, {\it{s2\/}}, {\it{sg\/}}, {\rm{car}}\,({\it{goals\/}}), {\rm{cdr}}\,({\it{goals\/}}))\index{main-hyps}) \\ 
$\rightarrow$$\;\;\;\;${\rm{theorem-list}}\,({\rm{subst}}\,(\=\+{\bf{f}}, \\ 
{\rm{apply-to-subst}}\,({\rm{apply-to-subst}}\,({\it{s2\/}}, {\it{sg\/}})\index{apply-to-subst}, {\rm{append}}\,({\it{s1\/}}, {\it{s2\/}}))\index{apply-to-subst}, \\ 
{\it{goals\/}})\-\index{subst})\index{theorem-list}\-
\end{tabbing}

\begin{verbatim};; I'll disable the two lemmas used above so that I avoid the possibility
;; of looping with COMPOSE-PROPERTY-REVERSED.

;; << 28 >>
\end{verbatim}
\noindent{\sc Event}:   Disable main-hyps-suffice-first-lemma.

\addvspace{18pt}
\begin{verbatim};; << 29 >>
\end{verbatim}
\noindent{\sc Event}:   Disable main-hyps-suffice-rest-lemma.

\addvspace{18pt}

\begin{verbatim};; All that remains now is to prove MAIN-HYPS-RELIEVED.  If we open up
;; MAIN-HYPS we see what the necessary subgoals are.  Recall the
;; definition of MAIN-HYPS:

#| 
(defn main-hyps (s1 s2 sg g p)
  (and (termp t g)
       (disjoint (all-vars t g) (domain sg))
       (termp f p)
       (disjoint (all-vars f p) (domain sg))
       (gen-setting-substitutions s1 s2 sg)
       (theorem-list (subst f (append s1 s2)
			    (cons (subst t (invert sg) g) p)))))
|#

;; << 30 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-1 \\ \index{main-hyps-relieved-1}
\=\+{\bf let }\=\+{\it{g\/}}{\bf $\;$ be$\;\;$}{\rm{caar}}\,({\it{state\/}})\- \\ 
{\bf in} \\ 
{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} $\rightarrow$ {\rm{termp}}\,({\bf{t}}, {\it{g\/}})\index{termp}$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; << 31 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-2 \\ \index{main-hyps-relieved-2}
\=\+{\bf let }\=\+{\it{g\/}}{\bf $\;$ be$\;\;$}{\rm{caar}}\,({\it{state\/}})\- \\ 
{\bf in} \\ 
{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} $\rightarrow$ {\rm{disjoint}}\,({\rm{all-vars}}\,({\bf{t}}, {\it{g\/}})\index{all-vars}, {\rm{domain}}\,({\it{sg\/}})\index{domain})\index{disjoint}$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; << 32 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-3 \\ \index{main-hyps-relieved-3}
\=\+{\bf let }\=\+{\it{p\/}}{\bf $\;$ be$\;\;$}{\rm{cdar}}\,({\it{state\/}})\- \\ 
{\bf in} \\ 
{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} $\rightarrow$ {\rm{termp}}\,({\bf{f}}, {\it{p\/}})\index{termp}$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; << 33 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-4 \\ \index{main-hyps-relieved-4}
\=\+{\bf let }\=\+{\it{p\/}}{\bf $\;$ be$\;\;$}{\rm{cdar}}\,({\it{state\/}})\- \\ 
{\bf in} \\ 
{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} $\rightarrow$ {\rm{disjoint}}\,({\rm{all-vars}}\,({\bf{f}}, {\it{p\/}})\index{all-vars}, {\rm{domain}}\,({\it{sg\/}})\index{domain})\index{disjoint}$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim}#|

(add-axiom main-hyps-relieved-5 (rewrite)
  (let ((g (caar state))
	(p (cdar state))
	(free (cdr state))
	(s (witnessing-instantiation (generalize sg state))))
    (let ((new-g (subst t (invert sg) g)))
      (let ((domain-1
	     (gen-closure (cons new-g p) free (all-vars t new-g))))
	(let ((s1 (restrict s domain-1))
	      (s2 (apply-to-subst (nullify-subst sg)
				  (co-restrict s domain-1))))
	  (implies (and (generalize-okp sg state)
			(valid-state (generalize sg state)))
		   (gen-setting-substitutions s1 s2 sg)))))))

(add-axiom main-hyps-relieved-6 (rewrite)
  (let ((g (caar state))
	(p (cdar state))
	(free (cdr state))
	(s (witnessing-instantiation (generalize sg state))))
    (let ((new-g (subst t (invert sg) g)))
      (let ((domain-1
	     (gen-closure (cons new-g p) free (all-vars t new-g))))
	(let ((s1 (restrict s domain-1))
	      (s2 (apply-to-subst (nullify-subst sg)
				  (co-restrict s domain-1))))
	  (implies (and (generalize-okp sg state)
			(valid-state (generalize sg state)))
		   (theorem-list (subst f (append s1 s2)
					(cons (subst t (invert sg) g) p)))))))))

(prove-lemma main-hyps-relieved (rewrite)
  (let ((g (caar state))
	(p (cdar state))
	(free (cdr state))
	(s (witnessing-instantiation (generalize sg state))))
    (let ((new-g (subst t (invert sg) g)))
      (let ((domain-1
	     (gen-closure (cons new-g p) free (all-vars t new-g))))
	(let ((s1 (restrict s domain-1))
	      (s2 (apply-to-subst (nullify-subst sg)
				  (co-restrict s domain-1))))
	  (implies (and (generalize-okp sg state)
			(valid-state (generalize sg state)))
		   (main-hyps s1 s2 sg g p))))))
  ((disable-theory t)
   (enable-theory ground-zero)
   (enable main-hyps main-hyps-relieved-1 main-hyps-relieved-2 main-hyps-relieved-3
	   main-hyps-relieved-4 main-hyps-relieved-5 main-hyps-relieved-6)))

|#

;; So, we have left the goals MAIN-HYPS-RELIEVED-5 and
;; MAIN-HYPS-RELIEVED-6.  Let us start with the first.  Opening up
;; GEN-SETTING-SUBSTITUTIONS gives us a number of subgoals.

;; The first two cases below do not require knowledge about DOMAIN-1
;; (or G, P, FREE, or NEW-G), but simply following from the validity
;; of the state (GENERALIZE SG STATE).  Disabling GENERALIZE is very
;; useful (probably not necessary, though I didn't let the prover run
;; long enough to find out).

;; << 34 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-5-lemma-1 \\ \index{main-hyps-relieved-5-lemma-1}
\=\+{\bf let }\=\+{\it{s\/}}{\bf $\;$ be$\;\;$}{\rm{witnessing-instantiation}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{witnessing-instantiation}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{restrict}, \\ 
{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{apply-to-subst}}\,({\rm{nullify-subst}}\,({\it{sg\/}})\index{nullify-subst}, {\rm{co-restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{co-restrict})\index{apply-to-subst}\- \\ 
{\bf in} \\ 
\=\+{\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state} \\ 
$\rightarrow$$\;\;\;\;$({\rm{var-substp}}\,({\it{s1\/}})\index{var-substp} $\wedge$ {\rm{var-substp}}\,({\it{s2\/}})\index{var-substp})\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; The next case is trivial.

;; << 35 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-5-lemma-2 \\ \index{main-hyps-relieved-5-lemma-2}
{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} $\rightarrow$ {\rm{var-substp}}\,({\it{sg\/}})\index{var-substp}
\end{tabbing}

\begin{verbatim};; The next case is also quite trivial; notice how abstracted it is.

;; << 36 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-5-lemma-3 \\ \index{main-hyps-relieved-5-lemma-3}
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{restrict}, \\ 
{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{apply-to-subst}}\,({\rm{nullify-subst}}\,({\it{sg\/}})\index{nullify-subst}, {\rm{co-restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{co-restrict})\index{apply-to-subst}\- \\ 
{\bf in} \\ 
{\rm{disjoint}}\,({\rm{domain}}\,({\it{s1\/}})\index{domain}, {\rm{domain}}\,({\it{s2\/}})\index{domain})\index{disjoint}$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; For the next two cases we first observe that (DOMAIN S) is disjoint
;; from (DOMAIN SG), and then we use SUBSETP-DISJOINT-1 where X is the
;; domain of S1 or S2, Y is the domain of S, and Z is the domain of
;; SG:
;;             (IMPLIES (AND (SUBSETP X Y) (DISJOINT Y Z))
;;                      (DISJOINT X Z))

;; << 37 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  witnessing-instantiation-is-disjoint-from-generalizing-substitution \\ \index{witnessing-instantiation-is-dis!joint-from-generalizing-substitution}
\=\+{\bf let }\=\+{\it{s\/}}{\bf $\;$ be$\;\;$}{\rm{witnessing-instantiation}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{witnessing-instantiation}\- \\ 
{\bf in} \\ 
\=\+({\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} $\wedge$ {\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state}) \\ 
$\rightarrow$$\;\;\;\;${\rm{disjoint}}\,({\rm{domain}}\,({\it{s\/}})\index{domain}, {\rm{domain}}\,({\it{sg\/}})\index{domain})\index{disjoint}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; In the next case we abstract away DOMAIN-1 (and hence G, P, FREE,
;; and NEW-G).  Incidentally, a similar phenomenon occurred here to
;; the one reported just above the statement above of MAIN-THEOREM-1-CASE-3:
;; final polishing resulted in the need for another lemma.  That extra
;; lemma is DISJOINT-SET-DIFF-SUFFICIENCY in this case, to be found
;; in "sets.events".

;; << 38 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-5-lemma-4 \\ \index{main-hyps-relieved-5-lemma-4}
\=\+{\bf let }\=\+{\it{s\/}}{\bf $\;$ be$\;\;$}{\rm{witnessing-instantiation}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{witnessing-instantiation}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{restrict}, \\ 
{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{apply-to-subst}}\,({\rm{nullify-subst}}\,({\it{sg\/}})\index{nullify-subst}, {\rm{co-restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{co-restrict})\index{apply-to-subst}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} \\ 
$\wedge$$\;\;\;\;${\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{disjoint}}\,({\rm{domain}}\,({\it{s1\/}})\index{domain}, {\rm{domain}}\,({\it{sg\/}})\index{domain})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{domain}}\,({\it{s2\/}})\index{domain}, {\rm{domain}}\,({\it{sg\/}})\index{domain})\index{disjoint})\-\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; The lemma MAIN-HYPS-RELIEVED-5-LEMMA-5-WIT is true because the
;; domain of s is contained in the free variables of the generalized
;; state (by choice, i.e. definition, of witnessing-instantiation),
;; which is disjoint from the intersection of the indicated
;; GEN-CLOSURE with the variables in the range of sg.  I'll use a
;; trick that I learned from Ken Kunen (definable Skolem function is
;; all, really) to reduce disjointness considerations to membership
;; considerations.

;; << 39 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-5-lemma-5-wit \\ \index{main-hyps-relieved-5-lemma-5-wit}
\=\+{\bf let }\=\+{\it{g\/}}{\bf $\;$ be$\;\;$}{\rm{caar}}\,({\it{state\/}}), \\ 
{\it{p\/}}{\bf $\;$ be$\;\;$}{\rm{cdar}}\,({\it{state\/}}), \\ 
{\it{free\/}}{\bf $\;$ be$\;\;$}{\rm{cdr}}\,({\it{state\/}}), \\ 
{\it{s\/}}{\bf $\;$ be$\;\;$}{\rm{witnessing-instantiation}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{witnessing-instantiation}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{new-g\/}}{\bf $\;$ be$\;\;$}{\rm{subst}}\,({\bf{t}}, {\rm{invert}}\,({\it{sg\/}})\index{invert}, {\it{g\/}})\index{subst}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{domain-1\/}}{\bf $\;$ be$\;\;$}{\rm{gen-closure}}\,(\=\+{\rm{cons}}\,({\it{new-g\/}}, {\it{p\/}}), \\ 
{\it{free\/}}, \\ 
{\rm{all-vars}}\,({\bf{t}}, {\it{new-g\/}})\index{all-vars})\-\index{gen-closure}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{restrict}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} \\ 
$\wedge$$\;\;\;\;${\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state} \\ 
$\wedge$$\;\;\;\;$({\it{wit\/}} $\in$ {\rm{all-vars}}\,({\bf{f}}, {\rm{range}}\,({\it{sg\/}})\index{range})\index{all-vars}) \\ 
$\wedge$$\;\;\;\;$({\it{wit\/}} $\in$ {\rm{domain}}\,({\it{s\/}})\index{domain}))\- \\ 
$\rightarrow$$\;\;\;\;$({\it{wit\/}} $\not\in$ {\it{domain-1\/}})\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; << 40 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-5-lemma-5 \\ \index{main-hyps-relieved-5-lemma-5}
\=\+{\bf let }\=\+{\it{g\/}}{\bf $\;$ be$\;\;$}{\rm{caar}}\,({\it{state\/}}), \\ 
{\it{p\/}}{\bf $\;$ be$\;\;$}{\rm{cdar}}\,({\it{state\/}}), \\ 
{\it{free\/}}{\bf $\;$ be$\;\;$}{\rm{cdr}}\,({\it{state\/}}), \\ 
{\it{s\/}}{\bf $\;$ be$\;\;$}{\rm{witnessing-instantiation}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{witnessing-instantiation}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{new-g\/}}{\bf $\;$ be$\;\;$}{\rm{subst}}\,({\bf{t}}, {\rm{invert}}\,({\it{sg\/}})\index{invert}, {\it{g\/}})\index{subst}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{domain-1\/}}{\bf $\;$ be$\;\;$}{\rm{gen-closure}}\,(\=\+{\rm{cons}}\,({\it{new-g\/}}, {\it{p\/}}), \\ 
{\it{free\/}}, \\ 
{\rm{all-vars}}\,({\bf{t}}, {\it{new-g\/}})\index{all-vars})\-\index{gen-closure}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{restrict}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} \\ 
$\wedge$$\;\;\;\;${\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{disjoint}}\,({\rm{all-vars}}\,({\bf{f}}, {\rm{range}}\,({\it{sg\/}})\index{range})\index{all-vars}, {\rm{domain}}\,({\it{s1\/}})\index{domain})\index{disjoint}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; << 41 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-5-lemma-6 \\ \index{main-hyps-relieved-5-lemma-6}
\=\+{\bf let }\=\+{\it{g\/}}{\bf $\;$ be$\;\;$}{\rm{caar}}\,({\it{state\/}}), \\ 
{\it{p\/}}{\bf $\;$ be$\;\;$}{\rm{cdar}}\,({\it{state\/}}), \\ 
{\it{free\/}}{\bf $\;$ be$\;\;$}{\rm{cdr}}\,({\it{state\/}}), \\ 
{\it{s\/}}{\bf $\;$ be$\;\;$}{\rm{witnessing-instantiation}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{witnessing-instantiation}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{new-g\/}}{\bf $\;$ be$\;\;$}{\rm{subst}}\,({\bf{t}}, {\rm{invert}}\,({\it{sg\/}})\index{invert}, {\it{g\/}})\index{subst}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{domain-1\/}}{\bf $\;$ be$\;\;$}{\rm{gen-closure}}\,(\=\+{\rm{cons}}\,({\it{new-g\/}}, {\it{p\/}}), \\ 
{\it{free\/}}, \\ 
{\rm{all-vars}}\,({\bf{t}}, {\it{new-g\/}})\index{all-vars})\-\index{gen-closure}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{apply-to-subst}}\,(\=\+{\rm{nullify-subst}}\,({\it{sg\/}})\index{nullify-subst}, \\ 
{\rm{co-restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{co-restrict})\-\index{apply-to-subst}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} \\ 
$\wedge$$\;\;\;\;${\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{disjoint}}\,({\rm{all-vars}}\,({\bf{f}}, {\rm{range}}\,({\it{s2\/}})\index{range})\index{all-vars}, {\rm{domain}}\,({\it{sg\/}})\index{domain})\index{disjoint}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; << 42 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-5 \\ \index{main-hyps-relieved-5}
\=\+{\bf let }\=\+{\it{g\/}}{\bf $\;$ be$\;\;$}{\rm{caar}}\,({\it{state\/}}), \\ 
{\it{p\/}}{\bf $\;$ be$\;\;$}{\rm{cdar}}\,({\it{state\/}}), \\ 
{\it{free\/}}{\bf $\;$ be$\;\;$}{\rm{cdr}}\,({\it{state\/}}), \\ 
{\it{s\/}}{\bf $\;$ be$\;\;$}{\rm{witnessing-instantiation}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{witnessing-instantiation}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{new-g\/}}{\bf $\;$ be$\;\;$}{\rm{subst}}\,({\bf{t}}, {\rm{invert}}\,({\it{sg\/}})\index{invert}, {\it{g\/}})\index{subst}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{domain-1\/}}{\bf $\;$ be$\;\;$}{\rm{gen-closure}}\,(\=\+{\rm{cons}}\,({\it{new-g\/}}, {\it{p\/}}), \\ 
{\it{free\/}}, \\ 
{\rm{all-vars}}\,({\bf{t}}, {\it{new-g\/}})\index{all-vars})\-\index{gen-closure}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{restrict}, \\ 
{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{apply-to-subst}}\,(\=\+{\rm{nullify-subst}}\,({\it{sg\/}})\index{nullify-subst}, \\ 
{\rm{co-restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{co-restrict})\-\index{apply-to-subst}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} \\ 
$\wedge$$\;\;\;\;${\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{gen-setting-substitutions}}\,({\it{s1\/}}, {\it{s2\/}}, {\it{sg\/}})\index{gen-setting-substitutions}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; Now all that is left is MAIN-HYPS-RELIEVED-6.  Actually, this lemma
;; doesn't have anything to do with inverse substitutions or even with
;; generalization, really.  The idea is simply that one takes a valid
;; state and wishes to split its witnessing substitution into two
;; parts.  The parts are the respective restriction and co-restriction
;; of the original substitution to some set that is ``closed'' in the
;; appropriate sense.  Actually, the co-restriction is allowed to have
;; a substitution applied to it, whose domain is disjoint from the
;; goals ``outside'' that closure.  Below we give the lemmas and the
;; proof of MAIN-HYPS-RELIEVED-6 from those lemmas.  But first let us
;; introduce the necessary notions.

;; << 43 >>
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{all-vars-disjoint-or-subsetp} \\  
\=\+{\rm{all-vars-disjoint-or-subsetp}}\,({\it{goals\/}}, {\it{free\/}}, {\it{x\/}})\index{all-vars-disjoint-or-subsetp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{goals\/}}) \\ 
{\bf then }\=\+(\=\+{\rm{subsetp}}\,({\rm{intersection}}\,({\it{free\/}}, {\rm{all-vars}}\,({\bf{t}}, {\rm{car}}\,({\it{goals\/}}))\index{all-vars})\index{intersection}, {\it{x\/}})\index{subsetp} \\ 
$\vee$$\;\;\;\;${\rm{disjoint}}\,({\rm{intersection}}\,({\it{free\/}}, {\rm{all-vars}}\,({\bf{t}}, {\rm{car}}\,({\it{goals\/}}))\index{all-vars})\index{intersection}, {\it{x\/}})\index{disjoint})\- \\ 
$\wedge$$\;\;\;\;${\rm{all-vars-disjoint-or-subsetp}}\,({\rm{cdr}}\,({\it{goals\/}}), {\it{free\/}}, {\it{x\/}})\index{all-vars-disjoint-or-subsetp}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};; Our plan will be to show that (CDR STATE) has the above property
;; with respect to the free variables of the generalized state and the
;; appropriate gen-closure.  In cases where one applies a substitution
;; of the form (append s1 s2) to such a list of goals, where the
;; domain of s1 is contained in the intersection of those free
;; variables with that closure and the domain of s2 is disjoint from
;; that intersection, we'll show that the result is a theorem-list iff
;; each of the following are theorem-lists:  apply s1 to the goals
;; whose vars intersect its domain, and apply s2 to the rest.
;; Reduction rules about applying restrictions etc. will then finish
;; the job.

;; Notice the similarity of the following definition with new-gen-vars.
;; Think of vars as the closure variables, and free as the free variable
;; set within which this all "takes place".

;; << 44 >>
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{goals-intersecting-vars} \\  
\=\+{\rm{goals-intersecting-vars}}\,({\it{goals\/}}, {\it{free\/}}, {\it{vars\/}})\index{goals-intersecting-vars} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{goals\/}}) \\ 
{\bf then }\=\+{\bf let }\=\+{\it{current-free-vars\/}}{\bf $\;$ be$\;\;$}{\rm{intersection}}\,(\=\+{\it{free\/}}, \\ 
{\rm{all-vars}}\,({\bf{t}}, {\rm{car}}\,({\it{goals\/}}))\index{all-vars})\-\index{intersection}\- \\ 
{\bf in} \\ 
\=\+{\bf if }{\rm{disjoint}}\,({\it{current-free-vars\/}}, {\it{vars\/}})\index{disjoint} \\ 
{\bf then }{\rm{goals-intersecting-vars}}\,({\rm{cdr}}\,({\it{goals\/}}), {\it{free\/}}, {\it{vars\/}})\index{goals-intersecting-vars} \\ 
{\bf else }{\rm{cons}}\,(\=\+{\rm{car}}\,({\it{goals\/}}), \\ 
{\rm{goals-intersecting-vars}}\,(\=\+{\rm{cdr}}\,({\it{goals\/}}), \\ 
{\it{free\/}}, \\ 
{\it{vars\/}})\-\index{goals-intersecting-vars})\-$\;${\bf  endif}\-$\;${\bf  endlet}\- \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};; << 45 >>
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{goals-disjoint-from-vars} \\  
\=\+{\rm{goals-disjoint-from-vars}}\,({\it{goals\/}}, {\it{free\/}}, {\it{vars\/}})\index{goals-disjoint-from-vars} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{goals\/}}) \\ 
{\bf then }\=\+{\bf let }\=\+{\it{current-free-vars\/}}{\bf $\;$ be$\;\;$}{\rm{intersection}}\,(\=\+{\it{free\/}}, \\ 
{\rm{all-vars}}\,({\bf{t}}, {\rm{car}}\,({\it{goals\/}}))\index{all-vars})\-\index{intersection}\- \\ 
{\bf in} \\ 
\=\+{\bf if }{\rm{disjoint}}\,({\it{current-free-vars\/}}, {\it{vars\/}})\index{disjoint} \\ 
{\bf then }{\rm{cons}}\,(\=\+{\rm{car}}\,({\it{goals\/}}), \\ 
{\rm{goals-disjoint-from-vars}}\,({\rm{cdr}}\,({\it{goals\/}}), {\it{free\/}}, {\it{vars\/}})\index{goals-disjoint-from-vars})\- \\ 
{\bf else }{\rm{goals-disjoint-from-vars}}\,({\rm{cdr}}\,({\it{goals\/}}), {\it{free\/}}, {\it{vars\/}})\index{goals-disjoint-from-vars}$\;${\bf  endif}\-$\;${\bf  endlet}\- \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};; Now we begin the remaining goal, MAIN-HYPS-RELIEVED-6.  The idea is
;; to show that the appropriate goal list is a theorem-list by showing
;; separately that the first and the rest are theorems, since the
;; reasons are slightly different.  The first is a theorem because its
;; free vars are all in domain-1, hence in the domain of s1; so, s2
;; can be dropped from the APPEND.  The rest all have the property
;; that their free vars are contained in or disjoint from domain-1,
;; and for those disjoint from it, they do not contain variables from
;; the domain of sg.  Notice that the new current goal may violate the
;; latter requirement, since it may have no free vars at all but
;; contain vars from the domain of sg, and that's why we have to make
;; a special case out of it.

#|

(add-axiom main-hyps-relieved-6-first (rewrite)
  (let ((g (caar state))
	(p (cdar state))
	(free (cdr state))
	(s (witnessing-instantiation (generalize sg state))))
    (let ((new-g (subst t (invert sg) g)))
      (let ((domain-1
	     (gen-closure (cons new-g p) free (all-vars t new-g))))
	(let ((s1 (restrict s domain-1))
	      (s2 (apply-to-subst (nullify-subst sg)
				  (co-restrict s domain-1))))
	  (implies (and (generalize-okp sg state)
			(valid-state (generalize sg state)))
		   (theorem (subst t (append s1 s2)
				   (subst t (invert sg) g)))))))))

(add-axiom main-hyps-relieved-6-rest (rewrite)
  (let ((g (caar state))
	(p (cdar state))
	(free (cdr state))
	(s (witnessing-instantiation (generalize sg state))))
    (let ((new-g (subst t (invert sg) g)))
      (let ((domain-1
	     (gen-closure (cons new-g p) free (all-vars t new-g))))
	(let ((s1 (restrict s domain-1))
	      (s2 (apply-to-subst (nullify-subst sg)
				  (co-restrict s domain-1))))
	  (implies (and (generalize-okp sg state)
			(valid-state (generalize sg state)))
		   (theorem-list (subst f (append s1 s2) p))))))))

(prove-lemma main-hyps-relieved-6 (rewrite)
  (let ((g (caar state))
	(p (cdar state))
	(free (cdr state))
	(s (witnessing-instantiation (generalize sg state))))
    (let ((new-g (subst t (invert sg) g)))
      (let ((domain-1
	     (gen-closure (cons new-g p) free (all-vars t new-g))))
	(let ((s1 (restrict s domain-1))
	      (s2 (apply-to-subst (nullify-subst sg)
				  (co-restrict s domain-1))))
	  (implies (and (generalize-okp sg state)
			(valid-state (generalize sg state)))
		   (theorem-list (subst f (append s1 s2)
					(cons (subst t (invert sg) g) p))))))))
  ((disable-theory t)
   (enable-theory ground-zero)
   (enable main-hyps-relieved-6-first main-hyps-relieved-6-rest subst theorem-list)))

|#

;; The first is true because the free vars in new-g are all in the
;; domain of s1, since they are all in domain-1.  By the way, the
;; proof-checker was useful here; I dove to the subst term (after
;; adding abbreviations and promoting hypotheses) and saw that I
;; wanted to rewrite with SUBST-APPEND-NOT-OCCUR-2.  I also notice the
;; need for GEN-CLOSURE-CONTAINS-THIRD-ARG during the attempt to prove
;; a goal.

;; First, we only want to open up GENERALIZE when we are looking at
;; goals, not when we are simply asking about the witnessing
;; substitution.

;; << 46 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  car-generalize \\ \index{car-generalize}
\=\+{\rm{car}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize}) \\ 
$=$$\;\;\;\;${\rm{cons}}\,({\rm{subst}}\,({\bf{t}}, {\rm{invert}}\,({\it{sg\/}})\index{invert}, {\rm{caar}}\,({\it{state\/}}))\index{subst}, {\rm{cdar}}\,({\it{state\/}}))\-
\end{tabbing}

\begin{verbatim};; << 47 >>
\end{verbatim}
\noindent{\sc Event}:   Disable generalize.

\addvspace{18pt}

\begin{verbatim};; Inspection of the proof of a subgoal of MAIN-HYPS-RELIEVED-6-FIRST
;; suggests that we need the following lemma.  Actually, before the
;; final polishing it was the case that the following version sufficed.
;; But final polishing led me to prove a "better" version, as well
;; as the lemma DISJOINT-SET-DIFF-GENERAL in "sets.events".

#|
(prove-lemma gen-closure-contains-third-arg (rewrite)
  (implies (subsetp domain free)
	   (subsetp (intersection domain free-vars-so-far)
		    (gen-closure goals free free-vars-so-far))))
|#

;; << 48 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  gen-closure-contains-third-arg \\ \index{gen-closure-contains-third-arg}
\=\+{\rm{subsetp}}\,({\it{x\/}}, {\rm{intersection}}\,({\it{free\/}}, {\it{free-vars-so-far\/}})\index{intersection})\index{subsetp} \\ 
$\rightarrow$$\;\;\;\;${\rm{subsetp}}\,({\it{x\/}}, {\rm{gen-closure}}\,({\it{goals\/}}, {\it{free\/}}, {\it{free-vars-so-far\/}})\index{gen-closure})\index{subsetp}\-
\end{tabbing}


\begin{verbatim};; << 49 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-6-first \\ \index{main-hyps-relieved-6-first}
\=\+{\bf let }\=\+{\it{g\/}}{\bf $\;$ be$\;\;$}{\rm{caar}}\,({\it{state\/}}), \\ 
{\it{p\/}}{\bf $\;$ be$\;\;$}{\rm{cdar}}\,({\it{state\/}}), \\ 
{\it{free\/}}{\bf $\;$ be$\;\;$}{\rm{cdr}}\,({\it{state\/}}), \\ 
{\it{s\/}}{\bf $\;$ be$\;\;$}{\rm{witnessing-instantiation}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{witnessing-instantiation}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{new-g\/}}{\bf $\;$ be$\;\;$}{\rm{subst}}\,({\bf{t}}, {\rm{invert}}\,({\it{sg\/}})\index{invert}, {\it{g\/}})\index{subst}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{domain-1\/}}{\bf $\;$ be$\;\;$}{\rm{gen-closure}}\,(\=\+{\rm{cons}}\,({\it{new-g\/}}, {\it{p\/}}), \\ 
{\it{free\/}}, \\ 
{\rm{all-vars}}\,({\bf{t}}, {\it{new-g\/}})\index{all-vars})\-\index{gen-closure}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{restrict}, \\ 
{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{apply-to-subst}}\,(\=\+{\rm{nullify-subst}}\,({\it{sg\/}})\index{nullify-subst}, \\ 
{\rm{co-restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{co-restrict})\-\index{apply-to-subst}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} \\ 
$\wedge$$\;\;\;\;${\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{theorem}}\,({\rm{subst}}\,({\bf{t}}, {\rm{append}}\,({\it{s1\/}}, {\it{s2\/}}), {\it{new-g\/}})\index{subst})\index{theorem}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-
\end{tabbing}


\begin{verbatim};; Now all that remains is MAIN-HYPS-RELIEVED-6-REST.

#|

;; I originally forgot the (TERMP F P) hypothesis below, but it wasn't
;; very hard to back up and fix this.

(add-axiom main-hyps-relieved-6-rest-generalization (rewrite)
  (let ((s1 (restrict s domain-1))
	(s2 (apply-to-subst (nullify-subst sg)
			    (co-restrict s domain-1))))
    (implies (and (var-substp sg)
		  (var-substp s)
		  (subsetp (domain s) new-free)
		  (termp f p)
		  (theorem-list (subst f s p)) 
		  (disjoint (domain sg)
			    (all-vars f (goals-disjoint-from-vars
					 p new-free domain-1)))
		  (all-vars-disjoint-or-subsetp p new-free domain-1)) 
	     (theorem-list (subst f (append s1 s2) p)))))

(add-axiom main-hyps-relieved-6-rest-lemma-1 (rewrite)
  (let ((g (caar state))
	(p (cdar state))
	(free (cdr state))
	(s (witnessing-instantiation (generalize sg state))))
    (let ((new-g (subst t (invert sg) g)))
      (let ((domain-1
	     (gen-closure (cons new-g p) free (all-vars t new-g))))
	(let ((s1 (restrict s domain-1))
	      (s2 (apply-to-subst (nullify-subst sg)
				  (co-restrict s domain-1))))
	  (implies (and (generalize-okp sg state)
			(valid-state (generalize sg state)))
		   (disjoint (domain sg)
			     (all-vars f (goals-disjoint-from-vars
					  p (cdr (generalize sg state)) domain-1)))))))))

;; Minor note:  I used the BREAK-LEMMA feature of NQTHM to realize
;; that I needed the following lemma.

(add-axiom main-hyps-relieved-6-rest-lemma-2 (rewrite)
  (let ((g (caar state))
	(p (cdar state))
	(free (cdr state))
	(s (witnessing-instantiation (generalize sg state))))
    (let ((new-g (subst t (invert sg) g)))
      (let ((domain-1
	     (gen-closure (cons new-g p) free (all-vars t new-g))))
	(let ((s1 (restrict s domain-1))
	      (s2 (apply-to-subst (nullify-subst sg)
				  (co-restrict s domain-1))))
	  (implies (and (generalize-okp sg state)
			(valid-state (generalize sg state)))
		   (all-vars-disjoint-or-subsetp p (cdr (generalize sg state)) domain-1)))))))

(prove-lemma main-hyps-relieved-6-rest (rewrite)
  (let ((g (caar state))
	(p (cdar state))
	(free (cdr state))
	(s (witnessing-instantiation (generalize sg state))))
    (let ((new-g (subst t (invert sg) g)))
      (let ((domain-1
	     (gen-closure (cons new-g p) free (all-vars t new-g))))
	(let ((s1 (restrict s domain-1))
	      (s2 (apply-to-subst (nullify-subst sg)
				  (co-restrict s domain-1))))
	  (implies (and (generalize-okp sg state)
			(valid-state (generalize sg state)))
		   (theorem-list (subst f (append s1 s2) p)))))))
  ((disable-theory t)
   (enable-theory ground-zero)
   (enable theorem-list subst car-generalize ;; so that we can get at p from (car state)
	   ;; relieving hyps of main-hyps-relieved-6-rest-generalization:
	   main-hyps-relieved-6-rest-lemma-1 main-hyps-relieved-6-rest-lemma-2
	   ;; to relieve the (termp f p) hypothesis in main-hyps-relieved-6-rest-generalization:
	   statep termp-list-cons
	   generalize-okp valid-state-opener main-hyps-relieved-6-rest-generalization)))

;; At this point I did a sanity check and sure enough, the pushed
;; lemmas all go through at this point:  main-hyps-relieved-6,
;; main-hyps-relieved, main-theorem-1-case-4, main-theorem-1, and
;; generalize-is-correct.

|#

;; It remains to prove MAIN-HYPS-RELIEVED-6-REST-LEMMA-1,
;; MAIN-HYPS-RELIEVED-6-REST-LEMMA-2, and
;; MAIN-HYPS-RELIEVED-6-REST-GENERALIZATION.

;; For the first of these we need the following trivial observation.

;; << 50 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  goals-disjoint-from-vars-subsetp \\ \index{goals-disjoint-from-vars-subsetp}
{\rm{subsetp}}\,({\rm{goals-disjoint-from-vars}}\,({\it{goals\/}}, {\it{free\/}}, {\it{vars\/}})\index{goals-disjoint-from-vars}, {\it{goals\/}})\index{subsetp}
\end{tabbing}

\begin{verbatim};; Unfortunately the observation above doesn't quite suffice, because
;; of a technical problem with free variables in hypotheses.  The
;; following consequence does, though.

;; << 51 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  disjoint-all-vars-goals-disjoint-from-vars \\ \index{disjoint-all-vars-goals-disjoint!-from-vars}
\=\+{\rm{disjoint}}\,({\it{x\/}}, {\rm{all-vars}}\,({\bf{f}}, {\it{goals\/}})\index{all-vars})\index{disjoint} \\ 
$\rightarrow$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\rm{all-vars}}\,({\bf{f}}, {\rm{goals-disjoint-from-vars}}\,({\it{goals\/}}, {\it{free\/}}, {\it{vars\/}})\index{goals-disjoint-from-vars})\index{all-vars})\index{disjoint}\-
\end{tabbing}

\begin{verbatim};; << 52 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-6-rest-lemma-1 \\ \index{main-hyps-relieved-6-rest-lemma!-1}
\=\+{\bf let }\=\+{\it{g\/}}{\bf $\;$ be$\;\;$}{\rm{caar}}\,({\it{state\/}}), \\ 
{\it{p\/}}{\bf $\;$ be$\;\;$}{\rm{cdar}}\,({\it{state\/}}), \\ 
{\it{free\/}}{\bf $\;$ be$\;\;$}{\rm{cdr}}\,({\it{state\/}}), \\ 
{\it{s\/}}{\bf $\;$ be$\;\;$}{\rm{witnessing-instantiation}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{witnessing-instantiation}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{new-g\/}}{\bf $\;$ be$\;\;$}{\rm{subst}}\,({\bf{t}}, {\rm{invert}}\,({\it{sg\/}})\index{invert}, {\it{g\/}})\index{subst}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{domain-1\/}}{\bf $\;$ be$\;\;$}{\rm{gen-closure}}\,(\=\+{\rm{cons}}\,({\it{new-g\/}}, {\it{p\/}}), \\ 
{\it{free\/}}, \\ 
{\rm{all-vars}}\,({\bf{t}}, {\it{new-g\/}})\index{all-vars})\-\index{gen-closure}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{restrict}, \\ 
{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{apply-to-subst}}\,(\=\+{\rm{nullify-subst}}\,({\it{sg\/}})\index{nullify-subst}, \\ 
{\rm{co-restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{co-restrict})\-\index{apply-to-subst}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} \\ 
$\wedge$$\;\;\;\;${\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{disjoint}}\,(\=\+{\rm{domain}}\,({\it{sg\/}})\index{domain}, \\ 
{\rm{all-vars}}\,(\=\+{\bf{f}}, \\ 
{\rm{goals-disjoint-from-vars}}\,(\=\+{\it{p\/}}, \\ 
{\rm{cdr}}\,({\rm{generalize}}\,(\=\+{\it{sg\/}}, \\ 
{\it{state\/}})\-\index{generalize}), \\ 
{\it{domain-1\/}})\-\index{goals-disjoint-from-vars})\-\index{all-vars})\-\index{disjoint}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; The next goal, MAIN-HYPS-RELIEVED-6-REST-LEMMA-2, needs the lemma
;; ALL-VARS-DISJOINT-OR-SUBSETP-GEN-CLOSURE below.  That lemma's
;; mechanical proof depends on the trivial observation
;; DISJOINT-INTERSECTION3-MIDDLE in file sets.events.

;; << 53 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  all-vars-disjoint-or-subsetp-gen-closure \\ \index{all-vars-disjoint-or-subsetp-ge!n-closure}
\=\+{\rm{subsetp}}\,({\it{domain\/}}, {\it{free\/}})\index{subsetp} \\ 
$\rightarrow$$\;\;\;\;${\rm{all-vars-disjoint-or-subsetp}}\,(\=\+{\it{goals\/}}, \\ 
{\it{domain\/}}, \\ 
{\rm{gen-closure}}\,({\rm{cons}}\,({\it{g\/}}, {\it{goals\/}}), {\it{free\/}}, {\it{vars\/}})\index{gen-closure})\-\index{all-vars-disjoint-or-subsetp}\-
\end{tabbing}

\begin{verbatim};; << 54 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-6-rest-lemma-2 \\ \index{main-hyps-relieved-6-rest-lemma!-2}
\=\+{\bf let }\=\+{\it{g\/}}{\bf $\;$ be$\;\;$}{\rm{caar}}\,({\it{state\/}}), \\ 
{\it{p\/}}{\bf $\;$ be$\;\;$}{\rm{cdar}}\,({\it{state\/}}), \\ 
{\it{free\/}}{\bf $\;$ be$\;\;$}{\rm{cdr}}\,({\it{state\/}}), \\ 
{\it{s\/}}{\bf $\;$ be$\;\;$}{\rm{witnessing-instantiation}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{witnessing-instantiation}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{new-g\/}}{\bf $\;$ be$\;\;$}{\rm{subst}}\,({\bf{t}}, {\rm{invert}}\,({\it{sg\/}})\index{invert}, {\it{g\/}})\index{subst}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{domain-1\/}}{\bf $\;$ be$\;\;$}{\rm{gen-closure}}\,(\=\+{\rm{cons}}\,({\it{new-g\/}}, {\it{p\/}}), \\ 
{\it{free\/}}, \\ 
{\rm{all-vars}}\,({\bf{t}}, {\it{new-g\/}})\index{all-vars})\-\index{gen-closure}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{restrict}, \\ 
{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{apply-to-subst}}\,(\=\+{\rm{nullify-subst}}\,({\it{sg\/}})\index{nullify-subst}, \\ 
{\rm{co-restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{co-restrict})\-\index{apply-to-subst}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} \\ 
$\wedge$$\;\;\;\;${\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{all-vars-disjoint-or-subsetp}}\,(\=\+{\it{p\/}}, \\ 
{\rm{cdr}}\,({\rm{generalize}}\,(\=\+{\it{sg\/}}, \\ 
{\it{state\/}})\-\index{generalize}), \\ 
{\it{domain-1\/}})\-\index{all-vars-disjoint-or-subsetp}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; Finally, all that's left is
;; MAIN-HYPS-RELIEVED-6-REST-GENERALIZATION.  An attempted proof by
;; induction of that theorem results in 11 goals, all but one of which
;; goes through automatically.  The remaining one is as follows.

#|

(IMPLIES
 (AND
  (DISJOINT NEW-FREE
	    (INTERSECTION DOMAIN-1
			  (ALL-VARS T X)))
  (THEOREM-LIST
   (SUBST F
	  (APPEND (RESTRICT S DOMAIN-1)
		  (APPLY-TO-SUBST (NULLIFY-SUBST SG)
				  (CO-RESTRICT S DOMAIN-1)))
	  Z))
  (MAPPING SG)
  (VARIABLE-LISTP (DOMAIN SG))
  (TERMP F (RANGE SG))
  (MAPPING S)
  (VARIABLE-LISTP (DOMAIN S))
  (TERMP F (RANGE S))
  (SUBSETP (DOMAIN S) NEW-FREE)
  (TERMP T X)
  (TERMP F Z)
  (THEOREM (SUBST T S X))
  (THEOREM-LIST (SUBST F S Z))
  (DISJOINT (DOMAIN SG) (ALL-VARS T X))
  (DISJOINT (DOMAIN SG)
	    (ALL-VARS F
		      (GOALS-DISJOINT-FROM-VARS Z NEW-FREE DOMAIN-1)))
  (ALL-VARS-DISJOINT-OR-SUBSETP Z NEW-FREE DOMAIN-1))
 (THEOREM (SUBST T
		 (APPEND (RESTRICT S DOMAIN-1)
			 (APPLY-TO-SUBST (NULLIFY-SUBST SG)
					 (CO-RESTRICT S DOMAIN-1)))
		 X)))

|#

;; Let us attempt to prove this goal with the proof-checker, thus
;; seeing why the rewriter can't handle it automatically.  We would
;; like to rewrite with SUBST-APPEND-NOT-OCCUR-1 to replace the
;; conclusion with:

#|
(THEOREM (SUBST T
		(APPLY-TO-SUBST (NULLIFY-SUBST SG)
				(CO-RESTRICT S DOMAIN-1))
		X))
|#

;; However, in order to do that we need to observe that under the
;; hypotheses, the following holds.

#|
(DISJOINT (ALL-VARS F
                    (DOMAIN (RESTRICT S DOMAIN-1)))
          (ALL-VARS T X))
|#

;; This is one of those cases of a problem with free variables in
;; hypotheses that are so annoying.  The lemma DOMAIN-RESTRICT has
;; been put in alists.events to help with this.  But then we lose the
;; fact that the first ALL-VARS in the goal above may be removed.  The
;; lemma VARIABLE-LISTP-INTERSECTION has been added to terms.events to
;; take care of that.

;; Now it looks like the rewrite using SUBST-APPEND-NOT-OCCUR-1 should
;; succeed, since all hypotheses are relieved by rewriting alone.
;; Just to make sure, we back up in the proof checker and see if BASH
;; uses this rule on our original goal.  Sure enough, it does.

;; Now our conclusion is the one displayed above, i.e.

#|
(THEOREM (SUBST T
		(APPLY-TO-SUBST (NULLIFY-SUBST SG)
				(CO-RESTRICT S DOMAIN-1))
		X))
|#

;; Since (as we already know) (NULLIFY-SUBST SG) has the same domain
;; as does SG, and since the hypotheses imply that (DOMAIN SG) is
;; disjoint from the variables of X, the SUBST expression in this
;; conclusion should simplify to:

#|
(SUBST T (NULLIFY-SUBST SG)
       (SUBST T (CO-RESTRICT S DOMAIN-1)
	      X))
|#

;; We therefore need the lemma SUBST-APPLY-TO-SUBST-ELIMINATOR below
;; (which is used under the substitution where S gets (CO-RESTRICT S
;; DOMAIN-1) and SG gets (NULLIFY-SUBST SG)).  However, we'll
;; immediately derive the desired consequence and then disable this
;; lemma, since it appears that it would loop with
;; COMPOSE-PROPERTY-REVERSED.

;; << 55 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  subst-apply-to-subst-eliminator \\ \index{subst-apply-to-subst-eliminator}
\=\+(\=\+{\rm{variable-listp}}\,({\rm{domain}}\,({\it{sg\/}})\index{domain})\index{variable-listp} \\ 
$\wedge$$\;\;\;\;${\rm{variable-listp}}\,({\rm{domain}}\,({\it{s\/}})\index{domain})\index{variable-listp} \\ 
$\wedge$$\;\;\;\;${\rm{termp}}\,({\bf{t}}, {\it{x\/}})\index{termp} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{domain}}\,({\it{sg\/}})\index{domain}, {\rm{all-vars}}\,({\bf{t}}, {\it{x\/}})\index{all-vars})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{subst}}\,({\bf{t}}, {\rm{apply-to-subst}}\,({\it{sg\/}}, {\it{s\/}})\index{apply-to-subst}, {\it{x\/}})\index{subst} $=$ {\rm{subst}}\,({\bf{t}}, {\it{sg\/}}, {\rm{subst}}\,({\bf{t}}, {\it{s\/}}, {\it{x\/}})\index{subst})\index{subst})\-
\end{tabbing}

\begin{verbatim};; << 56 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  theorem-subst-apply-to-subst-with-disjoint-domain \\ \index{theorem-subst-apply-to-subst-wit!h-disjoint-domain}
\=\+(\=\+{\rm{var-substp}}\,({\it{sg\/}})\index{var-substp} \\ 
$\wedge$$\;\;\;\;${\rm{var-substp}}\,({\it{s\/}})\index{var-substp} \\ 
$\wedge$$\;\;\;\;${\rm{termp}}\,({\bf{t}}, {\it{x\/}})\index{termp} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{domain}}\,({\it{sg\/}})\index{domain}, {\rm{all-vars}}\,({\bf{t}}, {\it{x\/}})\index{all-vars})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{theorem}}\,({\rm{subst}}\,({\bf{t}}, {\it{s\/}}, {\it{x\/}})\index{subst})\index{theorem})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{theorem}}\,({\rm{subst}}\,({\bf{t}}, {\rm{apply-to-subst}}\,({\it{sg\/}}, {\it{s\/}})\index{apply-to-subst}, {\it{x\/}})\index{subst})\index{theorem}\-
\end{tabbing}

\begin{verbatim};; << 57 >>
\end{verbatim}
\noindent{\sc Event}:   Disable subst-apply-to-subst-eliminator.

\addvspace{18pt}

\begin{verbatim};; The proof of the remaining goal should go through now, one might
;; think.  However, we need one more observation first, because we
;; need to apply the following lemma.

#|
(PROVE-LEMMA SUBST-CO-RESTRICT
             (REWRITE)
             (IMPLIES (AND (DISJOINT X
                                     (INTERSECTION (DOMAIN S)
                                                   (ALL-VARS FLG TERM)))
                           (VARIABLE-LISTP (DOMAIN S))
                           (TERMP FLG TERM))
                      (EQUAL (SUBST FLG (CO-RESTRICT S X) TERM)
                             (SUBST FLG S TERM))))
|#

;; but the first hypothesis of this lemma needs special handling because of
;; free variables.  The lemma DISJOINT-SUBSETP-HACK was proved at this point,
;; and appears now in sets.events.

;; And finally, we finish.  During polishing I suddenly needed the
;; lemma SUBSETP-INTERSECTION-MONOTONE-2, which is now included in
;; "sets.events", and which in turn suggested
;; SUBSETP-INTERSECTION-COMMUTER there.

;; << 58 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-6-rest-generalization \\ \index{main-hyps-relieved-6-rest-gener!alization}
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{restrict}, \\ 
{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{apply-to-subst}}\,({\rm{nullify-subst}}\,({\it{sg\/}})\index{nullify-subst}, {\rm{co-restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{co-restrict})\index{apply-to-subst}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{var-substp}}\,({\it{sg\/}})\index{var-substp} \\ 
$\wedge$$\;\;\;\;${\rm{var-substp}}\,({\it{s\/}})\index{var-substp} \\ 
$\wedge$$\;\;\;\;${\rm{subsetp}}\,({\rm{domain}}\,({\it{s\/}})\index{domain}, {\it{new-free\/}})\index{subsetp} \\ 
$\wedge$$\;\;\;\;${\rm{termp}}\,({\bf{f}}, {\it{p\/}})\index{termp} \\ 
$\wedge$$\;\;\;\;${\rm{theorem-list}}\,({\rm{subst}}\,({\bf{f}}, {\it{s\/}}, {\it{p\/}})\index{subst})\index{theorem-list} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,(\=\+{\rm{domain}}\,({\it{sg\/}})\index{domain}, \\ 
{\rm{all-vars}}\,(\=\+{\bf{f}}, \\ 
{\rm{goals-disjoint-from-vars}}\,(\=\+{\it{p\/}}, \\ 
{\it{new-free\/}}, \\ 
{\it{domain-1\/}})\-\index{goals-disjoint-from-vars})\-\index{all-vars})\-\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{all-vars-disjoint-or-subsetp}}\,({\it{p\/}}, {\it{new-free\/}}, {\it{domain-1\/}})\index{all-vars-disjoint-or-subsetp})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{theorem-list}}\,({\rm{subst}}\,({\bf{f}}, {\rm{append}}\,({\it{s1\/}}, {\it{s2\/}}), {\it{p\/}})\index{subst})\index{theorem-list}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; Now to clean up the goals that have been pushed above:

;; << 59 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-6-rest \\ \index{main-hyps-relieved-6-rest}
\=\+{\bf let }\=\+{\it{g\/}}{\bf $\;$ be$\;\;$}{\rm{caar}}\,({\it{state\/}}), \\ 
{\it{p\/}}{\bf $\;$ be$\;\;$}{\rm{cdar}}\,({\it{state\/}}), \\ 
{\it{free\/}}{\bf $\;$ be$\;\;$}{\rm{cdr}}\,({\it{state\/}}), \\ 
{\it{s\/}}{\bf $\;$ be$\;\;$}{\rm{witnessing-instantiation}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{witnessing-instantiation}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{new-g\/}}{\bf $\;$ be$\;\;$}{\rm{subst}}\,({\bf{t}}, {\rm{invert}}\,({\it{sg\/}})\index{invert}, {\it{g\/}})\index{subst}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{domain-1\/}}{\bf $\;$ be$\;\;$}{\rm{gen-closure}}\,(\=\+{\rm{cons}}\,({\it{new-g\/}}, {\it{p\/}}), \\ 
{\it{free\/}}, \\ 
{\rm{all-vars}}\,({\bf{t}}, {\it{new-g\/}})\index{all-vars})\-\index{gen-closure}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{restrict}, \\ 
{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{apply-to-subst}}\,(\=\+{\rm{nullify-subst}}\,({\it{sg\/}})\index{nullify-subst}, \\ 
{\rm{co-restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{co-restrict})\-\index{apply-to-subst}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} \\ 
$\wedge$$\;\;\;\;${\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{theorem-list}}\,({\rm{subst}}\,({\bf{f}}, {\rm{append}}\,({\it{s1\/}}, {\it{s2\/}}), {\it{p\/}})\index{subst})\index{theorem-list}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; << 60 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-6 \\ \index{main-hyps-relieved-6}
\=\+({\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} $\wedge$ {\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state}) \\ 
$\rightarrow$$\;\;\;\;${\rm{theorem-list}}\,({\rm{subst}}\,(\=\+{\bf{f}}, \\ 
{\rm{append}}\,(\=\+{\rm{restrict}}\,(\=\+{\rm{witnessing-instantiation}}\,({\rm{generalize}}\,(\=\+{\it{sg\/}}, \\ 
{\it{state\/}})\-\index{generalize})\index{witnessing-instantiation}, \\ 
{\rm{gen-closure}}\,(\=\+{\rm{cons}}\,(\=\+{\rm{subst}}\,(\=\+{\bf{t}}, \\ 
{\rm{invert}}\,({\it{sg\/}})\index{invert}, \\ 
{\rm{caar}}\,({\it{state\/}}))\-\index{subst}, \\ 
{\rm{cdar}}\,({\it{state\/}}))\-, \\ 
{\rm{cdr}}\,({\it{state\/}}), \\ 
{\rm{all-vars}}\,(\=\+{\bf{t}}, \\ 
{\rm{subst}}\,(\=\+{\bf{t}}, \\ 
{\rm{invert}}\,({\it{sg\/}})\index{invert}, \\ 
{\rm{caar}}\,({\it{state\/}}))\-\index{subst})\-\index{all-vars})\-\index{gen-closure})\-\index{restrict}, \\ 
{\rm{apply-to-subst}}\,(\=\+{\rm{nullify-subst}}\,({\it{sg\/}})\index{nullify-subst}, \\ 
{\rm{co-restrict}}\,(\=\+{\rm{witnessing-instantiation}}\,({\rm{generalize}}\,(\=\+{\it{sg\/}}, \\ 
{\it{state\/}})\-\index{generalize})\index{witnessing-instantiation}, \\ 
{\rm{gen-closure}}\,(\=\+{\rm{cons}}\,(\=\+{\rm{subst}}\,(\=\+{\bf{t}}, \\ 
{\rm{invert}}\,({\it{sg\/}})\index{invert}, \\ 
{\rm{caar}}\,({\it{state\/}}))\-\index{subst}, \\ 
{\rm{cdar}}\,({\it{state\/}}))\-, \\ 
{\rm{cdr}}\,({\it{state\/}}), \\ 
{\rm{all-vars}}\,(\=\+{\bf{t}}, \\ 
{\rm{subst}}\,(\=\+{\bf{t}}, \\ 
{\rm{invert}}\,({\it{sg\/}})\index{invert}, \\ 
{\rm{caar}}\,({\it{state\/}}))\-\index{subst})\-\index{all-vars})\-\index{gen-closure})\-\index{co-restrict})\-\index{apply-to-subst})\-, \\ 
{\rm{cons}}\,({\rm{subst}}\,({\bf{t}}, {\rm{invert}}\,({\it{sg\/}})\index{invert}, {\rm{caar}}\,({\it{state\/}}))\index{subst}, {\rm{cdar}}\,({\it{state\/}})))\-\index{subst})\index{theorem-list}\-
\end{tabbing}

\begin{verbatim};; << 61 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved \\ \index{main-hyps-relieved}
\=\+({\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} $\wedge$ {\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state}) \\ 
$\rightarrow$$\;\;\;\;${\rm{main-hyps}}\,(\=\+{\rm{restrict}}\,(\=\+{\rm{witnessing-instantiation}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{witnessing-instantiation}, \\ 
{\rm{gen-closure}}\,(\=\+{\rm{cons}}\,(\=\+{\rm{subst}}\,({\bf{t}}, {\rm{invert}}\,({\it{sg\/}})\index{invert}, {\rm{caar}}\,({\it{state\/}}))\index{subst}, \\ 
{\rm{cdar}}\,({\it{state\/}}))\-, \\ 
{\rm{cdr}}\,({\it{state\/}}), \\ 
{\rm{all-vars}}\,(\=\+{\bf{t}}, \\ 
{\rm{subst}}\,(\=\+{\bf{t}}, \\ 
{\rm{invert}}\,({\it{sg\/}})\index{invert}, \\ 
{\rm{caar}}\,({\it{state\/}}))\-\index{subst})\-\index{all-vars})\-\index{gen-closure})\-\index{restrict}, \\ 
{\rm{apply-to-subst}}\,(\=\+{\rm{nullify-subst}}\,({\it{sg\/}})\index{nullify-subst}, \\ 
{\rm{co-restrict}}\,(\=\+{\rm{witnessing-instantiation}}\,({\rm{generalize}}\,(\=\+{\it{sg\/}}, \\ 
{\it{state\/}})\-\index{generalize})\index{witnessing-instantiation}, \\ 
{\rm{gen-closure}}\,(\=\+{\rm{cons}}\,(\=\+{\rm{subst}}\,(\=\+{\bf{t}}, \\ 
{\rm{invert}}\,({\it{sg\/}})\index{invert}, \\ 
{\rm{caar}}\,({\it{state\/}}))\-\index{subst}, \\ 
{\rm{cdar}}\,({\it{state\/}}))\-, \\ 
{\rm{cdr}}\,({\it{state\/}}), \\ 
{\rm{all-vars}}\,(\=\+{\bf{t}}, \\ 
{\rm{subst}}\,(\=\+{\bf{t}}, \\ 
{\rm{invert}}\,({\it{sg\/}})\index{invert}, \\ 
{\rm{caar}}\,({\it{state\/}}))\-\index{subst})\-\index{all-vars})\-\index{gen-closure})\-\index{co-restrict})\-\index{apply-to-subst}, \\ 
{\it{sg\/}}, \\ 
{\rm{caar}}\,({\it{state\/}}), \\ 
{\rm{cdar}}\,({\it{state\/}}))\-\index{main-hyps}\-
\end{tabbing}

\begin{verbatim};; << 62 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-theorem-1-case-4 \\ \index{main-theorem-1-case-4}
\=\+({\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} $\wedge$ {\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state}) \\ 
$\rightarrow$$\;\;\;\;${\rm{theorem-list}}\,({\rm{subst}}\,({\bf{f}}, {\rm{gen-inst}}\,({\it{sg\/}}, {\it{state\/}})\index{gen-inst}, {\rm{car}}\,({\it{state\/}}))\index{subst})\index{theorem-list}\-
\end{tabbing}

\begin{verbatim};; << 63 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-theorem-1 \\ \index{main-theorem-1}
\=\+{\bf let }\=\+{\it{wit\/}}{\bf $\;$ be$\;\;$}{\rm{gen-inst}}\,({\it{sg\/}}, {\it{state\/}})\index{gen-inst}\- \\ 
{\bf in} \\ 
\=\+({\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} $\wedge$ {\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{statep}}\,({\it{state\/}})\index{statep} \\ 
$\wedge$$\;\;\;\;${\rm{var-substp}}\,({\it{wit\/}})\index{var-substp} \\ 
$\wedge$$\;\;\;\;${\rm{subsetp}}\,({\rm{domain}}\,({\it{wit\/}})\index{domain}, {\rm{cdr}}\,({\it{state\/}}))\index{subsetp} \\ 
$\wedge$$\;\;\;\;${\rm{theorem-list}}\,({\rm{subst}}\,({\bf{f}}, {\it{wit\/}}, {\rm{car}}\,({\it{state\/}}))\index{subst})\index{theorem-list})\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; << 64 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  generalize-is-correct \\ \index{generalize-is-correct}
\=\+({\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} $\wedge$ {\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state}) \\ 
$\rightarrow$$\;\;\;\;${\rm{valid-state}}\,({\it{state\/}})\index{valid-state}\-
\end{tabbing}


\noindent{\sc Event}:   Make the library {\tt{"generalize"}}.

\addvspace{18pt}

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