\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[]


\noindent{\sc Event}:   Start with the initial {\bf nqthm} theory.

\addvspace{18pt}

\begin{verbatim};;; The proof in here is based on the hint to exercise (8) on
;;; page 43 of Kunen's Set Theory book.

;; Imagine sets a and b and corresponding functions fa and fb which
;; map a to b and vice-versa, where both are one-one.

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

\begin{tabbing}{\sc Conservative Axiom}:  fa-and-fb-are-one-one \\ \index{fa-and-fb-are-one-one}
\=\+(({\rm{a}}\,({\it{x\/}})\index{a} $\wedge$ {\rm{a}}\,({\it{y\/}})\index{a} $\wedge$ ({\it{x\/}} $\not=$ {\it{y\/}})) $\rightarrow$ ({\rm{fa}}\,({\it{x\/}})\index{fa} $\not=$ {\rm{fa}}\,({\it{y\/}})\index{fa})) \\ 
$\wedge$$\;\;\;\;$(({\rm{b}}\,({\it{x\/}})\index{b} $\wedge$ {\rm{b}}\,({\it{y\/}})\index{b} $\wedge$ ({\it{x\/}} $\not=$ {\it{y\/}})) $\rightarrow$ ({\rm{fb}}\,({\it{x\/}})\index{fb} $\not=$ {\rm{fb}}\,({\it{y\/}})\index{fb})) \\ 
$\wedge$$\;\;\;\;$({\rm{a}}\,({\it{x\/}})\index{a} $\rightarrow$ {\rm{b}}\,({\rm{fa}}\,({\it{x\/}})\index{fa})\index{b}) \\ 
$\wedge$$\;\;\;\;$({\rm{b}}\,({\it{x\/}})\index{b} $\rightarrow$ {\rm{a}}\,({\rm{fb}}\,({\it{x\/}})\index{fb})\index{a}) \\ 
$\wedge$$\;\;\;\;$({\rm{truep}}\,({\rm{a}}\,({\it{x\/}})\index{a}) $\vee$ {\rm{falsep}}\,({\rm{a}}\,({\it{x\/}})\index{a})) \\ 
$\wedge$$\;\;\;\;$({\rm{truep}}\,({\rm{b}}\,({\it{x\/}})\index{b}) $\vee$ {\rm{falsep}}\,({\rm{b}}\,({\it{x\/}})\index{b}))\-
\end{tabbing}\noindent Simultaneously, we introduce the new function symbols {\it fa\/}, {\it fb\/}, {\it a\/}, and {\it b\/}.
 
\begin{tabbing}{\sc Definition}:\index{in-fa-range} \\  
{\rm{in-fa-range}}\,({\it{x\/}})\index{in-fa-range} $\leftrightarrow$ $\exists\;${\it{fa-1\/}}$\;$({\rm{a}}\,({\it{fa-1\/}})\index{a} $\wedge$ ({\rm{fa}}\,({\it{fa-1\/}})\index{fa} $=$ {\it{x\/}}))\index{exists}
\end{tabbing}

\begin{verbatim};; The following 3 events were generated automatically to help with
;; the proof-checker's application of the macro command SK*.

\end{verbatim}
\noindent{\sc Event}:   Disable in-fa-range.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  in-fa-range-suff \\ \index{in-fa-range-suff}
({\rm{a}}\,({\it{fa-1\/}})\index{a} $\wedge$ ({\rm{fa}}\,({\it{fa-1\/}})\index{fa} $=$ {\it{x\/}})) $\rightarrow$ {\rm{in-fa-range}}\,({\it{x\/}})\index{in-fa-range}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  in-fa-range-necc \\ \index{in-fa-range-necc}
($\neg$ ({\rm{a}}\,({\rm{fa-1}}\,({\it{x\/}})\index{fa-1})\index{a} $\wedge$ ({\rm{fa}}\,({\rm{fa-1}}\,({\it{x\/}})\index{fa-1})\index{fa} $=$ {\it{x\/}}))) $\rightarrow$ ($\neg$ {\rm{in-fa-range}}\,({\it{x\/}})\index{in-fa-range})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{in-fb-range} \\  
{\rm{in-fb-range}}\,({\it{x\/}})\index{in-fb-range} $\leftrightarrow$ $\exists\;${\it{fb-1\/}}$\;$({\rm{b}}\,({\it{fb-1\/}})\index{b} $\wedge$ ({\rm{fb}}\,({\it{fb-1\/}})\index{fb} $=$ {\it{x\/}}))\index{exists}
\end{tabbing}

\begin{verbatim};; The following 3 events were generated automatically to help with
;; the proof-checker's application of the macro command sk*.

\end{verbatim}
\noindent{\sc Event}:   Disable in-fb-range.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  in-fb-range-suff \\ \index{in-fb-range-suff}
({\rm{b}}\,({\it{fb-1\/}})\index{b} $\wedge$ ({\rm{fb}}\,({\it{fb-1\/}})\index{fb} $=$ {\it{x\/}})) $\rightarrow$ {\rm{in-fb-range}}\,({\it{x\/}})\index{in-fb-range}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  in-fb-range-necc \\ \index{in-fb-range-necc}
($\neg$ ({\rm{b}}\,({\rm{fb-1}}\,({\it{x\/}})\index{fb-1})\index{b} $\wedge$ ({\rm{fb}}\,({\rm{fb-1}}\,({\it{x\/}})\index{fb-1})\index{fb} $=$ {\it{x\/}}))) $\rightarrow$ ($\neg$ {\rm{in-fb-range}}\,({\it{x\/}})\index{in-fb-range})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{circled} \\  
\=\+{\rm{circled}}\,({\it{flg\/}}, {\it{x\/}}, {\it{n\/}})\index{circled} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{flg\/}} $=$ {\tt{'}}{\tt{a}} \\ 
{\bf then }\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{a}}\,({\it{x\/}})\index{a} \\ 
{\bf else }{\rm{in-fb-range}}\,({\it{x\/}})\index{in-fb-range} $\wedge$ {\rm{circled}}\,({\tt{'}}{\tt{b}}, {\rm{fb-1}}\,({\it{x\/}})\index{fb-1}, {\it{n\/}} $-\;1$)\index{circled}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{b}}\,({\it{x\/}})\index{b} \\ 
{\bf else }{\rm{in-fa-range}}\,({\it{x\/}})\index{in-fa-range} $\wedge$ {\rm{circled}}\,({\tt{'}}{\tt{a}}, {\rm{fa-1}}\,({\it{x\/}})\index{fa-1}, {\it{n\/}} $-\;1$)\index{circled}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{a-core} \\  
\=\+{\rm{a-core}}\,({\it{x\/}})\index{a-core} \\ 
$\leftrightarrow$$\;\;\;\;$(\=\+{\rm{a}}\,({\it{x\/}})\index{a} \\ 
$\wedge$$\;\;\;\;$$\forall\;${\it{a-level\/}}$\;$(\=\+(({\it{a-level\/}} $\in\;${\bf{N}}${}$) $\wedge$ {\rm{circled}}\,({\tt{'}}{\tt{a}}, {\it{x\/}}, {\it{a-level\/}})\index{circled}) \\ 
$\rightarrow$$\;\;\;\;${\rm{circled}}\,({\tt{'}}{\tt{a}}, {\it{x\/}}, $1\;+$ {\it{a-level\/}})\index{circled})\-\index{forall})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable a-core.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  a-core-necc-base \\ \index{a-core-necc-base}
(({\it{n\/}} $\simeq {\tt{0}}$) $\wedge$ {\rm{a-core}}\,({\it{x\/}})\index{a-core}) $\rightarrow$ {\rm{circled}}\,({\tt{'}}{\tt{a}}, {\it{x\/}}, {\it{n\/}})\index{circled}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a-core-necc-induction \\ \index{a-core-necc-induction}
(({\it{n\/}} $\not\simeq {\tt{0}}$) $\wedge$ {\rm{a-core}}\,({\it{x\/}})\index{a-core} $\wedge$ {\rm{circled}}\,({\tt{'}}{\tt{a}}, {\it{x\/}}, {\it{n\/}} $-\;1$)\index{circled}) $\rightarrow$ {\rm{circled}}\,({\tt{'}}{\tt{a}}, {\it{x\/}}, {\it{n\/}})\index{circled}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a-core-necc \\ \index{a-core-necc}
($\neg$ {\rm{circled}}\,({\tt{'}}{\tt{a}}, {\it{x\/}}, {\it{n\/}})\index{circled}) $\rightarrow$ ($\neg$ {\rm{a-core}}\,({\it{x\/}})\index{a-core})
\end{tabbing}


\noindent{\sc Event}:   Disable a-core-necc-base.

\addvspace{18pt}

\noindent{\sc Event}:   Disable a-core-necc-induction.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  a-core-suff \\ \index{a-core-suff}
\=\+(\=\+{\rm{a}}\,({\it{x\/}})\index{a} \\ 
$\wedge$$\;\;\;\;$(\=\+(({\rm{a-level}}\,({\it{x\/}})\index{a-level} $\in\;${\bf{N}}${}$) $\wedge$ {\rm{circled}}\,({\tt{'}}{\tt{a}}, {\it{x\/}}, {\rm{a-level}}\,({\it{x\/}})\index{a-level})\index{circled}) \\ 
$\rightarrow$$\;\;\;\;${\rm{circled}}\,({\tt{'}}{\tt{a}}, {\it{x\/}}, $1\;+$ {\rm{a-level}}\,({\it{x\/}})\index{a-level})\index{circled})\-)\- \\ 
$\rightarrow$$\;\;\;\;${\rm{a-core}}\,({\it{x\/}})\index{a-core}\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{b-core} \\  
\=\+{\rm{b-core}}\,({\it{x\/}})\index{b-core} \\ 
$\leftrightarrow$$\;\;\;\;$(\=\+{\rm{b}}\,({\it{x\/}})\index{b} \\ 
$\wedge$$\;\;\;\;$$\forall\;${\it{b-level\/}}$\;$(\=\+(({\it{b-level\/}} $\in\;${\bf{N}}${}$) $\wedge$ {\rm{circled}}\,({\tt{'}}{\tt{b}}, {\it{x\/}}, {\it{b-level\/}})\index{circled}) \\ 
$\rightarrow$$\;\;\;\;${\rm{circled}}\,({\tt{'}}{\tt{b}}, {\it{x\/}}, $1\;+$ {\it{b-level\/}})\index{circled})\-\index{forall})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable b-core.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  b-core-necc-base \\ \index{b-core-necc-base}
(({\it{n\/}} $\simeq {\tt{0}}$) $\wedge$ {\rm{b-core}}\,({\it{x\/}})\index{b-core}) $\rightarrow$ {\rm{circled}}\,({\tt{'}}{\tt{b}}, {\it{x\/}}, {\it{n\/}})\index{circled}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  b-core-necc-induction \\ \index{b-core-necc-induction}
(({\it{n\/}} $\not\simeq {\tt{0}}$) $\wedge$ {\rm{b-core}}\,({\it{x\/}})\index{b-core} $\wedge$ {\rm{circled}}\,({\tt{'}}{\tt{b}}, {\it{x\/}}, {\it{n\/}} $-\;1$)\index{circled}) $\rightarrow$ {\rm{circled}}\,({\tt{'}}{\tt{b}}, {\it{x\/}}, {\it{n\/}})\index{circled}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  b-core-necc \\ \index{b-core-necc}
($\neg$ {\rm{circled}}\,({\tt{'}}{\tt{b}}, {\it{x\/}}, {\it{n\/}})\index{circled}) $\rightarrow$ ($\neg$ {\rm{b-core}}\,({\it{x\/}})\index{b-core})
\end{tabbing}


\noindent{\sc Event}:   Disable b-core-necc-base.

\addvspace{18pt}

\noindent{\sc Event}:   Disable b-core-necc-induction.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  b-core-suff \\ \index{b-core-suff}
\=\+(\=\+{\rm{b}}\,({\it{x\/}})\index{b} \\ 
$\wedge$$\;\;\;\;$(\=\+(({\rm{b-level}}\,({\it{x\/}})\index{b-level} $\in\;${\bf{N}}${}$) $\wedge$ {\rm{circled}}\,({\tt{'}}{\tt{b}}, {\it{x\/}}, {\rm{b-level}}\,({\it{x\/}})\index{b-level})\index{circled}) \\ 
$\rightarrow$$\;\;\;\;${\rm{circled}}\,({\tt{'}}{\tt{b}}, {\it{x\/}}, $1\;+$ {\rm{b-level}}\,({\it{x\/}})\index{b-level})\index{circled})\-)\- \\ 
$\rightarrow$$\;\;\;\;${\rm{b-core}}\,({\it{x\/}})\index{b-core}\-
\end{tabbing}

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

\begin{tabbing}{\sc Definition}:\index{j} \\  
\=\+{\rm{j}}\,({\it{x\/}})\index{j} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{a-core}}\,({\it{x\/}})\index{a-core} $\vee$ {\rm{parity}}\,({\rm{a-level}}\,({\it{x\/}})\index{a-level})\index{parity}$\;\;${\bf then }{\rm{fa}}\,({\it{x\/}})\index{fa} \\ 
{\bf else }{\rm{fb-1}}\,({\it{x\/}})\index{fb-1}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{j-1} \\  
\=\+{\rm{j-1}}\,({\it{y\/}})\index{j-1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{b-core}}\,({\it{y\/}})\index{b-core} $\vee$ ($\neg$ {\rm{parity}}\,({\rm{b-level}}\,({\it{y\/}})\index{b-level})\index{parity})$\;\;${\bf then }{\rm{fa-1}}\,({\it{y\/}})\index{fa-1} \\ 
{\bf else }{\rm{fb}}\,({\it{y\/}})\index{fb}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; Our goals:
;(prove-lemma j-1-j (rewrite)
;  (implies (a x)
;           (equal (j-1 (j x)) x)))

;(prove-lemma j-j-1 (rewrite)
;  (implies (b y)
;           (equal (j (j-1 y)) y)))

;; We'll start on the first of these.  The theorem-prover output
;; suggests the following lemma:

;(prove-lemma b-core-fa (rewrite)
;  (implies (a x)
;           (iff (b-core (fa x))
;                (a-core x))))

;; A main lemma is that (a-core x) => (b-core (fa x)) for x in a.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  fa-1-inverts-fa \\ \index{fa-1-inverts-fa}
{\rm{a}}\,({\it{x\/}})\index{a} $\rightarrow$ ({\rm{fa-1}}\,({\rm{fa}}\,({\it{x\/}})\index{fa})\index{fa-1} $=$ {\it{x\/}})
\end{tabbing}

\begin{verbatim};; The following is useful for proof-checker rewriting:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  in-fa-range-fa \\ \index{in-fa-range-fa}
{\rm{a}}\,({\it{x\/}})\index{a} $\rightarrow$ {\rm{in-fa-range}}\,({\rm{fa}}\,({\it{x\/}})\index{fa})\index{in-fa-range}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  b-core-fa \\ \index{b-core-fa}
{\rm{a}}\,({\it{x\/}})\index{a} $\rightarrow$ ({\rm{b-core}}\,({\rm{fa}}\,({\it{x\/}})\index{fa})\index{b-core} $\leftrightarrow$ {\rm{a-core}}\,({\it{x\/}})\index{a-core})
\end{tabbing}

\begin{verbatim};; On to Case 2 of j-1-j.  We find there the following contradictory hyps:

;(AND (A X)
;     (PARITY (A-LEVEL X))
;     (NOT (A-CORE X))
;     (PARITY (B-LEVEL (FA X))))

;; We want to prove:

;; B-LEVEL-FA

;(IMPLIES (AND (A X) (NOT (A-CORE X)))
;         (EQUAL (B-LEVEL (FA X))
;                (ADD1 (A-LEVEL X))))

\end{verbatim}\begin{tabbing}{\sc Theorem}:  b-fa-equality-rewrite \\ \index{b-fa-equality-rewrite}
({\rm{a}}\,({\it{x\/}})\index{a} $\wedge$ ($\neg$ {\rm{b}}\,({\it{y\/}})\index{b})) $\rightarrow$ ({\rm{fa}}\,({\it{x\/}})\index{fa} $\not=$ {\it{y\/}})
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  fa-range-contained-in-b \\ \index{fa-range-contained-in-b}
($\neg$ {\rm{b}}\,({\it{y\/}})\index{b}) $\rightarrow$ ($\neg$ {\rm{in-fa-range}}\,({\it{y\/}})\index{in-fa-range})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  circled-implies-b \\ \index{circled-implies-b}
{\rm{circled}}\,({\tt{'}}{\tt{b}}, {\it{y\/}}, {\it{n\/}})\index{circled} $\rightarrow$ {\rm{b}}\,({\it{y\/}})\index{b}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a-fb-equality-rewrite \\ \index{a-fb-equality-rewrite}
({\rm{b}}\,({\it{y\/}})\index{b} $\wedge$ ($\neg$ {\rm{a}}\,({\it{x\/}})\index{a})) $\rightarrow$ ({\rm{fb}}\,({\it{y\/}})\index{fb} $\not=$ {\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  fb-range-contained-in-a \\ \index{fb-range-contained-in-a}
($\neg$ {\rm{a}}\,({\it{x\/}})\index{a}) $\rightarrow$ ($\neg$ {\rm{in-fb-range}}\,({\it{x\/}})\index{in-fb-range})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  circled-implies-a \\ \index{circled-implies-a}
{\rm{circled}}\,({\tt{'}}{\tt{a}}, {\it{y\/}}, {\it{n\/}})\index{circled} $\rightarrow$ {\rm{a}}\,({\it{y\/}})\index{a}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  circled-monotone \\ \index{circled-monotone}
({\rm{circled}}\,({\it{flg\/}}, {\it{x\/}}, {\it{j\/}})\index{circled} $\wedge$ ({\it{j\/}} $\not<$ {\it{i\/}})) $\rightarrow$ {\rm{circled}}\,({\it{flg\/}}, {\it{x\/}}, {\it{i\/}})\index{circled}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  circled-b-fa \\ \index{circled-b-fa}
{\rm{a}}\,({\it{x\/}})\index{a} $\rightarrow$ ({\rm{circled}}\,({\tt{'}}{\tt{b}}, {\rm{fa}}\,({\it{x\/}})\index{fa}, {\it{n\/}})\index{circled} $=$ {\rm{circled}}\,({\tt{'}}{\tt{a}}, {\it{x\/}}, {\it{n\/}} $-\;1$)\index{circled})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  b-level-fa-hack-lemma \\ \index{b-level-fa-hack-lemma}
\=\+({\rm{b-level}}\,({\rm{fa}}\,({\it{x\/}})\index{fa})\index{b-level} $\in\;${\bf{N}}${}$) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{b-level}}\,({\rm{fa}}\,({\it{x\/}})\index{fa})\index{b-level} $=$ ($1\;+$ {\rm{a-level}}\,({\it{x\/}})\index{a-level})) \\ 
$=$$\;\;\;\;$($\neg$ (\=\+({\rm{b-level}}\,({\rm{fa}}\,({\it{x\/}})\index{fa})\index{b-level} $<$ ($1\;+$ {\rm{a-level}}\,({\it{x\/}})\index{a-level})) \\ 
$\vee$$\;\;\;\;$(($1\;+$ {\rm{a-level}}\,({\it{x\/}})\index{a-level}) $<$ {\rm{b-level}}\,({\rm{fa}}\,({\it{x\/}})\index{fa})\index{b-level}))\-))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  b-level-fa \\ \index{b-level-fa}
({\rm{a}}\,({\it{x\/}})\index{a} $\wedge$ ($\neg$ {\rm{a-core}}\,({\it{x\/}})\index{a-core})) $\rightarrow$ ({\rm{b-level}}\,({\rm{fa}}\,({\it{x\/}})\index{fa})\index{b-level} $=$ ($1\;+$ {\rm{a-level}}\,({\it{x\/}})\index{a-level}))
\end{tabbing}
       

\begin{verbatim};; On to Case 3 of j-1-j.  Our first subgoal is:

;(IMPLIES (AND (A X)
;              (NOT (A-CORE X))
;              (NOT (PARITY (A-LEVEL X)))
;              (NOT (B-CORE (FB-1 X)))
;              (PARITY (B-LEVEL (FB-1 X))))
;         (EQUAL (FB (FB-1 X)) X))

;; and this follows from the following two lemmas.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  not-parity-a-level-implies-in-fb-range \\ \index{not-parity-a-level-implies-in-f!b-range}
({\rm{a}}\,({\it{x\/}})\index{a} $\wedge$ ($\neg$ {\rm{parity}}\,({\rm{a-level}}\,({\it{x\/}})\index{a-level})\index{parity})) $\rightarrow$ {\rm{in-fb-range}}\,({\it{x\/}})\index{in-fb-range}
\end{tabbing}

\begin{verbatim};; The next subcase of j-1-j is:

;(implies (and (a x)
;              (not (a-core x))
;              (not (parity (a-level x)))
;              (not (parity (b-level (fb-1 x)))))
;         (equal (fa-1 (fb-1 x)) x))

;; and this follows from:

;(prove-lemma b-level-fb-1 (rewrite)
;  (implies (and (a x)
;                (not (a-core x))
;                (in-fb-range x))
;           (equal (b-level (fb-1 x))
;                  (sub1 (a-level x)))))

;; I've proved nearly the analogous thing already for fa.  Let's prove that
;; one for fb and then deduce this from it.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  fb-1-inverts-fb \\ \index{fb-1-inverts-fb}
{\rm{b}}\,({\it{x\/}})\index{b} $\rightarrow$ ({\rm{fb-1}}\,({\rm{fb}}\,({\it{x\/}})\index{fb})\index{fb-1} $=$ {\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  in-fb-range-fb \\ \index{in-fb-range-fb}
{\rm{b}}\,({\it{x\/}})\index{b} $\rightarrow$ {\rm{in-fb-range}}\,({\rm{fb}}\,({\it{x\/}})\index{fb})\index{in-fb-range}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  circled-a-fb \\ \index{circled-a-fb}
{\rm{b}}\,({\it{x\/}})\index{b} $\rightarrow$ ({\rm{circled}}\,({\tt{'}}{\tt{a}}, {\rm{fb}}\,({\it{x\/}})\index{fb}, {\it{n\/}})\index{circled} $=$ {\rm{circled}}\,({\tt{'}}{\tt{b}}, {\it{x\/}}, {\it{n\/}} $-\;1$)\index{circled})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a-level-fb-hack-lemma \\ \index{a-level-fb-hack-lemma}
\=\+({\rm{a-level}}\,({\rm{fb}}\,({\it{x\/}})\index{fb})\index{a-level} $\in\;${\bf{N}}${}$) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{a-level}}\,({\rm{fb}}\,({\it{x\/}})\index{fb})\index{a-level} $=$ ($1\;+$ {\rm{b-level}}\,({\it{x\/}})\index{b-level})) \\ 
$=$$\;\;\;\;$($\neg$ (\=\+({\rm{a-level}}\,({\rm{fb}}\,({\it{x\/}})\index{fb})\index{a-level} $<$ ($1\;+$ {\rm{b-level}}\,({\it{x\/}})\index{b-level})) \\ 
$\vee$$\;\;\;\;$(($1\;+$ {\rm{b-level}}\,({\it{x\/}})\index{b-level}) $<$ {\rm{a-level}}\,({\rm{fb}}\,({\it{x\/}})\index{fb})\index{a-level}))\-))\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  a-core-fb \\ \index{a-core-fb}
{\rm{b}}\,({\it{x\/}})\index{b} $\rightarrow$ ({\rm{a-core}}\,({\rm{fb}}\,({\it{x\/}})\index{fb})\index{a-core} $\leftrightarrow$ {\rm{b-core}}\,({\it{x\/}})\index{b-core})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a-level-fb \\ \index{a-level-fb}
({\rm{b}}\,({\it{x\/}})\index{b} $\wedge$ ($\neg$ {\rm{b-core}}\,({\it{x\/}})\index{b-core})) $\rightarrow$ ({\rm{a-level}}\,({\rm{fb}}\,({\it{x\/}})\index{fb})\index{a-level} $=$ ($1\;+$ {\rm{b-level}}\,({\it{x\/}})\index{b-level}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  b-level-fb-1 \\ \index{b-level-fb-1}
\=\+({\rm{a}}\,({\it{x\/}})\index{a} $\wedge$ ($\neg$ {\rm{a-core}}\,({\it{x\/}})\index{a-core}) $\wedge$ {\rm{in-fb-range}}\,({\it{x\/}})\index{in-fb-range}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{b-level}}\,({\rm{fb-1}}\,({\it{x\/}})\index{fb-1})\index{b-level} $=$ ({\rm{a-level}}\,({\it{x\/}})\index{a-level} $-\;1$))\-
\end{tabbing}

\begin{verbatim};; It remains only to prove the following subcase, and then we're done with j-1-j:

;(implies (and (a x)
;              (not (a-core x))
;              (not (parity (a-level x)))
;              (b-core (fb-1 x)))
;         (equal (fa-1 (fb-1 x)) x))

;; I've already proved a-core-fb, and this should be useful.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  b-core-implies-b \\ \index{b-core-implies-b}
{\rm{b-core}}\,({\it{x\/}})\index{b-core} $\rightarrow$ {\rm{b}}\,({\it{x\/}})\index{b}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  fb-fb-1 \\ \index{fb-fb-1}
({\rm{a}}\,({\it{x\/}})\index{a} $\wedge$ {\rm{in-fb-range}}\,({\it{x\/}})\index{in-fb-range}) $\rightarrow$ ({\rm{fb}}\,({\rm{fb-1}}\,({\it{x\/}})\index{fb-1})\index{fb} $=$ {\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  b-core-fb-1 \\ \index{b-core-fb-1}
\=\+({\rm{a}}\,({\it{x\/}})\index{a} $\wedge$ ($\neg$ {\rm{a-core}}\,({\it{x\/}})\index{a-core}) $\wedge$ ($\neg$ {\rm{parity}}\,({\rm{a-level}}\,({\it{x\/}})\index{a-level})\index{parity})) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{b-core}}\,({\rm{fb-1}}\,({\it{x\/}})\index{fb-1})\index{b-core})\-
\end{tabbing}

\begin{verbatim};; Now finally for our first main goal:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  j-1-j \\ \index{j-1-j}
{\rm{a}}\,({\it{x\/}})\index{a} $\rightarrow$ ({\rm{j-1}}\,({\rm{j}}\,({\it{x\/}})\index{j})\index{j-1} $=$ {\it{x\/}})
\end{tabbing}

\begin{verbatim};;;; We're ready now for the converse.  Here's the first sticking point:

;(implies (and (b-core y)
;              (a-core (fa-1 y)))
;         (equal (fa (fa-1 y)) y))

;; We need only the following two easy lemmas:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  b-core-implies-in-fa-range \\ \index{b-core-implies-in-fa-range}
{\rm{b-core}}\,({\it{y\/}})\index{b-core} $\rightarrow$ {\rm{in-fa-range}}\,({\it{y\/}})\index{in-fa-range}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  fa-fa-1 \\ \index{fa-fa-1}
{\rm{in-fa-range}}\,({\it{y\/}})\index{in-fa-range} $\rightarrow$ ({\rm{fa}}\,({\rm{fa-1}}\,({\it{y\/}})\index{fa-1})\index{fa} $=$ {\it{y\/}})
\end{tabbing}

\begin{verbatim};; Our next goal is:

;(implies (and (b-core y)
;              (not (a-core (fa-1 y)))
;              (not (parity (a-level (fa-1 y)))))
;         (equal (fb-1 (fa-1 y)) y))

;;; which is taken care of simply by:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  a-core-fa-1 \\ \index{a-core-fa-1}
{\rm{in-fa-range}}\,({\it{y\/}})\index{in-fa-range} $\rightarrow$ ({\rm{a-core}}\,({\rm{fa-1}}\,({\it{y\/}})\index{fa-1})\index{a-core} $\leftrightarrow$ {\rm{b-core}}\,({\it{y\/}})\index{b-core})
\end{tabbing}

\begin{verbatim};; next we have to prove

;(implies (and (b y)
;              (not (parity (b-level y)))
;              (a-core (fa-1 y)))
;         (equal (fa (fa-1 y)) y))

;; which follows from fa-fa-1 together with an obvious analog of
;; NOT-PARITY-A-LEVEL-IMPLIES-IN-FB-RANGE:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  not-parity-b-level-implies-in-fa-range \\ \index{not-parity-b-level-implies-in-f!a-range}
({\rm{b}}\,({\it{y\/}})\index{b} $\wedge$ ($\neg$ {\rm{parity}}\,({\rm{b-level}}\,({\it{y\/}})\index{b-level})\index{parity})) $\rightarrow$ {\rm{in-fa-range}}\,({\it{y\/}})\index{in-fa-range}
\end{tabbing}

\begin{verbatim};; It remains only to prove:

;(implies (and (b y)
;              (not (parity (b-level y)))
;              (not (b-core y))
;              (not (parity (a-level (fa-1 y)))))
;         (equal (fb-1 (fa-1 y)) y))

;; which follows from an analogue of B-LEVEL-FB-1:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  a-level-fa-1 \\ \index{a-level-fa-1}
\=\+({\rm{b}}\,({\it{y\/}})\index{b} $\wedge$ ($\neg$ {\rm{b-core}}\,({\it{y\/}})\index{b-core}) $\wedge$ {\rm{in-fa-range}}\,({\it{y\/}})\index{in-fa-range}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{a-level}}\,({\rm{fa-1}}\,({\it{y\/}})\index{fa-1})\index{a-level} $=$ ({\rm{b-level}}\,({\it{y\/}})\index{b-level} $-\;1$))\-
\end{tabbing}

\begin{verbatim};;; and we're done!!!

\end{verbatim}\begin{tabbing}{\sc Theorem}:  j-j-1 \\ \index{j-j-1}
{\rm{b}}\,({\it{y\/}})\index{b} $\rightarrow$ ({\rm{j}}\,({\rm{j-1}}\,({\it{y\/}})\index{j-1})\index{j} $=$ {\it{y\/}})
\end{tabbing}

\begin{verbatim};; To summarize:

;; From the axiom saying that fa maps a one-one into b and fb maps b one-one into a,

;(constrain fa-and-fb-are-one-one (rewrite)
;  (and (implies (and (a x) (a y) (not (equal x y)))
;                (not (equal (fa x) (fa y))))
;       (implies (and (b x) (b y) (not (equal x y)))
;                (not (equal (fb x) (fb y))))
;       (implies (a x) (b (fa x)))
;       (implies (b x) (a (fb x)))
;       (or (truep (a x)) (falsep (a x)))
;       (or (truep (b x)) (falsep (b x))))
;  ((fa id) (fb id) (a (lambda (x) t)) (b (lambda (x) t))))

;; to finish this off we simply prove the obvious lemmas needed for
;; j-iso below.  For the first, j-range,
;; we need a lemma (as seen from observing the failed proof transcript).

\end{verbatim}\begin{tabbing}{\sc Theorem}:  in-fb-range-implies-b-fb-1 \\ \index{in-fb-range-implies-b-fb-1}
{\rm{in-fb-range}}\,({\it{y\/}})\index{in-fb-range} $\rightarrow$ {\rm{b}}\,({\rm{fb-1}}\,({\it{y\/}})\index{fb-1})\index{b}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  j-range \\ \index{j-range}
{\rm{a}}\,({\it{x\/}})\index{a} $\rightarrow$ {\rm{b}}\,({\rm{j}}\,({\it{x\/}})\index{j})\index{b}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  in-fa-range-implies-a-fa-1 \\ \index{in-fa-range-implies-a-fa-1}
{\rm{in-fa-range}}\,({\it{y\/}})\index{in-fa-range} $\rightarrow$ {\rm{a}}\,({\rm{fa-1}}\,({\it{y\/}})\index{fa-1})\index{a}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  j-1-range \\ \index{j-1-range}
{\rm{b}}\,({\it{x\/}})\index{b} $\rightarrow$ {\rm{a}}\,({\rm{j-1}}\,({\it{x\/}})\index{j-1})\index{a}
\end{tabbing}


\noindent{\sc Event}:   Disable j.

\addvspace{18pt}

\noindent{\sc Event}:   Disable j-1.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  j-is-one-one \\ \index{j-is-one-one}
({\rm{a}}\,({\it{x1\/}})\index{a} $\wedge$ {\rm{a}}\,({\it{x2\/}})\index{a} $\wedge$ ({\it{x1\/}} $\not=$ {\it{x2\/}})) $\rightarrow$ ({\rm{j}}\,({\it{x1\/}})\index{j} $\not=$ {\rm{j}}\,({\it{x2\/}})\index{j})
\end{tabbing}

\begin{verbatim};; we were able to conservatively extend the theory culminating in
;; definitions of a function j which maps a one-one into b:

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{j-iso} \\  
\=\+{\sc{j-iso}}\index{j-iso} \\ 
$\leftrightarrow$$\;\;\;\;$(\=\+$\forall\;${\it{x\/}}$\;$({\rm{a}}\,({\it{x\/}})\index{a} $\rightarrow$ {\rm{b}}\,({\rm{j}}\,({\it{x\/}})\index{j})\index{b})\index{forall} \\ 
$\wedge$$\;\;\;\;$$\forall\;${\it{x1\/}}, {\it{x2\/}}$\;$(\=\+({\rm{a}}\,({\it{x1\/}})\index{a} $\wedge$ {\rm{a}}\,({\it{x2\/}})\index{a} $\wedge$ ({\rm{j}}\,({\it{x1\/}})\index{j} $=$ {\rm{j}}\,({\it{x2\/}})\index{j})) \\ 
$\rightarrow$$\;\;\;\;$({\it{x1\/}} $=$ {\it{x2\/}}))\-\index{forall} \\ 
$\wedge$$\;\;\;\;$$\forall\;${\it{y\/}}$\;$({\rm{b}}\,({\it{y\/}})\index{b} $\rightarrow$ $\exists\;${\it{x\/}}$\;$({\rm{a}}\,({\it{x\/}})\index{a} $\wedge$ ({\rm{j}}\,({\it{x\/}})\index{j} $=$ {\it{y\/}}))\index{exists})\index{forall})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  j-is-an-isomorphism \\ \index{j-is-an-isomorphism}
{\sc{j-iso}}\index{j-iso}
\end{tabbing}


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