\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};; Koenig's tree lemma.

;; We use the formulation that says that any finitely
;; branching tree which is infinite has an infinite branch.

;; More precisely, we consider trees whose nodes are finite sequences
;; of natural numbers, such that each node's successors are a list
;; obtained by tacking on some natural number from 1 to the number of
;; successors.  For convenience, I'll keep each node as a list of
;; numbers where the root is the last element in the list.

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

\addvspace{18pt}

\begin{verbatim};; All this initial stuff is just to get the CONSTRAIN below accepted.

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

\begin{tabbing}{\sc Definition}:\index{all-ones} \\  
\=\+{\rm{all-ones}}\,({\it{s\/}})\index{all-ones} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{s\/}})$\;\;${\bf then }({\rm{car}}\,({\it{s\/}}) $=$ {\tt{1}}) $\wedge$ {\rm{all-ones}}\,({\rm{cdr}}\,({\it{s\/}}))\index{all-ones} \\ 
{\bf else }{\it{s\/}} $=$ {\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{length} \\  
\=\+{\rm{length}}\,({\it{s\/}})\index{length} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{s\/}})$\;\;${\bf then }$1\;+$ {\rm{length}}\,({\rm{cdr}}\,({\it{s\/}}))\index{length} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{subseq} \\  
\=\+{\rm{subseq}}\,({\it{s1\/}}, {\it{s2\/}})\index{subseq} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{s1\/}} $=$ {\it{s2\/}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\it{s2\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{f}} \\ 
{\bf else }{\rm{subseq}}\,({\it{s1\/}}, {\rm{cdr}}\,({\it{s2\/}}))\index{subseq}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subseq-all-ones \\ \index{subseq-all-ones}
({\rm{all-ones}}\,({\it{s1\/}})\index{all-ones} $\wedge$ {\rm{subseq}}\,({\it{s2\/}}, {\it{s1\/}})\index{subseq}) $\rightarrow$ {\rm{all-ones}}\,({\it{s2\/}})\index{all-ones}
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  plistp-all-ones \\ \index{plistp-all-ones}
{\rm{all-ones}}\,({\it{s\/}})\index{all-ones} $\rightarrow$ {\rm{plistp}}\,({\it{s\/}})\index{plistp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-ones-ones \\ \index{all-ones-ones}
{\rm{all-ones}}\,({\rm{ones}}\,({\it{n\/}})\index{ones})\index{all-ones}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ones-is-injective \\ \index{ones-is-injective}
(({\it{i\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{j\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{i\/}} $\not=$ {\it{j\/}})) $\rightarrow$ ({\rm{ones}}\,({\it{i\/}})\index{ones} $\not=$ {\rm{ones}}\,({\it{j\/}})\index{ones})
\end{tabbing}

\begin{tabbing}{\sc Conservative Axiom}:  koenig-intro \\ \index{koenig-intro}
\=\+{\rm{node-p}}\,({\bf{nil}})\index{node-p} \\ 
$\wedge$$\;\;\;\;$({\rm{truep}}\,({\rm{node-p}}\,({\it{s\/}})\index{node-p}) $\vee$ {\rm{falsep}}\,({\rm{node-p}}\,({\it{s\/}})\index{node-p})) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{node-p}}\,({\it{s\/}})\index{node-p} \\ 
$\rightarrow$$\;\;\;\;$({\rm{node-p}}\,({\rm{cons}}\,({\it{n\/}}, {\it{s\/}}))\index{node-p} $=$ (({\tt{0}} $<$ {\it{n\/}}) $\wedge$ ({\rm{succard}}\,({\it{s\/}})\index{succard} $\not<$ {\it{n\/}}))))\- \\ 
$\wedge$$\;\;\;\;$(({\rm{node-p}}\,({\it{s1\/}})\index{node-p} $\wedge$ {\rm{subseq}}\,({\it{s\/}}, {\it{s1\/}})\index{subseq}) $\rightarrow$ {\rm{node-p}}\,({\it{s\/}})\index{node-p}) \\ 
$\wedge$$\;\;\;\;${\rm{node-p}}\,({\rm{s-n}}\,({\it{n\/}})\index{s-n})\index{node-p} \\ 
$\wedge$$\;\;\;\;$((({\it{i\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{j\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{i\/}} $\not=$ {\it{j\/}})) $\rightarrow$ ({\rm{s-n}}\,({\it{i\/}})\index{s-n} $\not=$ {\rm{s-n}}\,({\it{j\/}})\index{s-n})) \\ 
$\wedge$$\;\;\;\;$(($\neg$ {\rm{plistp}}\,({\it{s\/}})\index{plistp}) $\rightarrow$ ($\neg$ {\rm{node-p}}\,({\it{s\/}})\index{node-p}))\-
\end{tabbing}\noindent Simultaneously, we introduce the new function symbols {\it node-p\/}, {\it succard\/}, and {\it s-n\/}.

\begin{verbatim};; We want to define a function s-height which returns an element of a given height.
;; The next several events culminate in the following lemma:

;; (prove-lemma length-s-height (rewrite)
;;   (equal (length (s-height n)) (fix n)))

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{succ-aux} \\  
\=\+{\rm{succ-aux}}\,({\it{s\/}}, {\it{n\/}})\index{succ-aux} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,({\rm{cons}}\,({\it{n\/}}, {\it{s\/}}), {\rm{succ-aux}}\,({\it{s\/}}, {\it{n\/}} $-\;1$)\index{succ-aux})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{successors}$\;\;$
{\rm{successors}}\,({\it{s\/}})\index{successors} $=$ {\rm{succ-aux}}\,({\it{s\/}}, {\rm{succard}}\,({\it{s\/}})\index{succard})\index{succ-aux}
\end{tabbing}

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

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

\begin{tabbing}{\sc Definition}:\index{init-tree} \\  
\=\+{\rm{init-tree}}\,({\it{n\/}})\index{init-tree} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{list}}\,({\bf{nil}}) \\ 
{\bf else }{\rm{append}}\,({\rm{level}}\,({\it{n\/}})\index{level}, {\rm{init-tree}}\,({\it{n\/}} $-\;1$)\index{init-tree})$\;${\bf  endif}\-\-
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  length-remove1 \\ \index{length-remove1}
({\it{a\/}} $\in$ {\it{x\/}}) $\rightarrow$ ({\rm{length}}\,({\rm{remove1}}\,({\it{a\/}}, {\it{x\/}})\index{remove1})\index{length} $<$ {\rm{length}}\,({\it{x\/}})\index{length})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{first-non-member-index} \\  
\=\+{\rm{first-non-member-index}}\,({\it{i\/}}, {\it{x\/}})\index{first-non-member-index} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{s-n}}\,({\it{i\/}})\index{s-n} $\in$ {\it{x\/}}$\;\;${\bf then }{\rm{first-non-member-index}}\,($1\;+$ {\it{i\/}}, {\rm{remove1}}\,({\rm{s-n}}\,({\it{i\/}})\index{s-n}, {\it{x\/}})\index{remove1})\index{first-non-member-index} \\ 
{\bf else }{\it{i\/}}$\;${\bf  endif}\-\-
\end{tabbing}

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

\begin{tabbing}{\sc Definition}:\index{s-height} \\  
\=\+{\rm{s-height}}\,({\it{n\/}})\index{s-height} \\ 
$=$$\;\;\;\;${\rm{nthcdr}}\,(\=\+{\rm{length}}\,({\rm{s-n}}\,({\rm{first-non-member-index}}\,({\tt{0}}, {\rm{init-tree}}\,({\it{n\/}})\index{init-tree})\index{first-non-member-index})\index{s-n})\index{length} $-$ {\it{n\/}}, \\ 
{\rm{s-n}}\,({\rm{first-non-member-index}}\,({\tt{0}}, {\rm{init-tree}}\,({\it{n\/}})\index{init-tree})\index{first-non-member-index})\index{s-n})\-\index{nthcdr}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  nthcdr-subseq \\ \index{nthcdr-subseq}
({\rm{length}}\,({\it{s\/}})\index{length} $\not<$ {\it{n\/}}) $\rightarrow$ {\rm{subseq}}\,({\rm{nthcdr}}\,({\it{n\/}}, {\it{s\/}})\index{nthcdr}, {\it{s\/}})\index{subseq}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  node-p-nthcdr \\ \index{node-p-nthcdr}
({\rm{node-p}}\,({\it{s\/}})\index{node-p} $\wedge$ ({\rm{length}}\,({\it{s\/}})\index{length} $\not<$ {\it{n\/}})) $\rightarrow$ {\rm{node-p}}\,({\rm{nthcdr}}\,({\it{n\/}}, {\it{s\/}})\index{nthcdr})\index{node-p}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-difference-1 \\ \index{lessp-difference-1}
({\it{x\/}} $<$ ({\it{x\/}} $-$ {\it{n\/}})) $=$ {\bf{f}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  node-p-s-height \\ \index{node-p-s-height}
{\rm{node-p}}\,({\rm{s-height}}\,({\it{n\/}})\index{s-height})\index{node-p}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-nthcdr \\ \index{length-nthcdr}
{\rm{length}}\,({\rm{nthcdr}}\,({\it{n\/}}, {\it{s\/}})\index{nthcdr})\index{length} $=$ ({\rm{length}}\,({\it{s\/}})\index{length} $-$ {\it{n\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  first-non-member-index-lessp \\ \index{first-non-member-index-lessp}
{\rm{first-non-member-index}}\,({\it{i\/}}, {\it{x\/}})\index{first-non-member-index} $\not<$ {\it{i\/}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  s-n-first-non-member-index-not-equal \\ \index{s-n-first-non-member-index-not-eq!ual}
\=\+({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\rightarrow$$\;\;\;\;$({\rm{s-n}}\,({\rm{first-non-member-index}}\,($1\;+$ {\it{i\/}}, {\rm{remove1}}\,({\rm{s-n}}\,({\it{i\/}})\index{s-n}, {\it{x\/}})\index{remove1})\index{first-non-member-index})\index{s-n} $\not=$ {\rm{s-n}}\,({\it{i\/}})\index{s-n})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-remove1 \\ \index{member-remove1}
({\it{a\/}} $\not=$ {\it{b\/}}) $\rightarrow$ (({\it{a\/}} $\in$ {\rm{remove1}}\,({\it{b\/}}, {\it{x\/}})\index{remove1}) $=$ ({\it{a\/}} $\in$ {\it{x\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  s-n-first-non-member-index \\ \index{s-n-first-non-member-index}
({\it{i\/}} $\in\;${\bf{N}}${}$) $\rightarrow$ ({\rm{s-n}}\,({\rm{first-non-member-index}}\,({\it{i\/}}, {\it{x\/}})\index{first-non-member-index})\index{s-n} $\not\in$ {\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-append \\ \index{member-append}
({\it{a\/}} $\in$ {\rm{append}}\,({\it{x\/}}, {\it{y\/}})) $=$ (({\it{a\/}} $\in$ {\it{x\/}}) $\vee$ ({\it{a\/}} $\in$ {\it{y\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-cons-succ-aux \\ \index{member-cons-succ-aux}
({\rm{cons}}\,({\it{z\/}}, {\it{v\/}}) $\in$ {\rm{succ-aux}}\,({\it{v\/}}, {\it{n\/}})\index{succ-aux}) $=$ (({\tt{0}} $<$ {\it{z\/}}) $\wedge$ ({\it{n\/}} $\not<$ {\it{z\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  node-p-cons-lemma \\ \index{node-p-cons-lemma}
($\neg$ {\rm{node-p}}\,({\it{s\/}})\index{node-p}) $\rightarrow$ ($\neg$ {\rm{node-p}}\,({\rm{cons}}\,({\it{n\/}}, {\it{s\/}}))\index{node-p})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  node-p-cons \\ \index{node-p-cons}
{\rm{node-p}}\,({\rm{cons}}\,({\it{n\/}}, {\it{s\/}}))\index{node-p} $=$ ({\rm{node-p}}\,({\it{s\/}})\index{node-p} $\wedge$ ({\tt{0}} $<$ {\it{n\/}}) $\wedge$ ({\rm{succard}}\,({\it{s\/}})\index{succard} $\not<$ {\it{n\/}}))
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{all-length-n} \\  
\=\+{\rm{all-length-n}}\,({\it{ss\/}}, {\it{n\/}})\index{all-length-n} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{ss\/}})$\;\;${\bf then }\=\+({\rm{length}}\,({\rm{car}}\,({\it{ss\/}}))\index{length} $=$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{all-length-n}}\,({\rm{cdr}}\,({\it{ss\/}}), {\it{n\/}})\index{all-length-n}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-length-n-append \\ \index{all-length-n-append}
\=\+{\rm{all-length-n}}\,({\rm{append}}\,({\it{ss1\/}}, {\it{ss2\/}}), {\it{n\/}})\index{all-length-n} \\ 
$=$$\;\;\;\;$({\rm{all-length-n}}\,({\it{ss1\/}}, {\it{n\/}})\index{all-length-n} $\wedge$ {\rm{all-length-n}}\,({\it{ss2\/}}, {\it{n\/}})\index{all-length-n})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-length-n-succ-aux \\ \index{all-length-n-succ-aux}
({\rm{length}}\,({\it{s\/}})\index{length} $=$ {\it{n\/}}) $\rightarrow$ {\rm{all-length-n}}\,({\rm{succ-aux}}\,({\it{s\/}}, {\it{k\/}})\index{succ-aux}, $1\;+$ {\it{n\/}})\index{all-length-n}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-length-n-successors-list \\ \index{all-length-n-successors-list}
{\rm{all-length-n}}\,({\it{ss\/}}, {\it{n\/}})\index{all-length-n} $\rightarrow$ {\rm{all-length-n}}\,({\rm{successors-list}}\,({\it{ss\/}})\index{successors-list}, $1\;+$ {\it{n\/}})\index{all-length-n}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-0 \\ \index{length-0}
({\rm{length}}\,({\it{s\/}})\index{length} $=$ {\tt{0}}) $=$ ({\it{s\/}} $\simeq\;${{\bf{nil}}}${}$)
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  succ-aux-listp \\ \index{succ-aux-listp}
($\neg$ {\rm{listp}}\,({\it{s\/}})) $\rightarrow$ ({\it{s\/}} $\not\in$ {\rm{succ-aux}}\,({\it{z\/}}, {\it{n\/}})\index{succ-aux})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  successors-list-listp \\ \index{successors-list-listp}
($\neg$ {\rm{listp}}\,({\it{s\/}})) $\rightarrow$ ({\it{s\/}} $\not\in$ {\rm{successors-list}}\,({\it{ss\/}})\index{successors-list})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-succ-aux \\ \index{member-succ-aux}
({\it{s\/}} $\in$ {\rm{succ-aux}}\,({\it{x\/}}, {\it{n\/}})\index{succ-aux}) $\rightarrow$ ({\rm{cdr}}\,({\it{s\/}}) $=$ {\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-successors-list-successors-list-witness \\ \index{member-successors-list-successo!rs-list-witness}
\=\+({\it{s\/}} $\in$ {\rm{successors-list}}\,({\it{ss\/}})\index{successors-list}) \\ 
$=$$\;\;\;\;$(({\rm{cdr}}\,({\it{s\/}}) $\in$ {\it{ss\/}}) $\wedge$ ({\it{s\/}} $\in$ {\rm{successors}}\,({\rm{cdr}}\,({\it{s\/}}))\index{successors}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-level \\ \index{member-level}
(({\it{n\/}} $\in\;${\bf{N}}${}$) $\wedge$ {\rm{node-p}}\,({\it{s\/}})\index{node-p}) $\rightarrow$ (({\it{s\/}} $\in$ {\rm{level}}\,({\it{n\/}})\index{level}) $=$ ({\rm{length}}\,({\it{s\/}})\index{length} $=$ {\it{n\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-init-tree \\ \index{member-init-tree}
{\rm{node-p}}\,({\it{s\/}})\index{node-p} $\rightarrow$ (({\it{s\/}} $\in$ {\rm{init-tree}}\,({\it{n\/}})\index{init-tree}) $=$ ({\it{n\/}} $\not<$ {\rm{length}}\,({\it{s\/}})\index{length}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-s-non-member-index \\ \index{length-s-non-member-index}
({\it{i\/}} $\in\;${\bf{N}}${}$) $\rightarrow$ ({\it{n\/}} $<$ {\rm{length}}\,({\rm{s-n}}\,({\rm{first-non-member-index}}\,({\it{i\/}}, {\rm{init-tree}}\,({\it{n\/}})\index{init-tree})\index{first-non-member-index})\index{s-n})\index{length})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-s-height \\ \index{length-s-height}
{\rm{length}}\,({\rm{s-height}}\,({\it{n\/}})\index{s-height})\index{length} $=$ {\rm{fix}}\,({\it{n\/}})
\end{tabbing}


\noindent{\sc Event}:   Disable s-height.

\addvspace{18pt}

\begin{verbatim};; End of s-height excursion.

;; Our goal:
#|
(prove-lemma konig-tree-lemma nil
  (and (node-p (k n))
       (implies (not (lessp j i))
		(subseq (k i) (k j)))
       (equal (length (k n)) (fix n))))
|#

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{inf} \\  
\=\+{\rm{inf}}\,({\it{s\/}})\index{inf} \\ 
$\leftrightarrow$$\;\;\;\;$$\forall\;${\it{big-h\/}}$\;$$\exists\;${\it{big-s\/}}$\;$(\=\+{\rm{subseq}}\,({\it{s\/}}, {\it{big-s\/}})\index{subseq} \\ 
$\wedge$$\;\;\;\;${\rm{node-p}}\,({\it{big-s\/}})\index{node-p} \\ 
$\wedge$$\;\;\;\;$({\it{big-h\/}} $<$ {\rm{length}}\,({\it{big-s\/}})\index{length}))\-\index{exists}\index{forall}\-
\end{tabbing}

\begin{verbatim};; The following three events were generated mechanically.  They are
;; useful especially for applying the Skolem axioms for INF inside the
;; proof-checker, via the macro command SK*.

\end{verbatim}
\noindent{\sc Event}:   Disable inf.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  inf-suff \\ \index{inf-suff}
\=\+({\rm{subseq}}\,({\it{s\/}}, {\it{big-s\/}})\index{subseq} $\wedge$ {\rm{node-p}}\,({\it{big-s\/}})\index{node-p} $\wedge$ ({\rm{big-h}}\,({\it{s\/}})\index{big-h} $<$ {\rm{length}}\,({\it{big-s\/}})\index{length})) \\ 
$\rightarrow$$\;\;\;\;${\rm{inf}}\,({\it{s\/}})\index{inf}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  inf-necc \\ \index{inf-necc}
\=\+($\neg$ (\=\+{\rm{subseq}}\,({\it{s\/}}, {\rm{big-s}}\,({\it{big-h\/}}, {\it{s\/}})\index{big-s})\index{subseq} \\ 
$\wedge$$\;\;\;\;${\rm{node-p}}\,({\rm{big-s}}\,({\it{big-h\/}}, {\it{s\/}})\index{big-s})\index{node-p} \\ 
$\wedge$$\;\;\;\;$({\it{big-h\/}} $<$ {\rm{length}}\,({\rm{big-s}}\,({\it{big-h\/}}, {\it{s\/}})\index{big-s})\index{length}))\-) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{inf}}\,({\it{s\/}})\index{inf})\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{next} \\  
\=\+{\rm{next}}\,({\it{s\/}}, {\it{max\/}})\index{next} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{max\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{cons}}\,({\tt{0}}, {\it{s\/}}) \\ 
{\bf elseif }{\rm{inf}}\,({\rm{cons}}\,({\it{max\/}}, {\it{s\/}}))\index{inf}$\;\;${\bf then }{\rm{cons}}\,({\it{max\/}}, {\it{s\/}}) \\ 
{\bf else }{\rm{next}}\,({\it{s\/}}, {\it{max\/}} $-\;1$)\index{next}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};; We want to show that NEXT gives us a successor with infinitely many
;; successors.

#| INF-IMPLIES-INF-NEXT:
(implies (and (node-p s)
	      (inf s))
	 (inf (next s (succard s))))
|#

;; Note that if some successor of s has infinitely many successors, so
;; does (NEXT S (SUCCARD S)).  This is the lemma
;; INF-CONS-IMPLIES-INF-NEXT below.  But first note:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  inf-implies-node-p \\ \index{inf-implies-node-p}
{\rm{inf}}\,({\it{s\/}})\index{inf} $\rightarrow$ {\rm{node-p}}\,({\it{s\/}})\index{node-p}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  not-inf-zerop \\ \index{not-inf-zerop}
({\it{i\/}} $\simeq {\tt{0}}$) $\rightarrow$ ($\neg$ {\rm{inf}}\,({\rm{cons}}\,({\it{i\/}}, {\it{s\/}}))\index{inf})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  inf-cons-implies-inf-next \\ \index{inf-cons-implies-inf-next}
({\rm{node-p}}\,({\it{s\/}})\index{node-p} $\wedge$ {\rm{inf}}\,({\rm{cons}}\,({\it{i\/}}, {\it{s\/}}))\index{inf} $\wedge$ ({\it{n\/}} $\not<$ {\it{i\/}})) $\rightarrow$ {\rm{inf}}\,({\rm{next}}\,({\it{s\/}}, {\it{n\/}})\index{next})\index{inf}
\end{tabbing}

\begin{verbatim};; Our goal now is to apply this lemma by proving that
;; (inf (cons i s)) for some i <= (succard s).

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{all-big-h} \\  
\=\+{\rm{all-big-h}}\,({\it{s\/}}, {\it{n\/}})\index{all-big-h} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }$1\;+$ {\rm{length}}\,({\it{s\/}})\index{length} \\ 
{\bf else }{\rm{big-h}}\,({\rm{cons}}\,({\it{n\/}}, {\it{s\/}}))\index{big-h} $+$ {\rm{all-big-h}}\,({\it{s\/}}, {\it{n\/}} $-\;1$)\index{all-big-h}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-big-h-length \\ \index{all-big-h-length}
{\rm{length}}\,({\it{s\/}})\index{length} $<$ {\rm{all-big-h}}\,({\it{s\/}}, {\it{n\/}})\index{all-big-h}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-big-h-lessp \\ \index{all-big-h-lessp}
\=\+(({\tt{0}} $<$ {\it{i\/}}) $\wedge$ ({\it{n\/}} $\not<$ {\it{i\/}})) \\ 
$\rightarrow$$\;\;\;\;$(({\rm{big-h}}\,({\rm{cons}}\,({\it{i\/}}, {\it{s\/}}))\index{big-h} $<$ {\rm{all-big-h}}\,({\it{s\/}}, {\it{n\/}})\index{all-big-h}) $=$ {\bf{t}})\-
\end{tabbing}

\begin{verbatim};; Here's a function which tells us which way s first branches on its
;; way to extending to s1.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{first-branch} \\  
\=\+{\rm{first-branch}}\,({\it{s\/}}, {\it{s1\/}})\index{first-branch} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{s\/}} $=$ {\rm{cdr}}\,({\it{s1\/}})$\;\;${\bf then }{\rm{car}}\,({\it{s1\/}}) \\ 
{\bf elseif }{\it{s1\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\rm{first-branch}}\,({\it{s\/}}, {\rm{cdr}}\,({\it{s1\/}}))\index{first-branch}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subseq-cons-first-branch \\ \index{subseq-cons-first-branch}
({\rm{subseq}}\,({\it{s\/}}, {\it{x\/}})\index{subseq} $\wedge$ ({\it{s\/}} $\not=$ {\it{x\/}})) $\rightarrow$ {\rm{subseq}}\,({\rm{cons}}\,({\rm{first-branch}}\,({\it{s\/}}, {\it{x\/}})\index{first-branch}, {\it{s\/}}), {\it{x\/}})\index{subseq}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-non-equal \\ \index{length-non-equal}
({\rm{length}}\,({\it{x\/}})\index{length} $<$ {\rm{length}}\,({\it{y\/}})\index{length}) $\rightarrow$ (({\it{x\/}} $=$ {\it{y\/}}) $=$ {\bf{f}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  first-branch-ok-for-succard \\ \index{first-branch-ok-for-succard}
\=\+({\rm{subseq}}\,({\it{s\/}}, {\it{big-s\/}})\index{subseq} $\wedge$ {\rm{node-p}}\,({\it{big-s\/}})\index{node-p} $\wedge$ ({\it{s\/}} $\not=$ {\it{big-s\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{first-branch}}\,({\it{s\/}}, {\it{big-s\/}})\index{first-branch} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\tt{0}} $<$ {\rm{first-branch}}\,({\it{s\/}}, {\it{big-s\/}})\index{first-branch}) \\ 
$\wedge$$\;\;\;\;$({\rm{succard}}\,({\it{s\/}})\index{succard} $\not<$ {\rm{first-branch}}\,({\it{s\/}}, {\it{big-s\/}})\index{first-branch}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-big-h-lessp-linear \\ \index{all-big-h-lessp-linear}
\=\+(({\tt{0}} $<$ {\it{i\/}}) $\wedge$ ({\rm{succard}}\,({\it{s\/}})\index{succard} $\not<$ {\it{i\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{big-h}}\,({\rm{cons}}\,({\it{i\/}}, {\it{s\/}}))\index{big-h} $<$ {\rm{all-big-h}}\,({\it{s\/}}, {\rm{succard}}\,({\it{s\/}})\index{succard})\index{all-big-h})\-
\end{tabbing}

\noindent{\sc Event}:   Disable all-big-h-lessp.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  inf-implies-inf-next \\ \index{inf-implies-inf-next}
({\rm{node-p}}\,({\it{s\/}})\index{node-p} $\wedge$ {\rm{inf}}\,({\it{s\/}})\index{inf}) $\rightarrow$ {\rm{inf}}\,({\rm{next}}\,({\it{s\/}}, {\rm{succard}}\,({\it{s\/}})\index{succard})\index{next})\index{inf}
\end{tabbing} 

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

\begin{tabbing}{\sc Theorem}:  subseq-nil \\ \index{subseq-nil}
{\rm{subseq}}\,({\bf{nil}}, {\it{x\/}})\index{subseq} $=$ {\rm{plistp}}\,({\it{x\/}})\index{plistp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  node-p-implies-plistp \\ \index{node-p-implies-plistp}
{\rm{node-p}}\,({\it{s\/}})\index{node-p} $\rightarrow$ {\rm{plistp}}\,({\it{s\/}})\index{plistp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  inf-nil \\ \index{inf-nil}
{\rm{inf}}\,({\bf{nil}})\index{inf}
\end{tabbing}


\noindent{\sc Event}:   Disable node-p-implies-plistp.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  konig-tree-lemma-1 \\ \index{konig-tree-lemma-1}
{\rm{inf}}\,({\rm{k}}\,({\it{n\/}})\index{k})\index{inf}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-next \\ \index{length-next}
{\rm{inf}}\,({\it{x\/}})\index{inf} $\rightarrow$ ({\rm{length}}\,({\rm{next}}\,({\it{s\/}}, {\it{n\/}})\index{next})\index{length} $=$ ($1\;+$ {\rm{length}}\,({\it{s\/}})\index{length}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  konig-tree-lemma-2 \\ \index{konig-tree-lemma-2}
{\rm{length}}\,({\rm{k}}\,({\it{n\/}})\index{k})\index{length} $=$ {\rm{fix}}\,({\it{n\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subseq-next \\ \index{subseq-next}
{\rm{subseq}}\,({\it{s1\/}}, {\it{s2\/}})\index{subseq} $\rightarrow$ {\rm{subseq}}\,({\it{s1\/}}, {\rm{next}}\,({\it{s2\/}}, {\it{n\/}})\index{next})\index{subseq}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  konig-tree-lemma-3 \\ \index{konig-tree-lemma-3}
({\it{j\/}} $\not<$ {\it{i\/}}) $\rightarrow$ {\rm{subseq}}\,({\rm{k}}\,({\it{i\/}})\index{k}, {\rm{k}}\,({\it{j\/}})\index{k})\index{subseq}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  konig-tree-lemma \\ \index{konig-tree-lemma}
\=\+{\rm{node-p}}\,({\rm{k}}\,({\it{n\/}})\index{k})\index{node-p} \\ 
$\wedge$$\;\;\;\;$(({\it{j\/}} $\not<$ {\it{i\/}}) $\rightarrow$ {\rm{subseq}}\,({\rm{k}}\,({\it{i\/}})\index{k}, {\rm{k}}\,({\it{j\/}})\index{k})\index{subseq}) \\ 
$\wedge$$\;\;\;\;$({\rm{length}}\,({\rm{k}}\,({\it{n\/}})\index{k})\index{length} $=$ {\rm{fix}}\,({\it{n\/}}))\-
\end{tabbing}

\begin{verbatim};; or, if one prefers:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  konig-tree-lemma-again \\ \index{konig-tree-lemma-again}
\=\+({\it{n\/}} $\in\;${\bf{N}}${}$) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{node-p}}\,({\rm{k}}\,({\it{n\/}})\index{k})\index{node-p} \\ 
$\wedge$$\;\;\;\;$(({\it{j\/}} $\not<$ {\it{i\/}}) $\rightarrow$ {\rm{subseq}}\,({\rm{k}}\,({\it{i\/}})\index{k}, {\rm{k}}\,({\it{j\/}})\index{k})\index{subseq}) \\ 
$\wedge$$\;\;\;\;$({\rm{length}}\,({\rm{k}}\,({\it{n\/}})\index{k})\index{length} $=$ {\it{n\/}}))\-\-
\end{tabbing}


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