; Copyright (C) 1995 by Ken Kunen.  All Rights Reserved.
; This script is hereby placed in the public domain, and therefore unlimited
; editing and redistribution is permitted.
; NO WARRANTY
; Ken Kunen PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT IS PROVIDED "AS
; IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED, INCLUDING, BUT
; NOT LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
; PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE
; SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU ASSUME THE COST OF
; ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
; IN NO EVENT WILL Ken Kunen BE LIABLE TO YOU FOR ANY DAMAGES, ANY LOST
; PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES
; ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT NOT
; LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED
; BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF SUCH
; DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.

; This is a proof of the Paris-Harrington Ramsey theorem,
; and some related results.
; The proof is described in our paper, "A Ramsey Theorem
; in Boyer-Moore Logic".
; The following takes [ 79.1 1561.9 92.8 ]  on a DECstation 5000/125

Event: Start with the initial nqthm theory.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;                        BASIC ARITHMETIC                                ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; (expt m n ) = m^n, as in Lisp

Definition: expt (m, n) = if n ≃ 0 then 1

else m ∗ expt (m, n − 1) endif Theorem: distributivity ((u ∗ y) + (a ∗ y)) = ((u + a) ∗ y)

Theorem: associativity-of-times (m ∗ u ∗ y) = ((m ∗ u) ∗ y)

Theorem: addition-of-exponents expt (m, a + b) = (expt (m, a) ∗ expt (m, b))

; consider the exponenial b^e -- it's monotonic as a function
; of b and of e separately
; as a function of b

Theorem: monoton-of-exp-1 (b1 ≤ b2 ) → (expt (b1 , e) ≤ expt (b2 , e))

Theorem: plus-difference ((e1 ≤ e2 ) ∧ (e1 ∈ N) ∧ (e2 ∈ N)) → ((e1 + (e2 − e1 )) = e2 )

; as a function of e:

Theorem: monoton-of-exp-aux1 ((e1 ≤ e2 ) ∧ (e1 ∈ N) ∧ (e2 ∈ N)) → (expt (b, e2 ) = (expt (b, e1 ) ∗ expt (b, e2 − e1 )))

Theorem: expt-is-positive (b ≄ 0) → (0 < expt (b, e))

Theorem: monoton-of-exp-aux2 (b ≄ 0) → (x ≤ (x ∗ expt (b, e)))

Theorem: monoton-of-exp-2 ((e1 ≤ e2 ) ∧ (e1 ∈ N) ∧ (e2 ∈ N) ∧ (b ≄ 0)) → (expt (b, e1 ) ≤ expt (b, e2 ))

; 0 is an exception because 0^0 = 1 but 0^1 = 0

Event: Disable monoton-of-exp-aux1.

Event: Disable monoton-of-exp-aux2.

; (magic s) is the function g(s) which "magically" makes the
; Ramsey proof work out.  Here we just prove some basic arithmetic properties
; of it

Definition: magic (s) = (((3 ∗ s) + 3) ∗ expt (s + 2, s + 2))

Theorem: magic-is-a-number magic (n) ∈ N

; now, we have to prove that magic is monotonic

Theorem: magic-is-monotonic-aux1 (m < n) → (((3 ∗ m) + 3) < ((3 ∗ n) + 3))

Theorem: magic-is-monotonic-aux2 (m < n) → (expt (m + 2, m + 2) ≤ expt (n + 2, n + 2))

Theorem: magic-is-monotonic-aux3 0 < expt (s + 2, s + 2)

Theorem: magic-is-monotonic-aux4 ((x < y) ∧ (a ≤ b) ∧ (0 < a) ∧ (0 < b)) → ((x ∗ a) < (y ∗ b))

Theorem: magic-is-monotonic (m < n) → (magic (m) < magic (n))

Event: Disable magic-is-monotonic-aux1.

Event: Disable magic-is-monotonic-aux2.

Event: Disable magic-is-monotonic-aux3.

Event: Disable magic-is-monotonic-aux4.

Event: Disable magic.

; we need that (magic n) >= n ; this should follow just by monotonicity

Theorem: magic-is-bigger-aux1 ((n ≠ 0) ∧ (magic (n) = 0)) → (n ∉ N)

Theorem: magic-is-bigger-aux2 ((n ∈ N) ∧ (magic (n − 1) ≮ (n − 1))) → (magic (n) ≮ n)

Theorem: magic-is-bigger (n ∈ N) → (magic (n) ≮ n)

Event: Disable magic-is-bigger-aux1.

Event: Disable magic-is-bigger-aux2.

; the above is sufficient for all the basic theory of {alpha}(n)
; and alpha-large sets.
; BUT, we need some further arithmetic properties of magic which
; get used in the Ramsey theorem
; first, let's prove that * is monotonic; + will be handled
; by built-in linear arithmetic

Theorem: times-is-monotonic ((x ≤ y) ∧ (a ≤ b)) → ((x ∗ a) ≤ (y ∗ b))

Theorem: times-right-ident (x ∈ N) → ((x ∗ 1) = x)

Theorem: times-left-ident (x ∈ N) → ((1 ∗ x) = x)

; now, just a chain of uninteresting inequalities culminating
; in exactly what we need about magic(s)
; call these magic-1, magic-2, ...
; they won't be rewrite rules, so we don't need to disable them later

Event: Enable magic.

; we need its defn for some other properties

Theorem: magic-1 ((2 ∗ s) + 3) ≤ magic (s)

Theorem: magic-2 (s ∈ N) → (expt (s, s) ≤ expt (s + 2, s + 2))

Theorem: magic-3 (r ∈ N) → (((3 ∗ r) ∗ expt (r, r)) ≤ magic (r))

Theorem: magic-4 (s ∈ N) → (expt (2, s) ≤ expt (s + 2, s + 2))

Theorem: magic-5 (s ∈ N) → (expt (2, s) ≤ magic (s))

Theorem: magic-6 (s ∈ N) → (expt (s, expt (2, s)) ≤ expt (magic (s), magic (s)))

Theorem: magic-7 (s ∈ N) → (((3 ∗ magic (s)) ∗ expt (s, expt (2, s)))

≤ ((3 ∗ magic (s)) ∗ expt (magic (s), magic (s))))

Theorem: magic-8 (s ∈ N) → (((3 ∗ magic (s)) ∗ expt (s, expt (2, s))) ≤ magic (magic (s)))

Theorem: magic-9 ((2 ∗ s) + 3 + (2 ∗ magic (s))) ≤ (3 ∗ magic (s))

Theorem: magic-10 (s ∈ N) → ((((2 ∗ s) + 3 + (2 ∗ magic (s))) ∗ expt (s, expt (2, s)))

≤ magic (magic (s)))

; now, let's throw in some more parameters.  We have
; a = the norm of some ordinal;
; d = a + c ; s = z + d, q >= magic(z + d), c > 0
; we want to conclude
;(leq
; (times
; (plus (times 2 a) (times 2 (magic z)) 3 c)
; (expt c (expt 2 z)) )
; (magic q) )
; 1. show (leq   (plus (times 2 a) (times 2 (magic z)) 3 c)
;                (plus (times 2 s) 3 (times 2 (magic s))))
; 2. show (leq (expt c (expt 2 z)) (expt s (expt 2 s)))
; then apply magic-10
; step 1

Theorem: magic-11 ((d = (a + c)) ∧ (s = (z + d)) ∧ (c ≄ 0)) → (((2 ∗ a) + (2 ∗ magic (z)) + 3 + c)

≤ ((2 ∗ s) + 3 + (2 ∗ magic (s))))

; step 2

Theorem: magic-12 ((d = (a + c)) ∧ (s = (z + d))) → (expt (2, z) ≤ expt (2, s))

Theorem: magic-13 ((d = (a + c)) ∧ (s = (z + d))) → (expt (c, expt (2, z)) ≤ expt (s, expt (2, s)))

; putting the two steps together:

Theorem: magic-14 ((d = (a + c)) ∧ (s = (z + d)) ∧ (c ≄ 0)) → ((((2 ∗ a) + (2 ∗ magic (z)) + 3 + c)

∗ expt (c, expt (2, z)))

≤ (((2 ∗ s) + 3 + (2 ∗ magic (s))) ∗ expt (s, expt (2, s))))

; now, adding magic-10

Theorem: magic-15 ((d = (a + c)) ∧ (s = (z + d)) ∧ (c ≄ 0)) → ((((2 ∗ a) + (2 ∗ magic (z)) + 3 + c)

∗ expt (c, expt (2, z))) ≤ magic (magic (s)))

; now, the final result doesn't mention s at all -- rather,
; it's in terms of q >= magic(z + d)  (where s is z+d)
; first, isolate the monotnicity of magic

Theorem: magic-16-aux1 (v ∉ N) → ((w ∗ v) = 0)

Theorem: magic-16 (v ∉ N) → (magic (v) = 12)

Event: Disable magic-16-aux1.

Theorem: magic-17 (v ≤ w) → (magic (v) ≤ magic (w))

Theorem: magic-18 ((d = (a + c)) ∧ (magic (z + d) ≤ q) ∧ (c ≄ 0)) → ((((2 ∗ a) + (2 ∗ magic (z)) + 3 + c)

∗ expt (c, expt (2, z)))

≤ magic (q))

; this concludes all the arithmetic facts about magic that we need

Event: Disable magic.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;                      PROPERTIES OF LISTS                               ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; append is build-in, but the following simple lemmas aren't

Theorem: append-works-left (x ∈ lst1 ) → (x ∈ append (lst1 , lst2 ))

Theorem: append-works-right (y ∈ lst2 ) → (y ∈ append (lst1 , lst2 ))

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

else 0 endif

Theorem: length-of-append length (append (lst1 , lst2 )) = (length (lst1 ) + length (lst2 ))

;;;;;;;;;;  product of two lists

Definition: cons-all (item, lst) = if listp (lst) then cons (cons (item, car (lst)), cons-all (item, cdr (lst)))

else nil endif

Definition: product (lst1 , lst2 ) = if lst1 ≃ nil then nil

else append (cons-all (car (lst1 ), lst2 ), product (cdr (lst1 ), lst2 )) endif

; (product '(1 2) '(3 4 5) ) -->
; ((1 . 3) (1 . 4) (1 . 5) (2 . 3) (2 . 4) (2 . 5))
; we need to prove this contains all pairs
; first, for cons-all

Theorem: all-pairs-in-cons-all (y ∈ lst) → (cons (item, y) ∈ cons-all (item, lst))

Theorem: all-pairs ((x ∈ lst1 ) ∧ (y ∈ lst2 )) → (cons (x, y) ∈ product (lst1 , lst2 ))

; We never need the other direction -- that the product
; contains only such pairs

Event: Disable product.

; there are two notions of "sublist" for lists
; 1: (subsetp s1 s2) means that every member of s1 is a member of s2
; 2: (sublistp lst1 lst2) means that lst1 is a consecutive
;     sublist of lst2 -- so, a list of length n always
;     has exactly 2^n sublists.
; For our intended representation of sets as increasing
; lists of natural numbers, (1) and (2) are equivalent.
; In general, (2) implies (1).
; in both cases, for non-nil-terminated lists -- e.g.
; (A1 A2 A3 . B), we ignore the B

Definition: subsetp (s1 , s2 ) = if listp (s1 ) then (car (s1 ) ∈ s2 ) ∧ subsetp (cdr (s1 ), s2 )

else t endif

; there are two fundamental properties of subsetp
; 1. If (subsetp s1 s2) and (member x s1) then (member x s2)
; 2. If (not (subsetp s1 s2)), then there is an x such
;    that (member x s1) and (not (member x s2))
;    Call this object (memb-of-dif s1 s2)

Theorem: subsetp-works-1 (subsetp (s1 , s2 ) ∧ and ∧ (x ∈ s1 )) → (x ∈ s2 )

Definition: memb-of-dif (s1 , s2 ) = if listp (s1 )

then if car (s1 ) ∈ s2 then memb-of-dif (cdr (s1 ), s2 )

else car (s1 ) endif else nil endif Theorem: subsetp-works-2 (¬ subsetp (s1 , s2 )) → ((memb-of-dif (s1 , s2 ) ∈ s1 ) ∧ (memb-of-dif (s1 , s2 ) ∉ s2 ))

Event: Disable memb-of-dif.

; It's really just a Skolem function for (not (subsetp s1 s2))
; We should never need its definition
; the following facts may also be useful:

Theorem: subset-of-empty-set listp (s) → (¬ subsetp (s, nil))

Theorem: transitivity-of-subset (subsetp (s1 , s2 ) ∧ subsetp (s2 , s3 )) → subsetp (s1 , s3 )

Theorem: cdr-is-subset-aux1 (x ∈ cdr (s)) → (x ∈ s)

Theorem: cdr-is-subset subsetp (cdr (s), s)

Event: Disable cdr-is-subset-aux1.

Theorem: cdr-of-subset (subsetp (s1 , s2 ) ∧ listp (s1 )) → subsetp (cdr (s1 ), s2 )

Theorem: nil-is-subset subsetp (nil, s)

; the following might useful in proving consequences
; of (subsetp s1 s2) by induction -- reducing to
; (subsetp s1 (cdr s2))

Theorem: subset-of-cdr (subsetp (s1 , s2 ) ∧ (car (s2 ) ∉ s1 )) → subsetp (s1 , cdr (s2 ))

Theorem: non-empty-subset (subsetp (lst1 , lst2 ) ∧ listp (lst1 )) → listp (lst2 )

Theorem: car-of-subset (subsetp (lst1 , lst2 ) ∧ listp (lst1 )) → (car (lst1 ) ∈ lst2 )

; now, consider sub-lists

Definition: sublistp (lst1 , lst2 ) = if listp (lst2 )

then sublistp (lst1 , cdr (lst2 )) ∨ (listp (lst1 )

∧ (car (lst1 ) = car (lst2 ))

∧ sublistp (cdr (lst1 ), cdr (lst2 )))

else ¬ listp (lst1 ) endif

Theorem: sublist-implies-subset sublistp (lst1 , lst2 ) → subsetp (lst1 , lst2 )

Theorem: transitivity-of-sublist (sublistp (s1 , s2 ) ∧ sublistp (s2 , s3 )) → sublistp (s1 , s3 )

; (power-set S) will actually be the set of all
; (nil-terminated)
; sublists of S -- but this will be all subsets
; in our intended "standard" representation of sets

Definition: power-set (set) = if listp (set)

then append (cons-all (car (set), power-set (cdr (set))), power-set (cdr (set)))

else list (nil) endif

; this has 2^(length elements)

Theorem: size-of-cons-all length (cons-all (item, lst)) = length (lst)

Theorem: size-of-power-set length (power-set (set)) = expt (2, length (set))

; now, we prove that the power-set contains all sublists,
; and only sublists -- of course, the power set is only
; collecting proper lists

Definition: properp (lst) = if listp (lst) then properp (cdr (lst))

else lst = nil endif

Theorem: cons-preserves-proper properp (lst) → properp (cons (item, lst))

Definition: members-all-properp (biglst) = if listp (biglst)

then properp (car (biglst)) ∧ members-all-properp (cdr (biglst))

else t endif

Theorem: append-preserves-members-all-properp (members-all-properp (biglst1 ) ∧ members-all-properp (biglst2 )) → members-all-properp (append (biglst1 , biglst2 ))

Theorem: cons-all-preserves-members-all-properp members-all-properp (biglst) → members-all-properp (cons-all (item, biglst))

; of coure, we chould check the defining property:

Theorem: members-all-properp-works ((lst ∈ biglst) ∧ members-all-properp (biglst)) → properp (lst)

Theorem: only-proper-aux1 members-all-properp (power-set (lst))

Theorem: only-proper (lst ∈ power-set (set)) → properp (lst)

Event: Disable only-proper-aux1.

Definition: members-all-sublistp (biglst, set) = if listp (biglst)

then sublistp (car (biglst), set)

∧ members-all-sublistp (cdr (biglst), set) else t endif

Theorem: append-preserves-members-all-sublistp (members-all-sublistp (biglst1 , set) ∧ members-all-sublistp (biglst2 , set)) → members-all-sublistp (append (biglst1 , biglst2 ), set)

Theorem: cons-all-preserves-members-all-sublistp members-all-sublistp (biglst, set) → members-all-sublistp (cons-all (item, biglst), cons (item, set))

; of coure, we chould check the defining property:

Theorem: members-all-sublistp-works ((lst ∈ biglst) ∧ members-all-sublistp (biglst, set)) → sublistp (lst, set)

Theorem: only-sublists-aux1 members-all-sublistp (power-set (set), set)

Theorem: only-sublists (lst ∈ power-set (set)) → sublistp (lst, set)

; also, we get all sublists

Theorem: all-sublists (sublistp (lst, set) ∧ properp (lst)) → (lst ∈ power-set (set))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;                           STANDARD SETS                                ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; These standard lists of numbers in strictly increasing order.

Definition: setp (s) = if listp (s)

then (car (s) ∈ N) ∧ setp (cdr (s)) ∧ ((cdr (s) = nil) ∨ (car (s) < cadr (s)))

else s = nil endif

;;;;; large, in Paris-Harrington sense:

Definition: largep (set) = (setp (set) ∧ listp (set) ∧ (length (set) ≮ car (set)))

Theorem: empty-is-nil (setp (s) ∧ (¬ listp (s))) → ((s = nil) = t)

; so it can be a rewrite rule -- can't rewrite a var

Theorem: increasing (setp (s) ∧ (x ∈ cdr (s))) → (car (s) < x)

; Since the order is increasing, the members don't occur twice

Theorem: not-again setp (s) → (car (s) ∉ cdr (s))

; the min of a set is its first element

Theorem: min-is-first (setp (s) ∧ (x < car (s))) → (x ∉ s)

; the max of a set is its last element

Definition: last (set) = if listp (set)

then if listp (cdr (set)) then last (cdr (set))

else car (set) endif else 0 endif

; the tail of a set is a set

Theorem: tail-of-a-set (setp (s) ∧ listp (s)) → setp (cdr (s))

; this is useful in inductive proofs about sets

Theorem: first-before-last (setp (s) ∧ listp (cdr (s))) → (car (s) < last (s))

Theorem: max-is-last (setp (s) ∧ (last (s) < x)) → (x ∉ s)

; sets are proper lists:

Theorem: sets-are-proper setp (s) → properp (s)

;; now, a few lemmas about the first elements of subsets

Theorem: compare-first-elts (setp (s1 ) ∧ setp (s2 ) ∧ listp (s1 ) ∧ subsetp (s1 , s2 )) → (car (s1 ) ≮ car (s2 ))

; now, if (subsetp s1 s2) -- there are two cases
; the cars are the same, or (car s2) is smaller

Theorem: smaller-cars-in-subset (setp (s1 ) ∧ setp (s2 ) ∧ listp (s1 ) ∧ subsetp (s1 , s2 ) ∧ (car (s2 ) < car (s1 ))) → subsetp (s1 , cdr (s2 ))

Theorem: same-cars-in-subset-aux1 (setp (s1 ) ∧ listp (s1 ) ∧ listp (cdr (s1 ))) → (car (s1 ) < cadr (s1 ))

Theorem: same-cars-in-subset-aux2 (setp (s1 ) ∧ setp (s2 ) ∧ listp (s1 ) ∧ subsetp (s1 , s2 ) ∧ listp (cdr (s1 )) ∧ (car (s2 ) = car (s1 ))) → subsetp (cdr (s1 ), cdr (s2 ))

Theorem: same-cars-in-subset (setp (s1 ) ∧ setp (s2 ) ∧ listp (s1 ) ∧ subsetp (s1 , s2 ) ∧ (car (s2 ) = car (s1 ))) → subsetp (cdr (s1 ), cdr (s2 ))

Event: Disable same-cars-in-subset-aux1.

Event: Disable same-cars-in-subset-aux2.

; now, we want to prove that subset implies sublist for sets

Definition: bad-for-subset-implies-sublist (set1 , set2 ) = (subsetp (set1 , set2 )

∧ setp (set1 ) ∧ setp (set2 ) ∧ (¬ sublistp (set1 , set2 )))

Theorem: subset-implies-sublist-aux1 (¬ listp (set1 )) → (¬ bad-for-subset-implies-sublist (set1 , set2 ))

Theorem: subset-implies-sublist-aux2 (¬ listp (set2 )) → (¬ bad-for-subset-implies-sublist (set1 , set2 ))

; now, we do induction-- if (subsetp set1 set2) and the cars are the
; same, and the cdrs are subsets

Theorem: subset-implies-sublist-aux3 (listp (set1 ) ∧ listp (set2 ) ∧ (car (set2 ) = car (set1 )) ∧ sublistp (cdr (set1 ), cdr (set2 ))) → sublistp (set1 , set2 )

Theorem: subset-implies-sublist-aux4 (listp (set1 ) ∧ listp (set2 ) ∧ (car (set2 ) = car (set1 )) ∧ bad-for-subset-implies-sublist (set1 , set2 )) → bad-for-subset-implies-sublist (cdr (set1 ), cdr (set2 ))

Theorem: subset-implies-sublist-aux5 (listp (set1 ) ∧ listp (set2 ) ∧ (car (set2 ) < car (set1 )) ∧ bad-for-subset-implies-sublist (set1 , set2 )) → bad-for-subset-implies-sublist (set1 , cdr (set2 ))

; Now, use the fact that (car set2) <= (car set1)

Theorem: subset-implies-sublist-aux6 (listp (set1 ) ∧ listp (set2 ) ∧ bad-for-subset-implies-sublist (set1 , set2 )) → ((car (set2 ) < car (set1 )) ∨ (car (set2 ) = car (set1 )))

Theorem: subset-implies-sublist-aux7 (listp (set1 ) ∧ listp (set2 ) ∧ bad-for-subset-implies-sublist (set1 , set2 )) → (bad-for-subset-implies-sublist (set1 , cdr (set2 ))

∨ bad-for-subset-implies-sublist (cdr (set1 ), cdr (set2 )))

; so there are no bad pairs, by induction -- we have to force the
; correct induction

Definition: subset-implies-sublist-kludge (set1 , set2 ) = if listp (set1 )

then if listp (set2 )

then subset-implies-sublist-kludge (cdr (set1 ), cdr (set2 )) + subset-implies-sublist-kludge (set1 , cdr (set2 ))

else 0 endif else 0 endif

Theorem: subset-implies-sublist-aux8 ¬ bad-for-subset-implies-sublist (set1 , set2 ) Event: Disable subset-implies-sublist-kludge. Event: Disable subset-implies-sublist-aux1. Event: Disable subset-implies-sublist-aux2. Event: Disable subset-implies-sublist-aux3. Event: Disable subset-implies-sublist-aux4. Event: Disable subset-implies-sublist-aux5. Event: Disable subset-implies-sublist-aux6. Event: Disable subset-implies-sublist-aux7. Theorem: subset-implies-sublist (subsetp (set1 , set2 ) ∧ setp (set1 ) ∧ setp (set2 )) → sublistp (set1 , set2 ) Event: Disable subset-implies-sublist-aux8. Event: Disable bad-for-subset-implies-sublist.

;;;;;;;;;;

; now,, we prove that every subset of set is in the power-set

Theorem: all-subsets (setp (set) ∧ setp (x) ∧ subsetp (x, set)) → (x ∈ power-set (set))

;;;;;;;;;;;;;;;;;;;  extensionality
; Two standard sets, s1, s2, are equal if they have the same members:
;  (implies
;      (and (setp s1) (setp s2) (subsetp s1 s2) (subsetp s2 s1))
;      (equal s1 s2) )
;  The proof is "by induction", but it requires a bunch of auxilliaries,
;  which we intruduce, and then disable after the proof

Definition: bad-for-ext (s1 , s2 ) = (setp (s1 )

∧ setp (s2 )

∧ subsetp (s1 , s2 ) ∧ subsetp (s2 , s1 ) ∧ (s1 ≠ s2 ))

; so, we want to show, by induction, that this can't happen.

Theorem: extensionality-aux1 (¬ listp (s1 )) → (¬ bad-for-ext (s1 , s2 ))

Theorem: extensionality-aux2 (¬ listp (s2 )) → (¬ bad-for-ext (s1 , s2 ))

; now, (bad-for-ext s1 s2) implies that s1, s2 aren't empty, and we can
; look at their first element.  By (subsetp s1 s2) (subsetp s2 s1)
; the first elements are the same.

Theorem: extensionality-aux3 (setp (s1 ) ∧ setp (s2 ) ∧ listp (s1 ) ∧ listp (s2 ) ∧ subsetp (s1 , s2 ) ∧ subsetp (s2 , s1 )) → (car (s1 ) = car (s2 ))

Theorem: extensionality-aux4 (listp (s1 ) ∧ listp (s2 ) ∧ bad-for-ext (s1 , s2 )) → (car (s1 ) = car (s2 ))

Event: Disable extensionality-aux3.

; now, we should get that the cdrs are bad

Theorem: extensionality-aux5 (listp (s1 ) ∧ listp (s2 ) ∧ bad-for-ext (s1 , s2 )) → bad-for-ext (cdr (s1 ), cdr (s2 ))

Event: Disable extensionality-aux4.

Definition: extensionality-kludge (s1 , s2 ) = if ¬ listp (s1 ) then 0

elseif ¬ listp (s2 ) then 0

else extensionality-kludge (cdr (s1 ), cdr (s2 )) endif

Theorem: extensionality-aux6 ¬ bad-for-ext (s1 , s2 )

Event: Disable extensionality-aux1.

Event: Disable extensionality-aux2.

Event: Disable extensionality-aux5.

Event: Disable extensionality-aux6.

Theorem: extensionality (setp (s1 ) ∧ setp (s2 ) ∧ subsetp (s1 , s2 ) ∧ subsetp (s2 , s1 )) → (s1 = s2 )

Event: Disable extensionality-kludge.

;;;;;;;;;;  segments
; (segment 3 6) is (3 4 5 6)
; These are special kinds of sets.  More on them will appear
; below; here we just put the defn and a few basic facts.

Definition: segment (m, n) = if (m ≤ n) ∧ (m ∈ N) ∧ (n ∈ N) then cons (m, segment (1 + m, n))

else nil endif

Theorem: size-of-segment ((m ≤ n) ∧ (m ∈ N) ∧ (n ∈ N)) → (length (segment (m, n)) = ((1 + n) − m))

Theorem: members-of-segment ((m ≤ n) ∧ (m ∈ N) ∧ (n ∈ N)) → ((x ∈ segment (m, n)) = ((x ∈ N) ∧ (x ≤ n) ∧ (m ≤ x)))

Event: Disable segment.

; for now

; some lemmas about length:

Theorem: length-of-sublist sublistp (lst1 , lst2 ) → (length (lst2 ) ≮ length (lst1 ))

Theorem: length-of-subset (setp (x) ∧ setp (y) ∧ subsetp (x, y)) → (length (y) ≮ length (x))

; a few more set facts

Theorem: empty-subset (¬ listp (s1 )) → subsetp (s1 , s2 )

Theorem: car-before-cadr (listp (cdr (s)) ∧ setp (s)) → (car (s) < cadr (s))

; now, we prove that (and (setp s1) (setp s2) (listp s1) (subsetp s1 s2))
; implies (subsetp (cdr s1) (cdr s2))
; this is by examination of cases:

Theorem: cdr-cdr-subset-aux1 (setp (s1 ) ∧ setp (s2 ) ∧ listp (s1 ) ∧ subsetp (s1 , s2 )) → ((car (s2 ) = car (s1 )) ∨ (car (s2 ) < car (s1 )))

Theorem: cdr-cdr-subset (setp (s1 ) ∧ setp (s2 ) ∧ listp (s1 ) ∧ subsetp (s1 , s2 )) → subsetp (cdr (s1 ), cdr (s2 ))

Event: Disable cdr-cdr-subset-aux1.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;                              ORDINALS                                  ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; ordinalp (the property of representing an ordinal < epsilon_0)
; and ord-lessp (the < on the ordinals) are built-in
; we define all the basic function so that they do the right thing
; on legal notations for ordinals; we don't care what they do on non-ordinals
; Ordinals are represented as:
; The natural number n represents itself.
; (alpha beta gamma . n) represents omega^alpha + omega^beta + omega^gamma + n
; For this to be legal, alpha >= beta >= gamma -- this ensures
;  that each ordinal has a unique representation

; temporarily disable some set stuff

Event: Disable subsetp.

Event: Disable setp.

Event: Disable max-is-last.

Event: Disable tail-of-a-set.

Event: Disable increasing.

Event: Disable compare-first-elts.

;;;;;;;  some basic properties of order on the ordinals

Theorem: irreflex ¬ ord-lessp (x, x)

Theorem: nocycle ¬ (ord-lessp (x, y) ∧ ord-lessp (y, x))

Theorem: no-cycle-alt ord-lessp (y, x) → (¬ ord-lessp (x, y))

Theorem: trichotomy (ordinalp (sigma) ∧ ordinalp (tau)) → ((sigma = tau) ∨ ord-lessp (sigma, tau) ∨ ord-lessp (tau, sigma))

Theorem: transitivity (ord-lessp (alpha, beta) ∧ ord-lessp (beta, gamma)) → ord-lessp (alpha, gamma)

Theorem: transitivity-alt (ordinalp (alpha) ∧ ordinalp (beta) ∧ ordinalp (gamma) ∧ (¬ ord-lessp (beta, alpha)) ∧ ord-lessp (beta, gamma)) → ord-lessp (alpha, gamma)

Theorem: ords-below-2 (ordinalp (alpha) ∧ (¬ ord-lessp (1, alpha))) → ((alpha = 0) ∨ (alpha = 1))

Theorem: postive-ord-lessp (ordinalp (gamma) ∧ ordinalp (delta) ∧ ord-lessp (gamma, delta)) → ord-lessp (0, delta)

;;;;;;;  successors and limit ordinals

Definition: successorp (alpha) = if listp (alpha) then successorp (cdr (alpha))

else 0 < alpha endif

Definition: limitp (alpha) = (listp (alpha) ∧ (¬ successorp (alpha)))

Theorem: successors-are-positive (ordinalp (alpha) ∧ successorp (alpha)) → ord-lessp (0, alpha)

Theorem: three-kinds ordinalp (alpha) → (limitp (alpha) ∨ successorp (alpha) ∨ (alpha = 0))

Definition: successor (alpha) = if listp (alpha) then cons (car (alpha), successor (cdr (alpha)))

else 1 + alpha endif

; the successor of 8 is 9
; the successor of (alpha beta . 8) is (alpha beta . 9)

Theorem: successor-is-an-ordinal ordinalp (alpha) → ordinalp (successor (alpha))

Theorem: successor-is-a-successor successorp (successor (alpha))

Theorem: successor-is-bigger ord-lessp (alpha, successor (alpha))

Theorem: succ-preserves-order ord-lessp (alpha, beta) → ord-lessp (successor (alpha), successor (beta))

Theorem: nothing-between ¬ (ord-lessp (alpha, beta) ∧ ord-lessp (beta, successor (alpha)))

Definition: predecessor (alpha) = if listp (alpha) then cons (car (alpha), predecessor (cdr (alpha)))

else alpha − 1 endif

; these are inverses of each other

Theorem: predecessor-suc ordinalp (alpha) → (predecessor (successor (alpha)) = alpha)

Theorem: suc-predecessor (ordinalp (alpha) ∧ successorp (alpha)) → (successor (predecessor (alpha)) = alpha)

Theorem: predecessor-is-an-ordinal ordinalp (alpha) → ordinalp (predecessor (alpha))

Theorem: predecessor-is-smaller (ordinalp (alpha) ∧ successorp (alpha)) → ord-lessp (predecessor (alpha), alpha)

Theorem: predecessor-of-0 predecessor (0) = 0

Theorem: predecessor-of-limit (ordinalp (alpha) ∧ limitp (alpha)) → (predecessor (alpha) = alpha)

;;;;;;;;;;  ord-leq :  a <= on ordinals

Definition: ord-leq (alpha, beta) = (¬ ord-lessp (beta, alpha))

Theorem: leq-as-an-or (ordinalp (rho) ∧ ordinalp (sigma) ∧ ord-leq (rho, sigma)) → (ord-lessp (rho, sigma) ∨ (rho = sigma))

Theorem: leq-0 (ordinalp (delta) ∧ ord-leq (delta, 0)) → ((delta = 0) = t)

Theorem: cars-go-down ordinalp (beta) → ord-leq (cadr (beta), car (beta))

Theorem: ord-leq-is-transitive (ordinalp (alpha) ∧ ordinalp (beta) ∧ ordinalp (gamma) ∧ ord-leq (alpha, beta) ∧ ord-leq (beta, gamma)) → ord-leq (alpha, gamma)

Theorem: ord-leq-zero (ordinalp (delta) ∧ ord-leq (delta, 0)) → ((delta = 0) = t)

Theorem: cars-are-ordinals ordinalp (alpha) → ordinalp (car (alpha))

Theorem: cdrs-are-ordinals ordinalp (alpha) → ordinalp (cdr (alpha))

; Now, we want to prove that (cdr alpha) < alpha
; this should be trivial but seems to require help

Definition: bad-for-cdrs-are-smaller (alpha) = (ordinalp (alpha)

∧ listp (alpha)

∧ (¬ ord-lessp (cdr (alpha), alpha)))

Theorem: cdrs-are-smaller-aux1 (alpha ≃ nil) → (¬ bad-for-cdrs-are-smaller (alpha))

Theorem: cdrs-are-smaller-aux2 (cdr (alpha) ≃ nil) → (¬ bad-for-cdrs-are-smaller (alpha))

Theorem: cdrs-are-smaller-aux3 (ordinalp (alpha) ∧ listp (cdr (alpha)) ∧ (car (alpha) = cadr (alpha)) ∧ ord-lessp (cddr (alpha), cdr (alpha))) → ord-lessp (cdr (alpha), alpha)

Theorem: cdrs-are-smaller-aux4 (ordinalp (alpha) ∧ listp (cdr (alpha)) ∧ ord-lessp (car (alpha), cadr (alpha))) → ord-lessp (cdr (alpha), alpha)

Theorem: cdrs-are-smaller-aux5 (ordinalp (alpha) ∧ listp (cdr (alpha))) → ((car (alpha) = cadr (alpha)) ∨ ord-lessp (cadr (alpha), car (alpha)))

Event: Disable cdrs-are-smaller-aux3.

Event: Disable cdrs-are-smaller-aux4.

Event: Disable cdrs-are-smaller-aux5.

Theorem: cdrs-are-smaller-aux6 (ordinalp (alpha) ∧ listp (cdr (alpha)) ∧ ord-lessp (cddr (alpha), cdr (alpha))) → ord-lessp (cdr (alpha), alpha)

Theorem: cdrs-are-smaller-aux7 (listp (cdr (alpha)) ∧ bad-for-cdrs-are-smaller (alpha)) → bad-for-cdrs-are-smaller (cdr (alpha))

Event: Disable cdrs-are-smaller-aux2.

Theorem: cdrs-are-smaller-aux8 bad-for-cdrs-are-smaller (alpha) → bad-for-cdrs-are-smaller (cdr (alpha))

Theorem: cdrs-are-smaller-aux9 ¬ bad-for-cdrs-are-smaller (alpha)

Event: Disable cdrs-are-smaller-aux1.

Event: Disable cdrs-are-smaller-aux6.

Event: Disable cdrs-are-smaller-aux7.

Event: Disable cdrs-are-smaller-aux8.

Event: Disable cdrs-are-smaller-aux9.

Theorem: cdrs-are-smaller (ordinalp (alpha) ∧ listp (alpha)) → ord-lessp (cdr (alpha), alpha)

Event: Disable bad-for-cdrs-are-smaller.

Theorem: cars-of-smaller-ordinals (ordinalp (alpha) ∧ ordinalp (beta) ∧ ord-lessp (alpha, beta)) → (ord-lessp (car (alpha), car (beta)) ∨ (car (alpha) = car (beta)))

Theorem: limit-not-succ (ordinalp (alpha) ∧ ordinalp (delta) ∧ limitp (alpha)) → (successor (delta) ≠ alpha)

Theorem: succ-below-limit (ordinalp (alpha) ∧ ordinalp (delta) ∧ ord-lessp (delta, alpha) ∧ limitp (alpha)) → ord-lessp (successor (delta), alpha)

Theorem: irreflex-of-ord-leq (ordinalp (sigma) ∧ ordinalp (tau) ∧ ord-leq (sigma, tau) ∧ ord-leq (tau, sigma)) → ((sigma = tau) = t)

Theorem: transitivity-alt2 (ordinalp (alpha) ∧ ordinalp (beta) ∧ ordinalp (gamma) ∧ ord-lessp (alpha, beta)

∧ ord-leq (beta, gamma)) → ord-lessp (alpha, gamma)

;;;;;;;;;;;;;;;;;;;;  multiplicities
; (mult delta alpha) is the coefficient of omega^delta in the
; Cantor normal form of alpha.  We want to define this, and
; prove that alpha is determined by its multiplicities
; This is slightly messy, since delta = 0 is a special case
; in the Boyer-Moore notation -- let's do that separately
; (mult 0 alpha) will be (number-part alpha)

Definition: number-part (alpha) = if alpha ≃ nil then alpha

else number-part (cdr (alpha)) endif

Theorem: number-part-is-a-number ordinalp (alpha) → (number-part (alpha) ∈ N)

; for delta > 0, (mult delta alpha) = (pos-mult delta alpha)

Definition: pos-mult (delta, alpha) = if alpha ≃ nil then 0

elseif delta = car (alpha) then 1 + pos-mult (delta, cdr (alpha))

else pos-mult (delta, cdr (alpha)) endif

Theorem: pos-mult-is-a-number pos-mult (delta, alpha) ∈ N

Definition: mult (delta, alpha) = if delta = 0 then number-part (alpha)

else pos-mult (delta, alpha) endif

Theorem: mult-is-a-number ordinalp (alpha) → (mult (delta, alpha) ∈ N)

Theorem: mult-in-a-number ((alpha ∈ N) ∧ (delta ≠ 0)) → (mult (delta, alpha) = 0)

; now, we prove if delta > (car alpha), (mult delta alpha) = 0
; this is true for numbers alpha because the car of a non-list = 0
; Prover needs help to find the correct induction

Definition: bad-for-bound-on-mult (delta, alpha) = (ordinalp (alpha)

∧ ordinalp (delta)

∧ ord-lessp (car (alpha), delta) ∧ (mult (delta, alpha) ≠ 0))

; we want to show this can't happen

Theorem: bound-on-mult-aux1 (alpha ≃ nil) → (¬ bad-for-bound-on-mult (delta, alpha))

Theorem: bound-on-mult-aux2 (listp (alpha) ∧ ordinalp (alpha)) → (¬ ord-lessp (car (alpha), cadr (alpha)))

Theorem: bound-on-mult-aux3 ordinalp (alpha) → ordinalp (car (alpha))

Theorem: bound-on-mult-aux4 ordinalp (alpha) → ordinalp (cadr (alpha))

Theorem: bound-on-mult-aux5 (listp (alpha) ∧ ordinalp (alpha) ∧ ordinalp (delta) ∧ ord-lessp (car (alpha), delta)) → ord-lessp (cadr (alpha), delta)

Theorem: bound-on-mult-aux6 (listp (alpha) ∧ bad-for-bound-on-mult (delta, alpha)) → bad-for-bound-on-mult (delta, cdr (alpha))

Definition: bound-on-mult-kludge (alpha) = if alpha ≃ nil then 0

else bound-on-mult-kludge (cdr (alpha)) endif

Theorem: bound-on-mult-aux7 ¬ bad-for-bound-on-mult (delta, alpha)

Theorem: bound-on-mult (ordinalp (alpha) ∧ ordinalp (delta) ∧ ord-lessp (car (alpha), delta)) → (mult (delta, alpha) = 0)

Event: Disable bound-on-mult-aux1. Event: Disable bound-on-mult-aux2. Event: Disable bound-on-mult-aux3. Event: Disable bound-on-mult-aux4. Event: Disable bound-on-mult-aux5. Event: Disable bound-on-mult-aux6. Event: Disable bound-on-mult-aux7. Event: Disable bad-for-bound-on-mult. Event: Disable bound-on-mult-kludge.

; now, (different-mult alpha beta) returns a delta
; such that (mult delta alpha) != (mult delta beta)

Definition: different-mult (alpha, beta) = if car (alpha) = car (beta)

then if listp (alpha) then different-mult (cdr (alpha), cdr (beta))

else 0 endif elseif ord-lessp (car (alpha), car (beta)) then car (beta) else car (alpha) endif

; summarize the features of the definition

Theorem: different-mult-is-ord (ordinalp (alpha) ∧ ordinalp (beta)) → ordinalp (different-mult (alpha, beta)) Theorem: different-mult-for-numbers ((alpha ∈ N) ∧ (beta ∈ N)) → (different-mult (alpha, beta) = 0)

;;;;;;;;;;  The following is causing us a lot of trouble:

Event: Disable transitivity-alt.

Event: Disable irreflex-of-ord-leq.

Theorem: different-mult-number-list ((alpha ∈ N) ∧ ordinalp (beta) ∧ listp (beta)) → (different-mult (alpha, beta) = car (beta))

Theorem: different-mult-list-number ((beta ∈ N) ∧ ordinalp (alpha) ∧ listp (alpha)) → (different-mult (alpha, beta) = car (alpha))

Theorem: different-mult-for-lists-same-car (ordinalp (alpha) ∧ ordinalp (beta) ∧ listp (alpha) ∧ listp (beta) ∧ (car (alpha) = car (beta))) → (different-mult (alpha, beta) = different-mult (cdr (alpha), cdr (beta)))

Theorem: different-mult-for-smaller-car ord-lessp (car (alpha), car (beta)) → (different-mult (alpha, beta) = car (beta))

Theorem: different-mult-for-larger-car ord-lessp (car (beta), car (alpha)) → (different-mult (alpha, beta) = car (alpha))

Event: Disable different-mult.

; now, we have to prove that it works
; this needs some help

Definition: bad-for-different-mult-works (alpha, beta) = (ordinalp (alpha)

∧ ordinalp (beta) ∧ (alpha ≠ beta) ∧ (mult (different-mult (alpha, beta), alpha)

= mult (different-mult (alpha, beta), beta)))

; if they have different cars, this should follow
; by "bound-on-mult"

Theorem: different-mult-works-aux1 (ordinalp (sigma) ∧ (car (sigma) ≠ 0)) → (mult (car (sigma), sigma) ≠ 0)

; the following is causing us a lot of trouble

Event: Disable no-cycle-alt.

Event: Disable ord-leq-is-transitive.

Theorem: different-mult-works-aux2 ord-lessp (car (alpha), car (beta)) → (¬ bad-for-different-mult-works (alpha, beta))

Theorem: different-mult-works-aux3 ord-lessp (car (beta), car (alpha)) → (¬ bad-for-different-mult-works (alpha, beta))

Theorem: different-mult-works-aux4 ((alpha ∈ N) ∧ (beta ∈ N)) → (¬ bad-for-different-mult-works (alpha, beta))

Theorem: different-mult-works-aux5 ((alpha ∈ N) ∧ ordinalp (beta) ∧ listp (beta)) → ord-lessp (car (alpha), car (beta))

Theorem: different-mult-works-aux6 ((alpha ≃ nil) ∧ listp (beta)) → (¬ bad-for-different-mult-works (alpha, beta))

Theorem: different-mult-works-aux7 (listp (alpha) ∧ (beta ≃ nil)) → (¬ bad-for-different-mult-works (alpha, beta))

Theorem: different-mult-works-aux8 ((alpha ≃ nil) ∧ (beta ≃ nil)) → (¬ bad-for-different-mult-works (alpha, beta))

Event: Disable different-mult-works-aux4.

Event: Disable different-mult-works-aux5.

Event: Disable different-mult-works-aux6.

Event: Disable different-mult-works-aux7.

Event: Disable different-mult-works-aux8.

Theorem: different-mult-works-aux9 ((alpha ≃ nil) ∨ (beta ≃ nil)) → (¬ bad-for-different-mult-works (alpha, beta))

; so, they are both compound

Event: Disable different-mult-works-aux1.

Event: Disable different-mult-works-aux2.

Event: Disable different-mult-works-aux3.

Theorem: different-mult-works-aux10 (car (beta) ≠ car (alpha)) → (¬ bad-for-different-mult-works (alpha, beta))

; so, if they are bad,  they are both compound and their cars
; are the same

Theorem: same-mult-for-cdr (listp (alpha) ∧ listp (beta) ∧ (car (alpha) = car (beta)) ∧ (mult (delta, alpha) = mult (delta, beta))) → (mult (delta, cdr (alpha)) = mult (delta, cdr (beta)))

Theorem: different-mult-works-aux11 (listp (alpha) ∧ listp (beta) ∧ (car (alpha) = car (beta)) ∧ bad-for-different-mult-works (alpha, beta)) → bad-for-different-mult-works (cdr (alpha), cdr (beta))

Event: Disable different-mult-works-aux10.

Theorem: different-mult-works-aux12 (listp (alpha) ∧ listp (beta) ∧ bad-for-different-mult-works (alpha, beta)) → bad-for-different-mult-works (cdr (alpha), cdr (beta))

Definition: different-mult-works-kludge (alpha, beta) = if listp (alpha) ∧ listp (beta)

then different-mult-works-kludge (cdr (alpha), cdr (beta))

else 0 endif

Theorem: different-mult-works-aux13 ¬ bad-for-different-mult-works (alpha, beta)

Event: Disable different-mult-works-kludge.

Event: Disable different-mult-works-aux9.

Event: Disable different-mult-works-aux11.

Event: Disable different-mult-works-aux12.

Event: Disable different-mult-works-aux13.

Theorem: different-mult-works (ordinalp (alpha) ∧ ordinalp (beta) ∧ (alpha ≠ beta)) → (mult (different-mult (alpha, beta), alpha)

≠ mult (different-mult (alpha, beta), beta))

Event: Disable bad-for-different-mult-works.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;                          NATURAL SUM                                   ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;  alpha # lambda
; this is defined by merging the Cantor Normal Forms
; as with the above, there are two cases because
; of the special treatment of numbers
; we must verify 5 things:
; 0. this is an ordinal
; 1. bound-below:  alpha # lambda > lambda  if alpha != 0
; 2. bound above:  car(alpha # lambda) is the larger of the two cars
; 3. monotonic:  alpha < beta --> alpha # lambda < beta # lambda
; 4. mult-is-additive:  mult(delta, alpha # lambda) =

;     mult(delta, alpha) + mult(delta, lambda)
;   this will easily imply that # is assoc and commutative
; we do this for lambda in omega and lambda = (sigma . 0)
;  and then put them together
; first alpha # n when n is a number

Definition: num-sharp (alpha, n) = if alpha ≃ nil then alpha + n

else cons (car (alpha), num-sharp (cdr (alpha), n)) endif

Theorem: num-sharp-is-an-ordinal (ordinalp (alpha) ∧ (n ∈ N)) → ordinalp (num-sharp (alpha, n))

Theorem: num-sharp-and-zero ordinalp (alpha) → (num-sharp (alpha, 0) = alpha)

Theorem: num-sharp-and-successor num-sharp (alpha, 1) = successor (alpha)

Theorem: num-sharp-gets-bigger (ordinalp (alpha) ∧ (n ∈ N) ∧ (n ≠ 0)) → ord-lessp (alpha, num-sharp (alpha, n))

Theorem: car-of-num-sharp (n ∈ N) → (car (num-sharp (alpha, n)) = car (alpha))

Theorem: num-sharp-is-monotonic (ordinalp (alpha) ∧ ordinalp (beta) ∧ (n ∈ N) ∧ ord-lessp (alpha, beta)) → ord-lessp (num-sharp (alpha, n), num-sharp (beta, n))

; check out multiplicities

Theorem: number-part-of-num-sharp number-part (num-sharp (alpha, n)) = (number-part (alpha) + n)

Theorem: pos-mult-of-num-sharp pos-mult (delta, num-sharp (alpha, n)) = pos-mult (delta, alpha)

Theorem: mult-of-num-sharp ((n ∈ N) ∧ ordinalp (delta) ∧ ordinalp (alpha)) → (mult (delta, num-sharp (alpha, n))

= (mult (delta, alpha) + mult (delta, n)))

; now, alpha # omega^delta where delta > 0
; this is (insert delta alpha) -- we insert delta in the CNF of alpha

Definition: insert (delta, alpha) = if alpha ≃ nil then cons (delta, alpha)

elseif ord-lessp (delta, car (alpha))

then cons (car (alpha), insert (delta, cdr (alpha)))

else cons (delta, alpha) endif

; the car is the larger of the two cars

Theorem: car-of-insert-a (ord-lessp (delta, car (alpha)) ∧ ordinalp (alpha)) → (car (insert (delta, alpha)) = car (alpha))

Theorem: car-of-insert-b (¬ ord-lessp (delta, car (alpha))) → (car (insert (delta, alpha)) = delta)

Theorem: insert-is-an-ordinal (ordinalp (alpha) ∧ ordinalp (delta) ∧ (delta ≠ 0)) → ordinalp (insert (delta, alpha))

; now, we want to show that alpha < (insert delta alpha)
; this need some help

Theorem: insert-is-cons (ordinalp (alpha) ∧ ordinalp (delta) ∧ (delta ≠ 0) ∧ (¬ ord-lessp (delta, car (alpha)))) → (insert (delta, alpha) = cons (delta, alpha))

Theorem: insert-is-bigger-aux1 (ordinalp (alpha) ∧ ordinalp (delta) ∧ (delta ≠ 0) ∧ listp (alpha) ∧ (¬ ord-lessp (delta, car (alpha)))) → ord-lessp (alpha, insert (delta, alpha))

Definition: bad-for-insert-is-bigger (alpha, delta) = (ordinalp (alpha)

∧ ordinalp (delta) ∧ (delta ≠ 0) ∧ (¬ ord-lessp (alpha, insert (delta, alpha))))

Theorem: insert-is-bigger-aux2 (alpha ≃ nil) → (¬ bad-for-insert-is-bigger (alpha, delta))

Theorem: insert-is-bigger-aux3 (listp (alpha) ∧ (¬ ord-lessp (delta, car (alpha)))) → (¬ bad-for-insert-is-bigger (alpha, delta))

Theorem: insert-small-ordinal (ordinalp (alpha) ∧ listp (alpha) ∧ ord-lessp (delta, car (alpha))) → (insert (delta, alpha) = cons (car (alpha), insert (delta, cdr (alpha))))

Theorem: insert-is-bigger-aux4 (ordinalp (alpha) ∧ listp (alpha) ∧ ord-lessp (delta, car (alpha)) ∧ ord-lessp (cdr (alpha), insert (delta, cdr (alpha)))) → ord-lessp (alpha, insert (delta, alpha))

Theorem: insert-is-bigger-aux5 (listp (alpha) ∧ ord-lessp (delta, car (alpha)) ∧ bad-for-insert-is-bigger (alpha, delta)) → bad-for-insert-is-bigger (cdr (alpha), delta)

Theorem: insert-is-bigger-aux6 (listp (alpha) ∧ bad-for-insert-is-bigger (alpha, delta)) → bad-for-insert-is-bigger (cdr (alpha), delta)

Theorem: insert-is-bigger-aux7 ¬ bad-for-insert-is-bigger (alpha, delta)

Theorem: insert-is-bigger (ordinalp (alpha) ∧ ordinalp (delta) ∧ (delta ≠ 0)) → ord-lessp (alpha, insert (delta, alpha))

Event: Disable insert-is-bigger-aux1.

Event: Disable insert-is-bigger-aux2.

Event: Disable insert-is-bigger-aux3.

Event: Disable insert-is-bigger-aux4.

Event: Disable insert-is-bigger-aux5.

Event: Disable insert-is-bigger-aux6.

Event: Disable insert-is-bigger-aux7.

;;;; now --  check out multiplicities

Theorem: number-part-of-insert number-part (insert (delta, alpha)) = number-part (alpha)

Theorem: pos-mult-same pos-mult (delta, insert (delta, alpha)) = (1 + pos-mult (delta, alpha))

Theorem: pos-mult-different (x ≠ delta) → (pos-mult (x, insert (delta, alpha)) = pos-mult (x, alpha))

Theorem: mult-of-insert-a (ordinalp (alpha) ∧ (sigma ≠ delta)) → (mult (sigma, insert (delta, alpha)) = mult (sigma, alpha))

Theorem: mult-of-insert-b (ordinalp (alpha) ∧ (delta ≠ 0)) → (mult (delta, insert (delta, alpha)) = (1 + mult (delta, alpha)))

; we still have to check monotonicity --
; but first, define #  and prove it's assoc and commut
; just to make sure we've got it right.

Definition: sharp (alpha, beta) = if beta ≃ nil then num-sharp (alpha, beta)

else insert (car (beta), sharp (alpha, cdr (beta))) endif

Theorem: sharp-is-an-ordinal (ordinalp (alpha) ∧ ordinalp (beta)) → ordinalp (sharp (alpha, beta))

Theorem: sharp-with-0 ordinalp (alpha) → (sharp (alpha, 0) = alpha)

Theorem: sharp-gets-bigger (ordinalp (alpha) ∧ ordinalp (beta) ∧ (beta ≠ 0)) → ord-lessp (alpha, sharp (alpha, beta))

; now we prove that (car (sharp alpha beta)) =  (car alpha)
; in the case that (car alpha) >= (car beta) -- the other way
; around will follow once we prove # is commutative

Theorem: car-of-insert-aux1 ((delta = car (alpha)) ∧ ordinalp (alpha) ∧ ordinalp (delta)) → (car (insert (delta, alpha)) = car (alpha))

Theorem: car-of-insert-c (ord-leq (delta, car (alpha)) ∧ ordinalp (alpha) ∧ ordinalp (delta)) → (car (insert (delta, alpha)) = car (alpha))

Theorem: car-of-sharp-aux1 ((¬ listp (beta)) ∧ ordinalp (alpha) ∧ ordinalp (beta)) → (car (sharp (alpha, beta)) = car (alpha))

Theorem: car-of-sharp-aux2 (ord-leq (car (beta), car (alpha)) ∧ ordinalp (alpha) ∧ ordinalp (beta)) → ord-leq (cadr (beta), car (alpha))

Theorem: car-of-sharp-a (ord-leq (car (beta), car (alpha)) ∧ ordinalp (alpha) ∧ ordinalp (beta)) → (car (sharp (alpha, beta)) = car (alpha))

Event: Disable car-of-sharp-aux1.

Event: Disable car-of-sharp-aux2.

; now, check out that multiplicities are additive

Definition: bad-for-mult-of-sharp (sigma, alpha, beta) = (ordinalp (sigma)

∧ ordinalp (alpha) ∧ ordinalp (beta) ∧ (mult (sigma, sharp (alpha, beta))

≠ (mult (sigma, alpha) + mult (sigma, beta))))

Theorem: mult-of-sharp-aux1 (beta ≃ nil) → (¬ bad-for-mult-of-sharp (sigma, alpha, beta))

Theorem: mult-of-sharp-aux2 (listp (beta) ∧ ordinalp (beta)) → (car (beta) ≠ 0)

Theorem: mult-of-sharp-aux3 (listp (beta) ∧ (sigma ≠ car (beta)) ∧ ordinalp (sigma) ∧ ordinalp (alpha) ∧ ordinalp (beta)) → (mult (sigma, sharp (alpha, cdr (beta))) = mult (sigma, sharp (alpha, beta)))

Theorem: mult-of-sharp-aux4 (listp (beta) ∧ (sigma ≠ car (beta))) → (mult (sigma, cdr (beta)) = mult (sigma, beta))

Theorem: mult-of-sharp-aux5 (listp (beta) ∧ bad-for-mult-of-sharp (sigma, alpha, beta) ∧ (sigma ≠ car (beta))) → bad-for-mult-of-sharp (sigma, alpha, cdr (beta))

Theorem: mult-of-sharp-aux6 (listp (beta) ∧ ordinalp (beta)) → (mult (car (beta), beta) = (1 + mult (car (beta), cdr (beta))))

Theorem: mult-of-sharp-aux7 (listp (beta) ∧ bad-for-mult-of-sharp (car (beta), alpha, beta)) → bad-for-mult-of-sharp (car (beta), alpha, cdr (beta))

Theorem: mult-of-sharp-aux8 (listp (beta) ∧ bad-for-mult-of-sharp (sigma, alpha, beta)) → bad-for-mult-of-sharp (sigma, alpha, cdr (beta))

Theorem: mult-of-sharp-aux9 ¬ bad-for-mult-of-sharp (sigma, alpha, beta)

Theorem: mult-of-sharp (ordinalp (sigma) ∧ ordinalp (alpha) ∧ ordinalp (beta)) → (mult (sigma, sharp (alpha, beta))

= (mult (sigma, alpha) + mult (sigma, beta)))

Event: Disable bad-for-mult-of-sharp.

Event: Disable mult-of-sharp-aux1. Event: Disable mult-of-sharp-aux2. Event: Disable mult-of-sharp-aux3. Event: Disable mult-of-sharp-aux4. Event: Disable mult-of-sharp-aux5. Event: Disable mult-of-sharp-aux6. Event: Disable mult-of-sharp-aux7. Event: Disable mult-of-sharp-aux8. Event: Disable mult-of-sharp-aux9.

; now, we should show that sharp is commutative and associative

Theorem: commut-of-sharp (ordinalp (alpha) ∧ ordinalp (beta)) → (sharp (alpha, beta) = sharp (beta, alpha)) Theorem: assoc-of-sharp (ordinalp (alpha) ∧ ordinalp (beta) ∧ ordinalp (gamma)) → (sharp (sharp (alpha, beta), gamma) = sharp (alpha, sharp (beta, gamma)))

;;; now, we can finish the discussion of the car of a #

Theorem: car-of-sharp-b (ord-leq (car (alpha), car (beta)) ∧ ordinalp (alpha) ∧ ordinalp (beta)) → (car (sharp (alpha, beta)) = car (beta))

; now, turn to monotonicity:  alpha < beta --> alpha # lambda < beta # lambda
; this should follow by induction if we can do monotonicty of insert
; first, do it in the case that delta >= (car beta)

Event: Disable car-of-insert-aux1.

Theorem: monotonicity-of-insert-aux1 (ordinalp (alpha) ∧ ordinalp (beta) ∧ ordinalp (delta) ∧ (¬ ord-lessp (delta, car (beta))) ∧ (delta ≠ 0) ∧ ord-lessp (alpha, beta)) → ord-lessp (insert (delta, alpha), insert (delta, beta))

; now, consider case that delta < (car beta)
; first, suppose also (car alpha) < (car beta)
; Then (car (insert delta alpha)) < (car beta)
; so (insert delta alpha) < beta < (insert delta beta)

Theorem: monotonicity-of-insert-aux2 (ordinalp (alpha) ∧ ordinalp (sigma) ∧ ordinalp (delta) ∧ ord-lessp (delta, sigma) ∧ ord-lessp (car (alpha), sigma)) → ord-lessp (car (insert (delta, alpha)), sigma)

Theorem: monotonicity-of-insert-aux3 (ordinalp (alpha) ∧ ordinalp (beta) ∧ ordinalp (delta) ∧ ord-lessp (delta, car (beta)) ∧ (delta ≠ 0) ∧ ord-lessp (car (alpha), car (beta))) → ord-lessp (insert (delta, alpha), beta)

Theorem: monotonicity-of-insert-aux4 (ordinalp (alpha) ∧ ordinalp (beta) ∧ ordinalp (delta) ∧ ord-lessp (delta, car (beta)) ∧ (delta ≠ 0) ∧ ord-lessp (car (alpha), car (beta))) → ord-lessp (insert (delta, alpha), insert (delta, beta))

; this concludes the case that delta < (car beta) and (car alpha) < (car beta)
; the remaining case is that delta < (car beta) and (car alpha) = (car beta)
; this should proceed by induction

Definition: bad-for-monotonicity-of-insert (alpha, beta, delta) = (ordinalp (alpha)

∧ ordinalp (beta) ∧ ordinalp (delta) ∧ (delta ≠ 0) ∧ ord-lessp (alpha, beta) ∧ (¬ ord-lessp (insert (delta, alpha), insert (delta, beta))))

Theorem: monotonicity-of-insert-aux5 bad-for-monotonicity-of-insert (alpha, beta, delta) → ord-lessp (delta, car (beta))

Theorem: monotonicity-of-insert-aux6 bad-for-monotonicity-of-insert (alpha, beta, delta) → (¬ ord-lessp (car (alpha), car (beta)))

Theorem: monotonicity-of-insert-aux7 bad-for-monotonicity-of-insert (alpha, beta, delta) → (car (alpha) = car (beta))

; now we know that any counter-example satisfies
; delta  car alpha = car beta
; so, the insert's start off with delta, and we can use induction
; check that alpha and beta are not numbers

Theorem: monotonicity-of-insert-aux8 bad-for-monotonicity-of-insert (alpha, beta, delta) → (listp (alpha) ∧ listp (beta))

Theorem: monotonicity-of-insert-aux9 bad-for-monotonicity-of-insert (alpha, beta, delta) → bad-for-monotonicity-of-insert (cdr (alpha), cdr (beta), delta)

Definition: monotonicity-of-insert-kludge (alpha, beta) = if listp (alpha) ∧ listp (beta)

then monotonicity-of-insert-kludge (cdr (alpha), cdr (beta))

else 0 endif Theorem: monotonicity-of-insert-aux10 ¬ bad-for-monotonicity-of-insert (alpha, beta, delta) Theorem: monotonicity-of-insert (ordinalp (alpha) ∧ ordinalp (beta) ∧ ordinalp (delta) ∧ (delta ≠ 0) ∧ ord-lessp (alpha, beta)) → ord-lessp (insert (delta, alpha), insert (delta, beta)) Event: Disable monotonicity-of-insert-aux1. Event: Disable monotonicity-of-insert-aux2. Event: Disable monotonicity-of-insert-aux3. Event: Disable monotonicity-of-insert-aux4. Event: Disable monotonicity-of-insert-aux5. Event: Disable monotonicity-of-insert-aux6. Event: Disable monotonicity-of-insert-aux7. Event: Disable monotonicity-of-insert-aux8. Event: Disable monotonicity-of-insert-aux9. Event: Disable monotonicity-of-insert-aux10. Event: Disable monotonicity-of-insert-kludge. Event: Disable bad-for-monotonicity-of-insert.

; now, we can prove monotonicity of sharp

Theorem: monotonicity-of-sharp (ordinalp (alpha) ∧ ordinalp (beta) ∧ ordinalp (lambda) ∧ ord-lessp (alpha, beta)) → ord-lessp (sharp (alpha, lambda), sharp (beta, lambda))

;;;;;;;  disable a bunch of stuff --  these are causing
;;;; a lot of trouble by firing when we don't want them to:

Event: Disable ord-lessp.

Event: Disable ord-leq.

Event: Disable leq-0.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;                          NORMS AND PRED                                ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;   norms = count ;

Definition: norm (x) = count (x)

; This defn is just so that we can disable norm without disabling count

Theorem: norm-is-a-number norm (x) ∈ N

Theorem: norm-of-a-number (n ∈ N) → (norm (n) = n)

Theorem: norm-of-successor ordinalp (alpha) → (norm (successor (alpha)) = (1 + norm (alpha)))

Theorem: norm-of-predecessor (ordinalp (alpha) ∧ successorp (alpha)) → (norm (predecessor (alpha)) = (norm (alpha) − 1))

Theorem: norm-of-cons listp (alpha) → (norm (alpha) = (1 + (norm (car (alpha)) + norm (cdr (alpha)))))

Theorem: norm-non-zero listp (alpha) → (norm (alpha) ≠ 0)

Event: Disable norm.

; now, (norm-up-to n) will contain all ordinals with
; norm n or below, plus a lot of other stuff

Definition: norm-up-to (n) = if n ≃ 0 then list (0)

else append (segment (0, n), product (norm-up-to (n − 1), norm-up-to (n − 1))) endif

Theorem: norm-up-to-big-enuf-aux1 (ordinalp (alpha) ∧ (norm (alpha) ≤ n) ∧ (alpha ≃ nil)) → (alpha ∈ norm-up-to (n))

; now, we just consider (listp alpha)

Theorem: norm-up-to-big-enuf-aux2 (listp (alpha) ∧ (norm (alpha) ≤ n)) → (n ≄ 0)

Theorem: norm-up-to-big-enuf-aux3 (ordinalp (alpha) ∧ (norm (alpha) ≤ n) ∧ (n ≃ 0)) → (alpha ∈ norm-up-to (n))

Theorem: norm-up-to-big-enuf-aux4 ((x ∈ norm-up-to (n)) ∧ (y ∈ norm-up-to (n))) → (cons (x, y) ∈ norm-up-to (1 + n))

Event: Disable norm-up-to.

Event: Disable norm-of-cons.

; needed for next defn to work

Definition: norm-up-to-big-enuf-kludge (alpha, n) = if listp (alpha) ∧ (n ≄ 0)

then norm-up-to-big-enuf-kludge (car (alpha), n − 1)

+ norm-up-to-big-enuf-kludge (cdr (alpha), n − 1) else 0 endif Event: Enable norm-of-cons.

Definition: bad-for-norm-up-to-big-enuf (alpha, n) = (ordinalp (alpha)

∧ (norm (alpha) ≤ n)

∧ (alpha ∉ norm-up-to (n)))

Theorem: norm-up-to-big-enuf-aux5 bad-for-norm-up-to-big-enuf (alpha, n) → (listp (alpha) ∧ (n ≄ 0))

Theorem: norm-up-to-big-enuf-aux6 (listp (alpha) ∧ (n ≄ 0) ∧ (¬ bad-for-norm-up-to-big-enuf (car (alpha), n − 1)) ∧ (¬ bad-for-norm-up-to-big-enuf (cdr (alpha), n − 1))) → (¬ bad-for-norm-up-to-big-enuf (alpha, n))

Theorem: norm-up-to-big-enuf-aux7 ¬ bad-for-norm-up-to-big-enuf (alpha, n)

Theorem: norm-up-to-big-enuf (ordinalp (alpha) ∧ (norm (alpha) ≤ n)) → (alpha ∈ norm-up-to (n))

Event: Disable norm-up-to-big-enuf-aux1.

Event: Disable norm-up-to-big-enuf-aux2.

Event: Disable norm-up-to-big-enuf-aux3.

Event: Disable norm-up-to-big-enuf-aux4.

Event: Disable norm-up-to-big-enuf-aux5.

Event: Disable norm-up-to-big-enuf-aux6.

Event: Disable norm-up-to-big-enuf-aux7.

Event: Disable norm-up-to-big-enuf-kludge.

Event: Disable bad-for-norm-up-to-big-enuf.

;;;; norm of sharp
; prove that the norm of alpha # beta is the sum of the norms

Theorem: norm-of-num-sharp (ordinalp (alpha) ∧ (n ∈ N)) → (norm (num-sharp (alpha, n)) = (norm (alpha) + norm (n)))

Theorem: norm-of-insert ordinalp (alpha) → (norm (insert (delta, alpha)) = (1 + (norm (delta) + norm (alpha))))

Theorem: norm-of-sharp (ordinalp (alpha) ∧ ordinalp (beta)) → (norm (sharp (alpha, beta)) = (norm (alpha) + norm (beta)))

;;;;;;;;;;;;;;;;;;  (pred alpha n)  = {alpha}(n)
; this is 0 if alpha = 0   ; otherwise, it's the largest ordinal
;   beta < alpha such that (norm beta) <= (norm alpha) + magic(n)
; first, define (max-below alpha lst) to be the largest ordinal in lst
; of norm <= n
; which is less than alpha.  Define it to be 0 in the default cases.

Definition: max-below (alpha, lst, n) = if listp (lst)

then if ordinalp (car (lst)) ∧ (norm (car (lst)) ≤ n) ∧ ord-lessp (max-below (alpha, cdr (lst), n), car (lst)) ∧ ord-lessp (car (lst), alpha) then car (lst)

else max-below (alpha, cdr (lst), n) endif else 0 endif

; let's prove the basic properties of this and then disable it

Theorem: max-below-is-an-ordinal ordinalp (max-below (alpha, lst, n))

Theorem: max-below-is-below ord-lessp (0, alpha) → ord-lessp (max-below (alpha, lst, n), alpha)

Theorem: max-below-is-max (ordinalp (beta) ∧ (norm (beta) ≤ n) ∧ (beta ∈ lst) ∧ ord-lessp (beta, alpha)) → (¬ ord-lessp (max-below (alpha, lst, n), beta))

Theorem: norm-of-max-below norm (max-below (alpha, lst, n)) ≤ n

Event: Enable ord-lessp.

Theorem: max-below-of-0 max-below (0, lst, n) = 0

Event: Disable ord-lessp.

Event: Disable max-below.

; we just need its properties
; now, we want to define {alpha}(n) = the largest
; ordinal < alpha with norm <= norm(alpha) + magic(n)
; The basic properties of magic have been derived in the
; beginning arithmetic section

Definition: pred (alpha, n) = max-below (alpha,

norm-up-to (norm (alpha) + magic (n)), norm (alpha) + magic (n))

; let's prove the basic properties of this and then disable it
; that is -- (pred 0 n) = 0
; if alpha > 0, then (pred alpha n) < alpha and is the largest
; ordinal < alpha whose norm <= (norm alpha) + magic(n)

Theorem: pred-of-0 pred (0, n) = 0

Theorem: pred-is-below ord-lessp (0, alpha) → ord-lessp (pred (alpha, n), alpha)

Theorem: pred-is-an-ordinal ordinalp (pred (alpha, n))

Theorem: upper-bound-on-norm-of-pred norm (pred (alpha, n)) ≤ (norm (alpha) + magic (n))

Theorem: pred-is-largest (ordinalp (alpha) ∧ ordinalp (beta) ∧ (norm (beta) ≤ (norm (alpha) + magic (n))) ∧ ord-lessp (beta, alpha)) → ord-leq (beta, pred (alpha, n))

Event: Disable pred.

; let's compute the norm of (pred alpha n) when alpha is a limit.

Event: Enable ord-lessp.

Theorem: pred-below-limit (ordinalp (alpha) ∧ limitp (alpha)) → ord-lessp (pred (alpha, n), alpha)

Event: Disable ord-lessp.

Theorem: norm-of-pred-of-limit-aux1 (ordinalp (alpha) ∧ limitp (alpha)) → ord-lessp (successor (pred (alpha, n)), alpha)

Theorem: norm-of-pred-of-limit-aux2 (ordinalp (alpha) ∧ limitp (alpha)) → ((norm (alpha) + magic (n)) < norm (successor (pred (alpha, n))))

Theorem: norm-of-pred-of-limit-aux3 (ordinalp (alpha) ∧ limitp (alpha)) → ((norm (alpha) + magic (n)) < (1 + norm (pred (alpha, n))))

Theorem: norm-of-pred-of-limit (ordinalp (alpha) ∧ limitp (alpha)) → (norm (pred (alpha, n)) = (norm (alpha) + magic (n)))

Event: Disable norm-of-pred-of-limit-aux1.

Event: Disable norm-of-pred-of-limit-aux2.

Event: Disable norm-of-pred-of-limit-aux3.

; now, consider (pred alpha n) for successor alpha

Theorem: pred-of-succ-aux1 (ordinalp (alpha) ∧ successorp (alpha)) → ord-lessp (pred (alpha, n), alpha)

Theorem: pred-of-succ-aux2 (ordinalp (alpha) ∧ successorp (alpha)) → ord-leq (pred (alpha, n), predecessor (alpha))

Theorem: pred-of-succ-aux3 (ordinalp (alpha) ∧ successorp (alpha)) → (norm (predecessor (alpha)) ≤ (norm (alpha) + magic (n)))

Theorem: pred-of-succ-aux4 (ordinalp (alpha) ∧ successorp (alpha)) → ord-leq (predecessor (alpha), pred (alpha, n))

Theorem: pred-of-succ (ordinalp (alpha) ∧ successorp (alpha)) → (pred (alpha, n) = predecessor (alpha))

Event: Disable pred-of-succ-aux1.

Event: Disable pred-of-succ-aux2.

Event: Disable pred-of-succ-aux3.

Event: Disable pred-of-succ-aux4.

Theorem: norm-of-pred-of-succ (ordinalp (alpha) ∧ successorp (alpha)) → (norm (pred (alpha, n)) = (norm (alpha) − 1))

; now, by cases {alpha}(n) has norm at least ||alpha||-1 for all alpha

Theorem: lower-bound-on-norm-of-pred ordinalp (alpha) → (norm (pred (alpha, n)) ≮ (norm (alpha) − 1))

;;;;;;;;; pred of a sharp
; if beta > 0,
; we show:  alpha # {beta}(n) <= {alpha # beta}(n)
; the proof is
; 1.  alpha # {beta}(n) < alpha # beta by monotonicity of #
; 2.  norm(alpha # {beta}(n)) <= norm(alpha # beta) + magic(n)
; 3. Result follows by lemma "pred-is-largest"
; step 1

Theorem: pred-sharp-below (ordinalp (alpha) ∧ ordinalp (beta) ∧ ord-lessp (0, beta)) → ord-lessp (sharp (alpha, pred (beta, n)), sharp (alpha, beta))

; step 2

Theorem: norm-of-pred-sharp (ordinalp (alpha) ∧ ordinalp (beta) ∧ (n ∈ N)) → (norm (sharp (alpha, pred (beta, n)))

≤ (norm (sharp (alpha, beta)) + magic (n)))

; step 3

Theorem: pred-sharp (ordinalp (alpha) ∧ ordinalp (beta) ∧ (n ∈ N) ∧ ord-lessp (0, beta)) → ord-leq (sharp (alpha, pred (beta, n)), pred (sharp (alpha, beta), n))

;;;;;;;;  monotonicity of pred
; {alpha}(n) is a monotonic function of n
; first, a trivial fact about ord-leq

Event: Enable ord-leq.

Theorem: ord-leq-is-idempotent ord-leq (x, x)

Event: Disable ord-leq.

Theorem: monot-of-pred-aux1 (ord-lessp (0, alpha) ∧ ordinalp (alpha) ∧ (m ∈ N) ∧ (n ∈ N) ∧ (m ≤ n)) → ord-leq (pred (alpha, m), pred (alpha, n))

Theorem: monot-of-pred-aux2 ((¬ ord-lessp (0, alpha)) ∧ ordinalp (alpha) ∧ (m ∈ N) ∧ (n ∈ N) ∧ (m ≤ n)) → ord-leq (pred (alpha, m), pred (alpha, n))

Theorem: monot-of-pred (ordinalp (alpha) ∧ (m ∈ N) ∧ (n ∈ N) ∧ (m ≤ n)) → ord-leq (pred (alpha, m), pred (alpha, n))

Event: Disable monot-of-pred-aux1.

Event: Disable monot-of-pred-aux2.

; the norm of pred is also monotonic
; we can prove this by cases -- successor, limit, 0

Theorem: monot-of-norm-of-pred-aux1 ((alpha = 0) ∧ ordinalp (alpha) ∧ (m ∈ N) ∧ (n ∈ N) ∧ (m ≤ n)) → (norm (pred (alpha, n)) ≮ norm (pred (alpha, m)))

Theorem: monot-of-norm-of-pred-aux2 (limitp (alpha) ∧ ordinalp (alpha) ∧ (m ∈ N) ∧ (n ∈ N) ∧ (m ≤ n)) → (norm (pred (alpha, n)) ≮ norm (pred (alpha, m)))

Theorem: monot-of-norm-of-pred-aux3 (successorp (alpha) ∧ ordinalp (alpha) ∧ (m ∈ N) ∧ (n ∈ N) ∧ (m ≤ n)) → (norm (pred (alpha, n)) ≮ norm (pred (alpha, m)))

Theorem: monot-of-norm-of-pred (ordinalp (alpha) ∧ (m ∈ N) ∧ (n ∈ N) ∧ (m ≤ n)) → (norm (pred (alpha, n)) ≮ norm (pred (alpha, m)))

Event: Disable monot-of-norm-of-pred-aux1.

Event: Disable monot-of-norm-of-pred-aux2.

Event: Disable monot-of-norm-of-pred-aux3.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;                           O-LARGE SETS                                 ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; We define the notion :  X is alpha-large
; It is intended that X is a set in standard form, so the car is the min
; Largep was the Paris-Harrington defn of large;
; o-largep is ordinal version

Definition: o-largep (set, alpha) = if alpha = 0 then t

elseif set ≃ nil then f

else o-largep (cdr (set), pred (alpha, car (set))) endif

; prove the basic properties and then disable the defn
; base cases

Theorem: all-zero-large o-largep (set, 0)

Theorem: empty-not-large ((alpha ≠ 0) ∧ (set ≃ nil)) → (¬ o-largep (set, alpha))

Theorem: recursive-case-for-large (listp (set) ∧ (alpha ≠ 0)) → (o-largep (set, alpha) = o-largep (cdr (set), pred (alpha, car (set))))

Theorem: positive-large (ordinalp (alpha) ∧ (¬ o-largep (set, alpha))) → ord-lessp (0, alpha)

Event: Disable o-largep.

; lookat alpha-large when alpha is a successor ordinal

Theorem: successor-large-non-empty (ordinalp (alpha) ∧ successorp (alpha) ∧ (¬ listp (set))) → (¬ o-largep (set, alpha))

Theorem: successor-large (ordinalp (alpha) ∧ successorp (alpha)) → (o-largep (set, alpha)

= (listp (set) ∧ o-largep (cdr (set), predecessor (alpha))))

; lookat n-large for numbers n

Theorem: number-large (n ∈ N) → (o-largep (set, n) = (n ≤ length (set)))

;;;;;;;;;;;;  omega
; more on omega = '(1 . 0)
; we want to discuss  omega-large -- but first
; we need to discuss {omega}(n) = magic(n) + 2

Theorem: omega-is-a-limit limitp ('(1 . 0))

Event: Enable ord-lessp.

Theorem: numbers-below-omega (ordinalp (alpha) ∧ ord-lessp (alpha, '(1 . 0))) → (alpha ∈ N)

Event: Disable ord-lessp.

Theorem: pred-of-omega-aux1 pred ('(1 . 0), n) ∈ N

Theorem: pred-of-omega-aux2 (n ∈ N) → (norm (pred ('(1 . 0), n)) = (magic (n) + 2))

Theorem: pred-of-omega (n ∈ N) → (pred ('(1 . 0), n) = (magic (n) + 2))

Event: Disable pred-of-omega-aux1.

Event: Disable pred-of-omega-aux2.

; now, consider omega-large -- here
; we use (setp set) -- so we know that (car set) is a number

Event: Enable setp.

Theorem: car-of-a-set setp (cons (x, tail)) → (x ∈ N)

Event: Disable setp.

Theorem: omega-large (setp (set) ∧ o-largep (set, '(1 . 0))) → (listp (set) ∧ ((magic (car (set)) + 3) ≤ length (set)))

; in particular, omega-large implies large in the Paris-Harrington sense:

Theorem: omega-large-implies-large (setp (set) ∧ o-largep (set, '(1 . 0))) → largep (set)

;;;;;;;;; let's see what it means for a singleton to be alpha-large
; this can only happen for alpha = 0 or 1
; First, note that {alpha}(n) = 0 implies alpha is 0 or 1

Theorem: norm-above-1-aux1 ((alpha ∈ N) ∧ ord-lessp (1, alpha) ∧ ordinalp (alpha)) → (1 < norm (alpha))

Event: Enable norm.

Event: Enable ord-lessp.

Theorem: norm-above-1-aux2 ((alpha ∉ N) ∧ ord-lessp (1, alpha) ∧ ordinalp (alpha)) → (1 < norm (alpha))

Event: Disable norm.

Event: Disable ord-lessp.

Theorem: norm-above-1 (ord-lessp (1, alpha) ∧ ordinalp (alpha)) → (1 < norm (alpha))

Event: Disable norm-above-1-aux1.

Event: Disable norm-above-1-aux2.

Theorem: pred-not-0 (ord-lessp (1, alpha) ∧ ordinalp (alpha)) → ord-leq (1, pred (alpha, n))

Theorem: singletons-not-large (o-largep (set, alpha) ∧ ordinalp (alpha) ∧ ord-lessp (1, alpha)) → listp (cdr (set))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;                      O-LARGE AND SUBSETS                               ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; The main fact here is:  Let x = min(X) = car(X).
; If X is beta-large, alpha <= beta, X is a subset of Y
; and norm(alpha) <= norm(beta) + magic(x),
; then Y is alpha-large.
; This is true even if X is empty, since then beta = alpha = 0
; (and x = car(nil) = 0)

Definition: bad-for-large-superset-ord (alpha, beta, x, y) = (ordinalp (alpha)

∧ ordinalp (beta)

∧ setp (x) ∧ setp (y) ∧ subsetp (x, y) ∧ o-largep (x, beta) ∧ ord-leq (alpha, beta) ∧ (norm (alpha) ≤ (norm (beta) + magic (car (x)))) ∧ (¬ o-largep (y, alpha)))

; we want to show this can't happen.
; first, some base cases

Theorem: large-superset-ord-aux1 bad-for-large-superset-ord (alpha, beta, x, y) → ord-lessp (0, alpha)

Theorem: large-superset-ord-aux2 (ordinalp (alpha)

∧ ordinalp (beta) ∧ ord-lessp (0, alpha) ∧ ord-leq (alpha, beta)) → ord-lessp (0, beta)

Theorem: large-superset-ord-aux3 bad-for-large-superset-ord (alpha, beta, x, y) → ord-lessp (0, beta)

; so, alpha and beta are larger than 0
; next, check that can't have alpha = beta = 1

Theorem: large-superset-ord-aux4 ¬ bad-for-large-superset-ord (1, 1, x, y)

; now,  show X can't be a singleton, and alpha > 1

Theorem: large-superset-ord-aux5 bad-for-large-superset-ord (alpha, beta, x, y) → (ordinalp (alpha) ∧ ordinalp (beta))

Theorem: large-superset-ord-aux6 bad-for-large-superset-ord (alpha, beta, x, y) → (ord-lessp (1, alpha) ∨ ord-lessp (1, beta))

Theorem: large-superset-ord-aux7 bad-for-large-superset-ord (alpha, beta, x, y) → ord-leq (alpha, beta)

Theorem: large-superset-ord-aux8 bad-for-large-superset-ord (alpha, beta, x, y) → ord-lessp (1, beta)

Theorem: large-superset-ord-aux9 bad-for-large-superset-ord (alpha, beta, x, y) → listp (cdr (x))

; now, we want to show that
; (bad-for-large-superset-ord alpha beta X Y) is always false
; we know it implies alpha > 0, beta > 1, and X, Y are lists (i.e., not empty)
; the induction splits into two cases:
; Case 1:  alpha = beta
; we show (bad-for-large-superset-ord
;        (pred alpha (car Y)) (pred alpha (car X)) (cdr X)  (cdr Y) )
; Case 2: alpha < beta
; we show (bad-for-large-superset-ord
;        alpha (pred beta (car X)) (cdr X)   Y )

; BEGIN Case 1  alpha = beta
; we check the various clauses in bad for
;        (pred alpha (car Y))  (pred alpha (car X)) (cdr X)  (cdr Y)
; as much as possible, we keep alpha, beta separate
; so the work can be used in Case 2

Theorem: large-superset-ord-aux10 bad-for-large-superset-ord (alpha, beta, x, y) → (ordinalp (pred (alpha, car (y))) ∧ ordinalp (pred (beta, car (x))))

Theorem: large-superset-ord-aux11 bad-for-large-superset-ord (alpha, beta, x, y) → (listp (x) ∧ listp (y))

Theorem: large-superset-ord-aux12 bad-for-large-superset-ord (alpha, beta, x, y) → (setp (cdr (x)) ∧ setp (cdr (y)))

Theorem: large-superset-ord-aux13 bad-for-large-superset-ord (alpha, beta, x, y) → subsetp (cdr (x), cdr (y))

Theorem: large-superset-ord-aux14 bad-for-large-superset-ord (alpha, beta, x, y) → o-largep (cdr (x), pred (beta, car (x)))

Theorem: large-superset-ord-aux15 bad-for-large-superset-ord (alpha, alpha, x, y) → ord-leq (pred (alpha, car (y)), pred (alpha, car (x)))

Theorem: large-superset-ord-aux16 bad-for-large-superset-ord (alpha, alpha, x, y) → (norm (pred (alpha, car (y)))

≤ (norm (pred (alpha, car (x))) + magic (car (cdr (x)))))

Theorem: large-superset-ord-aux17 bad-for-large-superset-ord (alpha, alpha, x, y) → (¬ o-largep (cdr (y), pred (alpha, car (y))))

Theorem: large-superset-ord-aux18 bad-for-large-superset-ord (alpha, alpha, x, y) → bad-for-large-superset-ord (pred (alpha, car (y)),

pred (alpha, car (x)), cdr (x), cdr (y))

; END Case 1
; BEGIN  Case 2: alpha < beta
; we check the various requrements for
;  (bad-for-large-superset-ord alpha (pred beta (car X)) (cdr X)   Y)
; alpha and (pred beta (car X)) are ordinals by  the defn of bad and aux10
; (cdr X) and Y are sets by the defn of bad and aux12
; (o-largep (cdr X) (pred beta (car X)))  by aux14
; (not (o-largep Y alpha))  by defn of bad
; next

Theorem: large-superset-ord-aux19 (bad-for-large-superset-ord (alpha, beta, x, y) ∧ ord-lessp (alpha, beta)) → ord-leq (alpha, pred (beta, car (x)))

; finally, we have to use (car X) < (cadr X) with the
; following simple ordinal fact:

Theorem: large-superset-ord-aux20 (ordinalp (beta) ∧ (v ∈ N) ∧ (z ∈ N) ∧ (v < z)) → ((norm (beta) + magic (v)) ≤ (norm (pred (beta, z)) + magic (z)))

; we use this with v = (car X) and z = (cadr X)

Theorem: large-superset-ord-aux21 bad-for-large-superset-ord (alpha, beta, x, y) → (car (x) < cadr (x))

Theorem: large-superset-ord-aux22 (bad-for-large-superset-ord (alpha, beta, x, y) ∧ ord-lessp (alpha, beta)) → (norm (alpha) ≤ (norm (pred (beta, car (x))) + magic (car (cdr (x)))))

Theorem: large-superset-ord-aux23 bad-for-large-superset-ord (alpha, beta, x, y) → subsetp (cdr (x), y)

Theorem: large-superset-ord-aux24 (bad-for-large-superset-ord (alpha, beta, x, y) ∧ ord-lessp (alpha, beta)) → bad-for-large-superset-ord (alpha, pred (beta, car (x)), cdr (x), y)

; END Case 2
; now, we should show that case 1 or case 2 holds

Theorem: large-superset-ord-aux25 bad-for-large-superset-ord (alpha, beta, x, y) → (ord-lessp (alpha, beta) ∨ (alpha = beta)) Event: Disable large-superset-ord-aux1. Event: Disable large-superset-ord-aux2. Event: Disable large-superset-ord-aux3. Event: Disable large-superset-ord-aux4. Event: Disable large-superset-ord-aux5. Event: Disable large-superset-ord-aux6. Event: Disable large-superset-ord-aux7. Event: Disable large-superset-ord-aux8. Event: Disable large-superset-ord-aux9. Event: Disable large-superset-ord-aux10. Event: Disable large-superset-ord-aux11. Event: Disable large-superset-ord-aux12. Event: Disable large-superset-ord-aux13. Event: Disable large-superset-ord-aux14. Event: Disable large-superset-ord-aux15. Event: Disable large-superset-ord-aux16.

Event: Disable large-superset-ord-aux17.

Event: Disable large-superset-ord-aux18.

Event: Disable large-superset-ord-aux19.

Event: Disable large-superset-ord-aux21.

Event: Disable large-superset-ord-aux22.

Event: Disable large-superset-ord-aux23.

Event: Disable large-superset-ord-aux24.

Event: Disable large-superset-ord-aux25.

; summarizing

Theorem: large-superset-ord-aux26 bad-for-large-superset-ord (alpha, beta, x, y) → (bad-for-large-superset-ord (alpha, pred (beta, car (x)), cdr (x), y)

∨ bad-for-large-superset-ord (pred (alpha, car (y)), pred (alpha, car (x)), cdr (x), cdr (y)))

Theorem: large-superset-ord-aux27 bad-for-large-superset-ord (alpha, beta, x, y) → listp (x)

Definition: large-superset-ord-kludge (alpha, beta, x, y) = if x ≃ nil then 0

else large-superset-ord-kludge (alpha, pred (beta, car (x)), cdr (x), y)

+ large-superset-ord-kludge (pred (alpha, car (y)), pred (alpha, car (x)), cdr (x), cdr (y)) endif

Theorem: large-superset-ord-aux28 ((¬ bad-for-large-superset-ord (alpha, pred (beta, car (x)), cdr (x), y))

∧ (¬ bad-for-large-superset-ord (pred (alpha, car (y)), pred (alpha, car (x)), cdr (x), cdr (y))))

→ (¬ bad-for-large-superset-ord (alpha, beta, x, y))

Theorem: large-superset-ord-aux29 ¬ bad-for-large-superset-ord (alpha, beta, x, y)

Theorem: large-superset-ord (ordinalp (alpha) ∧ ordinalp (beta) ∧ setp (x) ∧ setp (y) ∧ subsetp (x, y) ∧ o-largep (x, beta) ∧ ord-leq (alpha, beta) ∧ (norm (alpha) ≤ (norm (beta) + magic (car (x))))) → o-largep (y, alpha)

Event: Disable large-superset-ord-aux26.

Event: Disable large-superset-ord-aux27.

Event: Disable large-superset-ord-aux28.

Event: Disable large-superset-ord-aux29.

Event: Disable large-superset-ord-kludge.

;;;;;;;; two important special cases
; Special case 1 -- alpha = beta

Theorem: large-goes-up (ordinalp (alpha) ∧ setp (x) ∧ setp (y) ∧ subsetp (x, y) ∧ o-largep (x, alpha)) → o-largep (y, alpha)

; Special case 2 -- X = Y

Theorem: subsetp-is-idempotent subsetp (s, s)

Theorem: large-with-smaller-ord (ordinalp (alpha) ∧ ordinalp (beta) ∧ setp (x) ∧ o-largep (x, beta) ∧ ord-leq (alpha, beta) ∧ (norm (alpha) ≤ (norm (beta) + magic (car (x))))) → o-largep (x, alpha)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;                              PIGEON-2                                  ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; this is the two-set pigeon-hole principle:
; if X is a subset of A union B, and X is alpha # beta-large
; then A is alpha-large or B is beta-large
;;;;;; covers
; Rather than define union, we just define what it means
; for A union B to cover X

Definition: covers (a, b, x) = if x ≃ nil then t

else covers (a, b, cdr (x)) ∧ ((car (x) ∈ a) ∨ (car (x) ∈ b)) endif

; some basic lemmas expressing the recursion

Theorem: covers-empty (x ≃ nil) → covers (a, b, x)

Theorem: covers-negative (listp (x) ∧ (car (x) ∉ a) ∧ (car (x) ∉ b)) → (¬ covers (a, b, x))

Theorem: covers-positive-a (listp (x) ∧ covers (a, b, cdr (x)) ∧ (car (x) ∈ a)) → covers (a, b, x)

Theorem: covers-positive-b (listp (x) ∧ covers (a, b, cdr (x)) ∧ (car (x) ∈ b)) → covers (a, b, x)

Theorem: member-of-covered-set ((u ∈ x) ∧ covers (a, b, x)) → ((u ∈ a) ∨ (u ∈ b))

; if A,B don't cover X, we can compute an element of X which is not covered

Definition: uncovered (a, b, x) = if x ≃ nil then nil

elseif covers (a, b, cdr (x)) then car (x) else uncovered (a, b, cdr (x)) endif

Theorem: uncovered-isnt-covered (¬ covers (a, b, x)) → ((uncovered (a, b, x) ∈ x)

∧ (uncovered (a, b, x) ∉ a) ∧ (uncovered (a, b, x) ∉ b))

Theorem: cdr-is-covered covers (a, b, x) → covers (a, b, cdr (x))

; we probably don't need the defn of covers any more

Event: Disable covers.

Theorem: covers-is-symmetric covers (a, b, x) → covers (b, a, x)

Theorem: discard-the-car-a (covers (a, b, x) ∧ listp (a) ∧ (car (a) ∉ x)) → covers (cdr (a), b, x)

Theorem: discard-the-car-b (covers (a, b, x) ∧ listp (b) ∧ (car (b) ∉ x)) → covers (a, cdr (b), x)

;;;;  for sets
; special facts, for standard sets, using min-is-first

Theorem: discard-the-car-set-a (setp (a) ∧ listp (a) ∧ setp (x) ∧ covers (a, b, x) ∧ (car (a) < car (x))) → covers (cdr (a), b, x)

Theorem: discard-the-car-set-b (setp (b) ∧ listp (b) ∧ setp (x) ∧ covers (a, b, x) ∧ (car (b) < car (x))) → covers (a, cdr (b), x)

; now if X is non-empty and covered by A union B --
; there are two cases
; 1.  A is non-empty and its min is <= min X
; 2.  B is non-empty and its min is <= min X
; in case 1, (cdr X) is covered by (cdr A) union B
; likewise in case 2
; the two cases

Theorem: smaller-car-when-covered (setp (a) ∧ setp (b) ∧ setp (x) ∧ listp (x) ∧ covers (a, b, x)) → ((listp (a) ∧ (car (a) ≤ car (x)))

∨ (listp (b) ∧ (car (b) ≤ car (x))))

; now, consider case 1
; as auxiliaries, we consider sub-cases depending on whether
; (cdr X) is empty or not
; first, if (cdr X) is non-empty

Theorem: cdr-is-covered-set-a-aux1 (listp (cdr (x)) ∧ setp (a) ∧ setp (b) ∧ setp (x) ∧ listp (x) ∧ covers (a, b, x) ∧ listp (a) ∧ (car (a) ≤ car (x))) → (car (a) < cadr (x))

Theorem: cdr-is-covered-set-a-aux2 (listp (cdr (x)) ∧ setp (a) ∧ setp (b) ∧ setp (x) ∧ listp (x) ∧ covers (a, b, x) ∧ listp (a) ∧ (car (a) ≤ car (x))) → covers (cdr (a), b, cdr (x))

; now, if cdr X is empty, it's trivial, so

Theorem: cdr-is-covered-set-a (setp (a) ∧ setp (b) ∧ setp (x) ∧ listp (x) ∧ covers (a, b, x) ∧ listp (a) ∧ (car (a) ≤ car (x))) → covers (cdr (a), b, cdr (x))

Event: Disable cdr-is-covered-set-a-aux1.

Event: Disable cdr-is-covered-set-a-aux2.

; now, by symmetry:

Theorem: cdr-is-covered-set-b (setp (a) ∧ setp (b) ∧ setp (x) ∧ listp (x) ∧ covers (a, b, x) ∧ listp (b) ∧ (car (b) ≤ car (x))) → covers (a, cdr (b), cdr (x))

;;;;;;;;;; sharp-and-cdr
; before going to pigeon-hole, we need a lemma that
; if X is alpha # beta - large, beta > 0, and m <= (car X) then
; (cdr X) is alpha # {beta}(m) -- large
; Also, by symmetry, the same holds for alpha/beta reversed
; X must be non-empty, since (cdr nil) = 0 -- not a set
; first observe that (cdr X) is {alpha # beta}(x) -- large

Event: Enable o-largep.

Theorem: sharp-and-cdr-aux1 (ordinalp (alpha) ∧ ordinalp (beta) ∧ listp (x)

∧ o-largep (x, sharp (alpha, beta))) → o-largep (cdr (x), pred (sharp (alpha, beta), car (x)))

; now note that if (cdr X) is empty, {alpha # beta}(x) = 0
; this should be the "trivial" case

Theorem: sharp-and-cdr-aux2 ((cdr (x) ≃ nil) ∧ ordinalp (alpha) ∧ ordinalp (beta) ∧ listp (x) ∧ o-largep (x, sharp (alpha, beta))) → (pred (sharp (alpha, beta), car (x)) = 0)

Event: Disable o-largep.

; now, if m <= (car X) then alpha # {beta}(m) <= {alpha # beta}(car X)
; proof:  alpha # {beta}(m) <= {alpha # beta}(m) <= {alpha # beta}(car X)
; the first <= is by pred-sharp, the second by monoton of pred

Theorem: sharp-and-cdr-aux3 (ordinalp (alpha) ∧ ordinalp (beta) ∧ ord-lessp (0, beta) ∧ (m ∈ N) ∧ (n ∈ N) ∧ (m ≤ n)) → ord-leq (sharp (alpha, pred (beta, m)), pred (sharp (alpha, beta), n))

Theorem: sharp-and-cdr-aux4 (ordinalp (alpha) ∧ ordinalp (beta) ∧ ord-lessp (0, beta) ∧ setp (x) ∧ (m ∈ N) ∧ (m ≤ car (x))) → ord-leq (sharp (alpha, pred (beta, m)), pred (sharp (alpha, beta), car (x)))

; now, if (cdr X) is empty, alpha # {beta}(m) = 0

Theorem: sharp-and-cdr-aux5 (listp (x)

∧ (¬ listp (cdr (x))) ∧ o-largep (x, sharp (alpha, beta)) ∧ ordinalp (alpha) ∧ ordinalp (beta) ∧ ord-lessp (0, beta) ∧ setp (x) ∧ (m ∈ N) ∧ (m ≤ car (x))) → (sharp (alpha, pred (beta, m)) = 0)

; in particular, our result is trivial if (cdr X) is empty

Theorem: sharp-and-cdr-aux6 ((¬ listp (cdr (x))) ∧ ordinalp (alpha) ∧ ordinalp (beta) ∧ ord-lessp (0, beta) ∧ setp (x) ∧ listp (x) ∧ (m ∈ N) ∧ (m ≤ car (x)) ∧ o-largep (x, sharp (alpha, beta))) → o-largep (cdr (x), sharp (alpha, pred (beta, m)))

; now, consider the case where (cdr X) is non-empty

Theorem: sharp-and-cdr-aux7 (setp (x) ∧ listp (cdr (x)) ∧ (m ∈ N) ∧ (m ≤ car (x))) → (m < cadr (x))

; we have, from the above:
; aux1 : (o-largep (cdr X) (pred (sharp alpha beta) (car X))  )
; aux4
; (ord-leq (sharp alpha (pred beta m)) (pred (sharp alpha beta) (car X)) )
; aux7 :  m < (cadr X)
; we want to apply large-with-smaller-ordinal to (cdr X)
; so we need that
;  (norm (sharp alpha (pred beta m))) <=
;    (plus (norm (pred (sharp alpha beta) (car X))) (magic (cadr X)))
; prove this separately, as a lemma:

Theorem: sharp-and-cdr-aux8 (ordinalp (alpha) ∧ ordinalp (beta) ∧ ord-lessp (0, beta) ∧ (m ∈ N) ∧ (x0 ∈ N) ∧ (m < x1 )) → (norm (sharp (alpha, pred (beta, m)))

≤ (norm (pred (sharp (alpha, beta), x0 )) + magic (x1 )))

; intended :  x0 is (car X) ; x1 is (cadr x)

Theorem: sharp-and-cdr-aux9 (listp (cdr (x)) ∧ ordinalp (alpha) ∧ ordinalp (beta) ∧ ord-lessp (0, beta) ∧ setp (x) ∧ listp (x) ∧ (m ∈ N) ∧ (m ≤ car (x))) → (norm (sharp (alpha, pred (beta, m)))

≤ (norm (pred (sharp (alpha, beta), car (x))) + magic (cadr (x))))

Theorem: sharp-and-cdr-aux10 (listp (cdr (x)) ∧ ordinalp (alpha) ∧ ordinalp (beta) ∧ ord-lessp (0, beta) ∧ setp (x) ∧ listp (x) ∧ (m ∈ N) ∧ (m ≤ car (x)) ∧ o-largep (x, sharp (alpha, beta))) → o-largep (cdr (x), sharp (alpha, pred (beta, m)))

Theorem: sharp-and-cdr-b (ordinalp (alpha) ∧ ordinalp (beta) ∧ ord-lessp (0, beta) ∧ setp (x) ∧ listp (x) ∧ (m ∈ N) ∧ (m ≤ car (x)) ∧ o-largep (x, sharp (alpha, beta))) → o-largep (cdr (x), sharp (alpha, pred (beta, m)))

Event: Disable sharp-and-cdr-aux1.

Event: Disable sharp-and-cdr-aux2.

Event: Disable sharp-and-cdr-aux3.

Event: Disable sharp-and-cdr-aux4.

Event: Disable sharp-and-cdr-aux5.

Event: Disable sharp-and-cdr-aux6.

Event: Disable sharp-and-cdr-aux7.

Event: Disable sharp-and-cdr-aux8.

Event: Disable sharp-and-cdr-aux9.

Event: Disable sharp-and-cdr-aux10.

; the same thing with alpha replacing beta follows automatically by symmetry

Theorem: sharp-and-cdr-a (ordinalp (alpha) ∧ ordinalp (beta) ∧ ord-lessp (0, alpha) ∧ setp (x) ∧ listp (x) ∧ (m ∈ N) ∧ (m ≤ car (x)) ∧ o-largep (x, sharp (alpha, beta))) → o-largep (cdr (x), sharp (pred (alpha, m), beta))

;;;;;;;;;;;  Proof of pigeon-2
; This is the version with 2 holes:
; if (covers A B X) and X is alpha # beta -- large
; then A is alpha -- large     or      B is beta -- large

; we prove this by induction, showing the following can't happen

Definition: bad-for-pigeon-2 (a, b, x, alpha, beta) = (ordinalp (alpha)

∧ ordinalp (beta)

∧ setp (a) ∧ setp (b) ∧ setp (x) ∧ covers (a, b, x) ∧ o-largep (x, sharp (alpha, beta)) ∧ (¬ o-largep (a, alpha)) ∧ (¬ o-largep (b, beta)))

; first, kill off some base cases:
; alpha and beta are > 0

Theorem: pigeon-2-aux1 bad-for-pigeon-2 (a, b, x, alpha, beta) → ord-lessp (0, alpha)

Theorem: pigeon-2-aux2 bad-for-pigeon-2 (a, b, x, alpha, beta) → ord-lessp (0, beta)

Theorem: pigeon-2-aux3 bad-for-pigeon-2 (a, b, x, alpha, beta) → (ordinalp (alpha) ∧ ordinalp (beta))

Theorem: pigeon-2-aux4 bad-for-pigeon-2 (a, b, x, alpha, beta) → ord-lessp (0, sharp (alpha, beta))

Theorem: pigeon-2-aux5 bad-for-pigeon-2 (a, b, x, alpha, beta) → listp (x)

Theorem: pigeon-2-aux6 bad-for-pigeon-2 (a, b, x, alpha, beta) → (setp (a) ∧ setp (b) ∧ setp (x) ∧ listp (x) ∧ covers (a, b, x))

Theorem: pigeon-2-aux7 bad-for-pigeon-2 (a, b, x, alpha, beta) → ((listp (a) ∧ (car (a) ≤ car (x)))

∨ (listp (b) ∧ (car (b) ≤ car (x))))

; now, consider the first case:
; we have (and (listp A) (leq (car A) (car X)))
; we want to show that
; (bad-for-pigeon-2 (cdr A) B (cdr X)  (pred alpha (car A)) beta)
; we check the five lines  in the definition
; line1

Theorem: pigeon-2-aux8 bad-for-pigeon-2 (a, b, x, alpha, beta) → (ordinalp (pred (alpha, car (a))) ∧ ordinalp (beta))

; line2

Theorem: pigeon-2-aux9 (bad-for-pigeon-2 (a, b, x, alpha, beta) ∧ listp (a) ∧ (car (a) ≤ car (x))) → (setp (cdr (a))

∧ setp (b) ∧ setp (cdr (x)) ∧ covers (cdr (a), b, cdr (x)))

; line3

Theorem: pigeon-2-aux10 (bad-for-pigeon-2 (a, b, x, alpha, beta) ∧ (car (a) ≤ car (x))) → o-largep (cdr (x), sharp (pred (alpha, car (a)), beta))

; line4

Theorem: pigeon-2-aux11 (bad-for-pigeon-2 (a, b, x, alpha, beta) ∧ listp (a)) → (¬ o-largep (cdr (a), pred (alpha, car (a))))

; line5

Theorem: pigeon-2-aux12 bad-for-pigeon-2 (a, b, x, alpha, beta) → (¬ o-largep (b, beta))

; summarize what we need for
; (bad-for-pigeon-2 (cdr A) B (cdr X) (pred alpha (car A)) beta)

Theorem: pigeon-2-aux13 (ordinalp (pred (alpha, car (a))) ∧ ordinalp (beta)

∧ setp (cdr (a)) ∧ setp (b) ∧ setp (cdr (x)) ∧ covers (cdr (a), b, cdr (x)) ∧ o-largep (cdr (x), sharp (pred (alpha, car (a)), beta)) ∧ (¬ o-largep (cdr (a), pred (alpha, car (a)))) ∧ (¬ o-largep (b, beta))) → bad-for-pigeon-2 (cdr (a), b, cdr (x), pred (alpha, car (a)), beta)

; putting them together in the first case

Theorem: pigeon-2-aux14 (bad-for-pigeon-2 (a, b, x, alpha, beta) ∧ listp (a) ∧ (car (a) ≤ car (x))) → bad-for-pigeon-2 (cdr (a), b, cdr (x), pred (alpha, car (a)), beta)

; this ends the first case
; now, consider the second case
; we have (and (listp B) (leq (car B) (car X)))
; we want to show that
; (bad-for-pigeon-2  A (cdr B) (cdr X)  alpha (pred beta (car B)))
; again we check the five lines  in the definition
; line1

Theorem: pigeon-2-aux15 bad-for-pigeon-2 (a, b, x, alpha, beta) → (ordinalp (alpha) ∧ ordinalp (pred (beta, car (b))))

; line2

Theorem: pigeon-2-aux16 (bad-for-pigeon-2 (a, b, x, alpha, beta) ∧ listp (b) ∧ (car (b) ≤ car (x))) → (setp (a)

∧ setp (cdr (b)) ∧ setp (cdr (x)) ∧ covers (a, cdr (b), cdr (x)))

; line3

Theorem: pigeon-2-aux17 (bad-for-pigeon-2 (a, b, x, alpha, beta) ∧ (car (b) ≤ car (x))) → o-largep (cdr (x), sharp (alpha, pred (beta, car (b))))

; line5

Theorem: pigeon-2-aux18 (bad-for-pigeon-2 (a, b, x, alpha, beta) ∧ listp (b)) → (¬ o-largep (cdr (b), pred (beta, car (b))))

; line4

Theorem: pigeon-2-aux19 bad-for-pigeon-2 (a, b, x, alpha, beta) → (¬ o-largep (a, alpha))

; summarize what we need for
; (bad-for-pigeon-2  (cdr B) (cdr X) alpha (pred beta (car B)))

Theorem: pigeon-2-aux20 (ordinalp (alpha) ∧ ordinalp (pred (beta, car (b))) ∧ setp (a) ∧ setp (cdr (b)) ∧ setp (cdr (x)) ∧ covers (a, cdr (b), cdr (x)) ∧ o-largep (cdr (x), sharp (alpha, pred (beta, car (b)))) ∧ (¬ o-largep (a, alpha)) ∧ (¬ o-largep (cdr (b), pred (beta, car (b))))) → bad-for-pigeon-2 (a, cdr (b), cdr (x), alpha, pred (beta, car (b)))

; putting them together in the second case

Theorem: pigeon-2-aux21 (bad-for-pigeon-2 (a, b, x, alpha, beta) ∧ listp (b) ∧ (car (b) ≤ car (x))) → bad-for-pigeon-2 (a, cdr (b), cdr (x), alpha, pred (beta, car (b)))

; now the point is:  if (bad-for-pigeon-2 A B X alpha beta)
; then (listp X) ( by aux5 ) and (cdr X) messes
; up with something -- so we can induct on X

Theorem: pigeon-2-aux22 bad-for-pigeon-2 (a, b, x, alpha, beta) → (bad-for-pigeon-2 (cdr (a), b, cdr (x), pred (alpha, car (a)), beta)

∨ bad-for-pigeon-2 (a, cdr (b), cdr (x), alpha, pred (beta, car (b))))

Definition: pigeon-2-kludge (a, b, x, alpha, beta) = if x ≃ nil then 0

else pigeon-2-kludge (cdr (a), b, cdr (x), pred (alpha, car (a)), beta) + pigeon-2-kludge (a, cdr (b), cdr (x), alpha, pred (beta, car (b))) endif

Theorem: pigeon-2-aux23 ¬ bad-for-pigeon-2 (a, b, x, alpha, beta)

; finally, the GOAL:

Theorem: pigeon-2 (ordinalp (alpha) ∧ ordinalp (beta) ∧ setp (a) ∧ setp (b) ∧ setp (x) ∧ covers (a, b, x) ∧ o-largep (x, sharp (alpha, beta))) → (o-largep (a, alpha) ∨ o-largep (b, beta))

Event: Disable bad-for-pigeon-2.

Event: Disable pigeon-2-kludge.

Event: Disable pigeon-2-aux1.

Event: Disable pigeon-2-aux2.

Event: Disable pigeon-2-aux3.

Event: Disable pigeon-2-aux4.

Event: Disable pigeon-2-aux5.

Event: Disable pigeon-2-aux6.

Event: Disable pigeon-2-aux7.

Event: Disable pigeon-2-aux8.

Event: Disable pigeon-2-aux9. Event: Disable pigeon-2-aux10. Event: Disable pigeon-2-aux11. Event: Disable pigeon-2-aux12. Event: Disable pigeon-2-aux13. Event: Disable pigeon-2-aux14. Event: Disable pigeon-2-aux15. Event: Disable pigeon-2-aux16. Event: Disable pigeon-2-aux17. Event: Disable pigeon-2-aux18. Event: Disable pigeon-2-aux19. Event: Disable pigeon-2-aux20. Event: Disable pigeon-2-aux21. Event: Disable pigeon-2-aux22. Event: Disable pigeon-2-aux23.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;                 FUNCTIONS AND HOMOGENEOUS SETS                         ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; view every S-expression as an association list, and hence a function

Definition: funcall (g, x) = cadr (assoc (x, g))

; since (cadr nil) = 0, we always have 0 in the range:

Definition: range (g) = if g ≃ nil then list (0)

else cons (cadar (g), range (cdr (g))) endif

Theorem: range-is-big-enuf funcall (g, x) ∈ range (g)

Event: Disable range.

; we don't care exactly what it is

Event: Disable funcall.

; for now -- later, we'll need its definition to show that we
; can build up functions with prescribed definitions

Definition: mapsto (g, set1 , set2 ) = if set1 ≃ nil then t

else mapsto (g, cdr (set1 ), set2 )

∧ (funcall (g, car (set1 )) ∈ set2 ) endif

Theorem: mapsto-works (mapsto (g, set1 , set2 ) ∧ (x ∈ set1 )) → (funcall (g, x) ∈ set2 )

Event: Disable mapsto.

;;;;;;;;;;;;;;;;;;;;;;;;
; let's disable some ordinal stuff which seems to slow down the set proofs

Event: Disable numbers-below-omega.

Event: Disable cdrs-are-ordinals.

Event: Disable ord-leq-zero.

Event: Disable ord-leq-is-transitive.

;;;;;;;;;;;;  notion of homogeneous
; (homp set g n) means that  set is homogeneous for g as a partition
; of n-tuples:  that is,
; whenever s1, s2 are subsets of set of size <= n, and
; |s1| =|s2| and g(s1) = g(s2) < c, then g(s1) = g(s2)
; we first define what a counter-example would be
; search through the list of all possible counter-examples

Definition: hom-bad-pairp (x, y, set, g, n) = (sublistp (x, set)

∧ sublistp (y, set)

∧ setp (x) ∧ setp (y) ∧ (length (x) = n) ∧ (length (y) = n) ∧ (funcall (g, x) ≠ funcall (g, y)))

; use sublistp rather than subsetp because power-set was defined
; to work with sublistp.  These are equivalent anyway when
; (setp set), which is what we're interested in.
; pairs is a list of pairs which are possible counter-examples
; counter-hom looks for a pair (x y) which refutes homogeneous
; if it fails, it returns 0
; disable bad-pair temporarily

Event: Disable hom-bad-pairp.

Definition: counter-hom (set, g, n, pairs) = if pairs ≃ nil then 0

elseif listp (counter-hom (set, g, n, cdr (pairs)))

then counter-hom (set, g, n, cdr (pairs))

elseif hom-bad-pairp (caar (pairs), cdar (pairs), set, g, n)

then cons (caar (pairs), cdar (pairs))

else 0 endif

Theorem: bad-pair-is-bad listp (counter-hom (set, g, n, pairs))

→ hom-bad-pairp (car (counter-hom (set, g, n, pairs)), cdr (counter-hom (set, g, n, pairs)), set, g, n)

Theorem: counter-hom-finds-one ((cons (x, y) ∈ pairs) ∧ hom-bad-pairp (x, y, set, g, n)) → listp (counter-hom (set, g, n, pairs))

Event: Disable counter-hom.

; now -- homp means we search thru all pairs from the
; power-set and don't find one

Definition: homp (set, g, n) = (counter-hom (set, g, n, product (power-set (set), power-set (set))) ≃ nil)

; now, we prove that homp is necessary and sufficient
; this needs the defn of hom-bad-pairp

Event: Enable hom-bad-pairp.

Theorem: homp-is-sufficient-a (homp (set, g, n) ∧ sublistp (x, set) ∧ sublistp (y, set) ∧ setp (x) ∧ setp (y) ∧ (length (x) = n) ∧ (length (y) = n)) → (funcall (g, x) = funcall (g, y))

;;; in our paper, it would be less confusing to have a version
; to quote which uses subsetp instead of sublistp

Theorem: homp-is-sufficient (homp (set, g, n) ∧ subsetp (x, set) ∧ subsetp (y, set) ∧ setp (set)

∧ setp (x) ∧ setp (y) ∧ (length (x) = n) ∧ (length (y) = n)) → (funcall (g, x) = funcall (g, y))

; to prove necessary, it would be nice to have an abbreviation for
; the x and y coordinate of the counter-example

Definition: counter-hom-x (set, g, n) = car (counter-hom (set, g, n, product (power-set (set), power-set (set))))

Definition: counter-hom-y (set, g, n) = cdr (counter-hom (set, g, n, product (power-set (set), power-set (set))))

Theorem: homp-is-necessary (¬ homp (set, g, n)) → (sublistp (counter-hom-x (set, g, n), set)

∧ sublistp (counter-hom-y (set, g, n), set) ∧ setp (counter-hom-x (set, g, n)) ∧ setp (counter-hom-y (set, g, n)) ∧ (length (counter-hom-x (set, g, n)) = n) ∧ (length (counter-hom-y (set, g, n)) = n) ∧ (funcall (g, counter-hom-x (set, g, n))

≠ funcall (g, counter-hom-y (set, g, n))))

Event: Disable homp.

Event: Disable hom-bad-pairp.

Event: Disable counter-hom-x.

Event: Disable counter-hom-y.

;;;;;;;;;;;;;;;  add-on-end
; before discussing pre-homogeneous sets, we have to talk
; about adding one element at the end of a set -- maybe
; it's simpler to define this outright, rather than using "append"

Definition: add-on-end (item, set) = if set ≃ nil then list (item)

else cons (car (set), add-on-end (item, cdr (set))) endif

; for sets, this is set Union {item}

Theorem: add-in-end-is-last last (add-on-end (item, set)) = item

Theorem: add-in-end-and-length length (add-on-end (item, set)) = (1 + length (set))

; we should probably define all-but-last  -- everything
; except the last element

Theorem: all-but-last-aux1 listp (cdr (lst)) → listp (lst)

; needed for the recursion

Definition: all-but-last (lst) = if cdr (lst) ≃ nil then nil

else cons (car (lst), all-but-last (cdr (lst))) endif

Event: Disable all-but-last-aux1.

Theorem: all-but-last-and-length listp (cdr (lst)) → (length (all-but-last (lst)) = (length (lst) − 1))

Theorem: all-but-last-of-add-on-end properp (lst) → (all-but-last (add-on-end (item, lst)) = lst)

Event: Enable setp.

Theorem: add-on-end-makes-sets (setp (set) ∧ (n ∈ N) ∧ (last (set) < n)) → setp (add-on-end (n, set))

Event: Disable setp.

Theorem: all-but-last-is-sublist sublistp (all-but-last (lst), lst)

Theorem: all-but-last-is-sublist-a sublistp (s1 , set) → sublistp (all-but-last (s1 ), set)

Theorem: all-but-last-is-non-empty (2 ≤ length (lst)) → listp (all-but-last (lst))

Event: Enable setp.

Theorem: all-but-last-is-a-set setp (set) → setp (all-but-last (set))

Event: Disable setp.

Theorem: re-assemble-at-end (properp (lst) ∧ listp (lst)) → (add-on-end (last (lst), all-but-last (lst)) = lst)

Theorem: length-of-all-but-last listp (x) → (length (all-but-last (x)) = (length (x) − 1))

;;;;;;;;;;;;  notion of pre-homogeneous
; (pre-homp set g) means that  set is pre-homogeneous for g as a partition
; that is:  whenever s1 is a non-empty subset of set, y,z are members of
; set and are larger than max(s1) :
; g(s1 U {y}) = g(s1 U {z})
; we use the same "bad" method

Definition: pre-hom-bad-triplep (y, z, s1 , set, g) = (sublistp (s1 , set)

∧ listp (s1 ) ∧ setp (s1 ) ∧ (y ∈ set) ∧ (z ∈ set) ∧ (last (s1 ) < y) ∧ (last (s1 ) < z) ∧ (funcall (g, add-on-end (y, s1 )) ≠ funcall (g, add-on-end (z, s1 ))))

; disable bad-triple temporarily

Event: Disable pre-hom-bad-triplep.

; triples will be just ( (a .  b) .  c) -- so we get a,b,c as the
; caar, cdar, cdr
; then all triples are getten as (product (product set set) (power-set set))

Definition: counter-pre-hom (set, g, triples) = if triples ≃ nil then 0

elseif listp (counter-pre-hom (set, g, cdr (triples)))

then counter-pre-hom (set, g, cdr (triples)) elseif pre-hom-bad-triplep (caaar (triples),

cdaar (triples), cdar (triples), set, g) then cons (cons (caaar (triples), cdaar (triples)), cdar (triples)) else 0 endif

Theorem: bad-triple-is-bad listp (counter-pre-hom (set, g, triples)) → pre-hom-bad-triplep (caar (counter-pre-hom (set, g, triples)),

cdar (counter-pre-hom (set, g, triples)), cdr (counter-pre-hom (set, g, triples)), set, g)

Theorem: counter-pre-hom-finds-one ((cons (cons (y, z), s1 ) ∈ triples) ∧ pre-hom-bad-triplep (y, z, s1 , set, g)) → listp (counter-pre-hom (set, g, triples))

Event: Disable counter-pre-hom.

Definition: pre-homp (set, g) = (counter-pre-hom (set, g, product (product (set, set), power-set (set))) ≃ nil)

; now, we prove that pre-homp is necessary and sufficient
; this needs the defn of pre-hom-bad-triplep

Event: Enable pre-hom-bad-triplep.

Theorem: pre-homp-is-sufficient (pre-homp (set, g) ∧ sublistp (s1 , set)

∧ listp (s1 ) ∧ setp (s1 ) ∧ (y ∈ set) ∧ (z ∈ set) ∧ (last (s1 ) < y) ∧ (last (s1 ) < z)) → (funcall (g, add-on-end (y, s1 )) = funcall (g, add-on-end (z, s1 )))

;  to prove necessary, we use an abbreviation for
; the y,z, s1 of the counter-example

Definition: counter-pre-hom-y (set, g) = caar (counter-pre-hom (set, g, product (product (set, set), power-set (set))))

Definition: counter-pre-hom-z (set, g) = cdar (counter-pre-hom (set, g, product (product (set, set), power-set (set))))

Definition: counter-pre-hom-s1 (set, g) = cdr (counter-pre-hom (set, g, product (product (set, set), power-set (set))))

Theorem: pre-homp-is-necessary (¬ pre-homp (set, g)) → (sublistp (counter-pre-hom-s1 (set, g), set)

∧ listp (counter-pre-hom-s1 (set, g)) ∧ setp (counter-pre-hom-s1 (set, g)) ∧ (counter-pre-hom-y (set, g) ∈ set) ∧ (counter-pre-hom-z (set, g) ∈ set) ∧ (last (counter-pre-hom-s1 (set, g)) < counter-pre-hom-y (set, g)) ∧ (last (counter-pre-hom-s1 (set, g)) < counter-pre-hom-z (set, g)) ∧ (funcall (g,

add-on-end (counter-pre-hom-y (set, g),

counter-pre-hom-s1 (set, g)))

≠ funcall (g,

add-on-end (counter-pre-hom-z (set, g), counter-pre-hom-s1 (set, g)))))

Event: Disable pre-homp.

Event: Disable pre-hom-bad-triplep.

Event: Disable counter-pre-hom-y.

Event: Disable counter-pre-hom-z.

Event: Disable counter-pre-hom-s1.

;;;;;;;;;;;;;;;;;;;;   derived partitions
; This is used in the induction step in Ramsey's Theorem --
;  passing from n-1 - tuples to n - tuples
; Think of g as a partition of n-tuples (n >= 2)
; If set is pre-hom for g, there is a derived partition h, on n-1 - tuples
; such that whenever hset is homogeneous for h, hset is homogeneous for g
; to compute (h s1) :  apply g to s1 U {x}, where x =
; (find-larger-element s1 set) -- this returns an element x of set
; which is a number and larger than (last s1)
; it returns nil if there is no such number
; so -- by testing for numberp, we know if we have found one.

Definition: find-larger-element (s1 , set) = if set ≃ nil then nil

elseif (car (set) ∈ N) ∧ (last (s1 ) < car (set)) then car (set)

else find-larger-element (s1 , cdr (set)) endif

Theorem: find-larger-element-works-a (find-larger-element (s1 , set) ∈ N) → ((find-larger-element (s1 , set) ∈ set)

∧ (find-larger-element (s1 , set) ∈ N)

∧ (last (s1 ) < find-larger-element (s1 , set)))

Theorem: find-larger-element-works-b ((x ∈ set) ∧ (x ∈ N) ∧ (last (s1 ) < x)) → (find-larger-element (s1 , set) ∈ N)

Event: Disable find-larger-element.

; we don't care which one we found
; if s1 is a subset of set and s1 has length at least 2,
; then (find-larger-element (all-but-last) set )  really
; finds one -- since (last s1) is a candidate.
; first, we have to show it really is a candidate

; the following is probably needed also for properties
; of pre-homogeneous sets

Theorem: last-is-a-member listp (lst) → (last (lst) ∈ lst)

Theorem: last-is-a-candidate-1 (sublistp (s1 , set) ∧ (2 ≤ length (s1 ))) → (last (s1 ) ∈ set)

Event: Enable setp.

Theorem: members-are-numbers (setp (set) ∧ (x ∈ set)) → (x ∈ N)

Event: Disable setp.

Theorem: last-is-a-candidate-2 (setp (s1 ) ∧ (2 ≤ length (s1 ))) → (last (s1 ) ∈ N)

Event: Enable setp.

Theorem: last-is-a-candidate-3 (setp (s1 ) ∧ (2 ≤ length (s1 ))) → (last (all-but-last (s1 )) < last (s1 ))

Event: Disable setp.

Theorem: larger-elt-is-found (setp (s1 ) ∧ sublistp (s1 , set) ∧ (2 ≤ length (s1 ))) → (find-larger-element (all-but-last (s1 ), set) ∈ N)

; it follows that if g is pre-homogeneous on set, then (g s1) =
; (g  (add-on-end
;         (find-larger-element (all-but-last s1) set)
;         (all-but-last s1) ) )
; that is, (g s1) is determined as the derived partition
;  applied to (all-but-last s1)

Theorem: pre-hom-and-all-but-last (pre-homp (set, g) ∧ setp (s1 ) ∧ sublistp (s1 , set) ∧ (2 ≤ length (s1 ))) → (funcall (g, s1 )

= funcall (g,

add-on-end (find-larger-element (all-but-last (s1 ), set), all-but-last (s1 ))))

; now we simply define the derived partition h = (derived g set)  so that
;(h s) =
;(funcall g
;    (add-on-end
;        (find-larger-element s set)
;        s ))
; but to define a function h like this, we have to run down
; a list of subsets -- i.e., (power-set set)
; and construct h as a list of pairs

Definition: derived-aux (g, set, lst) = if lst ≃ nil then nil

else cons (list (car (lst),

funcall (g,

add-on-end (find-larger-element (car (lst),

set),

car (lst)))),

derived-aux (g, set, cdr (lst))) endif

Theorem: derived-aux1 (s ∈ lst) → (assoc (s, derived-aux (g, set, lst))

= list (s, funcall (g, add-on-end (find-larger-element (s, set), s))))

Event: Enable funcall.

Theorem: derived-aux2 (s ∈ lst) → (funcall (derived-aux (g, set, lst), s)

= funcall (g, add-on-end (find-larger-element (s, set), s)))

Event: Disable funcall.

Event: Disable derived-aux.

Event: Disable derived-aux1.

Definition: derived (g, set) = derived-aux (g, set, power-set (set))

Theorem: derived-works (sublistp (s, set) ∧ setp (s))

→ (funcall (derived (g, set), s)

= funcall (g, add-on-end (find-larger-element (s, set), s)))

Event: Disable derived.

Event: Disable derived-aux2.

; now, if g is pre-homogeneous, then
; (g s1) is computed from ((derived g set) s), where
; s = (all-but-last s1)

Theorem: derived-and-prehom (pre-homp (set, g) ∧ setp (s1 ) ∧ sublistp (s1 , set) ∧ (2 ≤ length (s1 ))) → (funcall (g, s1 ) = funcall (derived (g, set), all-but-last (s1 )))

; now suppose n>=2 and  g is prehom on set
; then say we find small-set is a subset of set which
; is homogeneous for (derivde g set) on the n-1 -- tuples
; then small-set is homogeneous for g on the n -- tuples
; to prove this, we consider any two subsets x, y of small-set
; of size n and prove that g(x) = h(all-but-last x) = h(all-but-last y)
; = g(y) , where h is the derived partition

Theorem: derived-partition-lemma-aux1 (length (x) ≮ 2) → (length (all-but-last (x)) = (length (x) − 1))

Theorem: derived-partition-lemma-aux2 ((2 ≤ n) ∧ pre-homp (set, g) ∧ sublistp (small-set, set) ∧ homp (small-set, derived (g, set), n − 1) ∧ sublistp (x, small-set) ∧ sublistp (y, small-set) ∧ setp (x) ∧ setp (y) ∧ (length (x) = n) ∧ (length (y) = n)) → (funcall (g, x) = funcall (g, y))

; now, if (homp small-set g n) fails, lookat a counter-example

Theorem: derived-partition-lemma ((2 ≤ n) ∧ pre-homp (set, g) ∧ sublistp (small-set, set) ∧ homp (small-set, derived (g, set), n − 1)) → homp (small-set, g, n)

Event: Disable derived-partition-lemma-aux1.

Event: Disable derived-partition-lemma-aux2.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;                           THE TAIL LEMMA                               ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Suppose ZZ is a set which is omega^alpha + omega + k  -- large.
; let z = min ZZ.
; If we take cdr's magic(z+d) times, we get a set QQ such that
; 1. QQ is a set and omega^alpha -- large
; 2. QQ is a subset of ZZ
; 3. min(QQ) >= min(ZZ) + magic(z+k).
; To prove this, we analyze ordinals delta of the forms:
;   type A: delta = omega^alpha + omega + k (k > 0)   (alpha 1 . k) k > 0
;   type B: delta = omega^alpha +  k        (k > 0)   (alpha . k)  k > 0
;   type C: delta = omega^alpha + omega               (alpha 1 . 0)
; As a first step, consider the {delta}(n) for these ordinals.
; type A  : (cons alpha (cons 1 k)) : k > 0

Event: Enable ord-lessp.

Theorem: type-a-is-ordinal (ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (0 < k)) → ordinalp (cons (alpha, cons (1, k)))

Event: Disable ord-lessp.

Theorem: type-a-is-a-successor (0 < k) → successorp (cons (alpha, cons (1, k)))

Theorem: predecessor-of-type-a (0 < k) → (predecessor (cons (alpha, cons (1, k))) = cons (alpha, cons (1, k − 1)))

Theorem: pred-type-a (ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (0 < k)) → (pred (cons (alpha, cons (1, k)), n) = cons (alpha, cons (1, k − 1)))

; type B  : (cons alpha k) : k > 0

Event: Enable ord-lessp.

Theorem: type-b-is-ordinal (ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (0 < k)) → ordinalp (cons (alpha, k))

Event: Disable ord-lessp.

Theorem: type-b-is-a-successor (0 < k) → successorp (cons (alpha, k))

Theorem: predecessor-of-type-b (0 < k) → (predecessor (cons (alpha, k)) = cons (alpha, k − 1))

Theorem: pred-type-b (ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (0 < k)) → (pred (cons (alpha, k), n) = cons (alpha, k − 1))

; type C  : (cons alpha (cons 1 0))

Event: Enable ord-lessp.

Theorem: type-c-is-ordinal (ordinalp (alpha) ∧ ord-leq (1, alpha)) → ordinalp (cons (alpha, cons (1, 0)))

Event: Disable ord-lessp.

Theorem: type-c-is-a-limit limitp (cons (alpha, cons (1, 0)))

; Now we want:
; (equal
;   (pred (cons alpha (cons 1 0)) n)

;   (cons alpha (plus (magic n) 2)) )
; first, compute the norms

Theorem: norm-of-type-c norm (cons (alpha, cons (1, 0))) = (norm (alpha) + 3)

Theorem: norm-of-pred-of-type-c (ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (n ∈ N)) → (norm (pred (cons (alpha, cons (1, 0)), n))

= (norm (alpha) + 3 + magic (n)))

Theorem: norm-of-right-answer-c (n ∈ N) → (norm (cons (alpha, magic (n) + 2))

= (norm (alpha) + 3 + magic (n)))

; now, we prove that the right answer,  omega^alpha + (magic n) + 2
; is less than omega^alpha + omega  -- then we need
; only show that anything strictly betwwen
; omega^alpha + (magic n) + 2 and omega^alpha + omega  has larger norm

Theorem: pred-type-c-aux1 ord-lessp (cons (alpha, magic (n) + 2), cons (alpha, cons (1, 0)))

Theorem: pred-type-c-aux2 (ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (n ∈ N)) → ord-leq (cons (alpha, magic (n) + 2), pred (cons (alpha, cons (1, 0)), n))

; so, the only remaining possibility is that
; (pred (cons alpha (cons 1 0)) n)   is strictly between
; (cons alpha (plus (magic n) 2))   and (cons alpha (cons 1 0))
; but then its norm would be too large
; any ordinal strictly between must be of the form
;  (cons alpha j)  where j > (plus (magic n) 2)

Theorem: pred-type-c-aux3 (ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ ordinalp (sigma)

∧ (r ∈ N) ∧ ord-lessp (cons (alpha, r), sigma) ∧ ord-lessp (sigma, cons (alpha, cons (1, 0)))) → ((car (sigma) = alpha) ∧ (cdr (sigma) ∈ N) ∧ (r < cdr (sigma)))

Theorem: pred-type-c-aux4 (ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ ordinalp (sigma) ∧ (n ∈ N) ∧ ord-lessp (cons (alpha, magic (n) + 2), sigma) ∧ ord-lessp (sigma, cons (alpha, cons (1, 0)))) → ((norm (alpha) + 3 + magic (n)) < norm (sigma))

Theorem: pred-type-c-aux5 (ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (n ∈ N)) → (¬ ord-lessp (cons (alpha, magic (n) + 2),

pred (cons (alpha, cons (1, 0)), n)))

Theorem: pred-type-c (ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (n ∈ N)) → (pred (cons (alpha, cons (1, 0)), n) = cons (alpha, magic (n) + 2))

Event: Disable pred-type-c-aux1.

Event: Disable pred-type-c-aux2.

Event: Disable pred-type-c-aux3.

Event: Disable pred-type-c-aux4.

Event: Disable pred-type-c-aux5.

;; OK -- that finishes the {delta}(n) discussion
;;;;;;;; nthcdr
; this is like the common lisp function

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

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

; some trivail properties:

Theorem: nthcdr-0 (n ≃ 0) → (nthcdr (n, lst) = lst)

Theorem: nthcdr-1 nthcdr (1, lst) = cdr (lst)

Theorem: nthcdr-add nthcdr (m, nthcdr (n, lst)) = nthcdr (m + n, lst)

; since the cdr of a non-list is 0:

Theorem: length-of-nthcdr (nthcdr (n, lst) ≠ 0) → (length (nthcdr (n, lst)) = (length (lst) − n))

; since non-lists are subsets of everying

Event: Enable subsetp.

Theorem: nthcdr-is-subset subsetp (nthcdr (n, lst), lst)

Event: Disable subsetp.

; now, special facts about sets --
; we want to know that (nthcdr n set) is a subset of set
; whose car is at least  (car set) + n
; (assuming  the nthdr isn't empty)

Theorem: cdr-is-a-set (setp (set) ∧ (cdr (set) ≠ 0)) → setp (cdr (set))

Theorem: nthcdr-is-a-set (setp (set) ∧ (nthcdr (n, set) ≠ 0)) → setp (nthcdr (n, set))

Theorem: cdr-is-above (setp (set) ∧ listp (cdr (set))) → (car (set) < car (cdr (set)))

Theorem: cdr-is-above-by-1 (setp (set) ∧ listp (cdr (set))) → (car (cdr (set)) ≮ (1 + car (set)))

Definition: bad-for-nthcdr-is-above-by-n (n, set) = (setp (set)

∧ listp (nthcdr (n, set))

∧ (car (nthcdr (n, set)) < (n + car (set))))

Theorem: nthcdr-is-above-by-n-aux1 (n ≃ 0) → (¬ bad-for-nthcdr-is-above-by-n (n, set))

Theorem: nthcdr-is-above-by-n-aux2 (setp (set) ∧ (¬ setp (nthcdr (n, set)))) → (¬ listp (cdr (nthcdr (n, set))))

Theorem: nthcdr-is-above-by-n-aux3 bad-for-nthcdr-is-above-by-n (1 + n, set) → bad-for-nthcdr-is-above-by-n (n, set)

Theorem: nthcdr-is-above-by-n-aux4 ¬ bad-for-nthcdr-is-above-by-n (n, set)

Theorem: nthcdr-is-above-by-n (setp (set) ∧ listp (nthcdr (n, set))) → (car (nthcdr (n, set)) ≮ (n + car (set)))

;;;;;;;;;;;
; now, suppose Z is omega^alpha + omega + d large (say, alpha > 0),
; and z = min(Z).   Let Q = (nthcdr (magic(z +d )  Z))
; then Q is omega^alpha large (in particular, non-empty) , and
; then, by the above, Q is a subset of Z and min(Q)  >= magic(z + d)
; we consider the three types of ordinals in sequence.
; one more simple fact -- needed in the following inductive proofs

Theorem: nthcdr-of-cdr (k ≄ 0) → (nthcdr (k − 1, cdr (set)) = nthcdr (k, set))

; type A  : (cons alpha (cons 1 k)) : k > 0  : omega^alpha + omega + k
; we iterate k times to get to Z' which is omega^alpha + omega -- large

Theorem: cdr-large-a (setp (set) ∧ ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (0 < k) ∧ o-largep (set, cons (alpha, cons (1, k)))) → o-largep (cdr (set), cons (alpha, cons (1, k − 1)))

Definition: bad-for-nthcdr-large-a (set, alpha, k) = (setp (set)

∧ ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (k ∈ N) ∧ o-largep (set, cons (alpha, cons (1, k))) ∧ ((¬ setp (nthcdr (k, set)))

∨ (¬ o-largep (nthcdr (k, set), cons (alpha, cons (1, 0))))))

Theorem: nthcdr-large-a-aux1 (k ≃ 0) → (¬ bad-for-nthcdr-large-a (set, alpha, k))

Theorem: nthcdr-large-a-aux2 setp (cons (z, x)) → setp (x)

Theorem: nthcdr-large-a-aux3 o-largep (v, cons (alpha, cons (1, k))) → listp (v)

Theorem: nthcdr-large-a-aux4 ((k ≄ 0) ∧ bad-for-nthcdr-large-a (set, alpha, k)) → bad-for-nthcdr-large-a (cdr (set), alpha, k − 1)

; force correct induction

Definition: nthcdr-large-a-kludge (set, alpha, k) = if 0 < k then nthcdr-large-a-kludge (cdr (set), alpha, k − 1)

else 0 endif

Theorem: nthcdr-large-a-aux5 ¬ bad-for-nthcdr-large-a (set, alpha, k)

Theorem: nthcdr-large-a (setp (set) ∧ ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (k ∈ N) ∧ o-largep (set, cons (alpha, cons (1, k)))) → (setp (nthcdr (k, set))

∧ o-largep (nthcdr (k, set), cons (alpha, cons (1, 0))))

Event: Disable nthcdr-large-a-aux1.

Event: Disable nthcdr-large-a-aux2.

Event: Disable nthcdr-large-a-aux3.

Event: Disable nthcdr-large-a-aux4.

Event: Disable nthcdr-large-a-aux5.

Event: Disable bad-for-nthcdr-large-a.

Event: Disable nthcdr-large-a-kludge.

; repeat for
; type B  : (cons alpha  k) : k > 0  : omega^alpha +  k
; start with Z whih is omega^alpha +  k -- large
; we iterate k times to get to Z' which is omega^alpha  -- large

Theorem: cdr-large-b (setp (set) ∧ ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (0 < k) ∧ o-largep (set, cons (alpha, k))) → o-largep (cdr (set), cons (alpha, k − 1))

Definition: bad-for-nthcdr-large-b (set, alpha, k) = (setp (set)

∧ ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (k ∈ N) ∧ o-largep (set, cons (alpha, k)) ∧ ((¬ setp (nthcdr (k, set)))

∨ (¬ o-largep (nthcdr (k, set), cons (alpha, 0)))))

Theorem: nthcdr-large-b-aux1 (k ≃ 0) → (¬ bad-for-nthcdr-large-b (set, alpha, k))

Theorem: nthcdr-large-b-aux2 setp (cons (z, x)) → setp (x)

Theorem: nthcdr-large-b-aux4 ((k ≄ 0) ∧ bad-for-nthcdr-large-b (set, alpha, k)) → bad-for-nthcdr-large-b (cdr (set), alpha, k − 1)

; force correct induction

Definition: nthcdr-large-b-kludge (set, alpha, k) = if 0 < k then nthcdr-large-b-kludge (cdr (set), alpha, k − 1)

else 0 endif

Theorem: nthcdr-large-b-aux5 ¬ bad-for-nthcdr-large-b (set, alpha, k)

Theorem: nthcdr-large-b (setp (set) ∧ ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (k ∈ N) ∧ o-largep (set, cons (alpha, k))) → (setp (nthcdr (k, set)) ∧ o-largep (nthcdr (k, set), cons (alpha, 0)))

Event: Disable nthcdr-large-b-aux1.

Event: Disable nthcdr-large-b-aux2.

Event: Disable nthcdr-large-b-aux4.

Event: Disable nthcdr-large-b-aux5.

Event: Disable bad-for-nthcdr-large-b.

Event: Disable nthcdr-large-b-kludge.

; type C  : (cons alpha (cons 1 0))  : omega^alpha + omega
; start with Z which is omega^alpha + omega -- large
; then its cdr is a set and is omega^alpha + (magic z) + 2 -- large

Theorem: nthcdr-c-1 (setp (set) ∧ ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ o-largep (set, cons (alpha, cons (1, 0)))) → setp (cdr (set))

Theorem: nthcdr-c-2 (setp (set) ∧ ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ o-largep (set, cons (alpha, cons (1, 0)))) → o-largep (cdr (set), cons (alpha, magic (car (set)) + 2))

; now; return to the tail lemma:
; Suppose ZZ is a set which is omega^alpha + omega + d  -- large.
; let z = min ZZ.
; If we take cdr's magic(z+d) times, we get a set QQ such that
; 1. QQ is a set and omega^alpha -- large
; 2. QQ is a subset of ZZ
; 3. min(QQ) >= min(ZZ) + magic(z+d).
; call these parts tail-lemma-1, tail-lemma-2, tail-lemma-3

; First, apply the reductions for types A, C, B in sequence,
; to get an omega^alpha -- large set

Theorem: tail-lemma-1-aux1 (setp (zz) ∧ ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (d ∈ N) ∧ o-largep (zz, cons (alpha, cons (1, d))) ∧ (z1 = nthcdr (d, zz)) ∧ (z2 = cdr (z1 )) ∧ (z3 = nthcdr (magic (car (z1 )) + 2, z2 ))) → (setp (z3 ) ∧ o-largep (z3 , cons (alpha, 0)))

Theorem: tail-lemma-1-aux2 (setp (zz) ∧ ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (d ∈ N) ∧ o-largep (zz, cons (alpha, cons (1, d))) ∧ (z1 = nthcdr (d, zz)) ∧ (z2 = cdr (z1 )) ∧ (z3 = nthcdr (magic (car (nthcdr (d, zz))) + 2, cdr (nthcdr (d, zz))))) → (setp (z3 ) ∧ o-largep (z3 , cons (alpha, 0)))

Theorem: tail-lemma-1-aux3 nthcdr (i, cdr (set)) = nthcdr (1 + i, set)

Theorem: tail-lemma-1-aux4 nthcdr (j + 2, cdr (nthcdr (d, zz))) = nthcdr (1 + (j + 2), nthcdr (d, zz))

Theorem: tail-lemma-1-aux5 nthcdr (j + 2, cdr (nthcdr (d, zz))) = nthcdr (j + 3 + d, zz)

Theorem: tail-lemma-1-aux6 nthcdr (magic (car (nthcdr (d, zz))) + 2, cdr (nthcdr (d, zz))) = nthcdr (magic (car (nthcdr (d, zz))) + 3 + d, zz)

Theorem: tail-lemma-1-aux7 (setp (zz) ∧ ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (d ∈ N) ∧ o-largep (zz, cons (alpha, cons (1, d))) ∧ (z3 = nthcdr (magic (car (nthcdr (d, zz))) + 3 + d, zz))) → (setp (z3 ) ∧ o-largep (z3 , cons (alpha, 0)))

; now, what we want is not Z3, but
; QQ = (nthcdr (magic (plus (car ZZ) d))  ZZ)
; so, we need that QQ is a subset of Z3, which involves
; showing that
;  (magic (plus (car ZZ) d)) <= (plus (magic (car (nthcdr d ZZ))) 3 d)
; magic is monotonic, so we need only:
; (plus (car ZZ) d) <=  (car (nthcdr d ZZ))

Theorem: tail-lemma-1-aux8 (setp (zz) ∧ ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (d ∈ N) ∧ o-largep (zz, cons (alpha, cons (1, d)))) → listp (nthcdr (d, zz))

Theorem: tail-lemma-1-aux9 (setp (zz) ∧ ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (d ∈ N) ∧ o-largep (zz, cons (alpha, cons (1, d)))) → (car (nthcdr (d, zz)) ≮ (car (zz) + d))

Theorem: tail-lemma-1-aux10 (setp (zz) ∧ ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (d ∈ N) ∧ o-largep (zz, cons (alpha, cons (1, d)))) → (magic (car (nthcdr (d, zz))) ≮ magic (car (zz) + d))

Theorem: tail-lemma-1-aux11 (setp (zz) ∧ ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (d ∈ N) ∧ o-largep (zz, cons (alpha, cons (1, d)))) → (magic (car (zz) + d) < (magic (car (nthcdr (d, zz))) + 3 + d))

Theorem: tail-lemma-1-aux12 (i < j ) → (((j − i) + i) = j )

Theorem: tail-lemma-1-aux13 (i < j ) → subsetp (nthcdr (j , zz), nthcdr (i, zz))

Theorem: tail-lemma-1-aux14 (setp (zz) ∧ ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (d ∈ N) ∧ o-largep (zz, cons (alpha, cons (1, d))) ∧ (qq = nthcdr (magic (car (zz) + d), zz)) ∧ (z3 = nthcdr (magic (car (nthcdr (d, zz))) + 3 + d, zz))) → subsetp (z3 , qq)

; now, QQ will be a set if it's not 0

Theorem: tail-lemma-1-aux15 (setp (zz) ∧ ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (d ∈ N) ∧ o-largep (zz, cons (alpha, cons (1, d))) ∧ (z3 = nthcdr (magic (car (nthcdr (d, zz))) + 3 + d, zz))) → listp (z3 )

; all these aux lemmas are getting in our way now -- let's
; just disable them and just quote the ones we need

Event: Disable tail-lemma-1-aux1. Event: Disable tail-lemma-1-aux2. Event: Disable tail-lemma-1-aux3. Event: Disable tail-lemma-1-aux4. Event: Disable tail-lemma-1-aux5. Event: Disable tail-lemma-1-aux6. Event: Disable tail-lemma-1-aux7. Event: Disable tail-lemma-1-aux8. Event: Disable tail-lemma-1-aux9. Event: Disable tail-lemma-1-aux10. Event: Disable tail-lemma-1-aux11. Event: Disable tail-lemma-1-aux12. Event: Disable tail-lemma-1-aux13. Event: Disable tail-lemma-1-aux14. Event: Disable tail-lemma-1-aux15. Theorem: tail-lemma-1-aux16 (setp (zz) ∧ ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (d ∈ N) ∧ o-largep (zz, cons (alpha, cons (1, d)))

∧ (qq = nthcdr (magic (car (zz) + d), zz)) ∧ (z3 = nthcdr (magic (car (nthcdr (d, zz))) + 3 + d, zz))) → listp (qq)

Event: Disable tail-lemma-1-aux16.

Theorem: tail-lemma-1-aux17 (setp (zz) ∧ ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (d ∈ N) ∧ o-largep (zz, cons (alpha, cons (1, d))) ∧ (qq = nthcdr (magic (car (zz) + d), zz)) ∧ (z3 = nthcdr (magic (car (nthcdr (d, zz))) + 3 + d, zz))) → (setp (qq) ∧ o-largep (qq, cons (alpha, 0)))

Theorem: tail-lemma-1 (setp (zz) ∧ ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (d ∈ N) ∧ o-largep (zz, cons (alpha, cons (1, d))) ∧ (qq = nthcdr (magic (car (zz) + d), zz))) → (setp (qq) ∧ o-largep (qq, cons (alpha, 0)))

Event: Disable tail-lemma-1-aux17.

; now return to parts 2 and 3 of the tail-lemma:
; Suppose ZZ is a set which is omega^alpha + omega + d  -- large.
; let z = min ZZ.
; If we take cdr's magic(z+d) times, we get a set QQ such that
; 1. QQ is a set and omega^alpha -- large
; 2. QQ is a subset of ZZ
; 3. min(QQ) >= min(ZZ) + magic(z+d).
; call these parts tail-lemma-1, tail-lemma-2, tail-lemma-3

Theorem: tail-lemma-2 (setp (zz) ∧ ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (d ∈ N) ∧ o-largep (zz, cons (alpha, cons (1, d)))

∧ (qq = nthcdr (magic (car (zz) + d), zz))) → subsetp (qq, zz)

Theorem: tail-lemma-aux1 (setp (zz) ∧ ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (d ∈ N) ∧ o-largep (zz, cons (alpha, cons (1, d))) ∧ (qq = nthcdr (magic (car (zz) + d), zz))) → listp (qq)

Theorem: tail-lemma-3 (setp (zz) ∧ ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (d ∈ N) ∧ o-largep (zz, cons (alpha, cons (1, d))) ∧ (qq = nthcdr (magic (car (zz) + d), zz))) → (car (qq) ≮ (car (zz) + magic (car (zz) + d)))

Event: Disable tail-lemma-aux1.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;                    PROPERTIES OF PHI AND STAR                          ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; phi(alpha, c) = omega^alpha + omega + norm(alpha) + c

Definition: phi (alpha, c) = if ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (c ∈ N)

then cons (alpha, cons (1, norm (alpha) + c)) else norm (alpha) + norm (alpha) + c + 3 endif

Theorem: phi-is-an-ord ordinalp (phi (alpha, c))

Theorem: norm-of-phi (c ∈ N) → (norm (phi (alpha, c)) = (norm (alpha) + norm (alpha) + c + 3))

Definition: star (alpha, n) = if n ≃ 0 then 0

else sharp (alpha, star (alpha, n − 1)) endif Theorem: star-is-an-ord ordinalp (alpha) → ordinalp (star (alpha, n))

Theorem: star-with-0 (n ≃ 0) → (star (alpha, n) = 0)

Theorem: star-with-1 ordinalp (alpha) → (star (alpha, 1) = alpha)

Theorem: norm-of-star (ordinalp (alpha) ∧ (n ∈ N)) → (norm (star (alpha, n)) = (n ∗ norm (alpha)))

Theorem: sharp-with-0-reversed ordinalp (alpha) → (sharp (alpha, 0) = alpha)

Theorem: car-of-star (ordinalp (alpha) ∧ (0 < n)) → (car (star (alpha, n)) = car (alpha))

;; now we show: "bound-on-phi":
; if alpha < beta , then phi(alpha,c) * n < omega^beta  (for any n)

Theorem: bound-on-phi-aux1 ordinalp (alpha) → ((¬ ord-leq (1, alpha)) = (alpha = 0))

Theorem: bound-on-phi-aux2 ord-lessp (car (sigma), car (tau)) → ord-lessp (sigma, tau)

; now, we just need to look at the cars:

Theorem: car-of-phi (ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (c ∈ N)) → (car (phi (alpha, c)) = alpha)

Theorem: bound-on-phi-aux3 (ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (c ∈ N) ∧ (n ≄ 0)) → (car (star (phi (alpha, c), n)) = alpha)

Theorem: bound-on-phi-aux4 (ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (c ∈ N) ∧ (n ≃ 0)) → (car (star (phi (alpha, c), n)) = 0)

Theorem: bound-on-phi-aux5 (ordinalp (alpha) ∧ (¬ ord-leq (1, alpha))) → (car (star (phi (alpha, c), n)) = 0)

Theorem: bound-on-phi (ordinalp (alpha) ∧ ordinalp (beta) ∧ ord-lessp (alpha, beta) ∧ (c ∈ N)) → ord-lessp (star (phi (alpha, c), n), cons (beta, 0))

Event: Disable bound-on-phi-aux1.

Event: Disable bound-on-phi-aux2.

Event: Disable bound-on-phi-aux3.

Event: Disable bound-on-phi-aux4.

Event: Disable bound-on-phi-aux5.

;;; we plan to apply norm-star-phi with n = c^{2^z}

Theorem: norm-star-phi-aux1 (ordinalp (alpha) ∧ (n ∈ N) ∧ (c ∈ N)) → (norm (star (phi (alpha, c), n))

= (n ∗ (norm (alpha) + norm (alpha) + c + 3)))

; revise the format to be consistent with lemma magic-18 in Basic arithmetic
; We need some trivial arithmetic to do this.

Theorem: times-with-zero-1 (x ≃ 0) → ((x ∗ y) = 0)

Theorem: times-with-zero-2 (y ≃ 0) → ((x ∗ y) = 0)

Theorem: commut-of-times-aux1 (z ∈ N) → ((y ∗ (1 + z)) = (y + (z ∗ y)))

Theorem: commut-of-times (x ∗ y) = (y ∗ x)

Theorem: norm-star-phi-aux2 ((x ∈ N) ∧ (c ∈ N)) → (((x + x) + (1 + (2 + c))) = (x + x + c + 3))

Theorem: norm-star-phi-aux3 ((x ∈ N) ∧ (n ∈ N) ∧ (c ∈ N)) → ((n ∗ (x + x + c + 3)) = (((2 ∗ x) + 3 + c) ∗ n))

Theorem: norm-star-phi (ordinalp (alpha) ∧ (n ∈ N) ∧ (c ∈ N)) → (norm (star (phi (alpha, c), n))

= (((2 ∗ norm (alpha)) + 3 + c) ∗ n))

Event: Disable norm-star-phi-aux1.

Event: Disable norm-star-phi-aux2.

Event: Disable norm-star-phi-aux3.

Event: Disable phi.

; probably we don't need its defn again

;;;;; lemma "norm-star-exp-phi"
;; One more arithmetic fact about phi -- to be used
; in the "cdr-lemma" below.
; suppose  alpha-hat = {alpha}(z),  c > 0
; d = norm(alpha) + c, and q >= magic(z+d).
; Then:    norm(phi(alpha-hat, c) * c^(2^z)) <= magic(q).
; reason   norm(alpha-hat) <= norm(alpha) + magic(z)
; so norm(phi(alpha-hat, c) * c^(2^z)) <=
;     2 norm (alpha) + 2 magic(z) + 3 + c  <=
;     magic(q)    (by lemma magic-18)
; first, all we use about alpha-hat is its norm

Theorem: norm-star-exp-phi-aux1 (alpha-hat = pred (alpha, z)) → (norm (alpha-hat) ≤ (norm (alpha) + magic (z)))

; second, plug alpha-hat into norm-star-phi

Theorem: norm-star-exp-phi-aux2 (ordinalp (alpha) ∧ (n ∈ N) ∧ (c ∈ N) ∧ (alpha-hat = pred (alpha, z))) → (norm (star (phi (alpha-hat, c), n))

= (((2 ∗ norm (alpha-hat)) + 3 + c) ∗ n))

; now, we apply aux1 to get an inequality
; since this involves a product with n, we need some preliminary
; arithmetic.  Think of
; a = norm(alpha)
; a-hat = norm(alpha-hat)
; nsp = (norm (star (phi alpha-hat c) n ))
; mz = (magic z)

Theorem: norm-star-exp-phi-aux3 (a-hat ≤ (a + mz)) → (((2 ∗ a-hat) + 3 + c)

≤ ((2 ∗ a) + (2 ∗ mz) + 3 + c))

Theorem: norm-star-exp-phi-aux4 (a-hat ≤ (a + mz)) → ((((2 ∗ a-hat) + 3 + c) ∗ n)

≤ (((2 ∗ a) + (2 ∗ mz) + 3 + c) ∗ n))

Theorem: norm-star-exp-phi-aux5 ((nsp = (((2 ∗ a-hat) + 3 + c) ∗ n)) ∧ (a-hat ≤ (a + mz))) → (nsp ≤ (((2 ∗ a) + (2 ∗ mz) + 3 + c) ∗ n))

Theorem: norm-star-exp-phi-aux6 (ordinalp (alpha) ∧ (n ∈ N) ∧ (c ∈ N) ∧ (alpha-hat = pred (alpha, z))) → (norm (star (phi (alpha-hat, c), n))

≤ (((2 ∗ norm (alpha)) + (2 ∗ magic (z)) + 3 + c) ∗ n))

Theorem: norm-star-exp-phi (ordinalp (alpha) ∧ (alpha-hat = pred (alpha, z)) ∧ (c ≄ 0) ∧ (d = (norm (alpha) + c)) ∧ (magic (z + d) ≤ q)) → (norm (star (phi (alpha-hat, c), expt (c, expt (2, z)))) ≤ magic (q))

Event: Disable norm-star-exp-phi-aux1.

Event: Disable norm-star-exp-phi-aux2.

Event: Disable norm-star-exp-phi-aux3.

Event: Disable norm-star-exp-phi-aux4.

Event: Disable norm-star-exp-phi-aux5. Event: Disable norm-star-exp-phi-aux6. Event: Disable norm-star-phi.

; this is firing when we don't want it to

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;                             THE CDR LEMMA                              ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Suppose ZZ is a set which is phi(alpha,c) -- large ; alpha >= 1 ; c >= 1
; let z = min ZZ, and alpha-hat = {alpha}(z)
; then
; 1. (cdr ZZ) is a set
; 2. (cdr ZZ) is phi(alpha-hat,c) * c^(2^z)  --  large
; call these cdr-lemma-1 and cdr-lemma-2
; cdr-lemma-1 should be a triviality -- it just says that ZZ is non-empty

Theorem: cdr-lemma-1 (setp (zz) ∧ o-largep (zz, phi (alpha, c))) → setp (cdr (zz))

; for cdr-lemma-2, let
;        d = norm(alpha) + c
;        QQ = (nthcdr (magic (plus (car ZZ) d)) ZZ )
;         q = (car QQ)
; by defn of phi, ZZ is omega^alpha + omega + d -- large
; then
; QQ is a set and is omega^alpha -- large (by tail-lemma-1)
; q >= z + magic(z+d)  (by tail-lemma 3)
; phi(alpha-hat,c)* c^(2^z) < omega^alpha (by bound-on-phi)
; norm( phi(alpha-hat,c)* c^(2^z)) <= magic(q) (by norm-star-exp-phi)
; QQ is phi(alpha-hat,c) * c^(2^z)  --  large  (by large-with-smaller-ord)
; QQ is a subset of (cdr Z)  (since (magic (plus (car ZZ) d)) >= 1)
; (cdr ZZ) is phi(alpha-hat,c) * c^(2^z)  --  large  (by large-goes-up)
; unwind defn of phi

Theorem: cdr-lemma-aux1 (ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (c ∈ N) ∧ setp (zz) ∧ o-largep (zz, phi (alpha, c)) ∧ (d = (norm (alpha) + c))) → o-largep (zz, cons (alpha, cons (1, d)))

Theorem: cdr-lemma-aux2 (ordinalp (alpha)

∧ ord-leq (1, alpha) ∧ (c ∈ N) ∧ setp (zz) ∧ o-largep (zz, phi (alpha, c)) ∧ (d = (norm (alpha) + c)) ∧ (qq = nthcdr (magic (car (zz) + d), zz))) → (setp (qq) ∧ o-largep (qq, cons (alpha, 0)))

Theorem: cdr-lemma-aux3 (ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (c ∈ N) ∧ setp (zz) ∧ o-largep (zz, phi (alpha, c)) ∧ (d = (norm (alpha) + c)) ∧ (qq = nthcdr (magic (car (zz) + d), zz))) → ((car (zz) + magic (car (zz) + d)) ≤ car (qq))

Theorem: cdr-lemma-aux4 (ordinalp (alpha) ∧ ord-leq (1, alpha)) → ord-lessp (0, alpha)

Theorem: cdr-lemma-aux5 (ordinalp (alpha) ∧ ord-leq (1, alpha)) → ord-lessp (pred (alpha, z), alpha)

Theorem: cdr-lemma-aux6 (ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (c ∈ N) ∧ (alpha-hat = pred (alpha, z))) → ord-lessp (star (phi (alpha-hat, c), n), cons (alpha, 0))

Theorem: cdr-lemma-aux7 (ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (c ≄ 0) ∧ setp (zz) ∧ (alpha-hat = pred (alpha, car (zz))) ∧ o-largep (zz, phi (alpha, c)) ∧ (d = (norm (alpha) + c)) ∧ (qq = nthcdr (magic (car (zz) + d), zz))) → (norm (star (phi (alpha-hat, c), expt (c, expt (2, car (zz)))))

≤ magic (car (qq)))

; the form of large-with-smaller-ord we need:

Theorem: cdr-lemma-aux8 (ordinalp (sigma) ∧ ordinalp (tau) ∧ setp (qq) ∧ o-largep (qq, tau) ∧ ord-lessp (sigma, tau) ∧ (norm (sigma) ≤ magic (car (qq)))) → o-largep (qq, sigma)

Theorem: cdr-lemma-aux9 (ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (c ≄ 0) ∧ (alpha-hat = pred (alpha, car (zz))) ∧ setp (zz) ∧ o-largep (zz, phi (alpha, c)) ∧ (d = (norm (alpha) + c)) ∧ (qq = nthcdr (magic (car (zz) + d), zz))) → o-largep (qq, star (phi (alpha-hat, c), expt (c, expt (2, car (zz)))))

; we know that (cdr ZZ) is a set (cdr-lemma-1) and
; that QQ is a set (aux2)
; now we just need that QQ is a subset of (cdr ZZ)

Theorem: cdr-lemma-aux10 (setp (zz) ∧ o-largep (zz, phi (alpha, c))) → listp (zz)

Theorem: cdr-lemma-aux11 2 < magic (s)

Theorem: cdr-lemma-aux12 (x ≄ 0) → (nthcdr (x, zz) = nthcdr (x − 1, cdr (zz)))

Theorem: cdr-lemma-aux13 (x ≄ 0) → subsetp (nthcdr (x, zz), cdr (zz))

Theorem: cdr-lemma-aux14 (setp (zz) ∧ (qq = nthcdr (magic (u), zz))) → subsetp (qq, cdr (zz))

Theorem: cdr-lemma-aux15 (ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (c ∈ N) ∧ setp (zz) ∧ o-largep (zz, phi (alpha, c))) → setp (nthcdr (magic (car (zz) + (norm (alpha) + c)), zz))

; disable all the aux's now -- the prover doesn't get them right

Event: Disable cdr-lemma-aux1. Event: Disable cdr-lemma-aux2. Event: Disable cdr-lemma-aux3. Event: Disable cdr-lemma-aux4. Event: Disable cdr-lemma-aux5. Event: Disable cdr-lemma-aux6. Event: Disable cdr-lemma-aux7. Event: Disable cdr-lemma-aux8. Event: Disable cdr-lemma-aux9. Event: Disable cdr-lemma-aux10. Event: Disable cdr-lemma-aux11. Event: Disable cdr-lemma-aux12. Event: Disable cdr-lemma-aux13. Event: Disable cdr-lemma-aux14. Event: Disable cdr-lemma-aux15. Theorem: cdr-lemma-2 (ordinalp (alpha) ∧ ord-leq (1, alpha) ∧ (c ≄ 0)

∧ (alpha-hat = pred (alpha, car (zz))) ∧ setp (zz) ∧ o-largep (zz, phi (alpha, c))) → o-largep (cdr (zz), star (phi (alpha-hat, c), expt (c, expt (2, car (zz)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;                      THE PIGEON-HOLE PRINCIPLE                         ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; We need a pigeon lemma which says:  If c>0,
;  (mapsto g XX lst),   XX is alpha * c -- large, and c >= |lst|
; then there is a  set YY such that YY is a subset of XX,
; YY is alpha -- large and  g is constant on YY.
; YY will be computed as: (extract-pigeon g XX lst alpha c)
; then the lemma has 4 parts:
; "pigeon-A" says that YY is a subset of XX
; "pigeon-B" says that YY is a set
; "pigeon-C" says that g is constant on YY
; "pigeon-D" says that YY is alpha-large

;;;; first, some facts about mapsto and constant
; define "g is constant on lst"

Definition: constantp (g, lst) = if lst ≃ nil then t

elseif cdr (lst) ≃ nil then t

else (funcall (g, car (lst)) = funcall (g, cadr (lst))) ∧ constantp (g, cdr (lst)) endif

Theorem: constant-same-value (constantp (g, lst) ∧ (x ∈ lst) ∧ (y ∈ lst)) → (funcall (g, x) = funcall (g, y))

; constantp is trivially true for lists of length 0 and 1

Theorem: constant-0 (lst ≃ nil) → constantp (g, lst)

Theorem: constant-1 (cdr (lst) ≃ nil) → constantp (g, lst)

; if not (constantp g lst),  there is a pair of members
; dif1(g,lst) and dif2(g,lst) such that
; g(dif1(g,lst)) != g(dif2(g,lst))

Definition: dif-pair (g, lst) = if lst ≃ nil then nil

elseif cdr (lst) ≃ nil then nil

elseif funcall (g, car (lst)) ≠ funcall (g, cadr (lst))

then cons (car (lst), cadr (lst)) else dif-pair (g, cdr (lst)) endif

Definition: dif1 (g, lst) = car (dif-pair (g, lst))

Definition: dif2 (g, lst) = cdr (dif-pair (g, lst))

Theorem: non-constant-different-values (¬ constantp (g, lst)) → ((dif1 (g, lst) ∈ lst)

∧ (dif2 (g, lst) ∈ lst)

∧ (funcall (g, dif1 (g, lst)) ≠ funcall (g, dif2 (g, lst))))

Event: Disable constantp.

Event: Disable dif-pair.

Event: Disable dif1.

Event: Disable dif2.

; if (mapgst g XX lst) and (length lst) <= 1 then g is constant on XX:

Theorem: constant-range-1-aux1 ((length (lst) ≤ 1) ∧ (u ∈ lst) ∧ (v ∈ lst)) → (u = v)

Theorem: constant-range-1 (mapsto (g, xx, lst) ∧ (length (lst) ≤ 1)) → constantp (g, xx)

Event: Disable constant-range-1-aux1.

;;;;; we prove the pigeon-hole principle as follows:
; Suppose (mapsto g XX lst) , and (listp lst)
; there are two subsets of XX:
; AA = (first-part g XX lst) = set of elements of XX which
;   map to the element (car lst)
; BB = (rest-part g XX lst) = set of elements of XX which
;   map into (cdr lst)
; then (covers AA BB XX), g is constant on AA, and maps BB to (cdr lst)
; (star alpha n) is (sharp alpha (star alpha (sub1 n)))
; so we will have that if XX is (star alpha n) -- large
; then either AA is alpha-large or BB is
;       (sharp alpha (star alpha (sub1 n))) -- large
;  AA:

Definition: first-part (g, xx, lst) = if xx ≃ nil then nil

elseif funcall (g, car (xx)) = car (lst)

then cons (car (xx), first-part (g, cdr (xx), lst))

else first-part (g, cdr (xx), lst) endif

Theorem: value-on-first-part (x ∈ first-part (g, xx, lst)) → (funcall (g, x) = car (lst))

Theorem: constantp-on-first-part constantp (g, first-part (g, xx, lst))

; BB:

Definition: rest-part (g, xx, lst) = if xx ≃ nil then nil

elseif funcall (g, car (xx)) ∈ cdr (lst)

then cons (car (xx), rest-part (g, cdr (xx), lst))

else rest-part (g, cdr (xx), lst) endif

Theorem: values-on-rest-part (x ∈ rest-part (g, xx, lst)) → (funcall (g, x) ∈ cdr (lst))

Theorem: mapsto-rest-part mapsto (g, rest-part (g, xx, lst), cdr (lst))

;; covering properties

Theorem: members-of-first-part (mapsto (g, xx, lst) ∧ (funcall (g, x) = car (lst)) ∧ (x ∈ xx)) → (x ∈ first-part (g, xx, lst))

Theorem: members-of-rest-part (mapsto (g, xx, lst) ∧ (funcall (g, x) ∈ cdr (lst)) ∧ (x ∈ xx)) → (x ∈ rest-part (g, xx, lst))

Theorem: first-rest-member (mapsto (g, xx, lst) ∧ (x ∈ xx)) → ((x ∈ first-part (g, xx, lst)) ∨ (x ∈ rest-part (g, xx, lst)))

Theorem: first-rest-cover mapsto (g, xx, lst) → covers (first-part (g, xx, lst), rest-part (g, xx, lst), xx)

; we also need that the first-part and the rest-part are subsets

Theorem: first-part-is-sublist sublistp (first-part (g, xx, lst), xx)

Theorem: rest-part-is-sublist sublistp (rest-part (g, xx, lst), xx)

Theorem: first-part-is-subset subsetp (first-part (g, xx, lst), xx)

Theorem: rest-part-is-subset subsetp (rest-part (g, xx, lst), xx)

; now, prove they are sets
; this is a little inelegant -- we just repeat the same
; argument for first-part and for rest-part
; first-part

Theorem: first-part-is-set-aux1 (u ∈ first-part (g, xx, lst)) → (u ∈ xx)

Theorem: first-part-is-set-aux2 (u ∈ first-part (g, cdr (xx), lst)) → (u ∈ cdr (xx))

Theorem: first-part-is-set-aux3 (setp (xx) ∧ (u ∈ first-part (g, cdr (xx), lst))) → (car (xx) < u)

Theorem: first-part-is-set-aux4 (setp (xx) ∧ listp (first-part (g, cdr (xx), lst))) → (car (xx) < car (first-part (g, cdr (xx), lst)))

; we need the following trivial set fact:

Event: Enable setp.

Theorem: set-builder (setp (s) ∧ (x ∈ N) ∧ (x < car (s))) → setp (cons (x, s))

Event: Disable setp.

Theorem: first-part-is-set-aux5 (setp (xx) ∧ listp (first-part (g, cdr (xx), lst)) ∧ setp (first-part (g, cdr (xx), lst))) → setp (first-part (g, xx, lst))

Theorem: first-part-is-set-aux6 (first-part (g, xx, lst) ≃ nil) → (first-part (g, xx, lst) = nil)

Theorem: first-part-is-set-aux7 (setp (xx) ∧ (first-part (g, cdr (xx), lst) ≃ nil)) → setp (first-part (g, xx, lst))

Theorem: first-part-is-set-aux8 (¬ listp (xx)) → setp (first-part (g, xx, lst))

Theorem: first-part-is-set-aux9 (setp (xx) ∧ setp (first-part (g, cdr (xx), lst))) → setp (first-part (g, xx, lst))

Theorem: first-part-is-set setp (xx) → setp (first-part (g, xx, lst))

Event: Disable first-part-is-set-aux1.

Event: Disable first-part-is-set-aux2.

Event: Disable first-part-is-set-aux3.

Event: Disable first-part-is-set-aux4.

Event: Disable first-part-is-set-aux5.

Event: Disable first-part-is-set-aux6.

Event: Disable first-part-is-set-aux7.

Event: Disable first-part-is-set-aux8.

Event: Disable first-part-is-set-aux9.

;;; rest-part

Theorem: rest-part-is-set-aux1 (u ∈ rest-part (g, xx, lst)) → (u ∈ xx)

Theorem: rest-part-is-set-aux2 (u ∈ rest-part (g, cdr (xx), lst)) → (u ∈ cdr (xx))

Theorem: rest-part-is-set-aux3 (setp (xx) ∧ (u ∈ rest-part (g, cdr (xx), lst))) → (car (xx) < u)

Theorem: rest-part-is-set-aux4 (setp (xx) ∧ listp (rest-part (g, cdr (xx), lst))) → (car (xx) < car (rest-part (g, cdr (xx), lst)))

Theorem: rest-part-is-set-aux5 (setp (xx) ∧ listp (rest-part (g, cdr (xx), lst)) ∧ setp (rest-part (g, cdr (xx), lst))) → setp (rest-part (g, xx, lst))

Theorem: rest-part-is-set-aux6 (rest-part (g, xx, lst) ≃ nil) → (rest-part (g, xx, lst) = nil)

; a trivial set fact:

Theorem: singleton-set (m ∈ N) → setp (list (m))

Theorem: rest-part-is-set-aux7 (setp (xx) ∧ (rest-part (g, cdr (xx), lst) ≃ nil)) → setp (rest-part (g, xx, lst))

Theorem: rest-part-is-set-aux8 (¬ listp (xx)) → setp (rest-part (g, xx, lst))

Theorem: rest-part-is-set-aux9 (setp (xx) ∧ setp (rest-part (g, cdr (xx), lst))) → setp (rest-part (g, xx, lst))

Theorem: rest-part-is-set setp (xx) → setp (rest-part (g, xx, lst))

Event: Disable rest-part-is-set-aux1.

Event: Disable rest-part-is-set-aux2.

Event: Disable rest-part-is-set-aux3.

Event: Disable rest-part-is-set-aux4.

Event: Disable rest-part-is-set-aux5.

Event: Disable rest-part-is-set-aux6.

Event: Disable rest-part-is-set-aux7.

Event: Disable rest-part-is-set-aux8.

Event: Disable rest-part-is-set-aux9.

;;;;;; now, back to the pigeon-hole principle:
; if (mapsto g XX lst) and XX is alpha * c -- large, and c >= |lst|
; and c > 0,
; then there is a YY subset XX such that YY is alpha -- large
; and g is constant on YY.
; YY will be (extract-pigeon g XX lst alpha c)

Definition: extract-pigeon (g, xx, lst, alpha, c) = if c ≤ 1 then xx

elseif o-largep (first-part (g, xx, lst), alpha) then first-part (g, xx, lst) else extract-pigeon (g, rest-part (g, xx, lst), cdr (lst), alpha, c − 1) endif

; "pigeon-A" says that YY is a subset of XX
; "pigeon-B" says that YY is a set
; "pigeon-C" says that g is constant on YY
; "pigeon-D" says that YY is alpha-large

Theorem: pigeon-a subsetp (extract-pigeon (g, xx, lst, alpha, c), xx)

Theorem: pigeon-b setp (xx) → setp (extract-pigeon (g, xx, lst, alpha, c))

Theorem: pigeon-c-aux1 (mapsto (g, xx, lst) ∧ (length (lst) ≤ c) ∧ (c ≤ 1)) → constantp (g, extract-pigeon (g, xx, lst, alpha, c))

Theorem: pigeon-c-aux2 ((1 < c) ∧ (¬ o-largep (first-part (g, xx, lst), alpha))) → (extract-pigeon (g, xx, lst, alpha, c)

= extract-pigeon (g, rest-part (g, xx, lst), cdr (lst), alpha, c − 1))

Theorem: pigeon-c (mapsto (g, xx, lst) ∧ (length (lst) ≤ c)) → constantp (g, extract-pigeon (g, xx, lst, alpha, c))

Event: Disable pigeon-c-aux1.

Event: Disable pigeon-c-aux2.

; now, for D, we have to induct on c

Definition: bad-for-pigeon-d (g, xx, lst, alpha, c) = (ordinalp (alpha)

∧ setp (xx)

∧ o-largep (xx, star (alpha, c))

∧ mapsto (g, xx, lst) ∧ (length (lst) ≤ c) ∧ (c ≄ 0) ∧ (¬ o-largep (extract-pigeon (g, xx, lst, alpha, c), alpha)))

; basis:

Theorem: pigeon-d-aux1 (c ≃ 0) → (¬ bad-for-pigeon-d (g, xx, lst, alpha, c))

Theorem: pigeon-d-aux2 ¬ bad-for-pigeon-d (g, xx, lst, alpha, 1)

; now we have to work on the induction step, where c > 1:

Theorem: pigeon-d-aux3 ((1 < c) ∧ bad-for-pigeon-d (g, xx, lst, alpha, c)) → (¬ o-largep (first-part (g, xx, lst), alpha))

Theorem: pigeon-d-aux4 ((1 < c) ∧ bad-for-pigeon-d (g, xx, lst, alpha, c)) → (extract-pigeon (g, xx, lst, alpha, c)

= extract-pigeon (g, rest-part (g, xx, lst), cdr (lst), alpha, c − 1))

Theorem: pigeon-d-aux5 (ordinalp (alpha) ∧ (1 < c) ∧ setp (a) ∧ setp (b) ∧ setp (x) ∧ covers (a, b, x) ∧ o-largep (x, star (alpha, c)) ∧ (¬ o-largep (a, alpha))) → o-largep (b, star (alpha, c − 1))

Theorem: pigeon-d-aux6 (ordinalp (alpha) ∧ mapsto (g, xx, lst) ∧ (1 < c) ∧ setp (xx) ∧ o-largep (xx, star (alpha, c)) ∧ (¬ o-largep (first-part (g, xx, lst), alpha))) → o-largep (rest-part (g, xx, lst), star (alpha, c − 1))

; induction step:

Theorem: pigeon-d-aux7 ((1 < c) ∧ listp (lst) ∧ bad-for-pigeon-d (g, xx, lst, alpha, c)) → bad-for-pigeon-d (g, rest-part (g, xx, lst), cdr (lst), alpha, c − 1)

; now, what if lst is empty

Theorem: pigeon-d-aux8 (mapsto (g, xx, lst) ∧ (¬ listp (lst))) → (¬ listp (xx))

Theorem: pigeon-d-aux9 (ordinalp (alpha) ∧ (alpha ≠ 0) ∧ (c ≄ 0)) → (star (alpha, c) ≠ 0)

Theorem: pigeon-d-aux10 (ordinalp (alpha) ∧ (c ≄ 0) ∧ o-largep (xx, star (alpha, c)) ∧ (xx ≃ nil)) → (alpha = 0)

Theorem: pigeon-d-aux11 ((c ≄ 0) ∧ (lst ≃ nil)) → (¬ bad-for-pigeon-d (g, xx, lst, alpha, c))

; revised induction step:

Theorem: pigeon-d-aux12 ((1 < c) ∧ bad-for-pigeon-d (g, xx, lst, alpha, c)) → bad-for-pigeon-d (g, rest-part (g, xx, lst), cdr (lst), alpha, c − 1)

; rephrase the  basis

Theorem: pigeon-d-aux13 (1 ≮ c) → (¬ bad-for-pigeon-d (g, xx, lst, alpha, c))

Theorem: pigeon-d-aux14 ¬ bad-for-pigeon-d (g, xx, lst, alpha, c)

Theorem: pigeon-d (ordinalp (alpha) ∧ setp (xx) ∧ o-largep (xx, star (alpha, c)) ∧ mapsto (g, xx, lst) ∧ (length (lst) ≤ c) ∧ (c ≄ 0)) → o-largep (extract-pigeon (g, xx, lst, alpha, c), alpha)

Event: Disable bad-for-pigeon-d.

Event: Disable pigeon-d-aux1.

Event: Disable pigeon-d-aux2.

Event: Disable pigeon-d-aux3.

Event: Disable pigeon-d-aux4.

Event: Disable pigeon-d-aux5.

Event: Disable pigeon-d-aux6.

Event: Disable pigeon-d-aux7.

Event: Disable pigeon-d-aux8.

Event: Disable pigeon-d-aux9.

Event: Disable pigeon-d-aux10.

Event: Disable pigeon-d-aux11.

Event: Disable pigeon-d-aux12.

Event: Disable pigeon-d-aux13.

Event: Disable pigeon-d-aux14.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;                                 RANGES                                 ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; We follow the usual set-theoretic convention that a partition into
; c pieces is just a map into c = {0 ... c-1}.
; when we work with partitions g on tuples from a set XX --
; it will be simpler to just assume that g of anything is < c
; Since our definition has (funcall g x) = 0 whenever x is
; outside the natural range of g, this will not cause any problem
; first, let's define the intended domain of g

Definition: domain (g) = if g ≃ nil then nil

elseif listp (car (g)) then cons (caar (g), domain (cdr (g)))

else domain (cdr (g)) endif

; even for 0, if 0 is not in (domain g), then (assoc 0 g) is an
; atom, so its cdr is 0

Theorem: assoc-outside-domain (x ∉ domain (g)) → (cdr (assoc (x, g)) = 0)

Event: Enable funcall.

Theorem: funcall-outside-domain (x ∉ domain (g)) → (funcall (g, x) = 0)

Event: Disable funcall.

Definition: rangep (g, c) = if g ≃ nil then 0 < c

else rangep (cdr (g), c) ∧ (cadar (g) ∈ N) ∧ (cadar (g) < c) endif

Theorem: rangep-is-positive rangep (g, c) → ((0 < c) = t)

Theorem: rangep-bounds rangep (g, c) → (funcall (g, x) < c)

Theorem: rangep-numbers rangep (g, c) → (funcall (g, x) ∈ N)

Event: Disable rangep.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;                             SEGMENTS                                  ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;; we need some more on segments now, since (segment 0 c) will
;; be used as the range of a function

Event: Enable segment.

Theorem: segments-non-empty ((m ≤ n) ∧ (m ∈ N) ∧ (n ∈ N)) → listp (segment (m, n))

Theorem: car-of-segment listp (segment (m, n)) → (car (segment (m, n)) = m)

Theorem: cdr-of-segment listp (segment (m, n)) → (cdr (segment (m, n)) = segment (1 + m, n))

Theorem: empty-segment ((m ∉ N) ∨ (n ∉ N) ∨ (n < m)) → (segment (m, n) = nil)

Theorem: non-list-segment (¬ listp (segment (m, n))) → (segment (m, n) = nil)

Theorem: recursive-case-for-segment ((m ≤ n) ∧ (m ∈ N) ∧ (n ∈ N)) → (segment (m, n) = cons (m, segment (1 + m, n)))

Event: Disable segment.

Theorem: singleton-segment (m ∈ N) → (segment (m, m) = list (m))

Theorem: cadr-of-segment listp (cdr (segment (m, n))) → (cadr (segment (m, n)) = (1 + m))

; let's prove segments are sets -- this is a bit of a pain

Definition: bad-for-segments-are-sets (m, n) = (¬ setp (segment (m, n)))

Theorem: segments-are-sets-aux1 bad-for-segments-are-sets (m, n) → ((m ∈ N) ∧ (n ∈ N) ∧ (m ≤ n))

Theorem: segments-are-sets-aux2 (m ∈ N) → (¬ bad-for-segments-are-sets (m, m))

Theorem: segments-are-sets-aux3 (¬ ((m ∈ N) ∧ (n ∈ N) ∧ (m < n))) → (¬ bad-for-segments-are-sets (m, n))

Theorem: segments-are-sets setp (segment (m, n))

Event: Disable segments-are-sets-aux1.

Event: Disable segments-are-sets-aux2.

Event: Disable segments-are-sets-aux3.

Event: Disable bad-for-segments-are-sets.

; another trivial segment fact:

Theorem: first-of-segment ((m ∈ N) ∧ (n ∈ N) ∧ (m ≤ n)) → (car (segment (m, n)) = m)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;                      BASIS OF RAMSEY THEOREM                           ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; This will be "ramsey-basis" -- the Ramsey theorem for 1-tuples.
; Suppose (rangep g c) (so c > 0), XX is a set which is alpha * c -- large.
; Then there is a  set YY such that YY is a subset of XX,
; YY is alpha -- large,  g is constant on the singletons of YY --
; that is:  (homp YY g 1)
; the proof is to define an auxilliary function h -- so that
; (funcall h x) = (funcall g (list x)),
; and then apply the pigeon-hole principle
; call this h "(sing-fn g)"
; this will be (sing-fn-aux g (domain g))
; if h = (sing-fn-aux g lst)  and (list x) is in lst, then
; (funcall h x) = (funcall g (list x))
; then YY will be (extract-ramsey-basis g XX alpha c) =
; (extract-pigeon (sing-fn g) XX (segment 0 c) alpha c)

Definition: sing-fn-aux (g, lst) = if lst ≃ nil then nil

elseif car (lst) = list (caar (lst))

then cons (list (caar (lst), funcall (g, car (lst))), sing-fn-aux (g, cdr (lst)))

else sing-fn-aux (g, cdr (lst)) endif

Theorem: sing-fn-aux-1 (list (x) ∈ lst) → (assoc (x, sing-fn-aux (g, lst)) = list (x, funcall (g, list (x))))

Theorem: sing-fn-aux-2 (list (x) ∉ lst) → (¬ listp (assoc (x, sing-fn-aux (g, lst))))

Event: Enable funcall.

Theorem: sing-fn-aux-3 (list (x) ∈ lst) → (funcall (sing-fn-aux (g, lst), x) = funcall (g, list (x)))

Theorem: sing-fn-aux-4 (list (x) ∉ lst) → (funcall (sing-fn-aux (g, lst), x) = 0)

Event: Disable funcall.

Definition: sing-fn (g) = sing-fn-aux (g, domain (g))

Theorem: sing-fn-on-sings funcall (sing-fn (g), x) = funcall (g, list (x))

Event: Disable sing-fn-aux.

Event: Disable sing-fn-aux-1.

Event: Disable sing-fn-aux-2.

Event: Disable sing-fn-aux-3.

Event: Disable sing-fn-aux-4.

Event: Disable sing-fn.

; all we need is its properties
; now, if (rangep g c) (so c > 0) , then
; g takes anything to (segment 0 (sub1 c)) = {0 ... c-1} = c
; this is a list of length c, so the pigeon hole principle
; should apply.
; as preliminaries

Theorem: size-of-initial-segment (0 < c) → (length (segment (0, c − 1)) = c)

Theorem: members-of-initial-segment (0 < c) → ((x ∈ segment (0, c − 1)) = ((x ∈ N) ∧ (x < c)))

Theorem: bound-values-of-sing-fn rangep (g, c) → (funcall (sing-fn (g), x) < c)

Theorem: number-values-of-sing-fn rangep (g, c) → (funcall (sing-fn (g), x) ∈ N)

Theorem: sing-fn-mapsto-aux1 rangep (g, c) → (funcall (sing-fn (g), x) ∈ segment (0, c − 1))

Theorem: sing-fn-mapsto rangep (g, c) → mapsto (sing-fn (g), xx, segment (0, c − 1))

Event: Disable sing-fn-mapsto-aux1.

;; now, we are set up for a proof of the basis of Ramsey's theorem
; the YY that works is given by

Definition: extract-ramsey-basis (g, xx, alpha, c) = extract-pigeon (sing-fn (g), xx, segment (0, c − 1), alpha, c)

; We're assuming
; (rangep g c) (so c > 0), XX is a set which is alpha * c -- large.
; "ramsey-basis-A" says that YY is a subset of XX
; "ramsey-basis-B" says that YY is a set
; "ramsey-basis-C" says that (homp YY g 1)
; "ramsey-basis-D" says that YY is alpha-large

Theorem: ramsey-basis-a subsetp (extract-ramsey-basis (g, xx, alpha, c), xx)

Theorem: ramsey-basis-b setp (xx) → setp (extract-ramsey-basis (g, xx, alpha, c))

; now to prove (homp YY g 1) --
; we need to prove that
; (constantp (sing-fn g) YY) implies (homp YY g 1)
; this is true because we've proved if (not ((homp YY g n)))
; we have an explicit counter-example
; first, let's recast this counter-example in the case n = 1

Theorem: ramsey-basis-c-aux1 sublistp (list (x), set) → (x ∈ set)

Definition: counter-hom-aux-x (set, g) = car (counter-hom-x (set, g, 1))

Definition: counter-hom-aux-y (set, g) = car (counter-hom-y (set, g, 1))

Theorem: ramsey-basis-c-aux2 (setp (lst) ∧ (length (lst) = 1)) → (list (car (lst)) = lst)

Theorem: ramsey-basis-c-aux3 (¬ homp (set, g, 1)) → (counter-hom-x (set, g, 1) = list (counter-hom-aux-x (set, g)))

Theorem: ramsey-basis-c-aux4 (¬ homp (set, g, 1)) → (counter-hom-y (set, g, 1) = list (counter-hom-aux-y (set, g)))

Theorem: ramsey-basis-c-aux5 (¬ homp (set, g, 1)) → ((counter-hom-aux-x (set, g) ∈ set)

∧ (counter-hom-aux-y (set, g) ∈ set)

∧ (funcall (sing-fn (g), counter-hom-aux-x (set, g)) ≠ funcall (sing-fn (g), counter-hom-aux-y (set, g))))

Theorem: ramsey-basis-c-aux6 constantp (sing-fn (g), set) → homp (set, g, 1)

Theorem: ramsey-basis-c rangep (g, c) → homp (extract-ramsey-basis (g, xx, alpha, c), g, 1)

Event: Disable counter-hom-aux-x.

Event: Disable counter-hom-aux-y.

Event: Disable ramsey-basis-c-aux1.

Event: Disable ramsey-basis-c-aux2.

Event: Disable ramsey-basis-c-aux3.

Event: Disable ramsey-basis-c-aux4.

Event: Disable ramsey-basis-c-aux5.

Event: Disable ramsey-basis-c-aux6.

Theorem: ramsey-basis-d (ordinalp (alpha) ∧ setp (xx) ∧ o-largep (xx, star (alpha, c)) ∧ rangep (g, c)) → o-largep (extract-ramsey-basis (g, xx, alpha, c), alpha)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;                     MISCELLANEOUS CONSTRUCTIONS                        ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;  vn
; first, to make our notation more compact:
; Look a number z as a von Neumann ordinal --
; the set of all smaller numbers.
; to make this a standard set, we list them in increasing order

Definition: vn (z) = if z ≃ 0 then nil

else add-on-end (z − 1, vn (z − 1)) endif

Theorem: size-of-vn (z ∈ N) → (length (vn (z)) = z)

Theorem: last-of-vn (z ≄ 0) → (last (vn (z)) = (z − 1))

Theorem: vn-is-a-set-aux1 ((1 < z) ∧ setp (vn (z − 1))) → setp (vn (z))

Theorem: vn-is-a-set-aux2 (z ≃ 0) → setp (vn (z))

Theorem: vn-is-a-set-aux3 setp (vn (1))

Theorem: vn-is-a-set setp (vn (z))

Event: Disable vn-is-a-set-aux1.

Event: Disable vn-is-a-set-aux2.

Event: Disable vn-is-a-set-aux3.

; to prove that the members of (vn z) are the numbers below z
; we have to say what the members of add-on-end are

Theorem: members-of-add-on-end (x ∈ add-on-end (item, lst)) = ((x ∈ lst) ∨ (x = item))

Theorem: members-of-vn-aux1 (z ≃ 0) → (x ∉ vn (z))

Theorem: members-of-vn-aux2 (z ≄ 0) → ((x ∈ vn (z)) = ((x ∈ vn (z − 1)) ∨ (x = (z − 1))))

Event: Disable vn.

; probably, we will never need its defn

Theorem: members-of-vn (x ∈ vn (z)) = ((x ∈ N) ∧ (x < z))

Event: Disable members-of-vn-aux1.

Event: Disable members-of-vn-aux2.

;;;;;;;;;;;;;;   all-maps
;;; let c>0
; (standard-fn g lst c) says that g is a function in standard
;  form from lst into c.   If lst = (x_1 ... x_n . foo), then
; g should be ( (x_1 v_1) ... (x_n v_n))
; we will build these in the induction step for Ramsey's theorem.
; now, we just want to prove that there are c^(length lst) of these
; we define (all-maps lst c), show that it contains all standard
; functions, and show that its size is c^(length lst)

Definition: standard-function (g, lst, c) = if lst ≃ nil then g = nil

else standard-function (cdr (g), cdr (lst), c) ∧ listp (car (g)) ∧ (car (g) = list (car (lst), cadar (g))) ∧ ((cadar (g) ∈ N) ∧ (cadar (g) < c)) endif

; in an r-loop
; *(standard-function '((a 3) (b 1)) '(a b) 4 )

;  T
; *(standard-function '((a 3) (b 1)) '(a b) 3 )
;  F
; *(standard-function '((a 3) (b 1)) '(a b c) 5 )
;  F

Theorem: tail-of-standard-function standard-function (g, cons (x, lst), c) → standard-function (cdr (g), lst, c)

; to build up (all-maps lst c):
; suppose g is a standard fn from (cons x lst) to c
; and (cdr g) is a member of a family FF
; then g is of the form (cons (list x i) h) for some i < c
; there are exactly c possibilites for (cons x i)
; we define (extend-family FF x c) to be all such g --
; then this will have length = c * |FF|

Definition: list-all (x, c) = if c ≃ 0 then nil

else cons (list (x, c − 1), list-all (x, c − 1)) endif

Theorem: list-all-gets-all ((i ∈ N) ∧ (i < c)) → (list (x, i) ∈ list-all (x, c))

; the list of all (list x i) ; with i < c

Theorem: size-of-list-all (c ∈ N) → (length (list-all (x, c)) = c)

Definition: all-maps (lst, c) = if lst ≃ nil then '(nil)

else product (list-all (car (lst), c), all-maps (cdr (lst), c)) endif

Theorem: all-maps-gets-all standard-function (g, lst, c) → (g ∈ all-maps (lst, c))

; now, to compute the size of (all-maps lst c)
; we first need to compute the size of the product of two lists

Event: Enable product.

Theorem: size-of-product length (product (lst1 , lst2 )) = (length (lst1 ) ∗ length (lst2 ))

Event: Disable product.

Theorem: size-of-all-maps (c ∈ N) → (length (all-maps (lst, c)) = expt (c, length (lst)))

;;;;;;;  constructing standard functions
; If OP is any defined function, we may construct a standard fn from
; lst to c by running down lst and applying OP
; Since we can't quantify over all defined functions without using
; something like $eval, we just do this for the one OP needed
; in the proof of Ramsey's theorem.
; Suppose (rangep g c) ; think of g as a partition of tuples
; we are trying to get a homogeneous set for.
; In an attempt to construct a pre-homogeneous set, we fix
; a z in omega and let lst be the power set of z  (so |lst| = 2^z)
; for a y > z, we consider g to define a map lst --> c
; which takes a set S to g(S union {z,y})
; we can call this new function (power-map g z y), and
; later try to get a large set of y's for which (power-map g z y) is the same.
; (power-map g z y)  will be (augmented-map g z y (power-set (vn z)))
; first, let's define (augmented-map g z y lst)

Definition: end-end (x, g, z, y) = funcall (g, add-on-end (y, add-on-end (z, x)))

; i.e., we're expecting x subset z < y, so we apply the partition
; g to x union {z,y}
; for now, we only care that this defines a function of x,
; with g,z,y as parameters, and that the values are < c
; if g has range c

Theorem: end-end-yields-numbers rangep (g, c) → (end-end (x, g, z, y) ∈ N)

Theorem: bound-on-end-end rangep (g, c) → (end-end (x, g, z, y) < c)

Event: Disable end-end.

Definition: augmented-map (g, z, y, lst) = if lst ≃ nil then nil

else cons (list (car (lst), end-end (car (lst), g, z, y)), augmented-map (g, z, y, cdr (lst))) endif

Theorem: augmented-map-is-standard rangep (g, c) → standard-function (augmented-map (g, z, y, lst), lst, c)

Theorem: values-of-augmented-map (x ∈ lst) → (funcall (augmented-map (g, z, y, lst), x) = end-end (x, g, z, y))

;;;;;;;  power-map
; now, let's develop the properties of (power-map g z y)

Definition: power-map (g, z, y) = augmented-map (g, z, y, power-set (vn (z)))

; intent :  z is in omega, and y > z
; then (power-map g z y) is a function which takes the
; sub-set S of z to  g(S U {z,y})
; first, let's consider the kind of object (power-map g z y) is,
; and show that there are  only c^(2^z) of these.

Definition: all-fns-on-power (z, c) = all-maps (power-set (vn (z)), c)

Theorem: size-of-all-fns-on-power ((c ∈ N) ∧ (z ∈ N)) → (length (all-fns-on-power (z, c)) = expt (c, expt (2, z)))

Theorem: power-map-in-all-fns rangep (g, c) → (power-map (g, z, y) ∈ all-fns-on-power (z, c))

; now, show that power-map takes sub-sets of z where they should go:

Theorem: value-of-power-map (setp (s) ∧ subsetp (s, vn (z))) → (funcall (power-map (g, z, y), s) = end-end (s, g, z, y))

; the main point of this is:  if we have a set YY such that
; (power-map g z y) is the same for all y in YY, then
; g(S U {z,y}) is independent of y in YY:

Theorem: same-power-maps (setp (s) ∧ subsetp (s, vn (z)) ∧ (power-map (g, z, y1 ) = power-map (g, z, y2 ))) → (funcall (g, add-on-end (y1 , add-on-end (z, s)))

= funcall (g, add-on-end (y2 , add-on-end (z, s))))

; now, in order to get such a YY, we consider (power-map g z y)
; as a function on YY, and then apply the pigeon-hole principle
; first, repeat the procedure to get a function on YY

Definition: power-power (g, z, yy) = if yy ≃ nil then nil

else cons (list (car (yy), power-map (g, z, car (yy))), power-power (g, z, cdr (yy))) endif

; this maps YY into (all-fns-on-power z c) -- i.e., the
; set of functions from power-set of z into c

Theorem: value-of-power-power (y ∈ yy) → (funcall (power-power (g, z, yy), y) = power-map (g, z, y))

Theorem: member-values-of-power-power (rangep (g, c) ∧ (y ∈ yy)) → (funcall (power-power (g, z, yy), y) ∈ all-fns-on-power (z, c))

Theorem: range-of-power-power-aux1 (rangep (g, c) ∧ subsetp (k, yy)) → mapsto (power-power (g, z, yy), k, all-fns-on-power (z, c))

; the following was a little tricky to prove, since
; we need to induct on the second YY -- with the first one fixed
; the "natural" induction will replace YY with (cdr YY) in both occurences

Theorem: range-of-power-power rangep (g, c) → mapsto (power-power (g, z, yy), yy, all-fns-on-power (z, c))

Event: Disable range-of-power-power-aux1.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;                           THE NICE SET LEMMA                           ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; assume z is a number and XX is a set
;      (we plan to have z < min XX)
; we want (nice g z XX)  to say that whenever x1,x2 are in X
; and S is a subset of z, g(S U {z,x1}) = g(S U {z,x2})
; since we will get this situation by applying the pigeon-hole
; principle, which uses constantp, we make that the official defn
; and then derive the main property

Definition: nice (g, z, xx) = constantp (power-power (g, z, xx), xx)

Theorem: nice-implies-constant (nice (g, z, xx) ∧ (x1 ∈ xx) ∧ (x2 ∈ xx)) → (funcall (power-power (g, z, xx), x1 ) = funcall (power-power (g, z, xx), x2 ))

Theorem: nice-implies-same-values (nice (g, z, xx) ∧ (x1 ∈ xx) ∧ (x2 ∈ xx) ∧ setp (s) ∧ subsetp (s, vn (z))) → (funcall (g, add-on-end (x1 , add-on-end (z, s)))

= funcall (g, add-on-end (x2 , add-on-end (z, s))))

;;;;;;;  lemma "nice-going-down"
; now, we plan to start with a big XX and apply the pigeon-hole
; principle to the map (power-power g z XX) to get a subset YY
; of XX such that (constantp (power-power g z XX) YY)
; we will need that this implies (constantp (power-power g z YY) YY) --
; i.e., (nice g z YY) :  lemma "nice-going-down"
; this is true because if y is in YY, a subset of XX
; then (funcall (power-power g z YY) y)  = (funcall (power-power g z XX) y)
; this is because both are equal to (power-map g z y)

Theorem: nice-goes-down-aux1 ((y ∈ yy) ∧ subsetp (yy, xx)) → (funcall (power-power (g, z, yy), y) = funcall (power-power (g, z, xx), y))

Theorem: nice-goes-down-aux2 (constantp (power-power (g, z, xx), yy) ∧ (y1 ∈ yy) ∧ (y2 ∈ yy) ∧ subsetp (yy, xx)) → (funcall (power-power (g, z, yy), y1 ) = funcall (power-power (g, z, yy), y2 ))

Event: Disable nice-goes-down-aux1.

Event: Disable nice-goes-down-aux2.

Theorem: nice-goes-down-aux3 (constantp (power-power (g, z, xx), yy) ∧ listp (vv) ∧ listp (cdr (vv)) ∧ subsetp (yy, xx) ∧ subsetp (vv, yy)) → (funcall (power-power (g, z, yy), car (vv))

= funcall (power-power (g, z, yy), cadr (vv)))

Theorem: nice-goes-down-aux4 (subsetp (vv, yy) ∧ listp (vv)) → subsetp (cdr (vv), yy)

Theorem: nice-goes-down-aux5 (constantp (power-power (g, z, xx), yy) ∧ subsetp (yy, xx) ∧ subsetp (vv, yy)) → constantp (power-power (g, z, yy), vv)

; we had the following problem in proving this:
; we want to prove  (constantp (power-power g z YY) YY) --
; but we have to induct on the second YY -- not the first --
; so we added a set VV:  assume VV subset YY subset XX
; and prove (constantp (power-power g z YY) VV) -- then set VV = YY  :

Theorem: nice-goes-down (constantp (power-power (g, z, xx), yy) ∧ subsetp (yy, xx)) → nice (g, z, yy)

Event: Disable nice-goes-down-aux3.

Event: Disable nice-goes-down-aux4.

Event: Disable nice-goes-down-aux5.

;;;;;;;;  now, back to the nice set lemma
; Suppose ZZ is a set which is phi(alpha,c) -- large ; alpha >= 1 ; c >= 1
; let z = min ZZ, and alpha-hat = {alpha}(z)
; then, by cdr-lemma-1 and cdr-lemma2
; 1. (cdr ZZ) is a set
; 2. (cdr ZZ) is phi(alpha-hat,c) * c^(2^z)  --  large
; now, suppose also that g maps into c.
; then, we can apply the pigeon-hole principle to the
; function (power-power g z (cdr ZZ)) to get a subset
; YY of (cdr ZZ) such that YY is phi(alpha-hat,c)  -- large
; and (power-power g z (cdr ZZ)) is constant on YY --
; so (nice g z YY)
; we obtain YY as (extract-nice g ZZ alpha c)
; we define extract-nice so that it will return NIL if the
; hypotheses to the nice set lemma aren't met

Definition: extract-nice (g, zz, alpha, c) = if ordinalp (alpha)

∧ (c ≄ 0)

∧ ord-leq (1, alpha) ∧ rangep (g, c) ∧ setp (zz) ∧ o-largep (zz, phi (alpha, c))

then extract-pigeon (power-power (g, car (zz), cdr (zz)), cdr (zz), all-fns-on-power (car (zz), c), phi (pred (alpha, car (zz)), c), expt (c, expt (2, car (zz))))

else nil endif

; if ZZ is a set and YY = (extract-nice g ZZ alpha c)
; "nice-set-A" says that YY is a set
; "nice-set-B" says that if ZZ is also phi(alpha,c) -- large
;           YY is a sub-set of (cdr ZZ)
; "nice-set-C" says that (nice g z YY)
; "nice-set-D" says that YY is phi(alpha-hat,c) -- large
;           whenever alpha is an ord >= 1, c > 0, and
;           ZZ is phi(alpha,c) -- large and (rangep g c)

; Here's a trivial property of phi:

Theorem: phi-non-zero phi (alpha, c) ≠ 0

Theorem: nice-set-a-aux1 (setp (zz) ∧ o-largep (zz, phi (alpha, c))) → listp (zz)

Theorem: nice-set-a-aux2 (setp (zz) ∧ o-largep (zz, phi (alpha, c))) → setp (cdr (zz))

Theorem: nice-set-a-aux3 setp (nil)

Theorem: nice-set-a setp (zz) → setp (extract-nice (g, zz, alpha, c))

Event: Disable nice-set-a-aux1.

Event: Disable nice-set-a-aux2.

Event: Disable nice-set-a-aux3.

Theorem: nice-set-b (setp (zz) ∧ o-largep (zz, phi (alpha, c))) → subsetp (extract-nice (g, zz, alpha, c), cdr (zz))

; for nice-set-C -- we need (contantp ...) which involves establishing
; "mapsto" hypothesis
; we have to show that the function, (power-power g (car ZZ) (cdr ZZ))
; which is mapping on (cdr ZZ), mapsto
; (all-fns-on-power (car ZZ) c)
;

Theorem: nice-set-c-aux1 rangep (g, c) → mapsto (power-power (g, car (zz), cdr (zz)),

cdr (zz),

all-fns-on-power (car (zz), c))

; we also need that the size of the range >= c^(2^z)
; which follows since c and z are numbers

Event: Enable nice-set-a-aux1.

; ZZ is non-empty, assuming (setp ZZ) and (o-largep ZZ (phi alpha c))

Theorem: nice-set-c-aux2 ((c ≄ 0) ∧ setp (zz) ∧ o-largep (zz, phi (alpha, c))) → (length (all-fns-on-power (car (zz), c)) = expt (c, expt (2, car (zz))))

; putting this together with pigeon-C, we get (constantp ...)

Theorem: nice-set-c-aux3 (ordinalp (alpha) ∧ (c ≄ 0) ∧ ord-leq (1, alpha) ∧ rangep (g, c) ∧ setp (zz) ∧ o-largep (zz, phi (alpha, c))) → constantp (power-power (g, car (zz), cdr (zz)), extract-nice (g, zz, alpha, c))

; actually, if the above hypotheses fail, then
; extract-nice returns nil, so we still have constantp

Theorem: nice-set-c-aux4 (¬ (ordinalp (alpha)

∧ (c ≄ 0)

∧ ord-leq (1, alpha) ∧ rangep (g, c) ∧ setp (zz) ∧ o-largep (zz, phi (alpha, c))))

→ constantp (power-power (g, car (zz), cdr (zz)), extract-nice (g, zz, alpha, c))

Theorem: nice-set-c-aux5 constantp (power-power (g, car (zz), cdr (zz)), extract-nice (g, zz, alpha, c))

; now, we apply nice-goes-down, since (extract-nice g ZZ alpha c)
; is a subset of (cdr ZZ) (by nice-set-B --
; assuming (and (setp ZZ) (o-largep ZZ (phi alpha c)))   )

Event: Disable nice-set-a-aux1.

Event: Disable nice-set-c-aux1.

Event: Disable nice-set-c-aux2.

Event: Disable nice-set-c-aux3.

Event: Disable nice-set-c-aux4.

Event: Disable nice-set-c-aux5.

Theorem: nice-set-c (setp (zz) ∧ o-largep (zz, phi (alpha, c))) → nice (g, car (zz), extract-nice (g, zz, alpha, c))

; finally, nice-set-D assumes the full hypotheses of extract-nice
; and concludes that (extract-nice g ZZ alpha c)
; is phi(alpha-hat,c) -- large, where alpha-hat is
; (pred alpha (car ZZ))
; this uses the fact that the set we're mapping from, (cdr ZZ)
; is (phi (pred alpha (car ZZ)) c) * (expt c (expt 2 (car ZZ))) -- large
; -- this is by the cdr-lemma
; then, we have to apply pigeon-D to get a large set

Theorem: nice-set-d (ordinalp (alpha) ∧ (c ≄ 0) ∧ ord-leq (1, alpha) ∧ rangep (g, c) ∧ setp (zz) ∧ o-largep (zz, phi (alpha, c))) → o-largep (extract-nice (g, zz, alpha, c), phi (pred (alpha, car (zz)), c))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;                 THE PRE-HOMOGENEOUS SET LEMMA                          ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; we iterate extract-nice to obtain a prehomogeneous set
;;;;;;;;;  Preliminaries
;;;;  nice-and-last :    a more useful version of nice
; we want this in terms of (last S)
; probably, we don't need the defn of nice any more

Event: Disable nice.

;;;  here's some simple fact about (last S)

Theorem: last-is-member (setp (s) ∧ listp (s)) → (last (s) ∈ s)

Theorem: subset-of-last-aux1 (listp (z) ∧ setp (cons (v, z))) → (v < last (z))

Theorem: subset-of-last-aux2 (setp (s) ∧ listp (s) ∧ (x ∈ all-but-last (s))) → (x < last (s))

Theorem: subset-of-last-aux3 (setp (s) ∧ listp (s) ∧ (x ∈ all-but-last (s))) → (x ∈ vn (last (s)))

Theorem: subset-of-last (setp (s) ∧ listp (s)) → subsetp (all-but-last (s), vn (last (s)))

Event: Disable subset-of-last-aux1.

Event: Disable subset-of-last-aux2.

Event: Disable subset-of-last-aux3.

Theorem: nice-and-last (nice (g, z, xx) ∧ setp (s) ∧ listp (s) ∧ (x1 ∈ xx) ∧ (x2 ∈ xx) ∧ (last (s) = z)) → (funcall (g, add-on-end (x1 , s)) = funcall (g, add-on-end (x2 , s)))

;;;;;;;  rephrase the nice set lemma
;; for iterating extract-nice, it will be simpler to have an
;; explicit name for the hypotheses under which it works
; then, this can be disabled when not needed

Definition: nice-set-hyp (g, zz, alpha, c) = (ordinalp (alpha)

∧ (c ≄ 0)

∧ ord-leq (1, alpha) ∧ rangep (g, c) ∧ setp (zz) ∧ o-largep (zz, phi (alpha, c)))

; if the hyp fails, extract-nice returns nil

Theorem: extract-nice-is-nil (¬ nice-set-hyp (g, zz, alpha, c)) → (extract-nice (g, zz, alpha, c) = nil)

; now, restate the four parts of the nice set lemma
; using this hyp
; probably, we don't need the defn of extract-nice any more

Event: Disable extract-nice.

Theorem: simple-nice-set-a nice-set-hyp (g, zz, alpha, c) → setp (extract-nice (g, zz, alpha, c))

Theorem: simple-nice-set-b nice-set-hyp (g, zz, alpha, c) → subsetp (extract-nice (g, zz, alpha, c), cdr (zz))

Theorem: simple-nice-set-c nice-set-hyp (g, zz, alpha, c) → nice (g, car (zz), extract-nice (g, zz, alpha, c))

Theorem: simple-nice-set-d nice-set-hyp (g, zz, alpha, c) → o-largep (extract-nice (g, zz, alpha, c), phi (pred (alpha, car (zz)), c))

;;;;;;  iterability
;; to prove that iterating extract-nice to a set produces
;; a subset, all we need is

Theorem: extract-nice-produces-subset (setp (zz) ∧ listp (zz)) → subsetp (extract-nice (g, zz, alpha, c), cdr (zz))

Theorem: extract-nice-produces-set (setp (zz) ∧ listp (zz)) → setp (extract-nice (g, zz, alpha, c))

; in the iteration, we also need that the hypotheses replicate
; themselves until alpha becomes 0

Theorem: replication-of-hyp-aux1 (nice-set-hyp (g, zz, alpha, c) ∧ ord-leq (1, pred (alpha, car (zz)))) → nice-set-hyp (g, extract-nice (g, zz, alpha, c), pred (alpha, car (zz)), c)

Theorem: replication-of-hyp-aux2 nice-set-hyp (g, zz, alpha, c) → ordinalp (pred (alpha, u))

Theorem: replication-of-hyp (nice-set-hyp (g, zz, alpha, c) ∧ (pred (alpha, car (zz)) ≠ 0)) → nice-set-hyp (g, extract-nice (g, zz, alpha, c), pred (alpha, car (zz)), c)

Event: Disable replication-of-hyp-aux1.

Event: Disable replication-of-hyp-aux2.

;;;;;;;;;  End Preliminaries

;; we get extract-prehom by iterating extract-nice
; to prove the recursion works -- we should prove
; that extract-nice returns a set of smaller length

Theorem: sublists-smaller-length (listp (zz) ∧ sublistp (uu, cdr (zz))) → (length (uu) < length (zz))

Theorem: subsets-smaller-length (listp (zz) ∧ setp (zz) ∧ setp (uu) ∧ subsetp (uu, cdr (zz))) → (length (uu) < length (zz))

Theorem: extract-prehom-aux1 (setp (zz) ∧ listp (zz)) → (length (extract-nice (g, zz, alpha, c)) < length (zz))

; the following keep getting in the way of the next defn

Event: Disable o-largep.

; let's keep this off permanently

Event: Disable large-goes-up.

Event: Disable setp.

Event: Disable simple-nice-set-a.

Definition: extract-prehom (g, zz, alpha, c) = if setp (zz) ∧ listp (zz) ∧ (alpha ≠ 0)

then cons (car (zz),

extract-prehom (g, extract-nice (g, zz, alpha, c), pred (alpha, car (zz)), c))

else nil endif

; use ordinary recursion, on length, not transfinite recursion on epsilon_0

Event: Enable large-goes-up.

Event: Enable setp.

Event: Enable simple-nice-set-a.

; this will return an alpha-large set
; so, if alpha = 0, any set will do
; so,   the intended hypotheses to extract-prehom are
; like that of extract-nice, except that alpha could be 0

Definition: prehom-set-hyp (g, zz, alpha, c) = (ordinalp (alpha)

∧ (c ≄ 0) ∧ rangep (g, c) ∧ setp (zz) ∧ o-largep (zz, phi (alpha, c)))

Theorem: compare-hyps (prehom-set-hyp (g, zz, alpha, c) ∧ (alpha ≠ 0)) → nice-set-hyp (g, zz, alpha, c)

;;; now if ZZ is a set and XX = (extract-prehom g ZZ alpha c)
; the PREHOMOGENEOUS SET LEMMA has 6 parts.  the first
; 3 don't use any properties of extract-nice -- only the
; lemma above that it returns a subset of (cdr ZZ)
; "prehom-set-A" says that if (listp ZZ) and alpha != 0 then
;           (car XX) = (car ZZ)
; "prehom-set-B" says that
;           XX is a sub-set of ZZ
; "prehom-set-C" says that if (listp ZZ) and alpha != 0  then
;            (listp XX)
; "prehom-set-D" says that XX is a set
; "prehom-set-E" says that if (prehom-set-hyp g ZZ alpha c)
;          then (o-largep XX alpha)
; "prehom-set-F" says that if (prehom-set-hyp g ZZ alpha c)
;          then (pre-homp XX g)

Theorem: prehom-set-a (setp (zz) ∧ listp (zz) ∧ (alpha ≠ 0)) → (car (extract-prehom (g, zz, alpha, c)) = car (zz))

Theorem: prehom-set-b-aux1 (listp (zz) ∧ subsetp (uu, ww) ∧ subsetp (ww, cdr (zz))) → subsetp (cons (car (zz), uu), zz)

Theorem: prehom-set-b-aux2 (setp (zz) ∧ listp (zz) ∧ subsetp (uu, extract-nice (g, zz, alpha, c))) → subsetp (cons (car (zz), uu), zz)

Theorem: prehom-set-b setp (zz) → subsetp (extract-prehom (g, zz, alpha, c), zz)

Event: Disable prehom-set-b-aux1.

Event: Disable prehom-set-b-aux2.

Theorem: prehom-set-c (setp (zz) ∧ listp (zz) ∧ (alpha ≠ 0)) → listp (extract-prehom (g, zz, alpha, c))

; for D, we will have to force the correct induction
; first, consider some trivial cases
; first, when (extract-prehom g ZZ alpha c) is empty

Theorem: prehom-set-d-aux1 (¬ setp (zz)) → setp (extract-prehom (g, zz, alpha, c))

Theorem: prehom-set-d-aux2 (¬ listp (zz)) → setp (extract-prehom (g, zz, alpha, c))

Theorem: prehom-set-d-aux3 (alpha = 0) → setp (extract-prehom (g, zz, alpha, c))

; next, when (extract-prehom g ZZ alpha c) is a singleton

Theorem: prehom-set-d-aux4 (setp (zz) ∧ listp (zz) ∧ (alpha ≠ 0) ∧ (extract-nice (g, zz, alpha, c) ≃ nil)) → setp (extract-prehom (g, zz, alpha, c))

; we can summarize the only case left to consider as:

Theorem: prehom-set-d-aux5 (¬ setp (extract-prehom (g, zz, alpha, c))) → (setp (zz)

∧ listp (zz) ∧ (alpha ≠ 0) ∧ listp (extract-nice (g, zz, alpha, c)))

Event: Disable prehom-set-d-aux1.

Event: Disable prehom-set-d-aux2.

Event: Disable prehom-set-d-aux3.

Event: Disable prehom-set-d-aux4.

; in the inductive case, we use lemma "set-builder", but we
; have to check that it applies.  It does, because
; "extract-nice" returns a subset of the cdr
; let UU = (extract-nice g ZZ alpha c)
; and let VV = (extract-prehom g  UU (pred alpha (car ZZ)) c)
; then (extract-prehom g ZZ alpha c)  =

; (cons (car ZZ) VV)
; first, state abstractly what we're using about sets:

Theorem: prehom-set-d-aux6 (setp (zz) ∧ listp (zz) ∧ listp (uu) ∧ subsetp (uu, cdr (zz))) → (car (zz) < car (uu))

Theorem: prehom-set-d-aux7 (setp (zz) ∧ listp (zz) ∧ setp (uu) ∧ listp (uu) ∧ setp (vv) ∧ listp (vv) ∧ (car (vv) = car (uu)) ∧ subsetp (uu, cdr (zz))) → setp (cons (car (zz), vv))

Event: Disable prehom-set-d-aux6.

; now, plug in what VV is:  of form
;    (extract-prehom g  UU delta c)
;  we still assume VV is a set (that's the induction), but
; we can drop the other hypotheses, since they follow
; from parts A,B,C of the lemma

Theorem: prehom-set-d-aux8 (setp (ee) ∧ setp (cons (z, x)) ∧ (¬ listp (ee))) → setp (cons (z, ee))

Theorem: prehom-set-d-aux9 listp (extract-prehom (g, uu, delta, c)) → (car (extract-prehom (g, uu, delta, c)) = car (uu))

Theorem: prehom-set-d-aux10 (setp (zz) ∧ listp (zz) ∧ setp (uu) ∧ listp (uu) ∧ subsetp (uu, cdr (zz)) ∧ setp (extract-prehom (g, uu, delta, c))) → setp (cons (car (zz), extract-prehom (g, uu, delta, c)))

Event: Disable prehom-set-d-aux7.

; now, plug in what UU is :  (extract-nice g ZZ alpha c)
; this is a set -- it may be empty, but we've already
; considered that case, so keep the hypothesis that it's non-empty
; it is always a subset of (cdr ZZ)

Theorem: prehom-set-d-aux11 (setp (zz) ∧ listp (zz) ∧ listp (extract-nice (g, zz, alpha, c)) ∧ setp (extract-prehom (g, extract-nice (g, zz, alpha, c), delta, c))) → setp (cons (car (zz),

extract-prehom (g, extract-nice (g, zz, alpha, c), delta, c)))

Event: Disable prehom-set-d-aux10.

; now, with delta =  (pred alpha (car ZZ)) , we have the induction step

Theorem: prehom-set-d-aux12 (setp (zz) ∧ listp (zz) ∧ listp (extract-nice (g, zz, alpha, c)) ∧ setp (extract-prehom (g,

extract-nice (g, zz, alpha, c), pred (alpha, car (zz)), c)))

→ setp (extract-prehom (g, zz, alpha, c))

; now, the induction should work

Theorem: prehom-set-d setp (extract-prehom (g, zz, alpha, c))

Event: Disable prehom-set-d-aux5.

Event: Disable prehom-set-d-aux8.

Event: Disable prehom-set-d-aux9.

Event: Disable prehom-set-d-aux11.

Event: Disable prehom-set-d-aux12.

; to do the inductions in E and F, we should check that
; the hypotheses replicates to the inductive call
; the following seem useful in general:

Theorem: prehom-hyp-implies-non-empty prehom-set-hyp (g, zz, alpha, c) → listp (zz)

Theorem: positive-ordinals (ordinalp (alpha) ∧ (alpha ≠ 0)) → ord-leq (1, alpha)

Theorem: replication-of-prehom-hyp-aux1 o-largep (zz, phi (alpha, c)) → listp (zz)

Theorem: replication-of-prehom-hyp (prehom-set-hyp (g, zz, alpha, c) ∧ (alpha ≠ 0)) → prehom-set-hyp (g, extract-nice (g, zz, alpha, c), pred (alpha, car (zz)), c)

Event: Disable replication-of-prehom-hyp-aux1.

; now, on to E.
; for the basis:

Theorem: prehom-set-e-aux1 o-largep (extract-prehom (g, zz, alpha, c), 0)

; for the induction, we need

Theorem: prehom-set-e-aux2 ((alpha ≠ 0) ∧ o-largep (extract-prehom (g,

extract-nice (g, zz, alpha, c), pred (alpha, car (zz)), c),

pred (alpha, car (zz))))

→ o-largep (cons (car (zz),

extract-prehom (g, extract-nice (g, zz, alpha, c), pred (alpha, car (zz)), c)),

alpha)

Theorem: prehom-set-e-aux3 (listp (zz) ∧ setp (zz) ∧ (alpha ≠ 0) ∧ o-largep (extract-prehom (g,

extract-nice (g, zz, alpha, c), pred (alpha, car (zz)), c),

pred (alpha, car (zz))))

→ o-largep (extract-prehom (g, zz, alpha, c), alpha)

; to force the correct induction

Theorem: prehom-set-e-aux4 (prehom-set-hyp (g, zz, alpha, c) ∧ (¬ o-largep (extract-prehom (g, zz, alpha, c), alpha))) → (¬ o-largep (extract-prehom (g,

extract-nice (g, zz, alpha, c), pred (alpha, car (zz)), c),

pred (alpha, car (zz))))

Theorem: prehom-set-e-aux5 (prehom-set-hyp (g, zz, alpha, c) ∧ (¬ o-largep (extract-prehom (g, zz, alpha, c), alpha))) → prehom-set-hyp (g, extract-nice (g, zz, alpha, c), pred (alpha, car (zz)), c)

Theorem: prehom-set-e prehom-set-hyp (g, zz, alpha, c) → o-largep (extract-prehom (g, zz, alpha, c), alpha)

Event: Disable prehom-set-e-aux1.

Event: Disable prehom-set-e-aux2.

Event: Disable prehom-set-e-aux3.

Event: Disable prehom-set-e-aux4.

Event: Disable prehom-set-e-aux5.

; finally, F -- that the resulting set
;  XX = (extract-prehom g ZZ alpha c) is pre-homogeneous
; so, we have to look at all non-empty subsets of XX  --
; but in fact, the defn of pre-homogeneous works will ALL sets
; S whose last element is in XX -- regardless of whether S is
; a subset of XX.
; That's not relevant to Ramsey's Theoreom, but this stronger
; statement is a lot easier to prove by induction.
; let's summarize what we're saying can't happen:

Definition: bad-for-prehom-set (g, zz, alpha, c, xx, s, x1 , x2 ) = (prehom-set-hyp (g, zz, alpha, c)

∧ (xx = extract-prehom (g, zz, alpha, c))

∧ setp (s) ∧ listp (s) ∧ (last (s) ∈ xx) ∧ (x1 ∈ xx) ∧ (x2 ∈ xx) ∧ (last (s) < x1 ) ∧ (last (s) < x2 ) ∧ (funcall (g, add-on-end (x1 , s)) ≠ funcall (g, add-on-end (x2 , s))))

; we show this can't happen by induction on ZZ (with a fixed SS)
; first, note that XX and ZZ are non-empty sets and 1 <= alpha
; and (car XX) = (car ZZ)

Theorem: prehom-set-f-aux1 bad-for-prehom-set (g, zz, alpha, c, xx, s, x1 , x2 ) → listp (xx)

Theorem: prehom-set-f-aux2 bad-for-prehom-set (g, zz, alpha, c, xx, s, x1 , x2 ) → setp (xx)

Theorem: prehom-set-f-aux3 bad-for-prehom-set (g, zz, alpha, c, xx, s, x1 , x2 ) → listp (zz)

Theorem: prehom-set-f-aux4 bad-for-prehom-set (g, zz, alpha, c, xx, s, x1 , x2 ) → setp (zz)

Theorem: prehom-set-f-aux5 bad-for-prehom-set (g, zz, alpha, c, xx, s, x1 , x2 ) → ordinalp (alpha)

Theorem: prehom-set-f-aux6 bad-for-prehom-set (g, zz, alpha, c, xx, s, x1 , x2 ) → ord-leq (1, alpha)

Theorem: prehom-set-f-aux7 bad-for-prehom-set (g, zz, alpha, c, xx, s, x1 , x2 ) → (xx = cons (car (zz),

extract-prehom (g, extract-nice (g, zz, alpha, c), pred (alpha, car (zz)), c)))

Theorem: prehom-set-f-aux8 bad-for-prehom-set (g, zz, alpha, c, xx, s, x1 , x2 ) → (car (xx) = car (zz))

Theorem: prehom-set-f-aux9 bad-for-prehom-set (g, zz, alpha, c, xx, s, x1 , x2 ) → (cdr (xx)

= extract-prehom (g, extract-nice (g, zz, alpha, c), pred (alpha, car (zz)), c))

; now, we plan to use the nice set lemma to contradict (last S) = (car XX),
; so then (last S) > (car XX), whence we can use induction on ZZ
; in either case, we need that x1,x2 are in
; (extract-prehom g (extract-nice g ZZ alpha c) (pred alpha (car ZZ))  c)

Theorem: prehom-set-f-aux10 (setp (xx) ∧ (u ∈ xx) ∧ (x ∈ xx) ∧ (u < x)) → (x ∈ cdr (xx))

Theorem: prehom-set-f-aux11 bad-for-prehom-set (g, zz, alpha, c, xx, s, x1 , x2 ) → (x1 ∈ cdr (xx))

Theorem: prehom-set-f-aux12 bad-for-prehom-set (g, zz, alpha, c, xx, s, x1 , x2 ) → (x2 ∈ cdr (xx))

Theorem: prehom-set-f-aux13 bad-for-prehom-set (g, zz, alpha, c, xx, s, x1 , x2 ) → (x1 ∈ extract-prehom (g,

extract-nice (g, zz, alpha, c), pred (alpha, car (zz)), c))

Theorem: prehom-set-f-aux14 bad-for-prehom-set (g, zz, alpha, c, xx, s, x1 , x2 ) → (x2 ∈ extract-prehom (g,

extract-nice (g, zz, alpha, c), pred (alpha, car (zz)), c))

; now, we work on refuting the case that (last S) = (car XX) ,
; using the nice set lemma
; for this, first note that x1,x2 are in (extract-nice g ZZ alpha c)

Theorem: prehom-set-f-aux15 bad-for-prehom-set (g, zz, alpha, c, xx, s, x1 , x2 ) → (x1 ∈ extract-nice (g, zz, alpha, c))

Theorem: prehom-set-f-aux16 bad-for-prehom-set (g, zz, alpha, c, xx, s, x1 , x2 ) → (x2 ∈ extract-nice (g, zz, alpha, c))

Theorem: prehom-set-f-aux17 (bad-for-prehom-set (g, zz, alpha, c, xx, s, x1 , x2 ) ∧ (last (s) = car (zz))) → (¬ nice (g, car (zz), extract-nice (g, zz, alpha, c)))

; but it should be nice, by nice-set-C

Theorem: prehom-set-f-aux18 bad-for-prehom-set (g, zz, alpha, c, xx, s, x1 , x2 ) → (last (s) ≠ car (zz))

; now, (car ZZ) = (car XX), so (last S) is a member of (cdr XX)

Theorem: prehom-set-f-aux19 bad-for-prehom-set (g, zz, alpha, c, xx, s, x1 , x2 ) → (last (s) ∈ cdr (xx))

; now, applying aux9, we get for (last S) what we already have for x1,x2

Theorem: prehom-set-f-aux20 bad-for-prehom-set (g, zz, alpha, c, xx, s, x1 , x2 ) → (last (s)

∈ extract-prehom (g, extract-nice (g, zz, alpha, c), pred (alpha, car (zz)), c))

; now, we almost have the induction, but we have to take
; car of the prehom-set-hyp part

Theorem: prehom-set-f-aux21 bad-for-prehom-set (g, zz, alpha, c, xx, s, x1 , x2 ) → prehom-set-hyp (g, extract-nice (g, zz, alpha, c), pred (alpha, car (zz)), c)

Theorem: prehom-set-f-aux22 bad-for-prehom-set (g, zz, alpha, c, xx, s, x1 , x2 ) → bad-for-prehom-set (g,

extract-nice (g, zz, alpha, c), pred (alpha, car (zz)), c, extract-prehom (g,

extract-nice (g, zz, alpha, c), pred (alpha, car (zz)), c),

s, x1 , x2 )

; now, force the correct induction

Event: Enable extract-prehom-aux1.

Event: Disable setp.

Event: Disable length-of-subset.

Event: Disable subsetp.

Definition: prehom-set-f-kludge (g, zz, alpha, c, xx, s, x1 , x2 ) = if setp (zz) ∧ listp (zz)

then prehom-set-f-kludge (g, extract-nice (g, zz, alpha, c), pred (alpha, car (zz)), c, extract-prehom (g,

extract-nice (g, zz, alpha, c), pred (alpha, car (zz)), c), s, x1 , x2 )

else nil endif

Event: Disable extract-prehom-aux1.

Event: Enable setp.

Event: Enable length-of-subset.

Event: Enable subsetp.

Theorem: prehom-set-f-aux23 ¬ bad-for-prehom-set (g, zz, alpha, c, xx, s, x1 , x2 )

; MAIN SUBGOAL:

Theorem: prehom-set-f-aux24 (prehom-set-hyp (g, zz, alpha, c) ∧ (xx = extract-prehom (g, zz, alpha, c)) ∧ setp (s) ∧ listp (s) ∧ (last (s) ∈ xx) ∧ (x1 ∈ xx) ∧ (x2 ∈ xx) ∧ (last (s) < x1 ) ∧ (last (s) < x2 )) → (funcall (g, add-on-end (x1 , s)) = funcall (g, add-on-end (x2 , s)))

Event: Disable bad-for-prehom-set.

Event: Disable prehom-set-f-kludge.

Event: Disable prehom-set-f-aux1.

Event: Disable prehom-set-f-aux2.

Event: Disable prehom-set-f-aux3.

Event: Disable prehom-set-f-aux4.

Event: Disable prehom-set-f-aux5. Event: Disable prehom-set-f-aux6. Event: Disable prehom-set-f-aux7. Event: Disable prehom-set-f-aux8. Event: Disable prehom-set-f-aux9. Event: Disable prehom-set-f-aux10. Event: Disable prehom-set-f-aux11. Event: Disable prehom-set-f-aux12. Event: Disable prehom-set-f-aux13. Event: Disable prehom-set-f-aux14. Event: Disable prehom-set-f-aux15. Event: Disable prehom-set-f-aux16. Event: Disable prehom-set-f-aux17. Event: Disable prehom-set-f-aux18. Event: Disable prehom-set-f-aux19. Event: Disable prehom-set-f-aux20. Event: Disable prehom-set-f-aux21. Event: Disable prehom-set-f-aux22.

Event: Disable prehom-set-f-aux23.

Theorem: prehom-set-f-aux25 (listp (s) ∧ subsetp (s, xx)) → (last (s) ∈ xx)

Theorem: prehom-set-f-aux26 (prehom-set-hyp (g, zz, alpha, c) ∧ (xx = extract-prehom (g, zz, alpha, c)) ∧ setp (s) ∧ listp (s) ∧ subsetp (s, xx) ∧ (x1 ∈ xx) ∧ (x2 ∈ xx) ∧ (last (s) < x1 ) ∧ (last (s) < x2 )) → (funcall (g, add-on-end (x1 , s)) = funcall (g, add-on-end (x2 , s)))

Event: Disable prehom-set-f-aux24.

Event: Disable prehom-set-f-aux25.

Event: Disable prehom-set-f-aux26.

Theorem: prehom-set-f prehom-set-hyp (g, zz, alpha, c) → pre-homp (extract-prehom (g, zz, alpha, c), g)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;                    RAMSEY THEOREM -- ORDINAL VERSION                   ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; This is really the main Ramsey theorem
; It says: a partition on n-tuples of a Gamma(alpha,n,c) -- large
; set has a homogeneous alpha-large set.
; first, define Gamma:

Definition: gamma (alpha, n, c) = if n ≤ 1 then star (alpha, c)

else phi (gamma (alpha, n − 1, c), c) endif

Theorem: gamma-is-an-ord ordinalp (alpha) → ordinalp (gamma (alpha, n, c))

; now, extract-ramsey produces the homogeneous set
; assuming ZZ is Gamma(alpha,n,c) -- large

Definition: extract-ramsey (g, zz, alpha, n, c) = if n ≤ 1 then extract-ramsey-basis (g, zz, alpha, c)

else extract-ramsey (derived (g,

extract-prehom (g, zz, gamma (alpha, n − 1, c), c)), extract-prehom (g, zz, gamma (alpha, n − 1, c), c), alpha, n − 1,

c) endif

;;; now, if ZZ is a set and YY = (extract-prehom g ZZ alpha c)
; "ord-ramsey-A" says that YY is a set and a subset of ZZ
; "ord-ramsey-B" says that YY is alpha-large
;    assuming (ordinalp alpha) and (rangep g c) and (not (zerop n))
;       and (o-largep ZZ (Gamma alpha n c))
; "ord-ramsey-C" says that (homp YY g n)
;    assuming (ordinalp alpha) and (rangep g c) and (not (zerop n))
;       and (o-largep ZZ (Gamma alpha n c))
; Then, we put these together in one "official-looking" theorem,
; "ord-ramsey"
; note -- (not (zerop c)) follows from "rangep-is-positive"
; the details of the following are probably all irrelevant now

Event: Disable extract-prehom.

Event: Disable extract-nice.

Event: Disable extract-ramsey-basis.

Theorem: ord-ramsey-a setp (zz) → (setp (extract-ramsey (g, zz, alpha, n, c))

∧ subsetp (extract-ramsey (g, zz, alpha, n, c), zz))

; for B, and C, we need that if (rangep g c), then
;  (rangep (derived g WW) c), so that (rangep g c) can be
; applied inductively to the derived partition

Theorem: range-of-derived-aux1 (rangep (g, c) ∧ (pr ∈ derived-aux (g, ww, lst))) → (cadr (pr) < c)

Theorem: range-of-derived-aux2 (rangep (g, c) ∧ (pr ∈ derived-aux (g, ww, lst))) → (cadr (pr) ∈ N)

Definition: counter-range (g, c) = if g ≃ nil then nil

elseif ¬ ((cadar (g) ∈ N) ∧ (cadar (g) < c)) then car (g)

else counter-range (cdr (g), c) endif

; let's list the ways rangep can fail if c is positive:

Event: Enable rangep.

Theorem: range-of-derived-aux3 ((0 < c) ∧ (¬ rangep (g, c))) → listp (g)

Theorem: range-of-derived-aux4 ((0 < c) ∧ (¬ rangep (g, c))) → ((¬ rangep (cdr (g), c)) ∨ (cadar (g) ∉ N) ∨ (cadar (g) ≮ c))

; in the positive direction

Theorem: range-of-derived-aux5 ((cadar (g) ∈ N) ∧ (cadar (g) < c) ∧ rangep (cdr (g), c)) → rangep (g, c)

Event: Disable rangep.

Theorem: range-of-derived-aux6 ((c ≠ 0) ∧ (c ∈ N) ∧ (¬ rangep (g, c))) → listp (g)

Theorem: range-of-derived-aux7 ((0 < c) ∧ (¬ rangep (g, c))) → (counter-range (g, c) ∈ g)

Theorem: range-of-derived-aux8 ((0 < c) ∧ (¬ rangep (g, c))) → (¬ ((cadr (counter-range (g, c)) ∈ N)

∧ (cadr (counter-range (g, c)) < c)))

Theorem: range-of-derived-aux9 rangep (g, c) → rangep (derived-aux (g, ww, lst), c) Theorem: range-of-derived rangep (g, c) → rangep (derived (g, ww), c) Event: Disable counter-range. Event: Disable range-of-derived-aux1. Event: Disable range-of-derived-aux2. Event: Disable range-of-derived-aux3. Event: Disable range-of-derived-aux4. Event: Disable range-of-derived-aux5. Event: Disable range-of-derived-aux6. Event: Disable range-of-derived-aux7. Event: Disable range-of-derived-aux8. Event: Disable range-of-derived-aux9.

; for B and C, which require a non-trivial induction,
; it is convenient to summarize the hypotheses.

Definition: ord-ramsey-hyp (g, zz, alpha, n, c) = (ordinalp (alpha)

∧ rangep (g, c) ∧ (n ≄ 0) ∧ setp (zz) ∧ o-largep (zz, gamma (alpha, n, c)))

; since some of the earlier hyps had c > 0,

Theorem: ord-ramsey-hyp-positive ord-ramsey-hyp (g, zz, alpha, n, c) → (c ≄ 0)

;;;;;;;  replication results
; these should be useful in inductions

Theorem: recursive-case-for-gamma (1 < n) → (gamma (alpha, n, c) = phi (gamma (alpha, n − 1, c), c))

; first, note that ZZ satisfies the prehom set hyp

Theorem: ord-ramsey-to-prehom-set-hyp ((1 < n) ∧ ord-ramsey-hyp (g, zz, alpha, n, c)) → prehom-set-hyp (g, zz, gamma (alpha, n − 1, c), c)

; now, consider XX = (extract-prehom g ZZ (Gamma alpha (sub1 n) c) c)
; XX will be (Gamma alpha (sub1 n) c) -- large and a set, so:

Theorem: replication-of-ord-ramsey-hyp ((1 < n) ∧ ord-ramsey-hyp (g, zz, alpha, n, c) ∧ (xx = extract-prehom (g, zz, gamma (alpha, n − 1, c), c))) → ord-ramsey-hyp (derived (g, xx), xx, alpha, n − 1, c)

; also, formalize the recursive case for extract-ramsey:

Theorem: recursive-case-for-extract-ramsey ((1 < n) ∧ (xx = extract-prehom (g, zz, gamma (alpha, n − 1, c), c))) → (extract-ramsey (g, zz, alpha, n, c)

= extract-ramsey (derived (g, xx), xx, alpha, n − 1, c))

; the basis for ramsey-B is:

Theorem: ord-ramsey-b-aux1 ord-ramsey-hyp (g, zz, alpha, 1, c) → o-largep (extract-ramsey (g, zz, alpha, 1, c), alpha)

; this is immediate by ramsey-basis-D
; now, the induction should work because a counter-example with
; n will generate a counter-example with n-1

Theorem: ord-ramsey-b-aux2 ((1 ≤ n) ∧ ord-ramsey-hyp (g, zz, alpha, n, c)) → o-largep (extract-ramsey (g, zz, alpha, n, c), alpha)

; but of course, the (leq 1 n) is irrelevant

Theorem: ord-ramsey-b ord-ramsey-hyp (g, zz, alpha, n, c) → o-largep (extract-ramsey (g, zz, alpha, n, c), alpha)

Event: Disable ord-ramsey-b-aux1.

Event: Disable ord-ramsey-b-aux2.

; the basis for ramsey-C is:

Theorem: ord-ramsey-c-aux1 ord-ramsey-hyp (g, zz, alpha, 1, c) → homp (extract-ramsey (g, zz, alpha, 1, c), g, 1)

; this is immediate by ramsey-basis-C
; now, the induction should work because a counter-example with
; n will generate a counter-example with n-1
; the induction will be:  if
; XX =  (extract-prehom g ZZ (Gamma alpha (sub1 n) c) c)
; YY = (extract-ramsey g ZZ alpha n c) =
;      (extract-ramsey (derived g XX) XX alpha (sub1 n) c)
;         (by recursive-case-for-extract-ramsey)
; and inductively,
;  (homp  YY  (derived g XX) (sub1 n))
; then by the derived partition lemma
; (homp YY g n)
; let's phrase the derived-partition-lemma in the current notation

Theorem: ord-ramsey-c-aux2 ((1 < n) ∧ pre-homp (xx, g) ∧ sublistp (yy, xx) ∧ homp (yy, derived (g, xx), n − 1)) → homp (yy, g, n)

; now, let's check that the XX and YY as above really
; satisfy the (pre-homp XX g)  and (sublistp YY XX)

Theorem: ord-ramsey-c-aux3 ((1 < n) ∧ ord-ramsey-hyp (g, zz, alpha, n, c) ∧ (xx = extract-prehom (g, zz, gamma (alpha, n − 1, c), c))) → pre-homp (xx, g)

Theorem: ord-ramsey-c-aux4 ((1 < n) ∧ ord-ramsey-hyp (g, zz, alpha, n, c) ∧ (xx = extract-prehom (g, zz, gamma (alpha, n − 1, c), c)) ∧ (yy = extract-ramsey (g, zz, alpha, n, c))) → sublistp (yy, xx)

; it follows that aux2 gives

Theorem: ord-ramsey-c-aux5 ((1 < n) ∧ ord-ramsey-hyp (g, zz, alpha, n, c) ∧ (xx = extract-prehom (g, zz, gamma (alpha, n − 1, c), c)) ∧ (yy = extract-ramsey (g, zz, alpha, n, c)) ∧ homp (yy, derived (g, xx), n − 1)) → homp (yy, g, n)

Theorem: ord-ramsey-c-aux6 ((1 ≤ n) ∧ ord-ramsey-hyp (g, zz, alpha, n, c)) → homp (extract-ramsey (g, zz, alpha, n, c), g, n)

; but of course, the (leq 1 n) is irrelevant

Theorem: ord-ramsey-c ord-ramsey-hyp (g, zz, alpha, n, c) → homp (extract-ramsey (g, zz, alpha, n, c), g, n)

Event: Disable ord-ramsey-c-aux1.

Event: Disable ord-ramsey-c-aux2.

Event: Disable ord-ramsey-c-aux3.

Event: Disable ord-ramsey-c-aux4.

Event: Disable ord-ramsey-c-aux5.

Event: Disable ord-ramsey-c-aux6.

; Finally, a version suitable for framing:

Theorem: ord-ramsey (ordinalp (alpha) ∧ rangep (g, c) ∧ (n ≄ 0) ∧ setp (zz) ∧ o-largep (zz, gamma (alpha, n, c)) ∧ (yy = extract-ramsey (g, zz, alpha, n, c))) → (setp (yy) ∧ subsetp (yy, zz) ∧ o-largep (yy, alpha) ∧ homp (yy, g, n))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;                  RAMSEY THEOREM -- PARIS-HARRINGTON VERSION            ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; FINALLY, we use epsilon_0 recursion/induction.  We define
; a function (lambda alpha k) such that ; (lambda alpha k) >= k,
; and the interval [k, (lamda alpha k)] is alpha - large
; This will show that applying the ordinal version of Ramsey's
; theorem to a suitable large interval will produce an
; omega-large (hence large) homogeneous set.

Definition: lambda kludge (alpha, k) = if ordinalp (alpha) then alpha

else 0 endif

; just to get the prover to accept the following definition

Definition: lambda (alpha, k) = if ord-lessp (0, alpha) ∧ ordinalp (alpha)

then lambda (pred (alpha, k), 1 + k)

else k endif

Event: Disable lambda kludge.

Theorem: lambda-is-a-number (k ∈ N) → (lambda (alpha, k) ∈ N)

Theorem: lambda-is-big (k ∈ N) → (lambda (alpha, k) ≮ k)

Theorem: base-case-for-lambda (¬ ord-lessp (0, alpha)) → (lambda (alpha, k) = k)

Theorem: recursive-case-for-lambda (ordinalp (alpha) ∧ ord-lessp (0, alpha)) → (lambda (alpha, k) = lambda (pred (alpha, k), 1 + k))

Event: Disable lambda.

; let's prove that (o-largep (segment k (lambda alpha k)) alpha)
; this is by induction
; base case:

Theorem: lambda-gives-large-segments-aux1 ((k ∈ N) ∧ ordinalp (alpha) ∧ (¬ ord-lessp (0, alpha))) → o-largep (segment (k, lambda (alpha, k)), alpha)

; for the recursive case:

Theorem: lambda-gives-large-segments-aux2 ((k ∈ N) ∧ ordinalp (alpha) ∧ ord-lessp (0, alpha)) → (segment (k, lambda (alpha, k))

= cons (k, segment (1 + k, lambda (pred (alpha, k), 1 + k))))

Theorem: lambda-gives-large-segments-aux3 ((k ∈ N) ∧ ordinalp (alpha) ∧ ord-lessp (0, alpha) ∧ o-largep (segment (1 + k, lambda (pred (alpha, k), 1 + k)), pred (alpha, k))) → o-largep (segment (k, lambda (alpha, k)), alpha)

Theorem: lambda-gives-large-segments ((k ∈ N) ∧ ordinalp (alpha)) → o-largep (segment (k, lambda (alpha, k)), alpha)

Event: Disable lambda-gives-large-segments-aux1.

Event: Disable lambda-gives-large-segments-aux2.

Event: Disable lambda-gives-large-segments-aux3.

; so, the Ramsey number is:

Definition: r (k, n, c) = lambda (gamma ('(1 . 0), n, c), k)

; this is a number:

Theorem: r-is-a-number (k ∈ N) → (r (k, n, c) ∈ N)

Theorem: r-is-a-big (k ∈ N) → (r (k, n, c) ≮ k)

; now, we will get YY as an omega--large subset of ZZ = [k, (R k n c)]
; we want to show that that implies that YY is
; large (in Paris-Harrington sense) and has size at least k
; (which follows from the defn of large)

Theorem: result-is-large-aux1 (setp (yy) ∧ o-largep (yy, '(1 . 0))) → (largep (yy) ∧ listp (yy) ∧ (length (yy) ≮ car (yy)))

Theorem: result-is-large-aux2 (x ∈ segment (k, j )) → (car (segment (k, j )) = k)

Theorem: result-is-large-aux3 (x ∈ segment (k, j )) → (x ≮ k)

Theorem: result-is-large-aux4 (listp (yy) ∧ subsetp (yy, segment (k, j ))) → (car (yy) ≮ k)

Theorem: result-is-large (setp (yy) ∧ subsetp (yy, segment (k, j )) ∧ o-largep (yy, '(1 . 0))) → (largep (yy) ∧ (length (yy) ≮ k))

Event: Disable result-is-large-aux1.

Event: Disable result-is-large-aux2.

Event: Disable result-is-large-aux3.

Event: Disable result-is-large-aux4.

;;;;;;;;  extracting the homogeneous set
; (extract-ramsey-P-H g k n c)  finds a subset
; of (segment 0 (R k n c))  which is large and of size at least k
; actually, it just finds an omega-large subset of [k, (R k n c)]

Definition: extract-ramsey-p-h (g, k, n, c) = extract-ramsey (g, segment (k, r (k, n, c)), '(1 . 0), n, c)

; first, let's see what we get by a direct application
; of the ord-ramsey theorem.  To apply that, we need that
; the segment  (segment k (R k n c))  is
; (Gamma omega n c) -- large

Theorem: r-segment-is-large (k ∈ N) → o-largep (segment (k, r (k, n, c)), gamma ('(1 . 0), n, c))

; applying ord-ramsey,

Theorem: ramsey-p-h-aux1 (rangep (g, c) ∧ (n ≄ 0) ∧ (k ∈ N) ∧ (r = r (k, n, c)) ∧ (yy = extract-ramsey-p-h (g, k, n, c))) → (setp (yy)

∧ subsetp (yy, segment (k, r)) ∧ homp (yy, g, n) ∧ o-largep (yy, '(1 . 0)))

Event: Disable ord-ramsey.

Event: Disable ord-ramsey-a.

Event: Disable ord-ramsey-b.

Event: Disable ord-ramsey-c.

; to convert to intended Ramsey theorem:

; we need that (subsetp YY (segment k R))
; implies (subsetp YY (segment 0 R))

Theorem: ramsey-p-h-aux2 ((k ∈ N) ∧ (r ∈ N) ∧ (k ≤ r) ∧ (x ∈ segment (k, r))) → (x ∈ segment (0, r))

Theorem: ramsey-p-h-aux3 ((k ∈ N) ∧ (r ∈ N) ∧ (k ≤ r)) → subsetp (segment (k, r), segment (0, r))

Theorem: ramsey-p-h-aux4 ((k ∈ N) ∧ (r ∈ N) ∧ (k ≤ r) ∧ subsetp (yy, segment (k, r))) → subsetp (yy, segment (0, r))

Event: Disable segment.

Event: Disable subsetp.

Event: Disable setp.

Event: Disable extract-ramsey.

Event: Disable extract-ramsey-p-h.

Event: Disable recursive-case-for-segment.

; Paris - Harrington version of Ramsey Theorem:

Theorem: ramsey-p-h (rangep (g, c) ∧ (n ≄ 0) ∧ (k ∈ N) ∧ (r = r (k, n, c)) ∧ (yy = extract-ramsey-p-h (g, k, n, c))) → (setp (yy)

∧ subsetp (yy, segment (0, r)) ∧ homp (yy, g, n) ∧ (k ≤ length (yy)) ∧ largep (yy))

;;; NOTE! : without the (largep YY), this would just be the
;;; standard Ramsey theorem, which is provable in PRA

Event: Make the library "paris-harrington" and compile it.

Index

add-in-end-and-length, 80 add-in-end-is-last, 80 add-on-end, 80, 81, 83, 85–87, 129,

130, 132, 134, 135, 141, 151, 155, 157

add-on-end-makes-sets, 80 addition-of-exponents, 2 all-but-last, 80, 81, 85, 87, 141 all-but-last-and-length, 80 all-but-last-aux1, 80 all-but-last-is-a-set, 81 all-but-last-is-non-empty, 81 all-but-last-is-sublist, 80 all-but-last-is-sublist-a, 81 all-but-last-of-add-on-end, 80 all-fns-on-power, 133, 134, 137–139 all-maps, 131–133 all-maps-gets-all, 131 all-pairs, 8 all-pairs-in-cons-all, 8 all-sublists, 12 all-subsets, 17 all-zero-large, 52 append-preserves-members-all-pr

operp, 11 append-preserves-members-all-su

blistp, 11 append-works-left, 7 append-works-right, 7 assoc-of-sharp, 39 assoc-outside-domain, 122 associativity-of-times, 2 augmented-map, 133 augmented-map-is-standard, 133

bad-for-bound-on-mult, 27 bad-for-cdrs-are-smaller, 23, 24 bad-for-different-mult-works, 29–32 bad-for-ext, 17, 18 bad-for-insert-is-bigger, 35 bad-for-large-superset-ord, 55–61 bad-for-monotonicity-of-insert, 41, 42 bad-for-mult-of-sharp, 37, 38 bad-for-norm-up-to-big-enuf, 45 bad-for-nthcdr-is-above-by-n, 93 bad-for-nthcdr-large-a, 94 bad-for-nthcdr-large-b, 95, 96 bad-for-pigeon-2, 70–74 bad-for-pigeon-d, 119–121 bad-for-prehom-set, 151–155 bad-for-segments-are-sets, 124 bad-for-subset-implies-sublist, 14–16 bad-pair-is-bad, 77 bad-triple-is-bad, 82 base-case-for-lambda, 165 bound-on-end-end, 133 bound-on-mult, 27 bound-on-mult-aux1, 27 bound-on-mult-aux2, 27 bound-on-mult-aux3, 27 bound-on-mult-aux4, 27 bound-on-mult-aux5, 27 bound-on-mult-aux6, 27 bound-on-mult-aux7, 27 bound-on-mult-kludge, 27 bound-on-phi, 104 bound-on-phi-aux1, 103 bound-on-phi-aux2, 103 bound-on-phi-aux3, 103 bound-on-phi-aux4, 103 bound-on-phi-aux5, 103 bound-values-of-sing-fn, 126

cadr-of-segment, 124 car-before-cadr, 19 car-of-a-set, 54 car-of-insert-a, 34 car-of-insert-aux1, 37 car-of-insert-b, 34 car-of-insert-c, 37 car-of-num-sharp, 33 car-of-phi, 103 car-of-segment, 123 car-of-sharp-a, 37 car-of-sharp-aux1, 37 car-of-sharp-aux2, 37 car-of-sharp-b, 39 car-of-star, 103 car-of-subset, 9 cars-are-ordinals, 23 cars-go-down, 23 cars-of-smaller-ordinals, 25 cdr-cdr-subset, 20 cdr-cdr-subset-aux1, 19 cdr-is-a-set, 92 cdr-is-above, 92 cdr-is-above-by-1, 92 cdr-is-covered, 63 cdr-is-covered-set-a, 65 cdr-is-covered-set-a-aux1, 64 cdr-is-covered-set-a-aux2, 64 cdr-is-covered-set-b, 65 cdr-is-subset, 9 cdr-is-subset-aux1, 9 cdr-large-a, 93 cdr-large-b, 95 cdr-lemma-1, 108 cdr-lemma-2, 111 cdr-lemma-aux1, 108 cdr-lemma-aux10, 110 cdr-lemma-aux11, 110 cdr-lemma-aux12, 110 cdr-lemma-aux13, 110 cdr-lemma-aux14, 110 cdr-lemma-aux15, 110 cdr-lemma-aux2, 108 cdr-lemma-aux3, 109 cdr-lemma-aux4, 109 cdr-lemma-aux5, 109 cdr-lemma-aux6, 109 cdr-lemma-aux7, 109 cdr-lemma-aux8, 110 cdr-lemma-aux9, 110 cdr-of-segment, 123 cdr-of-subset, 9 cdrs-are-ordinals, 23 cdrs-are-smaller, 25 cdrs-are-smaller-aux1, 24 cdrs-are-smaller-aux2, 24 cdrs-are-smaller-aux3, 24 cdrs-are-smaller-aux4, 24 cdrs-are-smaller-aux5, 24 cdrs-are-smaller-aux6, 24 cdrs-are-smaller-aux7, 24 cdrs-are-smaller-aux8, 24 cdrs-are-smaller-aux9, 24 commut-of-sharp, 39 commut-of-times, 104 commut-of-times-aux1, 104 compare-first-elts, 14 compare-hyps, 144 cons-all, 7, 8, 10–12 cons-all-preserves-members-all-

sublistp, 12 cons-all-preserves-members-all-p

roperp, 11 cons-preserves-proper, 11 constant-0, 112 constant-1, 112 constant-range-1, 113 constant-range-1-aux1, 113 constant-same-value, 112 constantp, 112–114, 119, 128, 135,

136, 139 constantp-on-first-part, 114 counter-hom, 77–79 counter-hom-aux-x, 127, 128 counter-hom-aux-y, 127, 128 counter-hom-finds-one, 78 counter-hom-x, 79, 127, 128 counter-hom-y, 79, 127, 128 counter-pre-hom, 82, 83 counter-pre-hom-finds-one, 82 counter-pre-hom-s1, 83 counter-pre-hom-y, 83 counter-pre-hom-z, 83 counter-range, 159 covers, 62–65, 70–74, 115, 120 covers-empty, 62 covers-is-symmetric, 63 covers-negative, 62 covers-positive-a, 62 covers-positive-b, 62

derived, 86–88, 158, 160–163 derived-and-prehom, 87 derived-aux, 86, 159, 160 derived-aux1, 86 derived-aux2, 86 derived-partition-lemma, 88 derived-partition-lemma-aux1, 87 derived-partition-lemma-aux2, 87 derived-works, 86 dif-pair, 113 dif1, 113 dif2, 113 different-mult, 28, 29, 32 different-mult-for-larger-car, 29 different-mult-for-lists-same-c

ar, 29 different-mult-for-numbers, 28 different-mult-for-smaller-car, 29 different-mult-is-ord, 28 different-mult-list-number, 29 different-mult-number-list, 29 different-mult-works, 32 different-mult-works-aux1, 30 different-mult-works-aux10, 31 different-mult-works-aux11, 31 different-mult-works-aux12, 31 different-mult-works-aux13, 32 different-mult-works-aux2, 30 different-mult-works-aux3, 30 different-mult-works-aux4, 30 different-mult-works-aux5, 30 different-mult-works-aux6, 30 different-mult-works-aux7, 30 different-mult-works-aux8, 30 different-mult-works-aux9, 31 different-mult-works-kludge, 32 discard-the-car-a, 63 discard-the-car-b, 63 discard-the-car-set-a, 63 discard-the-car-set-b, 63 distributivity, 2 domain, 122, 123, 126

empty-is-nil, 12 empty-not-large, 52 empty-segment, 123 empty-subset, 19 end-end, 132–134 end-end-yields-numbers, 132 expt, 1–6, 10, 106, 109, 110, 112, 132, 133, 137, 139

expt-is-positive, 2 extensionality, 18 extensionality-aux1, 17 extensionality-aux2, 17 extensionality-aux3, 17 extensionality-aux4, 18 extensionality-aux5, 18 extensionality-aux6, 18 extensionality-kludge, 18 extract-nice, 137–140, 142–146, 148– 150, 152–154

extract-nice-is-nil, 142

extract-nice-produces-set, 142 extract-nice-produces-subset, 142 extract-pigeon, 118–121, 127, 137 extract-prehom, 144–155, 157, 158,

161, 163 extract-prehom-aux1, 143 extract-ramsey, 158, 161–164, 167 extract-ramsey-basis, 127, 128, 158 extract-ramsey-p-h, 167, 168

find-larger-element, 84–87 find-larger-element-works-a, 84 find-larger-element-works-b, 84 first-before-last, 13 first-of-segment, 124 first-part, 114–116, 118–120 first-part-is-set, 116 first-part-is-set-aux1, 115 first-part-is-set-aux2, 115 first-part-is-set-aux3, 115 first-part-is-set-aux4, 115 first-part-is-set-aux5, 116 first-part-is-set-aux6, 116 first-part-is-set-aux7, 116 first-part-is-set-aux8, 116 first-part-is-set-aux9, 116 first-part-is-sublist, 115 first-part-is-subset, 115 first-rest-cover, 115 first-rest-member, 115 funcall, 76–79, 81, 83, 85–87, 112–

115, 123, 125, 126, 128, 132– 136, 141, 151, 155, 157

funcall-outside-domain, 123

gamma, 157, 158, 160, 161, 163, 164,

166, 167 gamma-is-an-ord, 157

hom-bad-pairp, 77, 78 homp, 78, 79, 87, 88, 128, 162–164,

167, 168 homp-is-necessary, 79 homp-is-sufficient, 78 homp-is-sufficient-a, 78

increasing, 13 insert, 34–37, 40–42, 46 insert-is-an-ordinal, 34 insert-is-bigger, 35 insert-is-bigger-aux1, 34 insert-is-bigger-aux2, 35 insert-is-bigger-aux3, 35 insert-is-bigger-aux4, 35 insert-is-bigger-aux5, 35 insert-is-bigger-aux6, 35 insert-is-bigger-aux7, 35 insert-is-cons, 34 insert-small-ordinal, 35 irreflex, 20 irreflex-of-ord-leq, 25

lambda, 164–166 lambda-gives-large-segments, 165 lambda-gives-large-segments-aux 1, 165 2, 165 3, 165

lambda-is-a-number, 165 lambda-is-big, 165 lambda kludge, 164 large-goes-up, 61 large-superset-ord, 61 large-superset-ord-aux1, 55 large-superset-ord-aux10, 57 large-superset-ord-aux11, 57 large-superset-ord-aux12, 57 large-superset-ord-aux13, 57 large-superset-ord-aux14, 57 large-superset-ord-aux15, 57 large-superset-ord-aux16, 57 large-superset-ord-aux17, 57 large-superset-ord-aux18, 57 large-superset-ord-aux19, 58 large-superset-ord-aux2, 55 large-superset-ord-aux20, 58 large-superset-ord-aux21, 58 large-superset-ord-aux22, 58 large-superset-ord-aux23, 58 large-superset-ord-aux24, 58 large-superset-ord-aux25, 59 large-superset-ord-aux26, 60 large-superset-ord-aux27, 60 large-superset-ord-aux28, 60 large-superset-ord-aux29, 61 large-superset-ord-aux3, 56 large-superset-ord-aux4, 56 large-superset-ord-aux5, 56 large-superset-ord-aux6, 56 large-superset-ord-aux7, 56 large-superset-ord-aux8, 56 large-superset-ord-aux9, 56 large-superset-ord-kludge, 60 large-with-smaller-ord, 62 largep, 12, 54, 166, 168 larger-elt-is-found, 85 last, 13, 80, 81, 83–85, 129, 141, 151,

153, 155, 157 last-is-a-candidate-1, 85 last-is-a-candidate-2, 85 last-is-a-candidate-3, 85 last-is-a-member, 85 last-is-member, 141 last-of-vn, 129 length, 7, 10, 12, 19, 53, 54, 77–81,

85, 87, 92, 113, 119, 121, 126, 128, 129, 131–133, 139, 143, 166, 168

length-of-all-but-last, 81 length-of-append, 7 length-of-nthcdr, 92 length-of-sublist, 19 length-of-subset, 19 leq-0, 23 leq-as-an-or, 23 limit-not-succ, 25 limitp, 21, 23, 25, 48, 51, 53, 89 list-all, 131 list-all-gets-all, 131 lower-bound-on-norm-of-pred, 49

magic, 3–6, 47–50, 53–55, 57, 58, 61, 62, 68, 90, 91, 97–99, 101, 102, 105, 106, 109, 110

magic-1, 4 magic-10, 5 magic-11, 5 magic-12, 6 magic-13, 6 magic-14, 6 magic-15, 6 magic-16, 6 magic-16-aux1, 6 magic-17, 6 magic-18, 6 magic-2, 4 magic-3, 4 magic-4, 5 magic-5, 5 magic-6, 5 magic-7, 5 magic-8, 5 magic-9, 5 magic-is-a-number, 3 magic-is-bigger, 4 magic-is-bigger-aux1, 3 magic-is-bigger-aux2, 3 magic-is-monotonic, 3 magic-is-monotonic-aux1, 3 magic-is-monotonic-aux2, 3 magic-is-monotonic-aux3, 3 magic-is-monotonic-aux4, 3 mapsto, 76, 113–115, 119–121, 127,

134, 138 mapsto-rest-part, 114 mapsto-works, 76 max-below, 46, 47 max-below-is-an-ordinal, 46 max-below-is-below, 46 max-below-is-max, 47 max-below-of-0, 47 max-is-last, 13 memb-of-dif, 8, 9 member-of-covered-set, 63 member-values-of-power-power, 134 members-all-properp, 11 members-all-properp-works, 11 members-all-sublistp, 11, 12 members-all-sublistp-works, 12 members-are-numbers, 85 members-of-add-on-end, 130 members-of-first-part, 115 members-of-initial-segment, 126 members-of-rest-part, 115 members-of-segment, 19 members-of-vn, 130 members-of-vn-aux1, 130 members-of-vn-aux2, 130 min-is-first, 13 monot-of-norm-of-pred, 51 monot-of-norm-of-pred-aux1, 51 monot-of-norm-of-pred-aux2, 51 monot-of-norm-of-pred-aux3, 51 monot-of-pred, 51 monot-of-pred-aux1, 51 monot-of-pred-aux2, 51 monoton-of-exp-1, 2 monoton-of-exp-2, 2 monoton-of-exp-aux1, 2 monoton-of-exp-aux2, 2 monotonicity-of-insert, 42 monotonicity-of-insert-aux1, 40 monotonicity-of-insert-aux10, 42 monotonicity-of-insert-aux2, 40 monotonicity-of-insert-aux3, 40 monotonicity-of-insert-aux4, 40 monotonicity-of-insert-aux5, 41 monotonicity-of-insert-aux6, 41 monotonicity-of-insert-aux7, 41 monotonicity-of-insert-aux8, 41 monotonicity-of-insert-aux9, 41 monotonicity-of-insert-kludge, 41 monotonicity-of-sharp, 43 mult, 26, 27, 29–33, 36–38 mult-in-a-number, 26 mult-is-a-number, 26 mult-of-insert-a, 36 mult-of-insert-b, 36 mult-of-num-sharp, 33 mult-of-sharp, 38 mult-of-sharp-aux1, 38 mult-of-sharp-aux2, 38 mult-of-sharp-aux3, 38 mult-of-sharp-aux4, 38 mult-of-sharp-aux5, 38 mult-of-sharp-aux6, 38 mult-of-sharp-aux7, 38 mult-of-sharp-aux8, 38 mult-of-sharp-aux9, 38

nice, 135, 136, 140–142, 153 nice-and-last, 141 nice-goes-down, 136 nice-goes-down-aux1, 136 nice-goes-down-aux2, 136 nice-goes-down-aux3, 136 nice-goes-down-aux4, 136 nice-goes-down-aux5, 136 nice-implies-constant, 135 nice-implies-same-values, 135 nice-set-a, 138 nice-set-a-aux1, 138 nice-set-a-aux2, 138 nice-set-a-aux3, 138 nice-set-b, 138 nice-set-c, 140 nice-set-c-aux1, 138 nice-set-c-aux2, 139 nice-set-c-aux3, 139 nice-set-c-aux4, 139 nice-set-c-aux5, 139 nice-set-d, 140 nice-set-hyp, 141–144 nil-is-subset, 9 no-cycle-alt, 21 nocycle, 21 non-constant-different-values, 113 non-empty-subset, 9 non-list-segment, 123 norm, 43–51, 53–55, 57, 58, 61, 62,

68, 90, 91, 102–106, 108– 110 norm-above-1, 54 norm-above-1-aux1, 54 norm-above-1-aux2, 54 norm-is-a-number, 43 norm-non-zero, 44 norm-of-a-number, 43 norm-of-cons, 43 norm-of-insert, 46 norm-of-max-below, 47 norm-of-num-sharp, 46 norm-of-phi, 102 norm-of-pred-of-limit, 48 norm-of-pred-of-limit-aux1, 48 norm-of-pred-of-limit-aux2, 48 norm-of-pred-of-limit-aux3, 48 norm-of-pred-of-succ, 49 norm-of-pred-of-type-c, 90 norm-of-pred-sharp, 50 norm-of-predecessor, 43 norm-of-right-answer-c, 90 norm-of-sharp, 46 norm-of-star, 103 norm-of-successor, 43 norm-of-type-c, 90 norm-star-exp-phi, 106 norm-star-exp-phi-aux1, 105 norm-star-exp-phi-aux2, 105 norm-star-exp-phi-aux3, 106 norm-star-exp-phi-aux4, 106 norm-star-exp-phi-aux5, 106 norm-star-exp-phi-aux6, 106 norm-star-phi, 105 norm-star-phi-aux1, 104 norm-star-phi-aux2, 104 norm-star-phi-aux3, 104 norm-up-to, 44, 45, 47 norm-up-to-big-enuf, 45 norm-up-to-big-enuf-aux1, 44 norm-up-to-big-enuf-aux2, 44 norm-up-to-big-enuf-aux3, 44 norm-up-to-big-enuf-aux4, 44 norm-up-to-big-enuf-aux5, 45 norm-up-to-big-enuf-aux6, 45 norm-up-to-big-enuf-aux7, 45 norm-up-to-big-enuf-kludge, 44 not-again, 13 nothing-between, 22 nthcdr, 91–99, 101, 102, 109, 110 nthcdr-0, 92 nthcdr-1, 92 nthcdr-add, 92 nthcdr-c-1, 96 nthcdr-c-2, 97 nthcdr-is-a-set, 92 nthcdr-is-above-by-n, 93 nthcdr-is-above-by-n-aux1, 93 nthcdr-is-above-by-n-aux2, 93 nthcdr-is-above-by-n-aux3, 93 nthcdr-is-above-by-n-aux4, 93 nthcdr-is-subset, 92 nthcdr-large-a, 94 nthcdr-large-a-aux1, 94 nthcdr-large-a-aux2, 94 nthcdr-large-a-aux3, 94 nthcdr-large-a-aux4, 94 nthcdr-large-a-aux5, 94 nthcdr-large-a-kludge, 94 nthcdr-large-b, 96 nthcdr-large-b-aux1, 95 nthcdr-large-b-aux2, 95 nthcdr-large-b-aux4, 95 nthcdr-large-b-aux5, 96 nthcdr-large-b-kludge, 96 nthcdr-of-cdr, 93 num-sharp, 33, 36, 46 num-sharp-and-successor, 33 num-sharp-and-zero, 33 num-sharp-gets-bigger, 33 num-sharp-is-an-ordinal, 33 num-sharp-is-monotonic, 33 number-large, 53 number-part, 26, 33, 36 number-part-is-a-number, 26 number-part-of-insert, 36 number-part-of-num-sharp, 33 number-values-of-sing-fn, 126 numbers-below-omega, 53

o-largep, 52–55, 57, 61, 62, 66–74, 93–102, 108–110, 112, 118– 121, 128, 137–140, 142, 144, 149, 150, 160–162, 164–167

omega-is-a-limit, 53 omega-large, 54 omega-large-implies-large, 54 only-proper, 11 only-proper-aux1, 11 only-sublists, 12 only-sublists-aux1, 12 ord-leq, 23, 25, 26, 37, 39, 48–51,

55–58, 61, 62, 66, 88–91, 93–103, 108–111, 137, 139, 140, 142, 143, 149, 152

ord-leq-is-idempotent, 50 ord-leq-is-transitive, 23 ord-leq-zero, 23 ord-ramsey, 164 ord-ramsey-a, 158 ord-ramsey-b, 162 ord-ramsey-b-aux1, 161 ord-ramsey-b-aux2, 162 ord-ramsey-c, 163 ord-ramsey-c-aux1, 162 ord-ramsey-c-aux2, 162 ord-ramsey-c-aux3, 163 ord-ramsey-c-aux4, 163 ord-ramsey-c-aux5, 163 ord-ramsey-c-aux6, 163 ord-ramsey-hyp, 160–163 ord-ramsey-hyp-positive, 161 ord-ramsey-to-prehom-set-hyp, 161 ords-below-2, 21

phi, 102–106, 108–110, 112, 137–140,

142, 144, 149, 157, 161 phi-is-an-ord, 102 phi-non-zero, 138 pigeon-2, 74 pigeon-2-aux1, 70 pigeon-2-aux10, 71 pigeon-2-aux11, 71 pigeon-2-aux12, 71 pigeon-2-aux13, 71 pigeon-2-aux14, 72 pigeon-2-aux15, 72 pigeon-2-aux16, 72 pigeon-2-aux17, 72 pigeon-2-aux18, 73 pigeon-2-aux19, 73 pigeon-2-aux2, 70 pigeon-2-aux20, 73 pigeon-2-aux21, 73 pigeon-2-aux22, 73 pigeon-2-aux23, 74 pigeon-2-aux3, 70 pigeon-2-aux4, 70 pigeon-2-aux5, 70 pigeon-2-aux6, 70 pigeon-2-aux7, 70 pigeon-2-aux8, 71 pigeon-2-aux9, 71 pigeon-2-kludge, 73, 74 pigeon-a, 119 pigeon-b, 119 pigeon-c, 119 pigeon-c-aux1, 119 pigeon-c-aux2, 119 pigeon-d, 121 pigeon-d-aux1, 119 pigeon-d-aux10, 120 pigeon-d-aux11, 121 pigeon-d-aux12, 121 pigeon-d-aux13, 121 pigeon-d-aux14, 121 pigeon-d-aux2, 119 pigeon-d-aux3, 120 pigeon-d-aux4, 120 pigeon-d-aux5, 120 pigeon-d-aux6, 120 pigeon-d-aux7, 120 pigeon-d-aux8, 120 pigeon-d-aux9, 120 plus-difference, 2 pos-mult, 26, 33, 36 pos-mult-different, 36 pos-mult-is-a-number, 26 pos-mult-of-num-sharp, 33 pos-mult-same, 36 positive-large, 52 positive-ordinals, 149 postive-ord-lessp, 21 power-map, 133, 134 power-map-in-all-fns, 133 power-power, 134–139 power-set, 10–12, 17, 78, 79, 82, 83,

86, 133 pre-hom-and-all-but-last, 85 pre-hom-bad-triplep, 81, 82 pre-homp, 82, 83, 85, 87, 88, 157,

162, 163 pre-homp-is-necessary, 83 pre-homp-is-sufficient, 82 pred, 47–53, 55, 57, 58, 60, 61, 66–

69, 71–74, 89–91, 105, 106, 109, 110, 112, 137, 140, 142– 144, 148–150, 152–154, 164, 165 pred-below-limit, 48 pred-is-an-ordinal, 48 pred-is-below, 47 pred-is-largest, 48 pred-not-0, 55 pred-of-0, 47 pred-of-omega, 53 pred-of-omega-aux1, 53 pred-of-omega-aux2, 53 pred-of-succ, 49 pred-of-succ-aux1, 49 pred-of-succ-aux2, 49 pred-of-succ-aux3, 49 pred-of-succ-aux4, 49 pred-sharp, 50 pred-sharp-below, 50 pred-type-a, 89 pred-type-b, 89 pred-type-c, 91 pred-type-c-aux1, 90 pred-type-c-aux2, 90 pred-type-c-aux3, 90 pred-type-c-aux4, 91 pred-type-c-aux5, 91 predecessor, 22, 23, 43, 49, 53, 89 predecessor-is-an-ordinal, 22 predecessor-is-smaller, 22 predecessor-of-0, 23 predecessor-of-limit, 23 predecessor-of-type-a, 89 predecessor-of-type-b, 89 predecessor-suc, 22 prehom-hyp-implies-non-empty, 149 prehom-set-a, 145 prehom-set-b, 145 prehom-set-b-aux1, 145 prehom-set-b-aux2, 145 prehom-set-c, 145 prehom-set-d, 148 prehom-set-d-aux1, 146 prehom-set-d-aux10, 147 prehom-set-d-aux11, 148 prehom-set-d-aux12, 148 prehom-set-d-aux2, 146 prehom-set-d-aux3, 146 prehom-set-d-aux4, 146 prehom-set-d-aux5, 146 prehom-set-d-aux6, 147 prehom-set-d-aux7, 147 prehom-set-d-aux8, 147 prehom-set-d-aux9, 147 prehom-set-e, 150 prehom-set-e-aux1, 149 prehom-set-e-aux2, 149 prehom-set-e-aux3, 150 prehom-set-e-aux4, 150 prehom-set-e-aux5, 150 prehom-set-f, 157 prehom-set-f-aux1, 151 prehom-set-f-aux10, 152 prehom-set-f-aux11, 152 prehom-set-f-aux12, 152 prehom-set-f-aux13, 152 prehom-set-f-aux14, 153 prehom-set-f-aux15, 153 prehom-set-f-aux16, 153 prehom-set-f-aux17, 153 prehom-set-f-aux18, 153 prehom-set-f-aux19, 153 prehom-set-f-aux2, 151 prehom-set-f-aux20, 153 prehom-set-f-aux21, 154 prehom-set-f-aux22, 154 prehom-set-f-aux23, 155 prehom-set-f-aux24, 155 prehom-set-f-aux25, 157 prehom-set-f-aux26, 157 prehom-set-f-aux3, 151 prehom-set-f-aux4, 151 prehom-set-f-aux5, 152 prehom-set-f-aux6, 152 prehom-set-f-aux7, 152 prehom-set-f-aux8, 152 prehom-set-f-aux9, 152 prehom-set-f-kludge, 154, 155 prehom-set-hyp, 144, 149–151, 154, 155, 157, 161 product, 7, 8, 44, 78, 79, 82, 83, 131,

132 properp, 11–13, 80, 81 r, 166–168 r-is-a-big, 166 r-is-a-number, 166 r-segment-is-large, 167 ramsey-basis-a, 127 ramsey-basis-b, 127 ramsey-basis-c, 128 ramsey-basis-c-aux1, 127 ramsey-basis-c-aux2, 128 ramsey-basis-c-aux3, 128 ramsey-basis-c-aux4, 128 ramsey-basis-c-aux5, 128 ramsey-basis-c-aux6, 128 ramsey-basis-d, 128 ramsey-p-h, 168 ramsey-p-h-aux1, 167 ramsey-p-h-aux2, 168 ramsey-p-h-aux3, 168 ramsey-p-h-aux4, 168 range, 76 range-is-big-enuf, 76 range-of-derived, 160 range-of-derived-aux1, 159 range-of-derived-aux2, 159 range-of-derived-aux3, 159 range-of-derived-aux4, 159 range-of-derived-aux5, 159 range-of-derived-aux6, 159 range-of-derived-aux7, 159 range-of-derived-aux8, 159 range-of-derived-aux9, 160 range-of-power-power, 134 range-of-power-power-aux1, 134 rangep, 123, 126–128, 132–134, 137–

140, 142, 144, 159, 160, 164, 167, 168

rangep-bounds, 123 rangep-is-positive, 123 rangep-numbers, 123 re-assemble-at-end, 81 recursive-case-for-extract-ramse

y, 161 recursive-case-for-gamma, 161 recursive-case-for-lambda, 165 recursive-case-for-large, 52 recursive-case-for-segment, 124 replication-of-hyp, 143 replication-of-hyp-aux1, 143 replication-of-hyp-aux2, 143 replication-of-ord-ramsey-hyp, 161 replication-of-prehom-hyp, 149 replication-of-prehom-hyp-aux1, 149 rest-part, 114, 115, 117–121 rest-part-is-set, 118 rest-part-is-set-aux1, 117 rest-part-is-set-aux2, 117 rest-part-is-set-aux3, 117 rest-part-is-set-aux4, 117 rest-part-is-set-aux5, 117 rest-part-is-set-aux6, 117 rest-part-is-set-aux7, 117 rest-part-is-set-aux8, 117 rest-part-is-set-aux9, 117 rest-part-is-sublist, 115 rest-part-is-subset, 115 result-is-large, 166 result-is-large-aux1, 166 result-is-large-aux2, 166 result-is-large-aux3, 166 result-is-large-aux4, 166

same-cars-in-subset, 14

same-cars-in-subset-aux1, 14 same-cars-in-subset-aux2, 14 same-mult-for-cdr, 31 same-power-maps, 134 segment, 19, 44, 123, 124, 126, 127,

165–168 segments-are-sets, 124 segments-are-sets-aux1, 124 segments-are-sets-aux2, 124 segments-are-sets-aux3, 124 segments-non-empty, 123 set-builder, 116 setp, 12–20, 54, 55, 57, 61–74, 77–

81, 83, 85–87, 92–102, 108– 110, 112, 115–121, 124, 127– 129, 134, 135, 137–148, 150– 152, 154, 155, 157, 158, 160, 164, 166–168

sets-are-proper, 13 sharp, 36–39, 43, 46, 50, 66–74, 102,

103 sharp-and-cdr-a, 69 sharp-and-cdr-aux1, 65 sharp-and-cdr-aux10, 68 sharp-and-cdr-aux2, 66 sharp-and-cdr-aux3, 66 sharp-and-cdr-aux4, 66 sharp-and-cdr-aux5, 66 sharp-and-cdr-aux6, 67 sharp-and-cdr-aux7, 67 sharp-and-cdr-aux8, 68 sharp-and-cdr-aux9, 68 sharp-and-cdr-b, 68 sharp-gets-bigger, 37 sharp-is-an-ordinal, 36 sharp-with-0, 37 sharp-with-0-reversed, 103 simple-nice-set-a, 142 simple-nice-set-b, 142 simple-nice-set-c, 142 simple-nice-set-d, 142 sing-fn, 126–128 sing-fn-aux, 125, 126 sing-fn-aux-1, 125 sing-fn-aux-2, 125 sing-fn-aux-3, 125 sing-fn-aux-4, 125 sing-fn-mapsto, 127 sing-fn-mapsto-aux1, 126 sing-fn-on-sings, 126 singleton-segment, 124 singleton-set, 117 singletons-not-large, 55 size-of-all-fns-on-power, 133 size-of-all-maps, 132 size-of-cons-all, 10 size-of-initial-segment, 126 size-of-list-all, 131 size-of-power-set, 10 size-of-product, 132 size-of-segment, 19 size-of-vn, 129 smaller-car-when-covered, 64 smaller-cars-in-subset, 14 standard-function, 130, 131, 133 star, 102–106, 109, 110, 112, 119– 121, 128, 157

star-is-an-ord, 103 star-with-0, 103 star-with-1, 103 sublist-implies-subset, 10 sublistp, 10–12, 15, 16, 19, 77–83,

85–88, 115, 127, 143, 162, 163 sublists-smaller-length, 143 subset-implies-sublist, 16 subset-implies-sublist-aux1, 15 subset-implies-sublist-aux2, 15 subset-implies-sublist-aux3, 15 subset-implies-sublist-aux4, 15 subset-implies-sublist-aux5, 15 subset-implies-sublist-aux6, 15 subset-implies-sublist-aux7, 15 subset-implies-sublist-aux8, 16 subset-implies-sublist-kludge, 16 subset-of-cdr, 9 subset-of-empty-set, 9 subset-of-last, 141 subset-of-last-aux1, 141 subset-of-last-aux2, 141 subset-of-last-aux3, 141 subsetp, 8–10, 14–20, 55, 57, 58, 61,

62, 78, 92, 99, 102, 110, 115, 119, 127, 134–136, 138, 141–143, 145, 147, 157, 158, 164, 166–168

subsetp-is-idempotent, 62

subsetp-works-1, 8 subsetp-works-2, 9 subsets-smaller-length, 143 suc-predecessor, 22 succ-below-limit, 25 succ-preserves-order, 22 successor, 22, 25, 33, 43, 48 successor-is-a-successor, 22 successor-is-an-ordinal, 22 successor-is-bigger, 22 successor-large, 53 successor-large-non-empty, 53 successorp, 21, 22, 43, 49, 51, 53,

88, 89 successors-are-positive, 21

tail-lemma-1, 101 tail-lemma-1-aux1, 97 tail-lemma-1-aux10, 99 tail-lemma-1-aux11, 99 tail-lemma-1-aux12, 99 tail-lemma-1-aux13, 99 tail-lemma-1-aux14, 99 tail-lemma-1-aux15, 99 tail-lemma-1-aux16, 100 tail-lemma-1-aux17, 101 tail-lemma-1-aux2, 97 tail-lemma-1-aux3, 97 tail-lemma-1-aux4, 98 tail-lemma-1-aux5, 98 tail-lemma-1-aux6, 98 tail-lemma-1-aux7, 98 tail-lemma-1-aux8, 98 tail-lemma-1-aux9, 98 tail-lemma-2, 101 tail-lemma-3, 102 tail-lemma-aux1, 102 tail-of-a-set, 13 tail-of-standard-function, 131 three-kinds, 21 times-is-monotonic, 4 times-left-ident, 4 times-right-ident, 4 times-with-zero-1, 104 times-with-zero-2, 104 transitivity, 21 transitivity-alt, 21 transitivity-alt2, 25 transitivity-of-sublist, 10 transitivity-of-subset, 9 trichotomy, 21 type-a-is-a-successor, 88 type-a-is-ordinal, 88 type-b-is-a-successor, 89 type-b-is-ordinal, 89 type-c-is-a-limit, 89 type-c-is-ordinal, 89

uncovered, 63

uncovered-isnt-covered, 63

upper-bound-on-norm-of-pred, 48

value-of-power-map, 134 value-of-power-power, 134 value-on-first-part, 114 values-of-augmented-map, 133 values-on-rest-part, 114 vn, 129, 130, 133–135, 141 vn-is-a-set, 129 vn-is-a-set-aux1, 129 vn-is-a-set-aux2, 129 vn-is-a-set-aux3, 129