; 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
; it takes [ 11.9 197.5 15.0 ] on a Pentium 133 running linux

(proveall "ramsey" '(


(boot-strap nqthm)


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


; (expt m n ) = m^n, as in Lisp
(defn expt (m n) (if (zerop n) 
	1
	(times m (expt m (sub1 n))) ) )

(prove-lemma distributivity (rewrite) (equal
	(plus (times u y) (times a y))
	(times (plus u a) y)))

(prove-lemma associativity-of-times (rewrite) (equal
	(times m u y) (times (times m u) y)))

(prove-lemma addition-of-exponents (rewrite) (equal
	(expt m (plus a b))
	(times (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
(prove-lemma monoton-of-exp-1 () (implies
	(leq b1 b2) 
	(leq (expt b1 e) (expt b2 e))))

(prove-lemma plus-difference (rewrite) (implies 
	(and (leq e1 e2)  (numberp e1) (numberp e2) )
	(equal
		(plus e1 (difference e2 e1))
		e2 )))
	
; as a function of e:  
(prove-lemma monoton-of-exp-aux1 () (implies
	(and (leq e1 e2)  (numberp e1) (numberp e2) )
	(equal (expt b e2) (times (expt b e1) (expt b (difference e2 e1)))))
( ; hints
(do-not-induct T)
(use (addition-of-exponents (m b) (a e1) (b (difference e2 e1))))
(disable addition-of-exponents)
))

(prove-lemma expt-is-positive (rewrite) (implies
	(not (zerop b))
	(lessp 0 (expt b e)) ))

(prove-lemma monoton-of-exp-aux2 ()  (implies
	(not (zerop b))
	(leq x (times x (expt b e)))))

(prove-lemma monoton-of-exp-2 () (implies
	(and (leq e1 e2)  (numberp e1) (numberp e2) (not (zerop b)))
	(leq (expt b e1) (expt b e2)))  
( ; hints
(do-not-induct T)
(use 
	(monoton-of-exp-aux1 (b b) (e1 e1) (e2 e2))   
	(monoton-of-exp-aux2 (b b) (x (expt b e1)) (e (difference e2 e1)))   ) 
))
; 0 is an exception because 0^0 = 1 but 0^1 = 0

(disable monoton-of-exp-aux1)
(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

(defn magic (s) (times
	(plus (times 3 s) 3)
	(expt (plus s 2) (plus s 2))))

(prove-lemma magic-is-a-number (rewrite)
	(numberp (magic n)))

; now, we have to prove that magic is monotonic

(prove-lemma magic-is-monotonic-aux1 ( ) (implies
	(lessp m n)
	(lessp  (plus (times 3 m) 3)  (plus (times 3 n) 3)  )))

(prove-lemma magic-is-monotonic-aux2 ( ) (implies
	(lessp m n)
	(leq
		(expt (plus m 2) (plus m 2))
		(expt (plus n 2) (plus n 2)))  )
( ; hints
(do-not-induct T)
(use
	(monoton-of-exp-1  (e (plus m 2)) (b1 (plus m 2)) (b2 (plus n 2)))
	(monoton-of-exp-2  (b (plus n 2)) (e1 (plus m 2)) (e2 (plus n 2)))  )
))

(prove-lemma magic-is-monotonic-aux3 (rewrite) 
	(lessp 0 (expt (plus s 2) (plus s 2)))
( ; hints
(do-not-induct T)
(use
	(expt-is-positive (b (plus s 2)) (e (plus s 2)) ))
))

(prove-lemma magic-is-monotonic-aux4 ()  (implies
	(and  (lessp x y) (leq a b) (lessp 0 a) (lessp 0 b))
	(lessp (times x a) (times y b))))

(prove-lemma magic-is-monotonic (rewrite) (implies
	(lessp m n)
	(lessp (magic m) (magic n)))
( ; hints
(do-not-induct T)
(use
	(magic-is-monotonic-aux4
		(x (plus (times 3 m) 3)) (y (plus (times 3 n) 3))
		(a (expt (plus m 2) (plus m 2))) (b (expt (plus n 2) (plus n 2))) )
	(magic-is-monotonic-aux3 (s m))
	(magic-is-monotonic-aux3 (s n))
	(magic-is-monotonic-aux1 (m m) (n n))
	(magic-is-monotonic-aux2 (m m) (n n))  )
(disable times addition-of-exponents magic-is-monotonic-aux3)
))


(disable magic-is-monotonic-aux1)
(disable magic-is-monotonic-aux2)
(disable magic-is-monotonic-aux3)
(disable magic-is-monotonic-aux4)

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

(prove-lemma magic-is-bigger-aux1 (rewrite) 
        (IMPLIES (AND (NOT (EQUAL N 0))
                      (EQUAL (MAGIC N) 0))
                 (NOT (NUMBERP N)))
( ; hints
(use (magic-is-monotonic (m 0) (n n)))
))

(prove-lemma magic-is-bigger-aux2 (rewrite)
(IMPLIES 
	(AND 
		(NUMBERP N)
		(NOT (LESSP (MAGIC (SUB1 N)) (SUB1 N)))  )
	(NOT (LESSP (MAGIC N) N)))
( ; hints
(use (magic-is-monotonic (m (sub1 n)) (n n)))
))

(prove-lemma magic-is-bigger (rewrite) (implies
	(numberp n)
	(not (lessp (magic n) n)))  )

(disable magic-is-bigger-aux1)
(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

(prove-lemma times-is-monotonic ()  (implies
	(and  (leq x y) (leq a b))
	(leq (times x a) (times y b))))

(prove-lemma times-right-ident (rewrite) (implies
	(numberp x) (equal (times x 1) x)))
(prove-lemma times-left-ident (rewrite) (implies
	(numberp x) (equal (times 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

(enable magic)  ; we need its defn for some other properties

(prove-lemma magic-1 () (leq
	(plus (times 2 s) 3)
	(magic s) )
( ; hints
(do-not-induct T)
(use 
	(expt-is-positive (b (plus s 2)) (e (plus s 2)))
	(times-is-monotonic 
		(x (plus (times 2 s) 3)) (a 1)
		(y (plus (times 3 s) 3)) (b (expt (plus s 2) (plus s 2))) ) )
(disable addition-of-exponents times)
))

(prove-lemma magic-2 () (implies
	(numberp s)
	(leq     (expt s s)     (expt (plus s 2) (plus s 2))) )
( ; hints
(do-not-induct T)
(use 
	(monoton-of-exp-1 (e s) (b1 s) (b2 (plus s 2)))
	(monoton-of-exp-2 (e1 s) (e2 (plus s 2)) (b (plus s 2))) )
))

(prove-lemma magic-3 () (implies
	(numberp r)
	(leq  
		(times (times 3 r) (expt r r))
		(magic r)) )
( ; hints
(do-not-induct T)
(use
	(magic-2 (s r))
	(times-is-monotonic 
		(x (times 3 r)) (a (expt r r))
		(y (plus (times 3 r) 3) )  (b (expt (plus r 2) (plus r 2)) )) )
(disable addition-of-exponents times)
))

(prove-lemma magic-4 () (implies
	(numberp s)
	(leq     (expt 2 s)     (expt (plus s 2) (plus s 2))) )
( ; hints
(do-not-induct T)
(use 
	(monoton-of-exp-1 (e s) (b1 2) (b2 (plus s 2)))
	(monoton-of-exp-2 (e1 s) (e2 (plus s 2)) (b (plus s 2))) )
))

(prove-lemma magic-5 () (implies
	(numberp s)
	(leq  
		(expt 2 s)
		(magic s)) )
( ; hints
(do-not-induct T)
(use
	(magic-4 (s s))
	(times-is-monotonic 
		(x 1) (a (expt 2 s))
		(y (plus (times 3 s) 3) )  (b (expt (plus s 2) (plus s 2)) )) )
(disable addition-of-exponents times)
))

(prove-lemma magic-6 () (implies
	(numberp s)
	(leq  
		(expt s (expt 2 s))
		(expt (magic s) (magic s)) ) )
( ; hints
(do-not-induct T)
(use
	(magic-5 (s s))
	(magic-is-bigger (n n))
	(monoton-of-exp-1 (b1 s) (b2 (magic s)) (e (expt 2 s)))
	(monoton-of-exp-2 (b (magic s)) (e1 (expt 2 s)) (e2 (magic s))) )
(disable magic addition-of-exponents times)
(hands-off magic)
))

(prove-lemma magic-7 () (implies
	(numberp s)
	(leq  
		(times (times 3 (magic s)) (expt s (expt 2 s)) )
		(times (times 3 (magic s)) (expt (magic s) (magic s)) ) ) )
( ; hints
(do-not-induct T)
(use
	(magic-6 (s s))
	(times-is-monotonic
		(x (times 3 (magic s))) (a (expt s (expt 2 s)) )
		(y (times 3 (magic s))) (b (expt (magic s) (magic s)))) )
(disable magic addition-of-exponents times)
(hands-off magic)
))

(prove-lemma magic-8 () (implies
	(numberp s)
	(leq  
		(times (times 3 (magic s)) (expt s (expt 2 s)) )
		(magic (magic s))) )
( ; hints
(do-not-induct T)
(use
	(magic-7 (s s))
	(magic-3 (r (magic s))))
(disable magic addition-of-exponents times)
(hands-off magic)
))

(prove-lemma magic-9 () 
	(leq  
		(plus (times 2 s) 3 (times 2 (magic s)))
		(times 3 (magic s)) )
( ; hints
(do-not-induct T)
(use (magic-1 (s s)))
(disable magic addition-of-exponents times)
(hands-off magic)
))

(prove-lemma magic-10 () 
	(implies
		(numberp s)
		(leq  
			(times  
				(plus (times 2 s) 3 (times 2 (magic s)))
				(expt s (expt 2 s)) )
			(magic (magic s))) ) 
( ; hints
(do-not-induct T)
(use 
	(times-is-monotonic
		(x (plus (times 2 s) 3 (times 2 (magic s)))) (y (times 3 (magic s)))
		(a (expt s (expt 2 s))) (b (expt s (expt 2 s)))  )
	(magic-8 (s s))
	(magic-9 (s s)))
(disable magic addition-of-exponents times)
(hands-off magic)
))

; 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

(prove-lemma magic-11 () (implies
	(and (equal d (plus a c)) (equal s (plus z d)) (not (zerop c)) )
	(leq
		(plus (times 2 a) (times 2 (magic z)) 3 c)
		(plus (times 2 s) 3 (times 2 (magic s))))  )
( ; hints
(do-not-induct T)
(use (magic-is-monotonic (m z) (n (plus z a c))))
(disable magic magic-is-monotonic)
))

; step 2

(prove-lemma magic-12 () (implies
	(and (equal d (plus a c)) (equal s (plus z d)) )
	(leq  (expt 2 z) (expt 2 s)))
( ; hints
(do-not-induct T)
(use
	(monoton-of-exp-2 (b 2) (e1 z) (e2 s)) )
(disable addition-of-exponents associativity-of-times)
))

(prove-lemma magic-13 () (implies
	(and (equal d (plus a c)) (equal s (plus z d)) )
	(leq  (expt c (expt 2 z)) (expt s (expt 2 s))))
( ; hints
(do-not-induct T)
(use
	(magic-12 (d d) (a a) (c c) (s s) (z z))
	(monoton-of-exp-1 (b1 c) (b2 s) (e (expt 2 z)))
	(monoton-of-exp-2 (b s) (e1 (expt 2 z)) (e2 (expt 2 s)))  )
(disable addition-of-exponents associativity-of-times)
))

; putting the two steps together:
(prove-lemma magic-14 () (implies
	(and (equal d (plus a c)) (equal s (plus z d)) (not (zerop c)) )
	(leq
		(times
			(plus (times 2 a) (times 2 (magic z)) 3 c)
			(expt c (expt 2 z)))
		(times
			(plus (times 2 s) 3 (times 2 (magic s)))
			(expt s (expt 2 s))   ) ) )
( ; hints
(do-not-induct T)
(use
	(magic-11 (d d) (a a) (c c) (s s) (z z))
	(magic-13 (d d) (a a) (c c) (s s) (z z))
	(times-is-monotonic
		(x (plus (times 2 a) (times 2 (magic z)) 3 c))
		(y (plus (times 2 s) 3 (times 2 (magic s))))
		(a (expt c (expt 2 z)))
		(b (expt s (expt 2 s))) )  )
(disable addition-of-exponents associativity-of-times magic times)
))

; now, adding magic-10
(prove-lemma magic-15 () (implies
	(and (equal d (plus a c)) (equal s (plus z d)) (not (zerop c)) )
	(leq
		(times
			(plus (times 2 a) (times 2 (magic z)) 3 c)
			(expt c (expt 2 z)))
		(magic (magic s)))  )
( ; hints
(do-not-induct T)
(use
	(magic-14 (d d) (a a) (c c) (s s) (z z))
	(magic-10 (s s)) )
(disable addition-of-exponents associativity-of-times magic times)
))

; 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
(prove-lemma magic-16-aux1 (rewrite) (implies
	(not (numberp v))
	(equal (times w v) 0)))

(prove-lemma magic-16 () (implies
	(not (numberp v))
	(equal (magic v) 12)))
(disable magic-16-aux1)

(prove-lemma magic-17 () (implies
	(leq v w)
	(leq (magic v) (magic w)))
( ;  hints
(do-not-induct T)
(use
	(magic-is-monotonic (m v) (n w) )
	(magic-16 (v w))
	(magic-16 (v v)))
(disable magic)
))

(prove-lemma magic-18 () (implies
	(and (equal d (plus a c)) (leq (magic (plus z d)) q) (not (zerop c)) )
	(leq
		(times
			(plus (times 2 a) (times 2 (magic z)) 3 c)
			(expt c (expt 2 z)))
		(magic q))  )
( ; hints
(do-not-induct T)
(use
	(magic-17 (v (magic (plus z d))) (w q))
	(magic-15 (d d) (a a) (c c) (s (plus z d)) (z z))  )
(disable addition-of-exponents associativity-of-times magic times)
))

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

(disable magic)


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


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

(prove-lemma append-works-left (rewrite) (implies
	(member x lst1)
	(member x (append lst1 lst2))))

(prove-lemma append-works-right (rewrite) (implies
	(member y lst2)
	(member y (append lst1 lst2))))

(defn length (set) (if (listp set)
	(add1 (length (cdr set)))
	0 ))

(prove-lemma length-of-append (rewrite) (equal
	(length (append lst1 lst2))
	(plus (length lst1) (length lst2)) ))


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

(defn cons-all (item lst) (if (listp lst)
	(cons (cons item (car lst)) (cons-all item (cdr lst)))
	nil ))

(defn product (lst1 lst2) (if (nlistp lst1)
	nil
	(append (cons-all (car lst1) lst2) (product (cdr lst1) lst2) ) ))
; (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

(prove-lemma all-pairs-in-cons-all (rewrite) (implies
	(member y lst)
	(member (cons item y) (cons-all item lst)) ))

(prove-lemma all-pairs (rewrite) (implies
	(and (member x lst1) (member y lst2))
	(member (cons x y) (product lst1 lst2))))

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

(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

(defn subsetp (s1 s2) 
	(if (listp s1)
		(and
			(member (car s1) s2)
			(subsetp (cdr s1) s2))
		T )) 

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

(prove-lemma subsetp-works-1 (rewrite) (implies
	(and (subsetp s1 s2) and (member x s1))
	(member x s2)))

(defn memb-of-dif (s1 s2)
	(if (listp s1)
		(if (member (car s1) s2)
			(memb-of-dif (cdr s1) s2)
			(car s1))
		NIL ))

(prove-lemma subsetp-works-2 (rewrite) (implies
	(not (subsetp s1 s2))
	(and
		(member (memb-of-dif s1 s2) s1) 
		(not (member (memb-of-dif s1 s2) s2)) ) ))

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

(prove-lemma subset-of-empty-set (rewrite) (implies
	(listp s) (not (subsetp s nil))))

(prove-lemma transitivity-of-subset (rewrite) (implies
	(and (subsetp s1 s2) (subsetp s2 s3))
	(subsetp s1 s3)))

(prove-lemma cdr-is-subset-aux1 (rewrite)  (implies
	(member x (cdr s))
	(member x s)))

(prove-lemma cdr-is-subset (rewrite) 
	(subsetp (cdr s) s)  
; hints
( (use (subsetp-works-2 (s1 (cdr s)) (s2 s)))  ))

(disable cdr-is-subset-aux1)

(prove-lemma cdr-of-subset (rewrite) (implies
	(and (subsetp s1 s2) (listp s1))
	(subsetp (cdr s1) s2)))

(prove-lemma nil-is-subset (rewrite)
	(subsetp nil s))

; the following might useful in proving consequences
; of (subsetp s1 s2) by induction -- reducing to
; (subsetp s1 (cdr s2))
(prove-lemma subset-of-cdr (rewrite) (implies
	(and (subsetp s1 s2) (not (member (car s2) s1)))
	(subsetp s1 (cdr s2))))

(prove-lemma non-empty-subset (rewrite) (implies
	(and (subsetp lst1 lst2) (listp lst1))
	(listp lst2)))

(prove-lemma car-of-subset (rewrite) (implies
	(and (subsetp lst1 lst2) (listp lst1))
	(member (car lst1) lst2)))

; now, consider sub-lists

(defn sublistp (lst1 lst2) (if (listp lst2) 
	(or
		(sublistp lst1 (cdr lst2))
		(and 
			(listp lst1)
			(equal (car lst1) (car lst2))
			(sublistp (cdr lst1) (cdr lst2)) ) )
	(not (listp lst1)) ))

(prove-lemma sublist-implies-subset () (implies
	(sublistp lst1 lst2)
	(subsetp lst1 lst2) )
( ;  hints
(induct (sublistp lst1 lst2))
))

(prove-lemma transitivity-of-sublist (rewrite) (implies
	(and (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

(defn power-set (set)  (if (listp set)
	(append 
		(cons-all (car set) (power-set (cdr set)))
		(power-set (cdr set)))  
	(list nil) ))

; this has 2^(length elements)

(prove-lemma size-of-cons-all (rewrite) (equal
	(length (cons-all item lst))
	(length lst) ))

(prove-lemma size-of-power-set (rewrite) (equal
	(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

(defn properp (lst) (if (listp lst)
	(properp (cdr lst))
	(equal lst nil)))

(prove-lemma cons-preserves-proper (rewrite) (implies
	(properp lst)
	(properp (cons item lst))))
	
(defn members-all-properp (biglst) (if (listp biglst)
	(and (properp (car biglst)) (members-all-properp (cdr biglst)))
	T ))

(prove-lemma append-preserves-members-all-properp (rewrite) (implies
	(and 
		(members-all-properp biglst1) 
		(members-all-properp biglst2)  )
	(members-all-properp (append biglst1 biglst2) ) ) )

(prove-lemma cons-all-preserves-members-all-properp (rewrite) (implies
	(members-all-properp biglst)  
	(members-all-properp (cons-all item biglst)) ))

; of coure, we chould check the defining property:
(prove-lemma members-all-properp-works (rewrite) (implies
	(and
		(member lst biglst)
		(members-all-properp biglst) )
	(properp lst)))

(prove-lemma only-proper-aux1 (rewrite) 
	(members-all-properp (power-set lst)))

(prove-lemma only-proper () (implies
	(member lst (power-set set))
	(properp lst)))

(disable only-proper-aux1)

(defn members-all-sublistp (biglst set) (if (listp biglst)
	(and (sublistp (car biglst) set) (members-all-sublistp (cdr biglst) set))
	T ))

(prove-lemma append-preserves-members-all-sublistp (rewrite) (implies
	(and 
		(members-all-sublistp biglst1 set) 
		(members-all-sublistp biglst2 set)  )
	(members-all-sublistp (append biglst1 biglst2) set ) ) )

(prove-lemma cons-all-preserves-members-all-sublistp (rewrite) (implies
	(members-all-sublistp biglst set)  
	(members-all-sublistp (cons-all item biglst) (cons item set) ) ))

; of coure, we chould check the defining property:
(prove-lemma members-all-sublistp-works (rewrite) (implies
	(and
		(member lst biglst)
		(members-all-sublistp biglst set) )
	(sublistp lst set)))

(prove-lemma only-sublists-aux1 (rewrite) 
	(members-all-sublistp (power-set set) set) )

(prove-lemma only-sublists (rewrite) (implies
	(member lst (power-set set))
	(sublistp lst set)))

; also, we get all sublists

(prove-lemma all-sublists (rewrite) (implies
	(and (sublistp lst set) (properp lst))
	(member lst (power-set set))))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;                           STANDARD SETS                                ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; These standard lists of numbers in strictly increasing order.

(defn setp (s) (if (listp s)
	; if it's a list (i.e., a cons) :
	(and 
		(numberp (car s))
		(setp (cdr s))
		(or
			(equal (cdr s) nil)
			(lessp (car s) (cadr s)) ))  ; increasing order
	; if it's not a cons, it must be the empty list, not some other atom
	(equal s nil)  ))


;;;;; large, in Paris-Harrington sense:
(defn largep (set) (and
	(setp set) (listp set)
	(not (lessp (length set) (car set)))))

(prove-lemma empty-is-nil (rewrite) (implies
	(and (setp s) (not (listp s)))
	(equal (equal s nil) T)))
	; so it can be a rewrite rule -- can't rewrite a var

(prove-lemma increasing (rewrite) (implies
	(and (setp s) (member x (cdr s)))
	(lessp (car s) x)))

; Since the order is increasing, the members don't occur twice
(prove-lemma not-again (rewrite) (implies 
	(setp s)
	(not (member (car s) (cdr s)))))

; the min of a set is its first element
(prove-lemma min-is-first (rewrite) (implies
	(and (setp s) (lessp x (car s)))
	(not (member x s))))
	
; the max of a set is its last element

(defn last (set) (if (listp set)
	(if (listp (cdr set)) 
		(last (cdr set))
		(car set) )
	0 ; really, undefined in this case, but the max of emptyset is 0
))

; the tail of a set is a set
(prove-lemma tail-of-a-set (rewrite) (implies
	(and (setp s) (listp s))
	(setp (cdr s))))
; this is useful in inductive proofs about sets


(prove-lemma first-before-last (rewrite) (implies
	(and (setp s) (listp (cdr s)))
	(lessp (car s) (last s))))


(prove-lemma max-is-last (rewrite) (implies
	(and (setp s) (lessp (last s) x ))
	(not (member x s)))
( ; hints
(disable min-is-first)
))

; sets are proper lists:
(prove-lemma sets-are-proper (rewrite)
	(implies (setp s) (properp s)))

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

(prove-lemma compare-first-elts (rewrite) (implies
	(and (setp s1) (setp s2) (listp s1) (subsetp s1 s2))
	(not (lessp (car s1) (car s2))) )   
( ; hints -- reason -- (car s1) is a member of s2
(do-not-induct T)
(use 
	(car-of-subset (s1 s1) (s2 s2))
	(min-is-first (x (car s1)) (s s2) ) )
(disable car-of-subset min-is-first setp)
))

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

(prove-lemma smaller-cars-in-subset (rewrite) (implies
	(and (setp s1) (setp s2) (listp s1) (subsetp s1 s2)
		(lessp (car s2) (car s1)) )
	(subsetp s1 (cdr s2)))
( ; hints -- reason -- (car s2) is not a member of s1
(do-not-induct T)
(use
	(subset-of-cdr (s1 s1) (s2 s2)) )
(disable subset-of-cdr)
))

(prove-lemma same-cars-in-subset-aux1 (rewrite) (implies
	(and (setp s1)  (listp s1) (listp (cdr s1)))
	(lessp (car s1) (cadr s1)) ))

(prove-lemma same-cars-in-subset-aux2 (rewrite) (implies
	(and (setp s1) (setp s2) (listp s1) (subsetp s1 s2)
		(listp (cdr s1))
		(equal (car s2) (car s1)) )
	(subsetp (cdr s1) (cdr s2))  )   
(; hints -- reason -- apply previous lemma to (cdr s1) s2
(use 
	(smaller-cars-in-subset (s1 (cdr s1)) (s2 s2))
	(same-cars-in-subset-aux1 (s1 s1)))
(do-not-induct T)
(disable smaller-cars-in-subset same-cars-in-subset-aux1 min-is-first
	not-again)
))

(prove-lemma same-cars-in-subset (rewrite) (implies
	(and (setp s1) (setp s2) (listp s1) (subsetp s1 s2)
		(equal (car s2) (car s1)) )
	(subsetp (cdr s1) (cdr s2))) 
(; hints -- reason -- apply previous lemma to (cdr s1) s2
(do-not-induct T)
(use (same-cars-in-subset-aux2 (s1 s1) (s2 s2)))
(disable same-cars-in-subset-aux2 not-again)
))

(disable same-cars-in-subset-aux1)
(disable same-cars-in-subset-aux2)

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

(defn bad-for-subset-implies-sublist (set1 set2) (and
	(subsetp set1 set2)
	(setp set1) (setp set2)
	(not (sublistp set1 set2)) )) 

(prove-lemma subset-implies-sublist-aux1 (rewrite) (implies
	(not (listp set1))
	(not (bad-for-subset-implies-sublist set1 set2)) ))

(prove-lemma subset-implies-sublist-aux2 (rewrite) (implies
	(not (listp set2))
	(not (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

(prove-lemma subset-implies-sublist-aux3 (rewrite) (implies
	(and
		(listp set1) (listp set2)
		(equal (car set2) (car set1))
		(sublistp (cdr set1) (cdr set2)))
	(sublistp set1 set2)  ))

(prove-lemma subset-implies-sublist-aux4 (rewrite) (implies
	(and
		(listp set1) (listp set2)
		(equal (car set2) (car set1))
		(bad-for-subset-implies-sublist set1 set2)  )
	(bad-for-subset-implies-sublist (cdr set1) (cdr set2))  )  
( ; hints
(do-not-induct T)
(disable subset-implies-sublist-aux1  subset-implies-sublist-aux2
	sublistp  empty-is-nil nil-is-subset power-set non-empty-subset )
))

(prove-lemma subset-implies-sublist-aux5 (rewrite) (implies
	(and
		(listp set1) (listp set2)
		(lessp (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)
(prove-lemma subset-implies-sublist-aux6 (rewrite) (implies
	(and
		(listp set1) (listp set2)
		(bad-for-subset-implies-sublist set1 set2)  )
	(or
		(lessp (car set2) (car set1))
		(equal (car set2) (car set1)) ) ))

(prove-lemma subset-implies-sublist-aux7 (rewrite) (implies
	(and
		(listp set1) (listp set2)
		(bad-for-subset-implies-sublist set1 set2)  )
	(or
		(bad-for-subset-implies-sublist  set1 (cdr set2))
		(bad-for-subset-implies-sublist  (cdr set1) (cdr set2))  )  )
( ; hints
(do-not-induct T)
(use (subset-implies-sublist-aux6 (set1 set1) (set2 set2) ))
(disable subset-implies-sublist-aux6 bad-for-subset-implies-sublist)
))

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

(defn subset-implies-sublist-kludge (set1 set2) (if (listp set1)
	(if (listp set2)
		(plus
			(subset-implies-sublist-kludge (cdr set1) (cdr set2))
			(subset-implies-sublist-kludge  set1 (cdr set2)) )
		0 )
	0 ))

(prove-lemma subset-implies-sublist-aux8 (rewrite) 
	(not (bad-for-subset-implies-sublist set1 set2)  )  
( ; hints
(induct (subset-implies-sublist-kludge set1 set2))
(use (subset-implies-sublist-aux7 (set1 set1) (set2 set2)))
(disable bad-for-subset-implies-sublist subset-implies-sublist-aux7)
))

(disable subset-implies-sublist-kludge)
(disable subset-implies-sublist-aux1)
(disable subset-implies-sublist-aux2)
(disable subset-implies-sublist-aux3)
(disable subset-implies-sublist-aux4)
(disable subset-implies-sublist-aux5)
(disable subset-implies-sublist-aux6)
(disable subset-implies-sublist-aux7)

(prove-lemma subset-implies-sublist () (implies
	(and
		(subsetp set1 set2)
		(setp set1) (setp set2) )
	(sublistp set1 set2)  )
( ; hints
(use (subset-implies-sublist-aux8 (set1 set1) (set2 set2)))
(disable subset-implies-sublist-aux8 )
)) 

(disable subset-implies-sublist-aux8)
(disable bad-for-subset-implies-sublist)

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

(prove-lemma all-subsets (rewrite) (implies
	(and (setp set) (setp x) (subsetp x set))
	(member x (power-set set)) )
(; hints
(do-not-induct T)
(use 
	(subset-implies-sublist (set1 x) (set2 set))
	(all-sublists (lst x) (set set) ) )
(disable subset-implies-sublist all-sublists transitivity-of-subset)
))


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

(defn bad-for-ext (s1 s2) (and
	(setp s1) (setp s2) (subsetp s1 s2) (subsetp s2 s1) (not (equal s1 s2))))

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

(prove-lemma extensionality-aux1 (rewrite) (implies
	(not (listp s1)) (not (bad-for-ext s1 s2))))

(prove-lemma extensionality-aux2 (rewrite) (implies
	(not (listp s2)) (not (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.

(prove-lemma extensionality-aux3 (rewrite) (implies
	(and 
		(setp s1) (setp s2) (listp s1) (listp s2)
		(subsetp s1 s2) (subsetp s2 s1))
	(equal (car s1) (car s2) ) ) 
( ; hints
(do-not-induct T)
(use 
	( compare-first-elts (s1 s1) (s2 s2) )
	( compare-first-elts (s1 s2) (s2 s1) ) )
(disable compare-first-elts)
))

(prove-lemma extensionality-aux4 (rewrite) (implies
	(and 
		(listp s1) (listp s2) (bad-for-ext s1 s2))
	(equal (car s1) (car s2) ) ) 
( ; hints
(do-not-induct T)
(use 
	(extensionality-aux3 (s1 s1) (s2 s2) ) )
(disable extensionality-aux3)
))

(disable extensionality-aux3)

; now, we should get that the cdrs are bad

(prove-lemma extensionality-aux5 (rewrite) (implies
	(and 
		(listp s1) (listp s2) (bad-for-ext s1 s2))
	(bad-for-ext (cdr s1) (cdr s2))   ) 
( ; hints
(use 
	(extensionality-aux4 (s1 s1) (s2 s2))
	(same-cars-in-subset (s1 s1) (s2 s2))
	(same-cars-in-subset (s1 s2) (s2 s1)) )
(disable 
	extensionality-aux4 same-cars-in-subset transitivity-of-subset
	setp not-again min-is-first max-is-last member subsetp )
))

(disable extensionality-aux4)

(defn extensionality-kludge (s1 s2) (if (not (listp s1))
	0 
	(if (not (listp s2)) 
		0
		(extensionality-kludge (cdr s1) (cdr s2)))))

(prove-lemma extensionality-aux6 (rewrite) 
	(not (bad-for-ext s1 s2))
; hints
(
	(induct (extensionality-kludge s1 s2))
	(disable bad-for-ext)
))

(disable extensionality-aux1)
(disable extensionality-aux2)
(disable extensionality-aux5)
(disable extensionality-aux6)

(prove-lemma extensionality () (implies
	(and (setp s1) (setp s2) (subsetp s1 s2) (subsetp s2 s1))
	(equal s1 s2) )   
; hints
(
	(do-not-induct T)
	(use (extensionality-aux6 (s1 s1) (s2 s2)))
))

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

(defn segment (m n) (if 
	(and (leq m n) (numberp m) (numberp n))
		(cons m (segment (add1 m) n))
		nil  )
( ; hints
(lessp (difference  (add1 n) m))
))

(prove-lemma size-of-segment (rewrite) (implies
	(and (leq m n) (numberp m) (numberp n))
	(equal (length (segment m n)) (difference (add1 n) m)) ))

(prove-lemma members-of-segment (rewrite) (implies
	(and (leq m n) (numberp m) (numberp n)) 
	(equal
		(member x (segment m n))
		(and (numberp x) (leq x n) (leq m x))) )
( ; hints
(induct (segment m n))  ; about twice as fast this way
))

(disable segment)   ; for now


; some lemmas about length:

(prove-lemma length-of-sublist (rewrite) (implies
	(sublistp lst1 lst2)
	(not (lessp (length lst2) (length lst1))))
( ; hints
(disable subsetp setp)
))

(prove-lemma length-of-subset (rewrite) (implies
	(and
		(setp X) (setp Y) (subsetp X Y))
	(not (lessp (length Y) (length X))))
( ; hints
(do-not-induct T)
(use 
	(length-of-sublist (lst1 X) (lst2 Y))
	(subset-implies-sublist (set1 X) (set2 Y)))
))


; a few more set facts

(prove-lemma empty-subset(rewrite) (implies
	(not (listp s1))
	(subsetp s1 s2)) )

(prove-lemma car-before-cadr (rewrite) (implies
	(and (listp (cdr s)) (setp s))
	(lessp (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:

(prove-lemma cdr-cdr-subset-aux1 () (implies
	(and (setp s1) (setp s2) (listp s1) (subsetp s1 s2))
	(or (equal (car s2) (car s1))  (lessp (car s2) (car s1)) )   )
( ; hints
(do-not-induct T)
(use (compare-first-elts (s1 s1) (s2 s2)))
))

(prove-lemma cdr-cdr-subset (rewrite) (implies
	(and (setp s1) (setp s2) (listp s1) (subsetp s1 s2))
	(subsetp (cdr s1) (cdr s2)))
( ; hints
(do-not-induct T)
(use (cdr-cdr-subset-aux1 (s1 s1) (s2 s2)))
(disable subsetp setp)
))

(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
(disable subsetp)
(disable setp)
(disable max-is-last)
(disable tail-of-a-set)
(disable increasing)
(disable compare-first-elts)


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

(prove-lemma irreflex (rewrite) (not (ord-lessp x x)))

(prove-lemma nocycle (rewrite) (not
	(and (ord-lessp x y) (ord-lessp y x))))

(prove-lemma no-cycle-alt (rewrite) (implies
	(ord-lessp y x)
	(not (ord-lessp x y))))

(prove-lemma trichotomy (rewrite) (implies 
	(and (ordinalp sigma) (ordinalp tau))
	(or
		(equal sigma tau)
		(ord-lessp sigma tau)
		(ord-lessp tau sigma) )  ))

(prove-lemma transitivity (rewrite) (implies
	(and 
		(ord-lessp alpha beta)
		(ord-lessp beta gamma))
	(ord-lessp alpha gamma) ))

(prove-lemma transitivity-alt (rewrite) (implies
	(and 
		(ordinalp alpha) (ordinalp beta) (ordinalp gamma)
		(not (ord-lessp beta alpha))  ; alpha <= beta
		(ord-lessp beta gamma))
	(ord-lessp alpha gamma) )
( ; hints
(do-not-induct T)
(use 
	(trichotomy (sigma  alpha) (tau beta)))
(disable trichotomy)
))

(prove-lemma ords-below-2 () (implies
	(and
		(ordinalp alpha)
		(not (ord-lessp 1 alpha)) )
	(or 
		(equal alpha 0) 
		(equal alpha 1)  )) )

(prove-lemma postive-ord-lessp (rewrite) (implies
	(and (ordinalp gamma) (ordinalp delta) (ord-lessp gamma delta))
	(ord-lessp 0 delta)))


;;;;;;;  successors and limit ordinals

(defn successorp (alpha) (if (listp alpha)
	(successorp (cdr alpha))
	(lessp 0 alpha) ))

(defn limitp (alpha) (and 
	(listp alpha) 
	(not (successorp alpha)) ))

(prove-lemma successors-are-positive (rewrite) (implies
	(and (ordinalp alpha) (successorp alpha))
	(ord-lessp 0 alpha)))

(prove-lemma three-kinds (rewrite) (implies
	(ordinalp alpha)
	(or
		(limitp alpha)
		(successorp alpha)
		(equal alpha 0))))

(defn successor (alpha) (if (listp alpha)
	(cons (car alpha) (successor (cdr alpha)))
	(add1 alpha) ))
; the successor of 8 is 9
; the successor of (alpha beta . 8) is (alpha beta . 9)

(prove-lemma successor-is-an-ordinal (rewrite) (implies
	(ordinalp alpha)
	(ordinalp (successor alpha))  ))

(prove-lemma successor-is-a-successor (rewrite) 
	(successorp (successor alpha)))

(prove-lemma successor-is-bigger (rewrite) 
	(ord-lessp alpha (successor alpha)))

(prove-lemma succ-preserves-order (rewrite) (implies
	(ord-lessp alpha beta)
	(ord-lessp (successor alpha) (successor beta)) ))

(prove-lemma nothing-between (rewrite) (not (and
	(ord-lessp alpha beta)
	(ord-lessp beta (successor alpha)) )))

(defn predecessor (alpha) (if (listp alpha)
	(cons (car alpha) (predecessor (cdr alpha)))
	(sub1 alpha) ))

; these are inverses of each other

(prove-lemma predecessor-suc (rewrite) (implies
	(ordinalp alpha)
	(equal (predecessor (successor alpha)) alpha)  ))

(prove-lemma suc-predecessor (rewrite) (implies
	(and (ordinalp alpha) (successorp alpha))
	(equal (successor (predecessor alpha)) alpha)  ))

(prove-lemma predecessor-is-an-ordinal (rewrite) (implies
	(ordinalp alpha) 
	(ordinalp (predecessor alpha))  ))

(prove-lemma predecessor-is-smaller (rewrite) (implies
	(and (ordinalp alpha) (successorp alpha))
	(ord-lessp (predecessor alpha) alpha)  ))

(prove-lemma predecessor-of-0 (rewrite) (equal 
	(predecessor 0) 0))

(prove-lemma predecessor-of-limit (rewrite) (implies
	(and (ordinalp alpha) (limitp alpha))
	(equal (predecessor alpha) alpha)  ))


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

(defn ord-leq (alpha beta) (not (ord-lessp beta alpha)))

(prove-lemma leq-as-an-or (rewrite) (implies 
	(and (ordinalp rho) (ordinalp sigma) (ord-leq rho sigma))
	(or (ord-lessp rho sigma) (equal rho sigma)))
; hints
(
(do-not-induct T)
(use (trichotomy (sigma rho) (tau sigma)))
(disable ord-lessp)
))

(prove-lemma leq-0 (rewrite) (implies 
	(and (ordinalp delta) (ord-leq delta 0))
	(equal (equal delta 0) T)))

(prove-lemma cars-go-down (rewrite) (implies
	(ordinalp beta)
	(ord-leq (cadr beta) (car beta))))

(prove-lemma ord-leq-is-transitive (rewrite) (implies
	(and 
		(ordinalp alpha) (ordinalp beta) (ordinalp gamma)
		(ord-leq alpha beta) (ord-leq beta gamma))
	(ord-leq alpha gamma)))

(prove-lemma ord-leq-zero (rewrite) (implies
	(and (ordinalp delta) (ord-leq delta 0))
	(equal (equal delta 0) T) ) )

(prove-lemma cars-are-ordinals (rewrite) (implies
	(ordinalp alpha) 
	(ordinalp (car alpha) )))

(prove-lemma cdrs-are-ordinals (rewrite) (implies
	(ordinalp alpha) 
	(ordinalp (cdr alpha) )))


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

(defn bad-for-cdrs-are-smaller (alpha) (and
	(ordinalp alpha) (listp alpha)
	(not (ord-lessp (cdr alpha) alpha))))

(prove-lemma cdrs-are-smaller-aux1 (rewrite) (implies
	(nlistp alpha)
	(not (bad-for-cdrs-are-smaller alpha))))

(prove-lemma cdrs-are-smaller-aux2 (rewrite) (implies
	(nlistp (cdr alpha))
	(not (bad-for-cdrs-are-smaller alpha))))

(prove-lemma cdrs-are-smaller-aux3 (rewrite) (implies
	(and (ordinalp alpha) (listp (cdr alpha)) 
		(equal (car alpha) (cadr alpha)) 
		(ord-lessp (cddr alpha) (cdr alpha)))
	(ord-lessp (cdr alpha) alpha)))

(prove-lemma cdrs-are-smaller-aux4 (rewrite) (implies
	(and (ordinalp alpha) (listp (cdr alpha)) 
		(ord-lessp (car alpha) (cadr alpha))  )
	(ord-lessp (cdr alpha) alpha)))

(prove-lemma cdrs-are-smaller-aux5 (rewrite) (implies
	(and (ordinalp alpha) (listp (cdr alpha)) )
	(or
		(equal (car alpha) (cadr alpha)) 
		(ord-lessp (cadr alpha) (car alpha)))  )  
( ; hints
(do-not-induct T)
(use (trichotomy (sigma (car alpha)) (tau (cadr alpha)))  )
))

(disable cdrs-are-smaller-aux3)
(disable cdrs-are-smaller-aux4)
(disable cdrs-are-smaller-aux5)

(prove-lemma cdrs-are-smaller-aux6 (rewrite) (implies
	(and (ordinalp alpha) (listp (cdr alpha)) 
		(ord-lessp (cddr alpha) (cdr alpha)))
	(ord-lessp (cdr alpha) alpha))

( ; hints
(do-not-induct T)
(use 
	(cdrs-are-smaller-aux3 (alpha alpha)) 
	(cdrs-are-smaller-aux4 (alpha alpha)) 
	(cdrs-are-smaller-aux5 (alpha alpha)) )
(disable ordinalp listp )
))

(prove-lemma cdrs-are-smaller-aux7 (rewrite) (implies
	(and (listp (cdr alpha)) (bad-for-cdrs-are-smaller alpha))
	(bad-for-cdrs-are-smaller (cdr alpha))))

(disable cdrs-are-smaller-aux2)

(prove-lemma cdrs-are-smaller-aux8 (rewrite) (implies
	(bad-for-cdrs-are-smaller alpha)
	(bad-for-cdrs-are-smaller (cdr alpha)))
( ; hints
(do-not-induct T)
(use 
	(cdrs-are-smaller-aux7 (alpha alpha))
	(cdrs-are-smaller-aux2 (alpha alpha))  )
(disable bad-for-cdrs-are-smaller)
))

(prove-lemma cdrs-are-smaller-aux9 (rewrite) (not
	(bad-for-cdrs-are-smaller  alpha ))
( ; hints
; (induct (cdrs-are-smaller-kludge 	alpha))
(induct (successor alpha))
(disable bad-for-cdrs-are-smaller)
))

(disable cdrs-are-smaller-aux1)
(disable cdrs-are-smaller-aux6)
(disable cdrs-are-smaller-aux7)
(disable cdrs-are-smaller-aux8)
(disable cdrs-are-smaller-aux9)

(prove-lemma cdrs-are-smaller (rewrite) (implies
	(and (ordinalp alpha) (listp alpha))
	(ord-lessp (cdr alpha) alpha))  
( ;hints
(use (cdrs-are-smaller-aux9 (alpha alpha)))
))

(disable bad-for-cdrs-are-smaller)


(prove-lemma cars-of-smaller-ordinals (rewrite) (implies
	(and (ordinalp alpha) (ordinalp beta) (ord-lessp alpha beta))
	(or (ord-lessp (car alpha) (car beta) ) (equal (car alpha) (car beta)))))

(prove-lemma limit-not-succ (rewrite) (implies
	(and
		(ordinalp alpha) (ordinalp delta)
		(limitp alpha))
	(not (equal (successor delta) alpha) )  ))

(prove-lemma succ-below-limit (rewrite) (implies
	(and
		(ordinalp alpha) (ordinalp delta)
		(ord-lessp delta alpha)
		(limitp alpha))
	(ord-lessp (successor delta) alpha) )   
( ; hints
(do-not-induct T)
(use 
	(nothing-between (alpha delta) (beta alpha))
	(trichotomy (sigma alpha) (tau (successor delta)))  )
))


(prove-lemma irreflex-of-ord-leq (rewrite) (implies
	(and (ordinalp sigma) (ordinalp tau)
		(ord-leq sigma tau) (ord-leq tau sigma))
	(equal (equal sigma tau) T))
( ; hints
(do-not-induct T)
(use (trichotomy (sigma sigma) (tau tau)))
(disable transitivity-alt no-cycle-alt ord-leq-zero)
))

(prove-lemma transitivity-alt2 () (implies
	(and
		(ordinalp alpha) (ordinalp beta) (ordinalp gamma)
		(ord-lessp alpha beta) (ord-leq beta gamma))
	(ord-lessp alpha gamma) )
( ; hints
(do-not-induct T)
(use (trichotomy (sigma beta) (tau gamma)))
(disable irreflex-of-ord-leq transitivity-alt no-cycle-alt ord-leq-zero)
))


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

(defn number-part (alpha) (if (nlistp alpha)
	alpha
	(number-part (cdr alpha))))

(prove-lemma number-part-is-a-number (rewrite) (implies
	(ordinalp alpha)
	(numberp (number-part alpha))  ))

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

(defn pos-mult (delta alpha) (if (nlistp alpha)
	0
	(if (equal delta (car alpha))
		(add1 (pos-mult delta (cdr alpha)))
		(pos-mult delta (cdr alpha))  )  ))

(prove-lemma pos-mult-is-a-number (rewrite) 
	(numberp (pos-mult delta alpha)))

(defn mult (delta alpha) (if (equal delta 0)
	(number-part alpha) 
	(pos-mult delta alpha)))

(prove-lemma mult-is-a-number (rewrite) (implies
	(ordinalp alpha)
	(numberp (mult delta alpha))  ))

(prove-lemma mult-in-a-number (rewrite) (implies
	(and (numberp alpha) (not (equal delta 0)))
	(equal (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

(defn bad-for-bound-on-mult (delta alpha) (and
	(ordinalp alpha) (ordinalp delta) (ord-lessp (car alpha) delta)
	(not (equal (mult delta alpha) 0)) ))

; we want to show this can't happen

(prove-lemma bound-on-mult-aux1 (rewrite) (implies
	(nlistp alpha)
	(not (bad-for-bound-on-mult delta alpha)))  )

(prove-lemma bound-on-mult-aux2 (rewrite) (implies
	(and (listp alpha) (ordinalp alpha))
	(not (ord-lessp (car alpha) (cadr alpha))) ))

(prove-lemma bound-on-mult-aux3 (rewrite) (implies
	(ordinalp alpha) (ordinalp (car alpha))))

(prove-lemma bound-on-mult-aux4 (rewrite) (implies
	(ordinalp alpha) (ordinalp (cadr alpha))))

(prove-lemma bound-on-mult-aux5 (rewrite) (implies
	(and (listp alpha) (ordinalp alpha) (ordinalp delta)
		(ord-lessp (car alpha) delta))
	(ord-lessp (cadr alpha) delta)) 
( ; hints
(do-not-induct T)
(use (transitivity-alt (alpha (cadr alpha)) (beta (car alpha)) (gamma delta)))
(disable transitivity-alt ordinalp ord-lessp)
))

(prove-lemma bound-on-mult-aux6 (rewrite) (implies
	(and (listp alpha) (bad-for-bound-on-mult delta alpha))
	(bad-for-bound-on-mult delta (cdr alpha)) ) 
( ; hints
(disable ord-leq transitivity-alt no-cycle-alt)
))

(defn bound-on-mult-kludge (alpha) ; force correct induction
	(if (nlistp alpha) 0 (bound-on-mult-kludge (cdr alpha))))

(prove-lemma bound-on-mult-aux7 () (not
	(bad-for-bound-on-mult delta alpha))
( ; hints
(disable bad-for-bound-on-mult)
(induct (bound-on-mult-kludge alpha))
))

(prove-lemma bound-on-mult (rewrite) (implies
	(and (ordinalp alpha) (ordinalp delta) (ord-lessp (car alpha) delta))
	(equal (mult delta alpha) 0) )
( ;  hint
(use (bound-on-mult-aux7 (delta delta) (alpha alpha)))
(disable ord-leq transitivity-alt)
))

(disable bound-on-mult-aux1)
(disable bound-on-mult-aux2)
(disable bound-on-mult-aux3)
(disable bound-on-mult-aux4)
(disable bound-on-mult-aux5)
(disable bound-on-mult-aux6)
(disable bound-on-mult-aux7)
(disable bad-for-bound-on-mult)
(disable bound-on-mult-kludge)

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

(defn different-mult (alpha beta) (if (equal (car alpha) (car beta))
	; if the cars are the same, consider two cases:
	; note that for ordinals, alpha is compound iff beta is
	(if (listp alpha)
		(different-mult (cdr alpha) (cdr beta))
		0 )   ; for numbers, return 0
	; if the cars are different, return the larger one
	(if (ord-lessp (car alpha) (car beta))
		(car beta)
		(car alpha) )  ) )

; summarize the features of the definition

(prove-lemma different-mult-is-ord (rewrite) (implies
	(and (ordinalp alpha) (ordinalp beta))
	(ordinalp (different-mult alpha beta)))
( ; hints
(induct (different-mult alpha beta))
(disable ordinalp ord-lessp)
))

(prove-lemma different-mult-for-numbers (rewrite) (implies
	(and (numberp alpha) (numberp beta))
	(equal (different-mult alpha beta) 0)))

;;;;;;;;;;  The following is causing us a lot of trouble:
(disable transitivity-alt)
(disable irreflex-of-ord-leq)

(prove-lemma different-mult-number-list (rewrite) (implies
	(and (numberp alpha) (ordinalp beta) (listp beta))
	(equal (different-mult alpha beta) (car beta))))

(prove-lemma different-mult-list-number (rewrite) (implies
	(and (numberp beta) (ordinalp alpha) (listp alpha))
	(equal (different-mult alpha beta) (car alpha))))

(prove-lemma different-mult-for-lists-same-car (rewrite) (implies
	(and (ordinalp alpha) (ordinalp beta) 
		(listp alpha) (listp beta)
		(equal (car alpha) (car beta)))
	(equal 
		(different-mult alpha beta)
		(different-mult (cdr alpha) (cdr beta))) )
( ; hints
(disable ord-leq no-cycle-alt)
))

(prove-lemma different-mult-for-smaller-car (rewrite) (implies
	(ord-lessp (car alpha) (car beta))
	(equal 
		(different-mult alpha beta)
		(car beta)) ))

(prove-lemma different-mult-for-larger-car (rewrite) (implies
	(ord-lessp (car beta) (car alpha))
	(equal 
		(different-mult alpha beta)
		(car alpha)) ))

(disable different-mult)

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

(defn bad-for-different-mult-works (alpha beta) (and
	(ordinalp alpha) (ordinalp beta) (not (equal alpha beta))
	(equal
		(mult (different-mult alpha beta) alpha)
		(mult (different-mult alpha beta) beta) ) ))

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

(prove-lemma different-mult-works-aux1 (rewrite) (implies
	(and (ordinalp sigma)  (not (equal (car sigma) 0)))
	(not (equal (mult (car sigma) sigma) 0) ) ))

; the following is causing us a lot of trouble
(disable no-cycle-alt)
(disable ord-leq-is-transitive)


(prove-lemma different-mult-works-aux2 (rewrite) (implies
	(ord-lessp (car alpha) (car beta))
	(not (bad-for-different-mult-works alpha beta)))
( ; hints
(do-not-induct T)
(use 
	(different-mult-works-aux1 (sigma beta))
	(bound-on-mult (alpha alpha) (delta (car beta))))
(disable ord-leq different-mult-works-aux1 bound-on-mult)
))

(prove-lemma different-mult-works-aux3 (rewrite) (implies
	(ord-lessp (car beta) (car alpha))
	(not (bad-for-different-mult-works alpha beta)))
( ; hints
(do-not-induct T)
(use 
	(different-mult-works-aux1 (sigma alpha))
	(bound-on-mult (alpha beta) (delta (car alpha))))
(disable different-mult-works-aux1 bound-on-mult)
))

(prove-lemma different-mult-works-aux4 (rewrite) (implies
	(and (numberp alpha) (numberp beta))
	(not (bad-for-different-mult-works alpha beta)) ))

(prove-lemma different-mult-works-aux5 (rewrite) (implies
	(and (numberp alpha) (ordinalp beta) (listp beta))
	(ord-lessp (car alpha) (car beta))))

(prove-lemma different-mult-works-aux6 (rewrite) (implies
	(and (nlistp alpha)  (listp beta))
	(not (bad-for-different-mult-works alpha beta)) ))

(prove-lemma different-mult-works-aux7 (rewrite) (implies
	(and (listp alpha)  (nlistp beta))
	(not (bad-for-different-mult-works alpha beta)) ))

(prove-lemma different-mult-works-aux8 (rewrite) (implies
	(and (nlistp alpha)  (nlistp beta))
	(not (bad-for-different-mult-works alpha beta)) ))

(disable different-mult-works-aux4 )
(disable different-mult-works-aux5 )
(disable different-mult-works-aux6 )
(disable different-mult-works-aux7 )
(disable different-mult-works-aux8 )

(prove-lemma different-mult-works-aux9 (rewrite) (implies
	(or (nlistp alpha)  (nlistp beta))
	(not (bad-for-different-mult-works alpha beta)) )
( ; hints
(disable bad-for-different-mult-works)
(use
	(different-mult-works-aux6 (alpha alpha) (beta beta))
	(different-mult-works-aux7 (alpha alpha) (beta beta))
	(different-mult-works-aux8 (alpha alpha) (beta beta)) )
))

; so, they are both compound

(disable different-mult-works-aux1 )
(disable different-mult-works-aux2 )
(disable different-mult-works-aux3 )

(prove-lemma different-mult-works-aux10 (rewrite) (implies
	(not (equal (car beta) (car alpha)))
	(not (bad-for-different-mult-works alpha beta)))
( ; hints
(use 
	(trichotomy (sigma (car alpha)) (tau (car beta)))
	(different-mult-works-aux2 (alpha alpha) (beta beta))
	(different-mult-works-aux3 (alpha alpha) (beta beta)) )
(disable  different-mult-works-aux9)
))


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

(prove-lemma same-mult-for-cdr (rewrite) (implies
	(and 
		(listp alpha) (listp beta) (equal (car alpha) (car beta))
		(equal (mult delta alpha) (mult delta beta)) )
	(equal (mult delta (cdr alpha)) (mult delta (cdr beta)) )  ))

(prove-lemma different-mult-works-aux11 (rewrite) (implies
	(and 
		(listp alpha) (listp beta) (equal (car alpha) (car beta))
		(bad-for-different-mult-works alpha beta) )
	(bad-for-different-mult-works (cdr alpha) (cdr beta)) )
( ;  hints
(use 
	(same-mult-for-cdr (alpha alpha) (beta beta) (delta
			(different-mult alpha beta))) )
(disable mult ordinalp ord-lessp same-mult-for-cdr)
))

(disable different-mult-works-aux10)

(prove-lemma different-mult-works-aux12 (rewrite) (implies
	(and 
		(listp alpha) (listp beta) 
		(bad-for-different-mult-works alpha beta) )
	(bad-for-different-mult-works (cdr alpha) (cdr beta)) ) 
( ; hints
(do-not-induct T)
(disable bad-for-different-mult-works)
(use (different-mult-works-aux10 (alpha alpha) (beta beta)))
))

(defn different-mult-works-kludge (alpha beta) (if
	(and (listp alpha) (listp beta))
	(different-mult-works-kludge (cdr alpha) (cdr beta))
	0 ))

(prove-lemma different-mult-works-aux13 (rewrite) 
	(not (bad-for-different-mult-works alpha beta))
( ; hints
(induct (different-mult-works-kludge alpha beta))
(disable bad-for-different-mult-works)
))

(disable different-mult-works-kludge)
(disable different-mult-works-aux9)
(disable different-mult-works-aux11)
(disable different-mult-works-aux12)
(disable different-mult-works-aux13)

(prove-lemma different-mult-works (rewrite) (implies
	(and (ordinalp alpha) (ordinalp beta) (not (equal alpha beta)))
	(not (equal
		(mult (different-mult alpha beta) alpha)
		(mult (different-mult alpha beta) beta) )) )
( ; hints
(use (different-mult-works-aux13 (alpha alpha) (beta beta)))
(disable mult)
))

(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

(defn num-sharp (alpha n)  (if (nlistp alpha)
	(plus alpha n)
	(cons (car alpha) (num-sharp (cdr alpha) n))))

(prove-lemma num-sharp-is-an-ordinal (rewrite) (implies
	(and (ordinalp alpha) (numberp n))
	(ordinalp (num-sharp alpha n))))

(prove-lemma num-sharp-and-zero (rewrite) (implies
	(ordinalp alpha)
	(equal (num-sharp alpha 0) alpha)))

(prove-lemma num-sharp-and-successor (rewrite)
	(equal (num-sharp alpha 1) (successor alpha)))

(prove-lemma num-sharp-gets-bigger (rewrite) (implies
	(and (ordinalp alpha) (numberp n) (not (equal n 0)))
	(ord-lessp alpha (num-sharp alpha n))))

(prove-lemma car-of-num-sharp (rewrite) (implies
	(numberp n)
	(equal (car (num-sharp alpha n)) (car alpha))))

(prove-lemma num-sharp-is-monotonic (rewrite) (implies
	(and (ordinalp alpha) (ordinalp beta) (numberp n)
		(ord-lessp alpha beta))
	(ord-lessp (num-sharp alpha n) (num-sharp beta n))))


; check out multiplicities

(prove-lemma number-part-of-num-sharp (rewrite) (equal
	(number-part (num-sharp alpha n))
	(plus (number-part alpha) n )))

(prove-lemma pos-mult-of-num-sharp (rewrite)
	(equal
		(pos-mult delta (num-sharp alpha n))
		(pos-mult delta alpha) )) 

(prove-lemma mult-of-num-sharp (rewrite) (implies
	(and (numberp n) (ordinalp delta) (ordinalp alpha))
	(equal
		(mult delta (num-sharp alpha n))
		(plus
			(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

(defn insert (delta alpha) (if (nlistp alpha)
	(cons delta alpha) 
	(if (ord-lessp delta (car alpha))
		(cons (car alpha) (insert delta (cdr alpha)))
		(cons delta alpha))))

; the car is the larger of the two cars

(prove-lemma car-of-insert-A (rewrite) (implies
	(and (ord-lessp delta (car alpha)) (ordinalp alpha))
	(equal (car (insert delta alpha)) (car alpha))))

(prove-lemma car-of-insert-B (rewrite) (implies
	(not (ord-lessp delta (car alpha))) 
	(equal (car (insert delta alpha)) delta)))


(prove-lemma insert-is-an-ordinal (rewrite) (implies
	(and (ordinalp alpha) (ordinalp delta) (not (equal delta 0)))
	(ordinalp (insert delta alpha)))
(  ; hints
(induct (insert delta alpha))
(enable no-cycle-alt)
(disable ord-leq-zero leq-0 ord-leq transitivity 
	car-of-insert-A car-of-insert-B)
))


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

(prove-lemma insert-is-cons (rewrite) (implies
	(and (ordinalp alpha) (ordinalp delta)  (not (equal delta 0))
		(not (ord-lessp delta (car alpha))))
	(equal
		(insert delta alpha)
		(cons delta alpha))))

(prove-lemma insert-is-bigger-aux1 (rewrite) (implies
	(and (ordinalp alpha) (ordinalp delta) (not (equal delta 0))
		(listp alpha) (not (ord-lessp delta (car alpha))))
	(ord-lessp alpha (insert delta alpha)) )
( ;  hints
(use (trichotomy (sigma delta) (tau (car alpha))))
(disable trichotomy)
))

(defn bad-for-insert-is-bigger (alpha delta) (and
	(ordinalp alpha) (ordinalp delta) (not (equal delta 0))
	(not (ord-lessp alpha (insert delta alpha)))))

(prove-lemma insert-is-bigger-aux2 (rewrite) (implies
	(nlistp alpha)
	(not (bad-for-insert-is-bigger alpha delta)) ))

(prove-lemma insert-is-bigger-aux3 (rewrite) (implies
	(and (listp alpha) (not (ord-lessp delta (car alpha))))
	(not (bad-for-insert-is-bigger alpha delta)) )
( ;  hints
(use (insert-is-bigger-aux1  (alpha alpha) (delta delta)))
(disable insert-is-bigger-aux1 )
(do-not-induct T)
) )

(prove-lemma insert-small-ordinal (rewrite) (implies
	(and (ordinalp alpha)  (listp alpha) 
		(ord-lessp delta (car alpha)))
	(equal
		(insert delta alpha)
		(cons (car alpha) (insert delta (cdr alpha))))))

(prove-lemma insert-is-bigger-aux4 (rewrite) (implies
	(and (ordinalp alpha)  (listp alpha) 
		(ord-lessp delta (car alpha))
		(ord-lessp (cdr alpha) (insert delta (cdr alpha))) )
	(ord-lessp alpha (insert delta alpha)))
(; hints
(use (insert-small-ordinal (alpha alpha) (delta delta)))
(disable ordinalp insert insert-small-ordinal)
))

(prove-lemma insert-is-bigger-aux5 (rewrite) (implies
	(and (listp alpha)  (ord-lessp delta (car alpha))
		(bad-for-insert-is-bigger alpha delta)  ) 
	(bad-for-insert-is-bigger (cdr alpha)  delta)) 
( ;  hints
(do-not-induct T)
(use (insert-is-bigger-aux4 (alpha alpha) (delta delta)))
(disable ordinalp ord-lessp insert-is-bigger-aux4 insert-small-ordinal insert)
))

(prove-lemma insert-is-bigger-aux6 (rewrite) (implies
	(and (listp alpha)  
		(bad-for-insert-is-bigger alpha delta)  ) 
	(bad-for-insert-is-bigger (cdr alpha)  delta)) 
( ;  hints
(do-not-induct T)
(use (insert-is-bigger-aux5 (alpha alpha) (delta delta)))
(disable bad-for-insert-is-bigger
ordinalp ord-lessp insert-is-bigger-aux5 insert-small-ordinal insert)
))

(prove-lemma insert-is-bigger-aux7 (rewrite) 
	(not (bad-for-insert-is-bigger alpha delta))
( ; hints
(induct (successor alpha))
(disable bad-for-insert-is-bigger)
))

(prove-lemma insert-is-bigger (rewrite) (implies
	(and (ordinalp alpha) (ordinalp delta) (not (equal delta 0)))
	(ord-lessp alpha (insert delta alpha)))
( ; hints
(do-not-induct T)
(use (insert-is-bigger-aux7 (alpha alpha) (delta delta)))
(disable insert-is-bigger-aux7)
))

(disable insert-is-bigger-aux1)
(disable insert-is-bigger-aux2)
(disable insert-is-bigger-aux3)
(disable insert-is-bigger-aux4)
(disable insert-is-bigger-aux5)
(disable insert-is-bigger-aux6)
(disable insert-is-bigger-aux7)


;;;; now --  check out multiplicities

(prove-lemma number-part-of-insert (rewrite) (equal
	(number-part (insert delta alpha))
	(number-part alpha)))

(prove-lemma pos-mult-same (rewrite) (equal
	(pos-mult delta (insert delta alpha))
	(add1 (pos-mult delta alpha))))

(prove-lemma pos-mult-different (rewrite)  (implies
	(not (equal x delta))
	(equal
		(pos-mult x (insert delta alpha))
		(pos-mult x alpha))))

(prove-lemma mult-of-insert-A (rewrite) (implies 
	(and (ordinalp alpha) (not (equal sigma delta)))
	(equal
		(mult sigma (insert delta alpha))
		(mult sigma alpha))))

(prove-lemma mult-of-insert-B (rewrite) (implies 
	(and (ordinalp alpha) (not (equal delta 0)))
	(equal
		(mult delta (insert delta alpha))
		(add1 (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.

(defn sharp (alpha beta) (if (nlistp beta)
	(num-sharp alpha beta)
	(insert (car beta) (sharp alpha (cdr beta)))))

(prove-lemma sharp-is-an-ordinal (rewrite) (implies
	(and (ordinalp alpha) (ordinalp beta))
	(ordinalp (sharp alpha beta))))

(prove-lemma sharp-with-0 (rewrite) (implies
	(ordinalp alpha)
	(equal (sharp alpha 0) alpha)))

(prove-lemma sharp-gets-bigger (rewrite) (implies
	(and (ordinalp alpha) (ordinalp beta) (not (equal beta 0)))
	(ord-lessp alpha (sharp alpha beta)))
( ; hints
(induct (successor beta)) ; i.e., go down cdrs, not cars
(disable num-sharp insert)
))


; 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

(prove-lemma car-of-insert-aux1 (rewrite) (implies
	(and (equal delta (car alpha)) (ordinalp alpha) (ordinalp delta))
	(equal (car (insert delta alpha)) (car alpha))))

(prove-lemma car-of-insert-C (rewrite) (implies
	(and (ord-leq delta (car alpha)) (ordinalp alpha) (ordinalp delta))
	(equal (car (insert delta alpha)) (car alpha)))
( ; hints
(do-not-induct T)
(use (leq-as-an-or (rho delta) (sigma (car alpha))))
(disable ord-leq ordinalp leq-as-an-or)
))

(prove-lemma car-of-sharp-aux1 (rewrite) (implies
	(and (not (listp beta))
		(ordinalp alpha) (ordinalp beta))
	(equal (car (sharp alpha beta)) (car alpha)))
(; hints
(induct (successor beta))
(disable ordinalp ord-leq)
))

(prove-lemma car-of-sharp-aux2 (rewrite) (implies
	(and (ord-leq (car beta) (car alpha)) 
		(ordinalp alpha) (ordinalp beta))
	(ord-leq (cadr beta) (car alpha)) )
(; hints
(do-not-induct T)
(use
	(ord-leq-is-transitive 
		(alpha (cadr beta)) (beta (car beta)) (gamma (car alpha)))
	(cars-go-down (beta beta)))
(disable ordinalp ord-leq cars-go-down ord-leq-is-transitive)
))

(prove-lemma car-of-sharp-A (rewrite) (implies
	(and (ord-leq (car beta) (car alpha)) 
		(ordinalp alpha) (ordinalp beta))
	(equal (car (sharp alpha beta)) (car alpha)))
(; hints
(induct (successor beta))
(disable ordinalp ord-leq)
))

(disable car-of-sharp-aux1)
(disable car-of-sharp-aux2)

; now, check out that multiplicities are additive

(defn bad-for-mult-of-sharp (sigma alpha beta) (and
	(ordinalp sigma) (ordinalp alpha) (ordinalp beta)
	(not (equal
		(mult sigma (sharp alpha beta))
		(plus (mult sigma alpha) (mult sigma beta)))) ))

(prove-lemma mult-of-sharp-aux1 (rewrite) (implies
	(nlistp beta)
	(not (bad-for-mult-of-sharp sigma alpha beta))))

(prove-lemma mult-of-sharp-aux2 (rewrite) (implies
	(and (listp beta) (ordinalp beta))
	(not (equal (car beta) 0))))

(prove-lemma mult-of-sharp-aux3 (rewrite) (implies
	(and (listp beta) (not (equal sigma (car beta)))
		(ordinalp sigma) (ordinalp alpha) (ordinalp beta))
	(equal 
		(mult sigma (sharp alpha (cdr beta)))
		(mult sigma (sharp alpha beta)) ))
( ;  hints
(do-not-induct T)
(use
	(mult-of-insert-A (sigma sigma) (alpha (sharp alpha (cdr beta))) 
		(delta (car beta))) )
(disable  same-mult-for-cdr  mult-of-insert-A mult-of-insert-B
	ordinalp ord-leq mult insert)
))

(prove-lemma mult-of-sharp-aux4 (rewrite) (implies
	(and (listp beta) (not (equal sigma (car beta))))
	(equal 
		(mult sigma (cdr beta))
		(mult sigma beta)))
( ; hints
(disable bound-on-mult same-mult-for-cdr)
))

(prove-lemma mult-of-sharp-aux5 (rewrite) (implies
	(and (listp beta) (bad-for-mult-of-sharp sigma alpha beta)
		(not (equal sigma (car beta))))
	(bad-for-mult-of-sharp sigma alpha (cdr beta))  ) 
( ; hints
(do-not-induct T)
(disable ordinalp sharp car-of-sharp-A)
))

(prove-lemma mult-of-sharp-aux6 (rewrite) (implies
	(and (listp beta) (ordinalp beta))
	(equal 
		(mult (car beta)  beta)
		(add1 (mult (car beta) (cdr beta)))))
( ; hints
(disable ordinalp bound-on-mult same-mult-for-cdr)
))

(prove-lemma mult-of-sharp-aux7 (rewrite) (implies
	(and (listp beta) (bad-for-mult-of-sharp (car beta) alpha beta))
	(bad-for-mult-of-sharp (car beta) alpha (cdr beta))  ) 
( ; hints
(do-not-induct T)
(disable same-mult-for-cdr mult-of-sharp-aux5 bound-on-mult
	ordinalp car-of-sharp-A)
))

(prove-lemma mult-of-sharp-aux8 (rewrite) (implies
	(and (listp beta) (bad-for-mult-of-sharp sigma alpha beta))
	(bad-for-mult-of-sharp sigma alpha (cdr beta))  ) 
( ; hints
(do-not-induct T)
(use
	(mult-of-sharp-aux7 (alpha alpha) (beta beta) )
	(mult-of-sharp-aux5 (alpha alpha) (beta beta) (sigma sigma)) )
(disable  bad-for-mult-of-sharp mult-of-sharp-aux5 mult-of-sharp-aux7)
))

(prove-lemma mult-of-sharp-aux9 (rewrite) 
	(not (bad-for-mult-of-sharp sigma alpha beta))
( ; hints
(disable bad-for-mult-of-sharp)
(induct (sharp alpha beta))))

(prove-lemma mult-of-sharp (rewrite) (implies
	(and
		(ordinalp sigma) (ordinalp alpha) (ordinalp beta))
	(equal
		(mult sigma (sharp alpha beta))
		(plus (mult sigma alpha) (mult sigma beta))))
( ; hints
(do-not-induct T)
(use ( mult-of-sharp-aux9 (alpha alpha) (beta beta) (sigma sigma)) )
(disable mult ord-leq ordinalp
	mult-of-sharp-aux2 mult-of-sharp-aux9)
))

(disable bad-for-mult-of-sharp)
(disable mult-of-sharp-aux1)
(disable mult-of-sharp-aux2)
(disable mult-of-sharp-aux3)
(disable mult-of-sharp-aux4)
(disable mult-of-sharp-aux5)
(disable mult-of-sharp-aux6)
(disable mult-of-sharp-aux7)
(disable mult-of-sharp-aux8)
(disable mult-of-sharp-aux9)


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

(prove-lemma commut-of-sharp (rewrite) (implies
	(and (ordinalp alpha) (ordinalp beta))
	(equal (sharp alpha beta) (sharp beta alpha))  )
( ; hints
(do-not-induct T)
(use 
	(different-mult-works 
		(alpha (sharp alpha beta)) (beta (sharp beta alpha)))  )
(disable ord-leq insert sharp ordinalp ord-lessp different-mult-works)
))

(prove-lemma assoc-of-sharp (rewrite) (implies
	(and (ordinalp alpha) (ordinalp beta) (ordinalp gamma))
	(equal 
		(sharp (sharp alpha beta) gamma)
		(sharp alpha (sharp beta gamma)) ) ) 
( ; hints
(do-not-induct T)
(use 
	(different-mult-works 
		(alpha (sharp (sharp alpha beta) gamma) ) 
		(beta (sharp alpha (sharp beta gamma))))  )
(disable ord-leq insert sharp ordinalp ord-lessp different-mult-works)
))

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

(prove-lemma car-of-sharp-B (rewrite) (implies
	(and (ord-leq (car alpha) (car beta)) 
		(ordinalp alpha) (ordinalp beta))
	(equal (car (sharp alpha beta)) (car beta)))
(; hints
(do-not-induct T)
(use 
	(car-of-sharp-A (alpha beta) (beta alpha))
	(commut-of-sharp (alpha alpha) (beta beta)))
(disable sharp ord-leq ordinalp)
))


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

(disable car-of-insert-aux1)

(prove-lemma monotonicity-of-insert-aux1 (rewrite) (implies
	(and 
		(ordinalp alpha) (ordinalp beta) (ordinalp delta)
		(not (ord-lessp delta (car beta)))
		(not (equal delta 0))
		(ord-lessp alpha beta) )
	(ord-lessp (insert delta alpha) (insert delta beta)))
( ; hints
(do-not-induct T)
(use 
	(insert-is-cons (alpha alpha) (delta delta))
	(insert-is-cons (alpha beta) (delta delta)) )
(disable  car-of-insert-A car-of-insert-B car-of-insert-C
	leq-0 insert ord-leq insert-is-cons)
))

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

(prove-lemma monotonicity-of-insert-aux2 (rewrite) (implies
	(and 
		(ordinalp alpha) (ordinalp sigma) (ordinalp delta)
		(ord-lessp delta sigma)
		(ord-lessp (car alpha) sigma )  )
	(ord-lessp (car (insert delta alpha)) sigma))
( ; hints
(do-not-induct T)
(use
	(car-of-insert-B (delta delta) (alpha alpha))
	(car-of-insert-C (delta delta) (alpha alpha)) )
(disable  
	leq-0 ordinalp car-of-insert-B car-of-insert-C)
))

(prove-lemma monotonicity-of-insert-aux3 (rewrite) (implies
	(and 
		(ordinalp alpha) (ordinalp beta) (ordinalp delta)
		(ord-lessp delta (car beta))
		(not (equal delta 0))
		(ord-lessp (car alpha) (car beta) ) )
	(ord-lessp (insert delta alpha) beta ))  
( ; hints
(do-not-induct T)
(disable ord-leq leq-0)
))

(prove-lemma monotonicity-of-insert-aux4 (rewrite) (implies
	(and 
		(ordinalp alpha) (ordinalp beta) (ordinalp delta)
		(ord-lessp delta (car beta))
		(not (equal delta 0))
		(ord-lessp (car alpha) (car beta) )  )
	(ord-lessp (insert delta alpha) (insert delta beta))) 
( ; hints
(do-not-induct T)
(disable ord-leq leq-0)
))

; 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

(defn bad-for-monotonicity-of-insert (alpha beta delta) (and
		(ordinalp alpha) (ordinalp beta) (ordinalp delta)
		(not (equal delta 0))
		(ord-lessp alpha beta) 
		(not (ord-lessp (insert delta alpha) (insert delta beta)))))

(prove-lemma monotonicity-of-insert-aux5 (rewrite) (implies
	(bad-for-monotonicity-of-insert alpha beta delta) 
	(ord-lessp delta (car beta)))
( ; hints
(do-not-induct T)
(disable  insert-is-cons insert
	ordinalp ord-lessp ord-leq leq-0)
))

(prove-lemma monotonicity-of-insert-aux6 (rewrite) (implies
	(bad-for-monotonicity-of-insert alpha beta delta) 
	(not (ord-lessp (car alpha) (car beta) )  ) )
( ; hints
(do-not-induct T)
(use
	(monotonicity-of-insert-aux5 (alpha alpha) (beta beta) (delta delta)))
(disable  insert-is-cons insert monotonicity-of-insert-aux5
	ordinalp ord-lessp ord-leq leq-0)
))

(prove-lemma monotonicity-of-insert-aux7 (rewrite) (implies
	(bad-for-monotonicity-of-insert alpha beta delta) 
	(equal (car alpha) (car beta)   ) )
( ; hints
(do-not-induct T)
(use
	(cars-of-smaller-ordinals (alpha alpha) (beta beta))
	(monotonicity-of-insert-aux6 (alpha alpha) (beta beta) (delta delta)))
(disable  ord-lessp
	insert-is-cons insert monotonicity-of-insert-aux6
	ordinalp ord-leq leq-0)
))

; 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

(prove-lemma monotonicity-of-insert-aux8 (rewrite) (implies
	(bad-for-monotonicity-of-insert alpha beta delta) 
	(and (listp alpha) (listp beta)))
( ; hints
(do-not-induct T)
(use
	(monotonicity-of-insert-aux5 (alpha alpha) (beta beta) (delta delta))
	(monotonicity-of-insert-aux7 (alpha alpha) (beta beta) (delta delta)))
(disable  
	insert-is-cons insert monotonicity-of-insert-aux7 
	bad-for-monotonicity-of-insert
	monotonicity-of-insert-aux5
	ordinalp ord-leq leq-0)
))

(prove-lemma monotonicity-of-insert-aux9 (rewrite) (implies
	(bad-for-monotonicity-of-insert alpha beta delta) 
	(bad-for-monotonicity-of-insert (cdr alpha) (cdr beta) delta) )
( ; hints
(do-not-induct T)
(use
	(insert-is-an-ordinal (delta delta) (alpha (cdr alpha)))
	(insert-is-an-ordinal (delta delta) (alpha (cdr beta)))
	(monotonicity-of-insert-aux5 (alpha alpha) (beta beta) (delta delta))
	(monotonicity-of-insert-aux7 (alpha alpha) (beta beta) (delta delta)))
(disable ordinalp insert  monotonicity-of-insert-aux3 
	monotonicity-of-insert-aux4 car-of-insert-A 
	car-of-insert-C car-of-insert-B
	insert-is-cons monotonicity-of-insert-aux7 monotonicity-of-insert-aux5
	ordinalp ord-leq leq-0)
))

(defn monotonicity-of-insert-kludge (alpha beta) (if
	(and (listp alpha) (listp beta))
	(monotonicity-of-insert-kludge (cdr alpha) (cdr beta))
	0 ))

(prove-lemma monotonicity-of-insert-aux10 (rewrite) (not
	(bad-for-monotonicity-of-insert alpha beta delta))
( ; hints
(disable bad-for-monotonicity-of-insert)
(induct (monotonicity-of-insert-kludge alpha beta)) 
))

(prove-lemma monotonicity-of-insert (rewrite) (implies
	(and 
		(ordinalp alpha) (ordinalp beta) (ordinalp delta)
		(not (equal delta 0))
		(ord-lessp alpha beta) )
	(ord-lessp (insert delta alpha) (insert delta beta)))
( ; hints
(do-not-induct T)
(use (monotonicity-of-insert-aux10 (alpha alpha) (beta beta) (delta delta)))
(disable ordinalp ord-lessp monotonicity-of-insert-aux10)
))

(disable monotonicity-of-insert-aux1)
(disable monotonicity-of-insert-aux2)
(disable monotonicity-of-insert-aux3)
(disable monotonicity-of-insert-aux4)
(disable monotonicity-of-insert-aux5)
(disable monotonicity-of-insert-aux6)
(disable monotonicity-of-insert-aux7)
(disable monotonicity-of-insert-aux8)
(disable monotonicity-of-insert-aux9)
(disable monotonicity-of-insert-aux10)
(disable monotonicity-of-insert-kludge)
(disable bad-for-monotonicity-of-insert)

; now, we can prove monotonicity of sharp

(prove-lemma monotonicity-of-sharp (rewrite) (implies
	(and 
		(ordinalp alpha) (ordinalp beta) (ordinalp lambda)
		(ord-lessp alpha beta) )
	(ord-lessp (sharp alpha lambda) (sharp beta lambda))) 
( ; hints
(induct (sharp alpha lambda))
(disable ord-leq
	insert-is-cons insert-small-ordinal
	leq-0 insert ord-leq)
))


;;;;;;;  disable a bunch of stuff --  these are causing
;;;; a lot of trouble by firing when we don't want them to:
(disable ord-lessp)
(disable ord-leq)
(disable leq-0)



;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;                          NORMS AND PRED                                ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;   norms = count ; 
(defn norm (x) (count x))
; This defn is just so that we can disable norm without disabling count

(prove-lemma norm-is-a-number (rewrite) (numberp (norm x)))

(prove-lemma norm-of-a-number (rewrite) (implies
	(numberp n)
	(equal (norm n) n)))

(prove-lemma norm-of-successor (rewrite) (implies 
	(ordinalp alpha)
	(equal (norm (successor alpha))  (add1 (norm alpha))) ))

(prove-lemma norm-of-predecessor (rewrite) (implies
	(and (ordinalp alpha) (successorp alpha))
	(equal (norm (predecessor alpha)) (sub1 (norm alpha))) )  
( ;  hints
(do-not-induct T)
(use 
	(norm-of-successor (alpha (predecessor alpha))) )
))

(prove-lemma norm-of-cons (rewrite) (implies
	(listp alpha)
	(equal (norm alpha) (add1 (plus 
		(norm (car alpha)) (norm (cdr alpha))  )))))

(prove-lemma norm-non-zero (rewrite) (implies
	(listp alpha)
	(not (equal (norm alpha) 0)))
( ; hints
(use
	(norm-of-cons (alpha alpha))
	(norm-is-a-number (x (car alpha)))
	(norm-is-a-number (x (cdr alpha))) )
(disable norm-of-cons norm-is-a-number )
))

(disable norm)

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

(defn norm-up-to (n) (if (zerop n)
	(list 0)
	(append 
		(segment 0 n)
		(product (norm-up-to (sub1 n)) (norm-up-to (sub1 n)) ) )))

(prove-lemma norm-up-to-big-enuf-aux1 (rewrite) (implies
	(and (ordinalp alpha) (leq (norm alpha) n) (nlistp alpha))
	(member alpha (norm-up-to n))))

; now, we just consider (listp alpha)

(prove-lemma norm-up-to-big-enuf-aux2 (rewrite) (implies
	(and (listp alpha) (leq (norm alpha) n))
	(not (zerop n))) )

(prove-lemma norm-up-to-big-enuf-aux3 (rewrite) (implies
	(and (ordinalp alpha) (leq (norm alpha) n) (zerop n))
	(member alpha (norm-up-to n)))
( ; hints
(do-not-induct T)
(use (norm-non-zero (alpha alpha)))
(disable norm-up-to norm-non-zero)
))

(prove-lemma norm-up-to-big-enuf-aux4 (rewrite) (implies
	(and (member x (norm-up-to n)) (member y (norm-up-to n)))
	(member (cons x y) (norm-up-to (add1 n)))))

(disable norm-up-to)

(disable norm-of-cons)   ; needed for next defn to work
(defn norm-up-to-big-enuf-kludge (alpha n) (if
	(and (listp alpha) (not (zerop n)))
	(plus
		(norm-up-to-big-enuf-kludge (car alpha) (sub1 n))
		(norm-up-to-big-enuf-kludge (cdr alpha) (sub1 n)) )
	0 ) )
(enable norm-of-cons)

(defn bad-for-norm-up-to-big-enuf (alpha n) (and
	(ordinalp alpha) (leq (norm alpha) n)
	(not (member alpha (norm-up-to n)))))

(prove-lemma norm-up-to-big-enuf-aux5 (rewrite) (implies
	(bad-for-norm-up-to-big-enuf alpha n) 
	(and (listp alpha) (not (zerop n)))) )

(prove-lemma norm-up-to-big-enuf-aux6 (rewrite) (implies
	(and
		(listp alpha) (not (zerop n))
		(not (bad-for-norm-up-to-big-enuf (car alpha)  (sub1 n)))
		(not (bad-for-norm-up-to-big-enuf (cdr alpha)  (sub1 n))) )
	(not (bad-for-norm-up-to-big-enuf alpha  n))) 
( ; hints
(do-not-induct T)
(use (norm-up-to-big-enuf-aux4 (x (car alpha)) (y (cdr alpha)) (n  (sub1 n))))
(disable norm-up-to-big-enuf-aux4 ordinalp)
))

(prove-lemma norm-up-to-big-enuf-aux7 (rewrite) (not
	(bad-for-norm-up-to-big-enuf alpha n))
( ; hints
(disable bad-for-norm-up-to-big-enuf)
(induct (norm-up-to-big-enuf-kludge alpha n))
))

(prove-lemma norm-up-to-big-enuf (rewrite) (implies
	(and (ordinalp alpha) (leq (norm alpha) n))
	(member alpha (norm-up-to n)))
( ; hints
(use (norm-up-to-big-enuf-aux7 (alpha alpha) (n n)))
(disable  norm-up-to-big-enuf-aux7)
))

(disable norm-up-to-big-enuf-aux1)
(disable norm-up-to-big-enuf-aux2)
(disable norm-up-to-big-enuf-aux3)
(disable norm-up-to-big-enuf-aux4)
(disable norm-up-to-big-enuf-aux5)
(disable norm-up-to-big-enuf-aux6)
(disable norm-up-to-big-enuf-aux7)
(disable norm-up-to-big-enuf-kludge)
(disable bad-for-norm-up-to-big-enuf)

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

(prove-lemma norm-of-num-sharp (rewrite) (implies
	(and (ordinalp alpha) (numberp n))
	(equal (norm (num-sharp alpha n)) (plus (norm alpha) (norm n)))))


(prove-lemma norm-of-insert (rewrite) (implies
	(ordinalp alpha)
	(equal 
		(norm (insert delta alpha))
		(add1 (plus (norm delta) (norm alpha))))))

(prove-lemma norm-of-sharp (rewrite) (implies
	(and (ordinalp alpha) (ordinalp beta))
	(equal (norm (sharp alpha beta)) (plus (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.

(defn max-below (alpha lst n) (if (listp lst)
	(if 
		(and 
			(ordinalp (car lst))
			(leq (norm (car lst)) n)
			(ord-lessp (max-below alpha (cdr lst) n) (car lst))
			(ord-lessp (car lst) alpha) )
		(car lst)
		(max-below alpha (cdr lst) n)     )
	0 ))

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

(prove-lemma max-below-is-an-ordinal (rewrite) 
	(ordinalp (max-below alpha lst n)))

(prove-lemma max-below-is-below (rewrite) (implies
	(ord-lessp 0 alpha)
	(ord-lessp (max-below alpha lst n) alpha) )  )

(prove-lemma max-below-is-max (rewrite) (implies
	(and
		(ordinalp beta)
		(leq (norm beta) n)
		(member beta lst)
		(ord-lessp beta alpha))
	(not (ord-lessp (max-below alpha lst n) beta))  ))

(prove-lemma norm-of-max-below () (leq
	(norm (max-below alpha lst n)) n))

(enable ord-lessp)
(prove-lemma max-below-of-0 (rewrite) (equal
	(max-below 0 lst n) 0))
(disable ord-lessp)

(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

(defn pred (alpha n) (max-below 
	alpha 
	(norm-up-to (plus (norm alpha) (magic  n)))
	(plus (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)

(prove-lemma pred-of-0 (rewrite) (equal (pred 0 n) 0))

(prove-lemma pred-is-below (rewrite) (implies
	(ord-lessp 0 alpha)
	(ord-lessp (pred alpha n) alpha) ) )

(prove-lemma pred-is-an-ordinal (rewrite) 
	(ordinalp (pred alpha n)))

(prove-lemma upper-bound-on-norm-of-pred () 
	(leq
		(norm (pred alpha n))
		(plus (norm alpha) (magic n))  ) 
( ; hints
(do-not-induct T)
(use 
	(norm-of-max-below (alpha alpha) (n (plus (norm alpha) (magic n))) 
		(lst (norm-up-to (plus (norm alpha) (magic  n))) )) )
))

(prove-lemma pred-is-largest (rewrite) (implies
	(and 
		(ordinalp alpha) 
		(ordinalp beta)
		(leq (norm beta) (plus (norm alpha) (magic n)))
		(ord-lessp beta alpha)  )
	(ord-leq beta (pred alpha n)))
( ; hints
(do-not-induct T)
(use 
	(max-below-is-max (alpha alpha) (beta beta) 
		(n (plus (norm alpha) (magic  n)))
		(lst (norm-up-to (plus (norm alpha) (magic  n)))) )
	(norm-up-to-big-enuf (alpha beta) (n (plus (norm alpha) (magic  n)))) )
(disable norm-up-to-big-enuf max-below-is-max)
(enable ord-leq)
))

(disable pred)

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

(enable ord-lessp)
(prove-lemma pred-below-limit (rewrite) (implies
	(and (ordinalp alpha) (limitp alpha))
	(ord-lessp (pred alpha n) alpha)))
(disable ord-lessp)

(prove-lemma norm-of-pred-of-limit-aux1 (rewrite) (implies
	(and (ordinalp alpha) (limitp alpha))
	(ord-lessp (successor (pred alpha n)) alpha)))

(prove-lemma norm-of-pred-of-limit-aux2 (rewrite) (implies
	(and (ordinalp alpha) (limitp alpha))
	(lessp 
		(plus (norm alpha) (magic  n))
		(norm (successor (pred alpha n))) ) )  
( ; hints
(do-not-induct T)
(use
	(pred-is-largest (alpha alpha) (beta (successor (pred alpha n)))) )
(disable pred-is-largest norm-of-cons)
(enable ord-leq)
))

(prove-lemma norm-of-pred-of-limit-aux3 (rewrite) (implies
	(and (ordinalp alpha) (limitp alpha))
	(lessp 
		(plus (norm alpha) (magic  n))
		(add1 (norm (pred alpha n))) ) )
( ; hints
(do-not-induct T)
(use
	(norm-of-pred-of-limit-aux2 (alpha alpha) (n n))
	(norm-of-successor (alpha (pred alpha n)))      )
(disable  ordinalp norm-of-successor limitp norm-of-cons)
))

(prove-lemma norm-of-pred-of-limit (rewrite) (implies
	(and (ordinalp alpha) (limitp alpha))
	(equal
		(norm (pred alpha n))
		(plus (norm alpha) (magic  n))  ))    
( ; hints
(do-not-induct T)
(use 
	(upper-bound-on-norm-of-pred (alpha alpha) (n n))
	(norm-of-pred-of-limit-aux3 (alpha alpha) (n n)) )
(disable norm-of-pred-of-limit-aux3  ordinalp limitp norm-of-cons)
))

(disable norm-of-pred-of-limit-aux1)
(disable norm-of-pred-of-limit-aux2)
(disable norm-of-pred-of-limit-aux3)

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

(prove-lemma pred-of-succ-aux1 (rewrite) (implies
	(and (ordinalp alpha) (successorp alpha))
	(ord-lessp (pred alpha n) alpha))  )

(prove-lemma pred-of-succ-aux2 (rewrite) (implies
	(and (ordinalp alpha) (successorp alpha))
	(ord-leq (pred alpha n) (predecessor alpha)) )  
( ; hints
(do-not-induct T)
(use
	(nothing-between (alpha (predecessor alpha)) (beta (pred alpha n)))
	(pred-of-succ-aux1 (alpha alpha) (n n)) )
(disable pred-of-succ-aux1)
(enable ord-leq)
))

(prove-lemma pred-of-succ-aux3 () (implies
	(and (ordinalp alpha) (successorp alpha))
	(leq 
		(norm (predecessor alpha)) 
		(plus (norm alpha) (magic n)) )))

(prove-lemma pred-of-succ-aux4 () (implies
	(and (ordinalp alpha) (successorp alpha))
	(ord-leq (predecessor alpha) (pred alpha n)))
( ;hints
(use (pred-of-succ-aux3 (alpha alpha) (n n)))
))

(prove-lemma pred-of-succ (rewrite) (implies
	(and (ordinalp alpha) (successorp alpha))
	(equal (pred alpha n) (predecessor alpha)))  
( ;  hints
(do-not-induct T)
(use 
	(pred-of-succ-aux2 (n n) (alpha alpha))
	(pred-of-succ-aux4 (n n) (alpha alpha)) )
(disable  predecessor-is-smaller norm-of-predecessor
	pred-of-succ-aux4 pred-of-succ-aux2 ordinalp)
(enable irreflex-of-ord-leq)
))

(disable  pred-of-succ-aux1)
(disable  pred-of-succ-aux2)
(disable  pred-of-succ-aux3)
(disable  pred-of-succ-aux4)

(prove-lemma norm-of-pred-of-succ (rewrite) (implies
	(and (ordinalp alpha) (successorp alpha))
	(equal (norm (pred alpha n)) (sub1 (norm alpha)))  ))

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

(prove-lemma lower-bound-on-norm-of-pred (rewrite) (implies 
	(ordinalp alpha)
	(not (lessp 
		(norm (pred alpha n)) 
		(sub1 (norm alpha)))) )
(; hints
(do-not-induct T)
(use 
	(three-kinds (alpha alpha)) )
(disable ordinalp limitp)
))


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

(prove-lemma pred-sharp-below (rewrite) (implies
	(and 
		(ordinalp alpha) (ordinalp beta)
		(ord-lessp 0 beta))
	(ord-lessp 
		(sharp alpha (pred beta n))
		(sharp alpha beta) ))
( ; hints
(do-not-induct T)
(use
	(monotonicity-of-sharp 
		(alpha (pred beta n)) (beta beta) (lambda alpha))
	(pred-is-below (alpha beta) (n n))   )
(disable ordinalp pred-is-below monotonicity-of-sharp)
))

; step 2

(prove-lemma norm-of-pred-sharp () (implies
	(and 
		(ordinalp alpha) (ordinalp beta) (numberp n ) )
	(leq
		(norm (sharp alpha (pred beta n)))
		(plus (norm (sharp alpha beta)) (magic n)))  )
( ; hints
(do-not-induct T)
(use 
	(upper-bound-on-norm-of-pred (alpha beta) (n n)))
))

; step 3

(prove-lemma pred-sharp () (implies
	(and 
		(ordinalp alpha) (ordinalp beta) (numberp n ) (ord-lessp 0 beta) )
	(ord-leq
		(sharp alpha (pred beta n))
		(pred (sharp alpha beta) n) )  )
( ; hints
(do-not-induct T)
(use 
	(norm-of-pred-sharp (alpha alpha) (beta beta) (n n)))
))


;;;;;;;;  monotonicity of pred

; {alpha}(n) is a monotonic function of n

; first, a trivial fact about ord-leq

(enable ord-leq)
(prove-lemma ord-leq-is-idempotent (rewrite) 
	(ord-leq x x))
(disable ord-leq)

(prove-lemma monot-of-pred-aux1 (rewrite) (implies 
	(and 
		(ord-lessp 0 alpha)
		(ordinalp alpha) (numberp m) (numberp n) (leq m n))
	(ord-leq (pred alpha m) (pred alpha n)))
( ; hints
(do-not-induct T)
(use
	(magic-is-monotonic (m m) (n n))
	(upper-bound-on-norm-of-pred (alpha alpha) (n m))
	(pred-is-largest (n n) (alpha alpha) (beta (pred alpha m)) )  )
(disable magic-is-monotonic
	pred-is-largest upper-bound-on-norm-of-pred ordinalp)
))
		
(prove-lemma monot-of-pred-aux2 (rewrite) (implies 
	(and 
		(not (ord-lessp 0 alpha))
		(ordinalp alpha) (numberp m) (numberp n) (leq m n))
	(ord-leq (pred alpha m) (pred alpha n)))
( ; hints
(use
	(pred-of-0 (alpha alpha) (n n))
	(pred-of-0 (alpha alpha) (n m)) )
(disable pred-of-0)
(enable ord-lessp)
(do-not-induct T)
))

(prove-lemma monot-of-pred (rewrite) (implies 
	(and 
		(ordinalp alpha) (numberp m) (numberp n) (leq m n))
	(ord-leq (pred alpha m) (pred alpha n))) 
( ; hints
(do-not-induct T)
(use
	(monot-of-pred-aux1 (alpha alpha) (m m) (n n))
	(monot-of-pred-aux2 (alpha alpha) (m m) (n n)) )
(disable monot-of-pred-aux1 monot-of-pred-aux2 ordinalp )
))

(disable monot-of-pred-aux1)
(disable monot-of-pred-aux2)

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

(prove-lemma monot-of-norm-of-pred-aux1 (rewrite) (implies 
	(and 
		(equal alpha 0)
		(ordinalp alpha) (numberp m) (numberp n) (leq m n))
	(not (lessp (norm (pred alpha n)) (norm (pred alpha m)))) ))

(prove-lemma monot-of-norm-of-pred-aux2 (rewrite) (implies 
	(and 
		(limitp alpha)
		(ordinalp alpha) (numberp m) (numberp n) (leq m n))
	(not (lessp (norm (pred alpha n)) (norm (pred alpha m)))) )
( ; hints
(do-not-induct T)
(use (magic-is-monotonic (m m) (n n)))
(disable limitp magic-is-monotonic)
))

(prove-lemma monot-of-norm-of-pred-aux3 (rewrite) (implies 
	(and 
		(successorp alpha)
		(ordinalp alpha) (numberp m) (numberp n) (leq m n))
	(not (lessp (norm (pred alpha n)) (norm (pred alpha m)))) ))

(prove-lemma monot-of-norm-of-pred (rewrite) (implies 
	(and 
		(ordinalp alpha) (numberp m) (numberp n) (leq m n))
	(not (lessp (norm (pred alpha n)) (norm (pred alpha m)))) )
( ; hints
(do-not-induct T)
(use (three-kinds (alpha alpha)))
(disable norm-of-pred-of-succ limitp
	norm-of-pred-of-limit
	ordinalp three-kinds pred-of-0 pred-of-succ )
))

(disable monot-of-norm-of-pred-aux1)
(disable monot-of-norm-of-pred-aux2)
(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

(defn o-largep (set alpha) (if (equal alpha 0)
	T
	(if (nlistp set)
		F
		(o-largep (cdr set) (pred alpha (car set))))))

; prove the basic properties and then disable the defn

; base cases

(prove-lemma all-zero-large (rewrite) 
	(o-largep set 0))

(prove-lemma empty-not-large (rewrite) (implies
	(and (not (equal alpha 0)) (nlistp set))
	(not (o-largep set alpha))))

(prove-lemma recursive-case-for-large (rewrite) (implies
	(and (listp set) (not (equal alpha 0)))
	(equal
		(o-largep set alpha)
		(o-largep (cdr set) (pred alpha (car set))))))

(prove-lemma positive-large (rewrite) (implies
	(and (ordinalp alpha) (not (o-largep set alpha)))
	(ord-lessp 0 alpha))
( ;  hints
(enable ord-lessp)
))

(disable o-largep)


; lookat alpha-large when alpha is a successor ordinal

(prove-lemma successor-large-non-empty (rewrite) (implies
	(and (ordinalp alpha) (successorp alpha) (not (listp set)))
	(not (o-largep set alpha))))

(prove-lemma successor-large (rewrite) (implies
	(and (ordinalp alpha) (successorp alpha))
	(equal
		(o-largep set alpha)
		(and
			(listp set)
			(o-largep (cdr set) (predecessor alpha)))))
( ; hints
(do-not-induct T)
(use
	(recursive-case-for-large (set set) (alpha alpha)) )
(disable recursive-case-for-large)
))

; lookat n-large for numbers n

(prove-lemma number-large (rewrite) (implies
	(numberp n)
	(equal
		(o-largep set n)
		(leq n (length set) ))) 
( ; hints
(induct (o-largep set n))
))

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

(prove-lemma omega-is-a-limit (rewrite) 
	(limitp '(1 . 0)))

(enable ord-lessp)
(prove-lemma numbers-below-omega (rewrite)  (implies
	(and (ordinalp alpha) (ord-lessp alpha '(1 . 0)))
	(numberp alpha)))
(disable ord-lessp)

(prove-lemma pred-of-omega-aux1 (rewrite)
	(numberp (pred '(1 . 0) n)))

(prove-lemma pred-of-omega-aux2 (rewrite) (implies
	(numberp n)
	(equal (norm (pred '(1 . 0) n))  (plus (magic n) 2))))

(prove-lemma pred-of-omega (rewrite) (implies
	(numberp n)
	(equal (pred '(1 . 0) n)  (plus (magic n) 2)))
( ; hints
(do-not-induct T)
(use 
	(pred-of-omega-aux2 (n n))
	(norm-of-pred-of-limit (alpha '(1 . 0)) (n n))
	(norm-of-a-number (n (pred '(1 . 0) n)))   )
(disable  limitp ordinalp
	pred-of-omega-aux2 norm-of-a-number norm-of-pred-of-limit)
))

(disable pred-of-omega-aux1)
(disable pred-of-omega-aux2)

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

(enable setp)
(prove-lemma car-of-a-set (rewrite) (implies
	(setp (cons x tail))
	(numberp x)))
(disable setp)

(prove-lemma omega-large ()  (implies
	(and (setp set) (o-largep set '(1 . 0)) )
	(and
		(listp set)
		(leq (plus (magic (car set)) 3) (length set)))) ) 

; in particular, omega-large implies large in the Paris-Harrington sense:
(prove-lemma omega-large-implies-large () (implies
	(and (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

(prove-lemma norm-above-1-aux1 (rewrite) (implies
	(and (numberp alpha) (ord-lessp 1 alpha) (ordinalp alpha))
	(lessp 1 (norm alpha)) ))

(enable norm)
(enable ord-lessp)
(prove-lemma norm-above-1-aux2 (rewrite) (implies
	(and (not (numberp alpha)) (ord-lessp 1 alpha) (ordinalp alpha))
	(lessp 1 (norm alpha)) ))
(disable norm)
(disable ord-lessp)

(prove-lemma norm-above-1 (rewrite) (implies
	(and  (ord-lessp 1 alpha) (ordinalp alpha))
	(lessp 1 (norm alpha)) )
( ; hints
(do-not-induct T)
(use 
	(norm-above-1-aux1 (alpha alpha))
	(norm-above-1-aux2 (alpha alpha)) )
))

(disable norm-above-1-aux1)
(disable norm-above-1-aux2)

(prove-lemma pred-not-0 (rewrite) (implies
	(and (ord-lessp 1 alpha) (ordinalp alpha))
	(ord-leq 1 (pred alpha n)))
( ; hints
(do-not-induct T)
(use (pred-is-largest (n n) (beta 1) (alpha alpha)))
(disable pred-is-largest ordinalp)
))

(prove-lemma singletons-not-large (rewrite) (implies
	(and 
		(o-largep set alpha)
		(ordinalp alpha)
		(ord-lessp 1 alpha) )
	(listp (cdr set))  )  ; set isn't a singleton
( ; hints
(do-not-induct T)
(use (pred-not-0 (alpha alpha) (n (car set))))
(disable  pred-is-largest norm-above-1
	pred-not-0  recursive-case-for-large empty-not-large)
(enable o-largep)
))


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

(defn bad-for-large-superset-ord (alpha beta X Y) (and
		(ordinalp alpha) (ordinalp beta) 
		(setp X) (setp Y) (subsetp X Y)
		(o-largep X beta)
		(ord-leq alpha beta) 
		(leq (norm alpha) (plus (norm beta) (magic (car X))) )
		(not (o-largep Y alpha))) )

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

(prove-lemma large-superset-ord-aux1 (rewrite) (implies
	(bad-for-large-superset-ord alpha beta X Y) 
	(ord-lessp 0 alpha))
( ; hints
(enable ord-lessp)
))

(prove-lemma large-superset-ord-aux2 () (implies
	(and  (ordinalp alpha) (ordinalp beta)
		(ord-lessp 0 alpha) (ord-leq alpha beta))
	(ord-lessp 0 beta))
( ; hints
(do-not-induct T)
(enable ord-leq)
(use 
	(trichotomy (sigma alpha) (tau beta)))
))

(prove-lemma large-superset-ord-aux3 (rewrite) (implies
	(bad-for-large-superset-ord alpha beta X Y) 
	(ord-lessp 0 beta)) 
( ; hints
(do-not-induct T)
(use 
	(large-superset-ord-aux1 (alpha alpha) (X X) (Y Y) (beta beta))
	(large-superset-ord-aux2 (alpha alpha) (beta beta)) ) 
(disable large-superset-ord-aux1)
))

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

(prove-lemma large-superset-ord-aux4 (rewrite) (not
	(bad-for-large-superset-ord 1 1 X Y) ))

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

(prove-lemma large-superset-ord-aux5 (rewrite) (implies
	(bad-for-large-superset-ord alpha beta X Y) 
	(and (ordinalp alpha) (ordinalp beta))))
	
(prove-lemma large-superset-ord-aux6 (rewrite) (implies
	(bad-for-large-superset-ord alpha beta X Y) 
	(or (ord-lessp 1 alpha) (ord-lessp 1 beta)))
( ; hints
(do-not-induct T)
(use  
	(large-superset-ord-aux1 (alpha alpha) (beta beta) (X X) (Y Y))
	(large-superset-ord-aux3 (alpha alpha) (beta beta) (X X) (Y Y))
	(ords-below-2 (alpha alpha))
	(ords-below-2 (alpha beta)) )
(disable transitivity large-superset-ord-aux1 large-superset-ord-aux3 
	bad-for-large-superset-ord ord-lessp)
))

(prove-lemma large-superset-ord-aux7 (rewrite) (implies
	(bad-for-large-superset-ord alpha beta X Y) 
	(ord-leq alpha beta)))

(prove-lemma large-superset-ord-aux8 (rewrite) (implies
	(bad-for-large-superset-ord alpha beta X Y) 
	(ord-lessp 1 beta) )
( ; hints
(do-not-induct T)
(use 
	(large-superset-ord-aux6 (alpha alpha) (beta beta) (X X) (Y Y))
	(transitivity-alt2 (alpha 1) (beta alpha) (gamma beta)))
(disable large-superset-ord-aux6 bad-for-large-superset-ord)
))

(prove-lemma large-superset-ord-aux9 (rewrite) (implies
	(bad-for-large-superset-ord alpha beta X Y) 
	(listp (cdr X)))
( ; hints
(do-not-induct T)
(use
	(large-superset-ord-aux8  (alpha alpha) (beta beta) (X X) (Y Y)))
(disable large-superset-ord-aux8)
))

; 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

(prove-lemma large-superset-ord-aux10 (rewrite) (implies
	(bad-for-large-superset-ord alpha beta X Y) 
	(and  (ordinalp (pred alpha (car Y))) (ordinalp (pred beta (car X))))))

(prove-lemma large-superset-ord-aux11 (rewrite) (implies
	(bad-for-large-superset-ord alpha beta X Y) 
	(and (listp X) (listp Y)))
( ; hints
(do-not-induct T)
(use (large-superset-ord-aux9 (X X) (Y Y) (alpha alpha) (beta beta)))
))

(prove-lemma large-superset-ord-aux12 (rewrite) (implies
	(bad-for-large-superset-ord alpha beta X Y) 
	(and (setp (cdr X)) (setp (cdr Y)) ))
( ; hints
(do-not-induct T)
(use
	(large-superset-ord-aux11 (X X) (Y Y) (alpha alpha) (beta beta))
	(tail-of-a-set (s X))
	(tail-of-a-set (s Y))  )
(disable  car-nlistp cdr-nlistp large-superset-ord-aux11
	transitivity-of-subset  large-superset-ord-aux10
	ord-leq-is-idempotent cdr-cdr-subset tail-of-a-set)
))

(prove-lemma large-superset-ord-aux13 (rewrite) (implies
	(bad-for-large-superset-ord alpha beta X Y) 
	(subsetp (cdr X) (cdr Y)) )
( ; hints
(do-not-induct T)
(use
	(large-superset-ord-aux11 (alpha alpha) (beta beta) (X X) (Y Y) )
	(cdr-cdr-subset (s1 X) (s2 Y))
	(tail-of-a-set (s X))
	(tail-of-a-set (s Y))  )
(disable   IRREFLEX-OF-ORD-LEQ ORD-LEQ-IS-TRANSITIVE
	MIN-IS-FIRST ORD-LEQ CARS-ARE-ORDINALS NUMBERS-BELOW-OMEGA
	transitivity-of-subset  large-superset-ord-aux11
	ord-leq-is-idempotent cdr-cdr-subset tail-of-a-set)
))

(prove-lemma large-superset-ord-aux14 (rewrite) (implies
	(bad-for-large-superset-ord alpha beta X Y) 
	(o-largep (cdr X) (pred beta (car X))  ))
( ; hints
(do-not-induct T)
(use
	(recursive-case-for-large (set X) (alpha beta))
	(large-superset-ord-aux11 (alpha alpha) (beta beta) (X X) (Y Y) ) )
(disable recursive-case-for-large  large-superset-ord-aux11)
))

(prove-lemma large-superset-ord-aux15 (rewrite) (implies
	(bad-for-large-superset-ord alpha alpha X Y) 
	(ord-leq (pred alpha (car Y)) (pred alpha (car X)))  )
( ; hints
(do-not-induct T)
(use
	(compare-first-elts (s1 X) (s2 Y))
	(large-superset-ord-aux11 (alpha alpha) (beta alpha) (X X) (Y Y) ) )
(disable large-superset-ord-aux11 compare-first-elts)
))

(prove-lemma large-superset-ord-aux16 () (implies
	(bad-for-large-superset-ord alpha alpha X Y) 
	(leq
		(norm (pred alpha (car Y)))
		(plus (norm (pred alpha (car X)))
			(magic (car (cdr X))))))
					; actually, don't need the magic ... here
					; since (car Y) <= (car X)
( ; hints
(do-not-induct T)
(use
	(monot-of-norm-of-pred (alpha alpha) (m (car Y)) (n (car X)))
	(compare-first-elts (s1 X) (s2 Y))
	(large-superset-ord-aux11 (alpha alpha) (beta alpha) (X X) (Y Y) ) )
(disable large-superset-ord-aux11 compare-first-elts)
))

(prove-lemma large-superset-ord-aux17 () (implies
	(bad-for-large-superset-ord alpha alpha X Y) 
	(not (o-largep (cdr Y) (pred alpha (car Y))))  )
( ; hints
(do-not-induct T)
(use
	(recursive-case-for-large (set Y) (alpha alpha))
	(large-superset-ord-aux11 (alpha alpha) (beta alpha) (X X) (Y Y) ) ) 
(disable large-superset-ord-aux11 recursive-case-for-large) 
))

(prove-lemma large-superset-ord-aux18 (rewrite) (implies
	(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) ))
( ; hints
(do-not-induct T)
(use
	(large-superset-ord-aux10 (alpha alpha) (beta alpha) (X X) (Y Y) )  
	(large-superset-ord-aux11 (alpha alpha) (beta alpha) (X X) (Y Y) )  
	(large-superset-ord-aux12 (alpha alpha) (beta alpha) (X X) (Y Y) )  
	(large-superset-ord-aux13 (alpha alpha) (beta alpha) (X X) (Y Y) )  
	(large-superset-ord-aux14 (alpha alpha) (beta alpha) (X X) (Y Y) )  
	(large-superset-ord-aux15 (alpha alpha) (beta alpha) (X X) (Y Y) )  
	(large-superset-ord-aux16 (alpha alpha) (beta alpha) (X X) (Y Y) )  
	(large-superset-ord-aux17 (alpha alpha) (beta alpha) (X X) (Y Y) )  )
(disable  subsetp ord-leq cdr-of-subset subset-of-cdr
	numbers-below-omega pred-is-largest norm cars-are-ordinals
	large-superset-ord-aux10 
	large-superset-ord-aux11 
	large-superset-ord-aux12 
	large-superset-ord-aux13 
	large-superset-ord-aux14 
	large-superset-ord-aux15 
	large-superset-ord-aux16 
	large-superset-ord-aux17 )
))

; 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 

(prove-lemma large-superset-ord-aux19 (rewrite) (implies
	(and
		(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:

(prove-lemma large-superset-ord-aux20 () (implies
	(and
		(ordinalp beta) (numberp v) (numberp z) (lessp v z))
	(leq
		(plus (norm beta) (magic v))
		(plus (norm (pred beta z)) (magic z)))  ))
; we use this with v = (car X) and z = (cadr X)

(prove-lemma large-superset-ord-aux21 () (implies
	(bad-for-large-superset-ord alpha beta X Y) 
	(lessp (car X) (cadr X)))
( ; hints
(do-not-induct T)
(use
	(large-superset-ord-aux9 (alpha alpha) (beta beta) (X X) (Y Y)))
))

(prove-lemma large-superset-ord-aux22 () (implies
	(and
		(bad-for-large-superset-ord alpha beta X Y) 
		(ord-lessp alpha beta))
	(leq 
		(norm alpha)
		(plus (norm (pred beta (car X))) (magic (car (cdr X))))) )
( ; hints
(do-not-induct T)
(use
	(large-superset-ord-aux21 (alpha alpha) (beta beta) (X X) (Y Y))
	(large-superset-ord-aux20 (beta beta) (v (car X)) (z (cadr X)))   )
))

(prove-lemma large-superset-ord-aux23 () (implies
	(bad-for-large-superset-ord alpha beta X Y) 
	(subsetp (cdr X) Y) )
( ; hints
(do-not-induct T)
(use (cdr-is-subset (s X)))
(disable cdr-is-subset)
))

(prove-lemma large-superset-ord-aux24 () (implies
	(and
		(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) )
( ; hints
(do-not-induct T)
(use
	(large-superset-ord-aux23 (alpha alpha) (beta beta) (X X) (Y Y)) 
	(large-superset-ord-aux10 (alpha alpha) (beta beta) (X X) (Y Y)) 
	(large-superset-ord-aux12 (alpha alpha) (beta beta) (X X) (Y Y)) 
	(large-superset-ord-aux14 (alpha alpha) (beta beta) (X X) (Y Y)) 
	(large-superset-ord-aux19 (alpha alpha) (beta beta) (X X) (Y Y)) 
	(large-superset-ord-aux22 (alpha alpha) (beta beta) (X X) (Y Y)) )
(disable 
	large-superset-ord-aux23
	large-superset-ord-aux10 
	large-superset-ord-aux11 
	large-superset-ord-aux12 
	large-superset-ord-aux14 
	large-superset-ord-aux19 
	large-superset-ord-aux22 )
))

; END Case 2

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

(prove-lemma large-superset-ord-aux25 () (implies
	(bad-for-large-superset-ord alpha beta X Y) 
	(or
		(ord-lessp alpha beta)
		(equal alpha beta)))
( ; hints
(do-not-induct T)
(use (trichotomy (sigma alpha) (tau beta)))
(enable ord-leq)
))

(disable large-superset-ord-aux1)
(disable large-superset-ord-aux2)
(disable large-superset-ord-aux3)
(disable large-superset-ord-aux4)
(disable large-superset-ord-aux5)
(disable large-superset-ord-aux6)
(disable large-superset-ord-aux7)
(disable large-superset-ord-aux8)
(disable large-superset-ord-aux9)
(disable large-superset-ord-aux10)
(disable large-superset-ord-aux11)
(disable large-superset-ord-aux12)
(disable large-superset-ord-aux13)
(disable large-superset-ord-aux14)
(disable large-superset-ord-aux15)
(disable large-superset-ord-aux16)
(disable large-superset-ord-aux17)
(disable large-superset-ord-aux18)
(disable large-superset-ord-aux19)
(disable large-superset-ord-aux21)
(disable large-superset-ord-aux22)
(disable large-superset-ord-aux23)
(disable large-superset-ord-aux24)
(disable large-superset-ord-aux25)

; summarizing

(prove-lemma large-superset-ord-aux26 (rewrite) (implies
	(bad-for-large-superset-ord alpha beta X Y) 
	(or
		(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) )    )  )
( ; hints
(do-not-induct T)
(use
	(large-superset-ord-aux24 (alpha alpha) (beta beta) (X X) (Y Y))
	(large-superset-ord-aux25 (alpha alpha) (beta beta) (X X) (Y Y))
	(large-superset-ord-aux18 (alpha alpha)  (X X) (Y Y)) )
(disable bad-for-large-superset-ord)  
))

(prove-lemma large-superset-ord-aux27 (rewrite) (implies
	(bad-for-large-superset-ord alpha beta X Y) 
	(listp X) )
( ; hints
(do-not-induct T)
(use
	(large-superset-ord-aux9 (alpha alpha) (beta beta) (X X) (Y Y)) )
(disable bad-for-large-superset-ord)  
))

(defn large-superset-ord-kludge (alpha beta X Y) (if (nlistp X)
	0
	(plus
		(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) )    )  ) )

(prove-lemma large-superset-ord-aux28 (rewrite) (implies
	(and
		(not (bad-for-large-superset-ord 
			alpha (pred beta (car X))
			(cdr X)   Y)  )
		(not (bad-for-large-superset-ord 
			(pred alpha (car Y))
			(pred alpha (car X))
			(cdr X)  (cdr Y) )    )  )
	(not (bad-for-large-superset-ord alpha beta X Y)  )  )
( ; hints
(do-not-induct T)
(use (large-superset-ord-aux26 (alpha alpha) (beta beta) (X X) (Y Y)))
(disable bad-for-large-superset-ord large-superset-ord-aux26)  
))

(prove-lemma large-superset-ord-aux29 (rewrite) 
	(not (bad-for-large-superset-ord alpha beta X Y) ) 
( ; hints
(induct (large-superset-ord-kludge alpha beta X Y))
(disable bad-for-large-superset-ord)  
))

(prove-lemma large-superset-ord (rewrite) (implies
	(and
		(ordinalp alpha) (ordinalp beta) 
		(setp X) (setp Y) (subsetp X Y)
		(o-largep X beta)
		(ord-leq alpha beta) 
		(leq (norm alpha) (plus (norm beta) (magic (car X))) ) )
	(o-largep Y alpha))
( ; hints
(do-not-induct T)
(use (large-superset-ord-aux29 (alpha alpha) (beta beta) (X X) (Y Y)))
(disable large-superset-ord-aux29)
))

(disable large-superset-ord-aux26)
(disable large-superset-ord-aux27)
(disable large-superset-ord-aux28)
(disable large-superset-ord-aux29)
(disable large-superset-ord-kludge)


;;;;;;;; two important special cases

; Special case 1 -- alpha = beta

(prove-lemma large-goes-up (rewrite) (implies
	(and
		(ordinalp alpha) 
		(setp X) (setp Y) (subsetp X Y)
		(o-largep X alpha) )
	(o-largep Y alpha)) 
( ; hints
(do-not-induct T)
(use (large-superset-ord (alpha alpha) (beta alpha) (X X) (Y Y)))
))

; Special case 2 -- X = Y

(prove-lemma subsetp-is-idempotent (rewrite) (subsetp s s)
( ; hints
(use (subsetp-works-2 (s1 s) (s2 s)))
(disable subsetp-works-2)
))

(prove-lemma large-with-smaller-ord (rewrite) (implies
	(and
		(ordinalp alpha) (ordinalp beta) 
		(setp X) 
		(o-largep X beta)
		(ord-leq alpha beta) 
		(leq (norm alpha) (plus (norm beta) (magic (car X))) ) )
	(o-largep X alpha))  
( ; hints
(do-not-induct T)
(use (large-superset-ord (alpha alpha) (beta beta) (X X) (Y X)) )
))


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

(defn covers (A B X) (if (nlistp X) T
	(and 
		(covers A B (cdr X))
		(or
			(member (car X) A)
			(member (car X) B)  ))))

; some basic lemmas expressing the recursion

(prove-lemma covers-empty (rewrite) (implies
	(nlistp X)
	(covers A B X)))

(prove-lemma covers-negative (rewrite) (implies
	(and 
		(listp X)
		(not (member (car X) A))
		(not (member (car X) B)) )
	(not (covers A B X))))

(prove-lemma covers-positive-A (rewrite) (implies
	(and
		(listp X)
		(covers A B (cdr X))
		(member (car X) A))
	(covers A B X)))

(prove-lemma covers-positive-B (rewrite) (implies
	(and
		(listp X)
		(covers A B (cdr X))
		(member (car X) B))
	(covers A B X)))

(prove-lemma member-of-covered-set (rewrite) (implies
	(and
		(member u X)
		(covers A B X))
	(or
		(member u A)
		(member u B))))

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

(defn uncovered (A B X) (if (nlistp X)
	nil
	(if (covers A B (cdr X))
		(car X)
		(uncovered A B (cdr X)))))

(prove-lemma uncovered-isnt-covered (rewrite) (implies
	(not (covers A B X))
	(and
		(member (uncovered A B X) X)
		(not (member (uncovered A B X) A))
		(not (member (uncovered A B X) B))  )))

(prove-lemma cdr-is-covered (rewrite) (implies
	(covers A B X)
	(covers A B (cdr X))))

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

(disable covers)

(prove-lemma covers-is-symmetric ( ) (implies
	(covers A B X)
	(covers B A X))
( ; hints
(do-not-induct T)
(use
	(member-of-covered-set (A A) (B B) (X X) (u (uncovered B A X) ))
	(uncovered-isnt-covered (A B) (B A) (X X)))
(disable uncovered-isnt-covered member-of-covered-set)
))

(prove-lemma discard-the-car-A (rewrite) (implies
	(and
		(covers A B X)
		(listp A)
		(not (member (car A) X)) )
	(covers (cdr A) B X) )
( ; hints
(do-not-induct T)
(use
	(member-of-covered-set (A A) (B B) (X X) (u (uncovered (cdr A) B X) ))
	(uncovered-isnt-covered (A (cdr A)) (B B) (X X)))
(disable uncovered-isnt-covered member-of-covered-set)
))

(prove-lemma discard-the-car-B (rewrite) (implies
	(and
		(covers A B X)
		(listp B)
		(not (member (car B) X)) )
	(covers  A (cdr B) X) )
( ; hints
(do-not-induct T)
(use
	(member-of-covered-set (A A) (B B) (X X) (u (uncovered A (cdr B) X) ))
	(uncovered-isnt-covered (A A) (B (cdr B)) (X X)))
(disable uncovered-isnt-covered member-of-covered-set)
))

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

(prove-lemma discard-the-car-set-A (rewrite) (implies
	(and
		(setp A) (listp A) (setp X) (covers A B X) 
		(lessp (car A) (car X)) )
	(covers (cdr A) B X) ))

(prove-lemma discard-the-car-set-B (rewrite) (implies
	(and
		(setp B) (listp B) (setp X) (covers A B X) 
		(lessp (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
(prove-lemma smaller-car-when-covered (rewrite) (implies
	(and
		(setp A) (setp B) (setp X) (listp X) (covers A B X)  )
	(or
		(and (listp A) (leq (car A) (car X)))
		(and (listp B) (leq (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
(prove-lemma cdr-is-covered-set-A-aux1 (rewrite) (implies
	(and
		(listp (cdr X))
		(setp A) (setp B) (setp X) (listp X) (covers A B X) 
		(listp A) (leq (car A) (car X)))
	(lessp (car A) (cadr X)))   )

(prove-lemma cdr-is-covered-set-A-aux2 (rewrite) (implies
	(and
		(listp (cdr X))
		(setp A) (setp B) (setp X) (listp X) (covers A B X) 
		(listp A) (leq (car A) (car X)))
	(covers (cdr A) B (cdr X)) )  
( ; hints
(use 
	(tail-of-a-set (s X))
	(cdr-is-covered-set-A-aux1 (A A) (B B) (X X))
	(discard-the-car-set-A (A A) (B B) (X (cdr X)))  )
(disable discard-the-car-set-A tail-of-a-set)
))

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

(prove-lemma  cdr-is-covered-set-A (rewrite) (implies
	(and
		(setp A) (setp B) (setp X) (listp X) (covers A B X) 
		(listp A) (leq (car A) (car X)))
	(covers (cdr A) B (cdr X)) )  
( ; hints
(do-not-induct T)
(use 
	(cdr-is-covered-set-A-aux2 (A A) (B B) (X X)) )
(disable cdr-is-covered-set-A-aux2)
))

(disable cdr-is-covered-set-A-aux1)
(disable cdr-is-covered-set-A-aux2)

; now, by symmetry:

(prove-lemma cdr-is-covered-set-B (rewrite) (implies
	(and
		(setp A) (setp B) (setp X) (listp X) (covers A B X) 
		(listp B) (leq (car B) (car X)))
	(covers  A (cdr B) (cdr X)) ) 
( ; hints
(do-not-induct T)
(use 
	(cdr-is-covered-set-A (A B) (B A) (X X))
	(covers-is-symmetric (A A) (B B) (X X))
	(covers-is-symmetric (A (cdr B)) (B A) (X (cdr X))) )
(disable covers-negative min-is-first cars-are-ordinals car-of-a-set
	 cdr-is-covered-set-A covers-is-symmetric cdr-is-covered)
))


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

(enable o-largep)
(prove-lemma sharp-and-cdr-aux1 (rewrite) (implies
	(and
		(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

(prove-lemma sharp-and-cdr-aux2 (rewrite) (implies
	(and
		(nlistp (cdr X))
		(ordinalp alpha) (ordinalp beta) (listp X)
		(o-largep X (sharp alpha beta))  )
	(equal (pred (sharp alpha beta) (car X)) 0 ) ))

(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

(prove-lemma sharp-and-cdr-aux3 (rewrite) (implies
	(and
		(ordinalp alpha) (ordinalp beta) (ord-lessp 0 beta)
        (numberp m) (numberp n) (leq m n)  )
	(ord-leq 
		(sharp alpha (pred beta m)) 
		(pred (sharp alpha beta) n) ) )
( ; hints
(do-not-induct T)
(use
	(ord-leq-is-transitive 
		(alpha (sharp alpha (pred beta m)))
		(beta (pred (sharp alpha beta) m))
		(gamma (pred (sharp alpha beta) n)) )
	(pred-sharp (alpha alpha) (beta beta) (n m))
	(monot-of-pred (m m) (n n) (alpha (sharp alpha beta))) )
(disable ordinalp pred-sharp monot-of-pred ord-leq-is-transitive)
))

(prove-lemma sharp-and-cdr-aux4 (rewrite) (implies
	(and
		(ordinalp alpha) (ordinalp beta) (ord-lessp 0 beta)
		(setp X) (numberp m) (leq m (car X)))
	(ord-leq 
		(sharp alpha (pred beta m)) 
		(pred (sharp alpha beta) (car X)) ) )
( ; hints
(do-not-induct T)
(use
	(sharp-and-cdr-aux3 (alpha alpha) (beta beta) (m m) (n (car X))))
(disable cars-are-ordinals cdrs-are-ordinals ordinalp sharp-and-cdr-aux3)
))

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

(prove-lemma sharp-and-cdr-aux5 (rewrite) (implies
	(and
		(listp X) (not (listp (cdr X)))
		(o-largep X (sharp alpha beta)) 
		(ordinalp alpha) (ordinalp beta) (ord-lessp 0 beta)
		(setp X) (numberp m) (leq m (car X)))
	(equal (sharp alpha (pred beta m))  0 ))
( ; hints
(do-not-induct T)
(use
	(sharp-and-cdr-aux2 (X X) (alpha alpha) (beta beta))
	(sharp-and-cdr-aux4 (X X) (m m) (alpha alpha) (beta beta)))
(disable   subsetp-is-idempotent large-goes-up
	ord-leq pred-is-largest
	ordinalp sharp-and-cdr-aux2
	sharp-and-cdr-aux3 sharp-and-cdr-aux4)
))

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

(prove-lemma sharp-and-cdr-aux6 (rewrite) (implies
	(and
		(not (listp (cdr X)))
		(ordinalp alpha) (ordinalp beta) (ord-lessp 0 beta)
		(setp X) (listp X) (numberp m) (leq 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

(prove-lemma sharp-and-cdr-aux7 (rewrite) (implies
	(and
		(setp X) (listp (cdr X)) (numberp m) (leq m (car X)) )
	(lessp 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:

(prove-lemma sharp-and-cdr-aux8 () (implies
	(and
		(ordinalp alpha) (ordinalp beta) (ord-lessp 0 beta)
		(numberp m) (numberp x0) (lessp m x1)  )
	(leq
		(norm (sharp alpha (pred beta m)))
		(plus (norm (pred (sharp alpha beta) x0)) (magic x1)) ) )
( ; hints
(do-not-induct T)
(use
	(upper-bound-on-norm-of-pred (alpha beta) (n m))
	(magic-is-monotonic (m m) (n x1))
	(lower-bound-on-norm-of-pred  (alpha (sharp alpha beta)) (n x0)) )
))
; intended :  x0 is (car X) ; x1 is (cadr x)

(prove-lemma sharp-and-cdr-aux9 () (implies
	(and
		(listp (cdr X))
		(ordinalp alpha) (ordinalp beta) (ord-lessp 0 beta)
		(setp X) (listp X) (numberp m) (leq m (car X)) )
	(leq
		(norm (sharp alpha (pred beta m)))
		(plus (norm (pred (sharp alpha beta) (car X))) (magic (cadr X))) ) )
( ; hints
(use (sharp-and-cdr-aux8 (alpha alpha) (beta beta)
		(x0 (car X)) (x1 (cadr X))))
(disable  norm lower-bound-on-norm-of-pred pred sharp
	ord-leq-zero numbers-below-omega ord-leq)
))

(prove-lemma sharp-and-cdr-aux10 (rewrite) (implies
	(and
		(listp (cdr X))
		(ordinalp alpha) (ordinalp beta) (ord-lessp 0 beta)
		(setp X) (listp X) (numberp m) (leq m (car X))
		(o-largep X (sharp alpha beta))  )
	(o-largep (cdr X) (sharp alpha (pred beta m)))  ) 
( ; hints
(do-not-induct T)
(use 
	(large-with-smaller-ord 
		(alpha (sharp alpha (pred beta m)))
		(beta (pred (sharp alpha beta) (car X)))
		(X (cdr X)) )
	(tail-of-a-set (s X))
	(sharp-and-cdr-aux1 (alpha alpha) (beta beta) (X X))
	(sharp-and-cdr-aux4 (alpha alpha) (beta beta) (m m) (X X))
	(sharp-and-cdr-aux9 (alpha alpha) (beta beta) (m m) (X X))     )
(disable  large-with-smaller-ord tail-of-a-set
	first-before-last large-superset-ord norm-of-pred-of-succ 
	subsetp subsetp-is-idempotent large-goes-up
	norm-of-a-number sharp-and-cdr-aux3
	singletons-not-large norm-of-pred-of-limit
	pred-of-succ successorp transitivity 
	sharp norm pred-is-largest insert-is-cons
	norm-of-sharp sharp-and-cdr-aux9 sharp-and-cdr-aux1
	sharp-and-cdr-aux4 ord-leq insert 
	ord-leq-zero numbers-below-omega)
))

(prove-lemma sharp-and-cdr-B (rewrite) (implies
	(and
		(ordinalp alpha) (ordinalp beta) (ord-lessp 0 beta)
		(setp X) (listp X) (numberp m) (leq m (car X))
		(o-largep X (sharp alpha beta))  )
	(o-largep (cdr X) (sharp alpha (pred beta m)))  )
( ; hints
(do-not-induct T)
(use 
	(sharp-and-cdr-aux10 (alpha alpha) (beta beta) (m m) (X X)))
(disable sharp-and-cdr-aux10)
))

(disable sharp-and-cdr-aux1)
(disable sharp-and-cdr-aux2)
(disable sharp-and-cdr-aux3)
(disable sharp-and-cdr-aux4)
(disable sharp-and-cdr-aux5)
(disable sharp-and-cdr-aux6)
(disable sharp-and-cdr-aux7)
(disable sharp-and-cdr-aux8)
(disable sharp-and-cdr-aux9)
(disable sharp-and-cdr-aux10)

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

(prove-lemma sharp-and-cdr-A (rewrite) (implies
	(and
		(ordinalp alpha) (ordinalp beta) (ord-lessp 0 alpha)
		(setp X) (listp X) (numberp m) (leq 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

(defn bad-for-pigeon-2 (A B X alpha beta) (and
		(ordinalp alpha) (ordinalp beta)
		(setp A) (setp B) (setp X) (covers A B X)
		(o-largep X (sharp alpha beta))  
		(not (o-largep A alpha))
		(not (o-largep B beta))  ) )

; first, kill off some base cases:

; alpha and beta are > 0

(prove-lemma pigeon-2-aux1 (rewrite) (implies
	(bad-for-pigeon-2 A B X alpha beta)
	(ord-lessp 0 alpha) ) )

(prove-lemma pigeon-2-aux2 (rewrite) (implies
	(bad-for-pigeon-2 A B X alpha beta)
	(ord-lessp 0 beta) ) )

(prove-lemma pigeon-2-aux3 (rewrite) (implies
	(bad-for-pigeon-2 A B X alpha beta)
	(and (ordinalp alpha) (ordinalp beta))))

(prove-lemma pigeon-2-aux4 (rewrite) (implies
	(bad-for-pigeon-2 A B X alpha beta)
	(ord-lessp 0 (sharp alpha beta)) ) 
( ;  hints
(do-not-induct T)
(use 
	(postive-ord-lessp (gamma alpha) (delta (sharp alpha beta)))
	(sharp-gets-bigger (alpha alpha) (beta beta))
	(pigeon-2-aux2 (A A) (B B) (X X) (alpha alpha) (beta beta)) )
(disable ordinalp postive-ord-lessp
	bad-for-pigeon-2 pigeon-2-aux2)
))

(prove-lemma pigeon-2-aux5 (rewrite) (implies
	(bad-for-pigeon-2 A B X alpha beta)
	(listp X))
( ; hints
(do-not-induct T)
(use 
	(pigeon-2-aux4 (A A) (B B) (X X) (alpha alpha) (beta beta))
	(empty-not-large (set X) (alpha (sharp alpha beta))))
(disable pigeon-2-aux4  insert sharp o-largep numbers-below-omega 
	 ORD-LEQ ORD-LEQ-IS-TRANSITIVE empty-not-large subsetp-is-idempotent  )
))

(prove-lemma pigeon-2-aux6 (rewrite) (implies
	(bad-for-pigeon-2 A B X alpha beta)
	(and
		(setp A) (setp B) (setp X) (listp X) (covers A B X)  ) )
( ; hints
(do-not-induct T)
(use 
	(pigeon-2-aux5 (A A) (B B) (X X) (alpha alpha) (beta beta)) )
(hands-off ordinalp setp o-largep)
(disable pigeon-2-aux5 LARGE-GOES-UP SHARP-IS-AN-ORDINAL)
))

(prove-lemma pigeon-2-aux7 (rewrite) (implies
	(bad-for-pigeon-2 A B X alpha beta)
	(or
		(and (listp A) (leq (car A) (car X)))
		(and (listp B) (leq (car B) (car X))) )  )
( ; hints
(do-not-induct T)
(use
	(pigeon-2-aux6 (A A) (B B) (X X) (alpha alpha) (beta beta) )
	(smaller-car-when-covered (A A) (B B) (X X)))
(disable smaller-car-when-covered covers-empty  pigeon-2-aux6 o-largep
	bad-for-pigeon-2 cars-are-ordinals)
(hands-off ordinalp)
))

; 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
(prove-lemma pigeon-2-aux8 (rewrite) (implies
	(bad-for-pigeon-2 A B X alpha beta)
	(and (ordinalp (pred alpha (car A))) (ordinalp beta)  )))

; line2
(prove-lemma pigeon-2-aux9 (rewrite) (implies
	(and
		(bad-for-pigeon-2 A B X alpha beta)
		(listp A) (leq (car A) (car X))  ) 
	(and
		(setp (cdr A)) (setp B) (setp (cdr X)) (covers (cdr A) B (cdr X))  )  )
( ;  hints
(do-not-induct T)
(use
	(tail-of-a-set (s A))
	(tail-of-a-set (s X))
	(cdr-is-covered-set-A (A A) (B B) (X X))
	(pigeon-2-aux6 (A A) (B B) (X X) (alpha alpha) (beta beta) ) )
(disable CARS-ARE-ORDINALS  IRREFLEX-OF-ORD-LEQ ORD-LEQ-ZERO       
	NUMBERS-BELOW-OMEGA
 	bad-for-pigeon-2 pigeon-2-aux6  cdr-is-covered-set-A)
(hands-off covers ord-leq )
))

; line3
(prove-lemma pigeon-2-aux10 (rewrite) (implies
	(and
		(bad-for-pigeon-2 A B X alpha beta)
		(leq (car A) (car X))  ) 
	(o-largep (cdr X) (sharp (pred alpha (car A)) beta))  ) 
( ; hints
(do-not-induct T)
(use 
	(pigeon-2-aux5 (A A) (B B) (X X) (alpha alpha) (beta beta)  )
	(sharp-and-cdr-A  (X X) (alpha alpha) (beta beta) (m (car A))))
(disable 
	CARS-ARE-ORDINALS  O-LARGEP  NUMBERS-BELOW-OMEGA IRREFLEX-OF-ORD-LEQ  
	ORD-LEQ-ZERO        pigeon-2-aux5
	o-largep sharp sharp-and-cdr-A)
(hands-off o-largep )
))

; line4
(prove-lemma pigeon-2-aux11 (rewrite) (implies
	(and
		(bad-for-pigeon-2 A B X alpha beta)
		(listp A) )
	(not (o-largep (cdr A) (pred alpha (car A))))  )
( ; hints
(do-not-induct T)
(use 
	(recursive-case-for-large (set A) (alpha alpha)) )
(disable recursive-case-for-large)
))

; line5
(prove-lemma pigeon-2-aux12 (rewrite) (implies
	(bad-for-pigeon-2 A B X alpha beta)
	(not (o-largep B beta))  ) )

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

(prove-lemma pigeon-2-aux13 (rewrite) (implies
	(and
		(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))  
		(not (o-largep (cdr A) (pred alpha (car A))))
		(not (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
(prove-lemma pigeon-2-aux14 (rewrite) (implies
	(and
		(bad-for-pigeon-2 A B X alpha beta)
		(listp A) (leq (car A) (car X))  ) 
	(bad-for-pigeon-2 (cdr A) B (cdr X) (pred alpha (car A)) beta) ) 
( ; hints
(do-not-induct T)
(use 
	(pigeon-2-aux8 (A A) (B B) (X X) (alpha alpha) (beta beta)  )
	(pigeon-2-aux9 (A A) (B B) (X X) (alpha alpha) (beta beta)  )
	(pigeon-2-aux10 (A A) (B B) (X X) (alpha alpha) (beta beta)  )
	(pigeon-2-aux11 (A A) (B B) (X X) (alpha alpha) (beta beta)  )
	(pigeon-2-aux12 (A A) (B B) (X X) (alpha alpha) (beta beta)  )
	(pigeon-2-aux13 (A A) (B B) (X X) (alpha alpha) (beta beta)  ) )
(hands-off ordinalp setp o-largep sharp insert)
(disable pigeon-2-aux8 pigeon-2-aux9 pigeon-2-aux10 pigeon-2-aux11
	pigeon-2-aux12 bad-for-pigeon-2 setp)
))

; 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
(prove-lemma pigeon-2-aux15 (rewrite) (implies
	(bad-for-pigeon-2 A B X alpha beta)
	(and (ordinalp alpha) (ordinalp (pred beta (car B)))   )))

; line2
(prove-lemma pigeon-2-aux16 (rewrite) (implies
	(and
		(bad-for-pigeon-2 A B X alpha beta)
		(listp B) (leq (car B) (car X))  ) 
	(and
		(setp  A) (setp (cdr B)) (setp (cdr X)) (covers A (cdr B)(cdr X))  )  )
( ;  hints
(do-not-induct T)
(use
	(tail-of-a-set (s B))
	(tail-of-a-set (s X))
	(cdr-is-covered-set-B (A A) (B B) (X X))
	(pigeon-2-aux6 (A A) (B B) (X X) (alpha alpha) (beta beta) ) )
(disable CARS-ARE-ORDINALS  IRREFLEX-OF-ORD-LEQ ORD-LEQ-ZERO       
	NUMBERS-BELOW-OMEGA
 	bad-for-pigeon-2 pigeon-2-aux6  cdr-is-covered-set-A)
(hands-off covers ord-leq )
))

; line3
(prove-lemma pigeon-2-aux17 (rewrite) (implies
	(and
		(bad-for-pigeon-2 A B X alpha beta)
		(leq (car B) (car X))  ) 
	(o-largep (cdr X) (sharp alpha (pred beta (car B))))  ) 
( ; hints
(do-not-induct T)
(use 
	(pigeon-2-aux5 (A A) (B B) (X X) (alpha alpha) (beta beta)  )
	(sharp-and-cdr-B  (X X) (alpha alpha) (beta beta) (m (car B))))
(disable 
	CARS-ARE-ORDINALS  O-LARGEP  NUMBERS-BELOW-OMEGA IRREFLEX-OF-ORD-LEQ  
	ORD-LEQ-ZERO        pigeon-2-aux5
	o-largep sharp sharp-and-cdr-B)
(hands-off o-largep )
))

; line5
(prove-lemma pigeon-2-aux18 (rewrite) (implies
	(and
		(bad-for-pigeon-2 A B X alpha beta)
		(listp B) )
	(not (o-largep (cdr B) (pred beta (car B))))  )
( ; hints
(do-not-induct T)
(use 
	(recursive-case-for-large (set B) (alpha beta)) )
(disable recursive-case-for-large)
))

; line4
(prove-lemma pigeon-2-aux19 (rewrite) (implies
	(bad-for-pigeon-2 A B X alpha beta)
	(not (o-largep A alpha))  ) )

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

(prove-lemma pigeon-2-aux20 (rewrite) (implies
	(and
		(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)) ))  
		(not (o-largep A alpha))  
		(not (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
(prove-lemma pigeon-2-aux21 (rewrite) (implies
	(and
		(bad-for-pigeon-2 A B X alpha beta)
		(listp B) (leq (car B) (car X))  ) 
	(bad-for-pigeon-2  A (cdr B) (cdr X) alpha (pred beta (car B)) ) )
( ; hints
(do-not-induct T)
(use 
	(pigeon-2-aux15 (A A) (B B) (X X) (alpha alpha) (beta beta)  )
	(pigeon-2-aux16 (A A) (B B) (X X) (alpha alpha) (beta beta)  )
	(pigeon-2-aux17 (A A) (B B) (X X) (alpha alpha) (beta beta)  )
	(pigeon-2-aux18 (A A) (B B) (X X) (alpha alpha) (beta beta)  )
	(pigeon-2-aux19 (A A) (B B) (X X) (alpha alpha) (beta beta)  )
	(pigeon-2-aux20 (A A) (B B) (X X) (alpha alpha) (beta beta)  ) )
(hands-off ordinalp setp o-largep sharp insert)
(disable pigeon-2-aux15 pigeon-2-aux16 pigeon-2-aux17 pigeon-2-aux18
	pigeon-2-aux19 bad-for-pigeon-2 setp)
))

; 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

(prove-lemma pigeon-2-aux22 (rewrite) (implies
	(bad-for-pigeon-2 A B X alpha beta)
	(or
		(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)) ) ) )
( ; hints
(do-not-induct T)
(use 
	(pigeon-2-aux7 (A A) (B B) (X X) (alpha alpha) (beta beta)  )
	(pigeon-2-aux14 (A A) (B B) (X X) (alpha alpha) (beta beta)  )
	(pigeon-2-aux21 (A A) (B B) (X X) (alpha alpha) (beta beta)  ) )
(disable bad-for-pigeon-2 
	CARS-ARE-ORDINALS IRREFLEX-OF-ORD-LEQ ORD-LEQ-ZERO 
	NUMBERS-BELOW-OMEGA ORD-LEQ   )
(hands-off ord-leq)
))

(defn pigeon-2-kludge (A B X alpha beta) (if (nlistp X) 
	0
	(plus
		(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)) ) ) ))

(prove-lemma pigeon-2-aux23 (rewrite) (not
	(bad-for-pigeon-2 A B X alpha beta) )
( ; hints
(disable bad-for-pigeon-2 )
(induct (pigeon-2-kludge A B X alpha beta))
(use 
	(pigeon-2-aux22 (A A) (B B) (X X) (alpha alpha) (beta beta)  ) )
))

; finally, the GOAL:
(prove-lemma pigeon-2 (rewrite) (implies
	(and 
		(ordinalp alpha) (ordinalp beta)
		(setp A) (setp B) (setp X) (covers A B X)
		(o-largep X (sharp alpha beta))  )
	(or
		(o-largep A alpha)
		(o-largep B beta)  )  )
( ; hints
(do-not-induct T)
(use (pigeon-2-aux23  (A A) (B B) (X X) (alpha alpha) (beta beta)  ) )
(disable pigeon-2-aux23 )
))

(disable bad-for-pigeon-2)     (disable pigeon-2-kludge)
(disable pigeon-2-aux1) (disable pigeon-2-aux2)
(disable pigeon-2-aux3) (disable pigeon-2-aux4)
(disable pigeon-2-aux5) (disable pigeon-2-aux6)
(disable pigeon-2-aux7) (disable pigeon-2-aux8)
(disable pigeon-2-aux9) (disable pigeon-2-aux10)
(disable pigeon-2-aux11) (disable pigeon-2-aux12)
(disable pigeon-2-aux13) (disable pigeon-2-aux14)
(disable pigeon-2-aux15) (disable pigeon-2-aux16)
(disable pigeon-2-aux17) (disable pigeon-2-aux18)
(disable pigeon-2-aux19) (disable pigeon-2-aux20)
(disable pigeon-2-aux21) (disable pigeon-2-aux22)
(disable pigeon-2-aux23)




;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;                 FUNCTIONS AND HOMOGENEOUS SETS                         ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; view every S-expression as an association list, and hence a function

(defn funcall (g x) (cadr (assoc x g)))

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

(defn range (g) (if (nlistp g)
	(list 0)
	(cons (cadar g) (range (cdr g)))  ))

(prove-lemma range-is-big-enuf (rewrite) (member (funcall g x) (range g)))

(disable range)
; we don't care exactly what it is

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

(defn mapsto (g set1 set2) (if (nlistp set1)
	T
	(and
		(mapsto g (cdr set1) set2)
		(member (funcall g (car set1)) set2) ) ))

(prove-lemma mapsto-works (rewrite) (implies
	(and (mapsto g set1 set2) (member x set1))
	(member (funcall g x) set2) ))

(disable mapsto)

;;;;;;;;;;;;;;;;;;;;;;;;
; let's disable some ordinal stuff which seems to slow down the set proofs
(disable numbers-below-omega)
(disable cdrs-are-ordinals)
(disable ord-leq-zero)
(disable ord-leq-is-transitive)


;;;;;;;;;;;;  notion of homogeneous

; (homp set g n) means that  set is homogeneous for g as a partition
; of n-tuple