;; 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.

Event: Start with the initial nqthm theory.

;; All this initial stuff is just to get the CONSTRAIN below accepted.

Definition: ones (n) = if n ≃ 0 then nil

else cons (1, ones (n − 1)) endif

Definition: all-ones (s) = if listp (s) then (car (s) = 1) ∧ all-ones (cdr (s))

else s = nil endif

Definition: length (s) = if listp (s) then 1 + length (cdr (s))

else 0 endif

Definition: subseq (s1 , s2 ) = if s1 = s2 then t

elseif s2 ≃ nil then f

else subseq (s1 , cdr (s2 )) endif

Theorem: subseq-all-ones (all-ones (s1 ) ∧ subseq (s2 , s1 )) → all-ones (s2 )

Definition: plistp (s) = if listp (s) then plistp (cdr (s))

else s = nil endif Theorem: plistp-all-ones all-ones (s) → plistp (s)

Theorem: all-ones-ones all-ones (ones (n))

Theorem: ones-is-injective ((i ∈ N) ∧ (j ∈ N) ∧ (i ≠ j )) → (ones (i) ≠ ones (j ))

Conservative Axiom: koenig-intro node-p (nil) ∧ (truep (node-p (s)) ∨ falsep (node-p (s))) ∧ (node-p (s)

→ (node-p (cons (n, s)) = ((0 < n) ∧ (succard (s) ≮ n)))) ∧ ((node-p (s1 ) ∧ subseq (s, s1 )) → node-p (s)) ∧ node-p (s-n (n)) ∧ (((i ∈ N) ∧ (j ∈ N) ∧ (i ≠ j )) → (s-n (i) ≠ s-n (j ))) ∧ ((¬ plistp (s)) → (¬ node-p (s)))

Simultaneously, we introduce the new function symbols node-p, succard, and s-n.

;; 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)))

Definition: succ-aux (s, n) = if n ≃ 0 then nil

else cons (cons (n, s), succ-aux (s, n − 1)) endif

Definition: successors (s) = succ-aux (s, succard (s))

Definition: successors-list (ss) = if listp (ss)

then append (successors (car (ss)), successors-list (cdr (ss)))

else nil endif

Definition: level (n) = if n ≃ 0 then list (nil)

else successors-list (level (n − 1)) endif Definition: init-tree (n) = if n ≃ 0 then list (nil)

else append (level (n), init-tree (n − 1)) endif

Definition: remove1 (a, x) = if listp (x)

then if a = car (x) then cdr (x)

else cons (car (x), remove1 (a, cdr (x))) endif else x endif

Theorem: length-remove1 (a ∈ x) → (length (remove1 (a, x)) < length (x))

Definition: first-non-member-index (i, x) = if s-n (i) ∈ x then first-non-member-index (1 + i, remove1 (s-n (i), x))

else i endif

Definition: nthcdr (n, s) = if n ≃ 0 then s

else nthcdr (n − 1, cdr (s)) endif

Definition: s-height (n) = nthcdr (length (s-n (first-non-member-index (0, init-tree (n)))) − n,

s-n (first-non-member-index (0, init-tree (n))))

Theorem: nthcdr-subseq (length (s) ≮ n) → subseq (nthcdr (n, s), s)

Theorem: node-p-nthcdr (node-p (s) ∧ (length (s) ≮ n)) → node-p (nthcdr (n, s))

Theorem: lessp-difference-1 (x < (x − n)) = f

Theorem: node-p-s-height node-p (s-height (n))

Theorem: length-nthcdr length (nthcdr (n, s)) = (length (s) − n)

Theorem: first-non-member-index-lessp first-non-member-index (i, x) ≮ i Theorem: s-n-first-non-member-index-not-equal (i ∈ N) → (s-n (first-non-member-index (1 + i, remove1 (s-n (i), x))) ≠ s-n (i))

Theorem: member-remove1 (a ≠ b) → ((a ∈ remove1 (b, x)) = (a ∈ x))

Theorem: s-n-first-non-member-index (i ∈ N) → (s-n (first-non-member-index (i, x)) ∉ x)

Theorem: member-append (a ∈ append (x, y)) = ((a ∈ x) ∨ (a ∈ y))

Theorem: member-cons-succ-aux (cons (z, v) ∈ succ-aux (v, n)) = ((0 < z) ∧ (n ≮ z))

Theorem: node-p-cons-lemma (¬ node-p (s)) → (¬ node-p (cons (n, s)))

Theorem: node-p-cons node-p (cons (n, s)) = (node-p (s) ∧ (0 < n) ∧ (succard (s) ≮ n))

Definition: all-length-n (ss, n) = if listp (ss) then (length (car (ss)) = n)

∧ all-length-n (cdr (ss), n)

else t endif

Theorem: all-length-n-append all-length-n (append (ss1 , ss2 ), n) = (all-length-n (ss1 , n) ∧ all-length-n (ss2 , n))

Theorem: all-length-n-succ-aux (length (s) = n) → all-length-n (succ-aux (s, k), 1 + n)

Theorem: all-length-n-successors-list all-length-n (ss, n) → all-length-n (successors-list (ss), 1 + n)

Theorem: length-0 (length (s) = 0) = (s ≃ nil)

Definition: member-level-induction (s, n) = if n ≃ 0 then t

else member-level-induction (cdr (s), n − 1) endif Theorem: succ-aux-listp (¬ listp (s)) → (s ∉ succ-aux (z, n))

Theorem: successors-list-listp (¬ listp (s)) → (s ∉ successors-list (ss))

Theorem: member-succ-aux (s ∈ succ-aux (x, n)) → (cdr (s) = x)

Theorem: member-successors-list-successors-list-witness (s ∈ successors-list (ss)) = ((cdr (s) ∈ ss) ∧ (s ∈ successors (cdr (s))))

Theorem: member-level ((n ∈ N) ∧ node-p (s)) → ((s ∈ level (n)) = (length (s) = n))

Theorem: member-init-tree node-p (s) → ((s ∈ init-tree (n)) = (n ≮ length (s)))

Theorem: length-s-non-member-index (i ∈ N) → (n < length (s-n (first-non-member-index (i, init-tree (n)))))

Theorem: length-s-height length (s-height (n)) = fix (n)

Event: Disable s-height.

;; 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))))
|#

Definition: inf (s) ↔ ∀ big-h ∃ big-s (subseq (s, big-s)

∧ node-p (big-s)

∧ (big-h < length (big-s)))

;; 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*.

Event: Disable inf.

Theorem: inf-suff (subseq (s, big-s) ∧ node-p (big-s) ∧ (big-h (s) < length (big-s))) → inf (s)

Theorem: inf-necc (¬ (subseq (s, big-s (big-h, s))

∧ node-p (big-s (big-h, s))

∧ (big-h < length (big-s (big-h, s))))) → (¬ inf (s))

Definition: next (s, max) = if max ≃ 0 then cons (0, s)

elseif inf (cons (max, s)) then cons (max, s)

else next (s, max − 1) endif

;; 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:

Theorem: inf-implies-node-p inf (s) → node-p (s)

Theorem: not-inf-zerop (i ≃ 0) → (¬ inf (cons (i, s)))

Theorem: inf-cons-implies-inf-next (node-p (s) ∧ inf (cons (i, s)) ∧ (n ≮ i)) → inf (next (s, n))

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

Definition: all-big-h (s, n) = if n ≃ 0 then 1 + length (s)

else big-h (cons (n, s)) + all-big-h (s, n − 1) endif

Theorem: all-big-h-length length (s) < all-big-h (s, n)

Theorem: all-big-h-lessp ((0 < i) ∧ (n ≮ i)) → ((big-h (cons (i, s)) < all-big-h (s, n)) = t)

;; Here's a function which tells us which way s first branches on its
;; way to extending to s1.

Definition: first-branch (s, s1 ) = if s = cdr (s1 ) then car (s1 )

elseif s1 ≃ nil then 0

else first-branch (s, cdr (s1 )) endif

Theorem: subseq-cons-first-branch (subseq (s, x) ∧ (s ≠ x)) → subseq (cons (first-branch (s, x), s), x)

Theorem: length-non-equal (length (x) < length (y)) → ((x = y) = f)

Theorem: first-branch-ok-for-succard (subseq (s, big-s) ∧ node-p (big-s) ∧ (s ≠ big-s)) → ((first-branch (s, big-s) ∈ N)

∧ (0 < first-branch (s, big-s))

∧ (succard (s) ≮ first-branch (s, big-s)))

Theorem: all-big-h-lessp-linear ((0 < i) ∧ (succard (s) ≮ i)) → (big-h (cons (i, s)) < all-big-h (s, succard (s)))

Event: Disable all-big-h-lessp.

Theorem: inf-implies-inf-next (node-p (s) ∧ inf (s)) → inf (next (s, succard (s)))

Definition: k (n) = if n ≃ 0 then nil

else next (k (n − 1), succard (k (n − 1))) endif

Theorem: subseq-nil subseq (nil, x) = plistp (x)

Theorem: node-p-implies-plistp node-p (s) → plistp (s)

Theorem: inf-nil inf (nil)

Event: Disable node-p-implies-plistp.

Theorem: konig-tree-lemma-1 inf (k (n))

Theorem: length-next inf (x) → (length (next (s, n)) = (1 + length (s)))

Theorem: konig-tree-lemma-2 length (k (n)) = fix (n)

Theorem: subseq-next subseq (s1 , s2 ) → subseq (s1 , next (s2 , n))

Theorem: konig-tree-lemma-3 (j ≮ i) → subseq (k (i), k (j ))

Theorem: konig-tree-lemma node-p (k (n)) ∧ ((j ≮ i) → subseq (k (i), k (j ))) ∧ (length (k (n)) = fix (n))

;; or, if one prefers:

Theorem: konig-tree-lemma-again (n ∈ N) → (node-p (k (n))

∧ ((j ≮ i) → subseq (k (i), k (j )))

∧ (length (k (n)) = n))

Index

all-big-h, 7 all-big-h-length, 7 all-big-h-lessp, 7 all-big-h-lessp-linear, 7 all-length-n, 4 all-length-n-append, 4 all-length-n-succ-aux, 4 all-length-n-successors-list, 4 all-ones, 1, 2 all-ones-ones, 2

big-h, 6, 7 big-s, 6

exists, 5

first-branch, 7 first-branch-ok-for-succard, 7 first-non-member-index, 3–5 first-non-member-index-lessp, 3 forall, 5

inf, 5–8 inf-cons-implies-inf-next, 6 inf-implies-inf-next, 7 inf-implies-node-p, 6 inf-necc, 6 inf-nil, 8 inf-suff, 6 init-tree, 3, 5

k, 8 koenig-intro, 2 konig-tree-lemma, 8 konig-tree-lemma-1, 8 konig-tree-lemma-2, 8 konig-tree-lemma-3, 8 konig-tree-lemma-again, 8

length, 1, 3–8 length-0, 4 length-next, 8 length-non-equal, 7 length-nthcdr, 3 length-remove1, 3 length-s-height, 5 length-s-non-member-index, 5 lessp-difference-1, 3 level, 2, 3, 5

member-append, 4

member-cons-succ-aux, 4

member-init-tree, 5 member-level, 5 member-level-induction, 4 member-remove1, 4 member-succ-aux, 5 member-successors-list-successo

rs-list-witness, 5

next, 6–8 node-p, 2–8 node-p-cons, 4 node-p-cons-lemma, 4 node-p-implies-plistp, 8 node-p-nthcdr, 3 node-p-s-height, 3 not-inf-zerop, 6 nthcdr, 3 nthcdr-subseq, 3

ones, 1, 2

ones-is-injective, 2

plistp, 1, 2, 8 plistp-all-ones, 2

remove1, 3, 4

s-height, 3, 5 s-n, 2–5 s-n-first-non-member-index, 4 s-n-first-non-member-index-not-eq

ual, 4 subseq, 1–3, 5–8 subseq-all-ones, 1 subseq-cons-first-branch, 7 subseq-next, 8 subseq-nil, 8 succ-aux, 2, 4, 5 succ-aux-listp, 5 succard, 2, 4, 7, 8 successors, 2, 5 successors-list, 2, 4, 5 successors-list-listp, 5