(include-book "ordinals/ordinals" :dir :system)

(defthm small-dividend-non-int-quotient
 (implies (and (integerp n) (posp d)
	       (< n d)
	       (< 0 n))
	  (not (integerp (* (/ d) n))))
 :hints (("Goal" :cases ((and (< 0 (* (/ d) n)) (< (* (/ d) n) 1))))))

(defthm if-num-ge-dem-then-quotient-ge-one
 (implies (and (rationalp r)
	       (>= (numerator r) (denominator r)))
	  (<= 1 (/ (numerator r) (denominator r))))
 :hints (("Goal" :in-theory (disable rational-implies2))))

(defthm if-num-ge-dem-then-ge
 (implies (and (rationalp r)
	       (>= (numerator r) (denominator r)))
	  (<= 1 r))
 :hints (("Goal" :cases ((<= 1 (/ (numerator r) (denominator r)))))
	 ("Subgoal 2" :in-theory (disable rational-implies2))))

(defthm if-less-one-then-num-less-dem
 (implies
  (and (rationalp r)
       (< r 1))
  (< (numerator r) (denominator r))))

(defthm nniq-same-after-scale
 (implies (and (natp n) (posp d)
	       (rationalp s)
	       (natp (* n s)) (posp (* d s)))
	  (equal (nonnegative-integer-quotient (* n s) (* d s))
		 (nonnegative-integer-quotient n d)))
 :hints (("Goal" :cases ((not (< 0 s))))
	 ("Subgoal 2'" :induct t)))

(defthm ratio-one-implies-equal
 (implies (and (rationalp a) (rationalp b)
	       (not (equal b 0))
	       (equal (* a (/ b)) 1))
	  (equal (equal a b) t)))

(defthm den-ito-num-ratio
 (implies (and (posp n) (posp d))
	  (equal (* d (/ (numerator (* (/ d) n)) n)
		    (/ (denominator (* (/ d) n)))) 1))
 :rule-classes ((:rewrite :corollary
			  (implies (and (posp n) (posp d))
				   (equal (* d (/ n) (numerator (* (/ d) n)))
					  (denominator (* (/ d) n))))
		:hints (("Goal" :in-theory (disable rational-implies2))))))

(defthmd rewrite-nniq-of-reduced-factor-num-pos
 (implies (and (posp n) (posp d))
	  (equal (nonnegative-integer-quotient (numerator (* (/ d) n))
					       (denominator (* (/ d) n)))
		 (nonnegative-integer-quotient
		  (* n (/ (numerator (* (/ d) n)) n))
		  (* d (/ (numerator (* (/ d) n)) n))))))


(defthm nniq-same-after-reduce-num-pos
 (implies (and (posp n) (posp d))
	  (equal (nonnegative-integer-quotient (numerator (* (/ d) n))
					       (denominator (* (/ d) n)))
		 (nonnegative-integer-quotient n d)))
 :hints (("Goal" :use ((:instance rewrite-nniq-of-reduced-factor-num-pos)
		       (:instance nniq-same-after-scale
				  (s (/ (numerator (* (/ d) n)) n)))))))

(defthm rewrite-floor-to-nniq
 (implies (and (natp n) (posp d))
	  (equal (floor n d) (nonnegative-integer-quotient n d))))

(defun floor-log-b (b n)
  (cond ((zp b) 0)
	((= b 1) 0)
	((< (nfix n) b) 0)
	(t (+ 1 (floor-log-b b (floor n b))))))

(defthm bound-nniq-times-b
 (implies (and (natp n)
	       (natp b))
	  (<= (* b (nonnegative-integer-quotient n b)) n)))

(defthmd nonlinear-multi-ineq-1
 (implies (and (natp b)
	       (natp b2)
	       (natp a)
	       (>= a 0)
	       (<= b2 b))
	  (<= (* a b2) (* a b))))

(defthmd nonlinear-multi-ineq-2
 (implies (and (natp a) (natp b) (natp b2)
	       (<= (* a b) n)
	       (>= a 0)
	       (<= b2 b))
	  (<= (* a b2) n))
 :hints (("Goal" :use (:instance nonlinear-multi-ineq-1)
	  :in-theory (theory 'minimal-theory))))

(defthm nniq-ordering-lemma-1
 (implies (and (natp n)
	       (natp b)
	       (natp k)
	       (<= 2 b)
	       (<= k (nonnegative-integer-quotient n b)))
	  (<= (* b k) n))
 :hints (("Goal" :use ((:instance bound-nniq-times-b)
		       (:instance nonlinear-multi-ineq-2 (a b)
				  (b2 k)
				  (b (nonnegative-integer-quotient n b)))
		       (:theorem (natp (nonnegative-integer-quotient n b))))
	  :in-theory (theory 'minimal-theory)
	  :do-not-induct t)
	 ("Subgoal 2''" :in-theory (current-theory :here))
	 ("Subgoal 1" :in-theory (current-theory :here))))

(defthm b-to-the-floor-log-bound
 (implies (and (posp n)
	       (integerp b)
	       (<= 2 b))
	  (<= (expt b (floor-log-b b n)) n)))

(defthm not-less-divisor-then-quotient-positive
 (implies (and (posp d)
	       (>= n d)
	       (integerp n))
	  (> (nonnegative-integer-quotient n d)
	     0)))

(defthm first-coeff-is-positive
 (implies (and (<= 2 b)
	       (integerp b)
	       (posp n))
	  (> (nonnegative-integer-quotient n (expt b (floor-log-b b n)))
	     0))
 :hints (("Goal" :use ((:instance not-less-divisor-then-quotient-positive
				  (d (expt b (floor-log-b b n))))
		       (:instance b-to-the-floor-log-bound))
	  :in-theory (disable not-less-divisor-then-quotient-positive
			      b-to-the-floor-log-bound)
	  :do-not-induct t)))

(defthm b-to-the-floor-log-b-is-pos
 (implies (posp b)
	  (posp (expt b (floor-log-b b n))))
 :rule-classes (:type-prescription))

(defthm base-b-progress-lemma-nniq
 (implies
  (and (integerp b)
       (<= 2 b)
       (integerp n)
       (<= b n))
  (< (+ n
	 (- (* (expt b (floor-log-b b n))
	       (nonnegative-integer-quotient n (expt b (floor-log-b b n))))))
      n))
 :hints (("Goal" :do-not-induct t
	  :use (:instance first-coeff-is-positive))))

(in-theory (disable floor))

(defun natural-induction (n)
  (if (zp n) nil (natural-induction (- n 1))))

(defthm cancel-product-inside-nniq
 (implies (and (posp a)
	       (natp b))
	  (equal (nonnegative-integer-quotient (* a b) a)
		 b))
 :hints (("Goal" :induct (natural-induction b))))

(defthm increment-divide-bound
 (implies (and (integerp b)
	       (<= 2 b)
	       (posp n))
	  (<= (+ 1 (nonnegative-integer-quotient n b)) n)))

(defthm floor-log-b-less-than-ident
 (implies (and (integerp b)
	       (<= 2 b)
	       (posp n))
	  (< (floor-log-b b n) n))
 :hints (("Subgoal *1/5''" :use (:instance increment-divide-bound)
	  :in-theory (disable increment-divide-bound))))

(defun hered-base-b-ordinal-make (b n)
  (cond ((< (nfix b) 2) 0)
	((< (nfix n) b) n)
	(t (let* ((power (floor-log-b b n))
		  (coeff (nonnegative-integer-quotient n (expt b power)))
		  (remain (- n (* coeff (expt b power)))))
	     (make-ord (hered-base-b-ordinal-make b power) coeff
		       (hered-base-b-ordinal-make b remain))))))

(defthm hered-base-b-ordinal-make-zero-only-if-n-is
 (implies (and (natp n) (integerp b) (<= 2 b))
	  (equal (equal (hered-base-b-ordinal-make b n) 0)
		 (equal n 0))))

(defthm floor-log-b-not-zero-if-n-bigger-than-b
 (implies (and (natp n)
	       (integerp b)
	       (<= 2 b)
	       (<= b n))
	  (not (equal (floor-log-b b n) 0))))

(defthm first-expt-of-hbb-ord-make
 (implies (and (natp n)
	       (integerp b)
	       (<= 2 b))
	  (equal (o-first-expt (hered-base-b-ordinal-make b n))
		 (hered-base-b-ordinal-make b (floor-log-b b n)))))

(defthm dividing-positive-by-two-or-more-is-less
 (implies (and (posp n)
	       (natp d)
	       (<= 2 d))
	  (< (nonnegative-integer-quotient n d)
	     n)))

(defthm coeff-progress-lemma
 (implies (and (integerp b) (<= 2 b)
	       (natp n)
	       (<= b n))
	  (< (nonnegative-integer-quotient n (expt b (floor-log-b b n)))
	     n)))

(defun dual-hered-ordering-induction (b n1 n2)
  (cond ((< (nfix b) 2) nil)
	((< (nfix n1) b) nil)
	((< (nfix n2) b) nil)
	(t (let* ((power1 (floor-log-b b n1))
		  (power2 (floor-log-b b n2))
		  (coeff1 (nonnegative-integer-quotient n1 (expt b power1)))
		  (coeff2 (nonnegative-integer-quotient n2 (expt b power2)))
		  (remain1 (- n1 (* coeff1 (expt b power1))))
		  (remain2 (- n2 (* coeff2 (expt b power2)))))
	     (list (dual-hered-ordering-induction b power1 power2)
		   (dual-hered-ordering-induction b coeff1 coeff2)
		   (dual-hered-ordering-induction b remain1 remain2))))))

(defun dual-floor-log-b-induction (b n1 n2)
  (cond ((zp b) nil)
	((equal b 1) nil)
	((< (nfix n1) b) nil)
	((< (nfix n2) b) nil)
	(t (dual-floor-log-b-induction b (floor n1 b) (floor n2 b)))))

(defun dual-nniq-induction (n1 n2 d)
  (cond ((equal (nfix d) 0) nil)
	((< (ifix n1) d) nil)
	((< (ifix n2) d) nil)
	(t (dual-nniq-induction (- n1 d) (- n2 d) d))))

(defthm nniq-monotonic-in-n
 (implies (and (natp n1) (natp n2)
	       (<= n1 n2)
	       (posp b))
	  (<= (nonnegative-integer-quotient n1 b)
	      (nonnegative-integer-quotient n2 b)))
 :hints (("Goal" :induct (dual-nniq-induction n1 n2 b))))

(defthm floor-log-b-monotonic-in-n
 (implies (and (natp n1) (natp n2)
	       (<= n1 n2)
	       (integerp b)
	       (<= 2 b))
	  (<= (floor-log-b b n1)
	      (floor-log-b b n2)))
 :hints (("Goal" :induct (dual-floor-log-b-induction b n1 n2))))

(defthm floor-log-b-equality-from-monotonic
 (implies (and (natp n1) (natp n2)
	       (< n1 n2)
	       (integerp b)
	       (<= (floor-log-b b n2)
		   (floor-log-b b n1))
	       (<= 2 b))
	  (equal (floor-log-b b n1)
		 (floor-log-b b n2)))
 :hints (("Goal" :use (floor-log-b-monotonic-in-n)
	  :do-not-induct t :in-theory (disable floor-log-b-monotonic-in-n))))

(defthm nniq-equality-from-monotonic
 (implies (and (<= (nonnegative-integer-quotient n2 b)
		   (nonnegative-integer-quotient n1 b))
	       (natp n1) (natp n2)
	       (< n1 n2)
	       (posp b))
	  (equal (equal (nonnegative-integer-quotient n1 b)
			(nonnegative-integer-quotient n2 b)) t))
 :hints (("Goal" :use (nniq-monotonic-in-n)
	  :do-not-induct t :in-theory (disable nniq-monotonic-in-n))))

(defthm remain-monotonic
 (implies (and (natp n1) (natp n2)
	       (< n1 n2)
	       (integerp p)
	       (equal q1 q2))
	  (< (+ n1 (- (* p q1)))
	     (+ n2 (- (* p q2))))))
 
(defthm hbb-ord-make-monotonic
 (implies (and (natp n1) (natp n2)
	       (< n1 n2)
	       (integerp b)
	       (<= 2 b))
	  (o< (hered-base-b-ordinal-make b n1)
	      (hered-base-b-ordinal-make b n2)))
 :hints (("Goal" :induct (dual-hered-ordering-induction b n1 n2))))

(defthm remainder-less-than-divisor
 (implies (and (natp n)
	       (posp k))
	  (< (+ n (- (* k (nonnegative-integer-quotient n k))))
	     k)))

(defun b-n-logn-induction (b n logn)
  (cond ((< (nfix b) 2) nil)
	((zp n) nil)
	((zp logn) nil)
	(t (b-n-logn-induction b (nonnegative-integer-quotient n b)
			       (+ -1 logn)))))

(defthm if-less-than-expt-then-floor-log-less-log
 (implies (and (natp n)
	       (integerp b)
	       (<= 2 b)
	       (posp k)
	       (< n (expt b k)))
	  (< (floor-log-b b n) k))
 :hints (("Goal" :induct (b-n-logn-induction b n k))))
	       
(defthm hered-base-b-ordinal-make-o-p
 (implies (and (natp n) (integerp b) (<= 2 b))
	  (o-p (hered-base-b-ordinal-make b n))))

(defun ordinal-to-num (b ord)
  (cond ((not (o-p ord)) 0)
	((o-finp ord) ord)
	(t (let ((power (o-first-expt ord))
		 (coeff (o-first-coeff ord))
		 (rest (o-rst ord)))
	     (+ (* coeff (expt b (ordinal-to-num b power)))
		(ordinal-to-num b rest))))))

(defthm ordinal-to-num-is-nat
 (implies (and (posp b) (o-p ord))
	  (natp (ordinal-to-num b ord)))
 :rule-classes (:rewrite :type-prescription))

(defthm ord-to-num-hbb-ord-make-identity
 (implies (and (natp n) (integerp b) (<= 2 b))
	  (equal (ordinal-to-num b (hered-base-b-ordinal-make b n))
		 n)))

(defun goodstein-ord-step (b ord)
  (hered-base-b-ordinal-make b (+ -1 (ordinal-to-num b ord))))

(defun ord-max-int (ord)
  (cond ((not (o-p ord)) 0)
	((o-finp ord) ord)
	(t (max (ord-max-int (o-first-expt ord))
		(max (o-first-coeff ord)
		     (ord-max-int (o-rst ord)))))))

(defthm ord-max-int-is-nat
 (natp (ord-max-int ord))
 :rule-classes (:rewrite :type-prescription))

(defthm mult-by-pos-is-still-greater
 (implies (and (< n b)
	       (posp b)
	       (posp x))
	  (< n (* b x)))
 :hints (("Goal" :cases ((<= b (* b x))))))

(defthm random-weird-equality-ordering-lemma
 (implies (and (<= b n)
	       (not (posp (+ (- b) n)))
	       (integerp n)
	       (posp b)
	       (rationalp x)
	       (< 1 x))
	  (< n (* b x)))
 :hints (("Goal" :cases ((= b n)))))

(defthm nniq-monotonic-step-by-one
 (implies (and (posp n)
	       (integerp b)
	       (<= 2 b)
	       (posp x)
	       (< (nonnegative-integer-quotient n b)
		  x))
	  (< (nonnegative-integer-quotient (+ -1 n) b)
	     x))
 :hints (("Goal" :use (:instance nniq-monotonic-in-n (n1 (- n 1)) (n2 n))
	  :in-theory (disable nniq-monotonic-in-n)
	  :do-not-induct t)))

(defthm nniq-ordering-preserved-after-mult-by-denom
 (implies (and (posp n) (integerp b) (<= 2 b) (posp x)
	       (< (nonnegative-integer-quotient n b) x))
	  (< n (* b x)))
 :hints (("Goal" :induct (natural-induction n))))

(defthm b-to-the-floor-log-other-bound
 (implies (and (posp n) (integerp b) (<= 2 b))
	  (< n (* b (expt b (floor-log-b b n))))))

(defthm cancellation-argument-1
 (implies (and (rationalp n) (rationalp b)
	       (rationalp a) (< 1 a) (rationalp q)
	       (<= q (/ n a))
	       (< n (* b a)))
	  (< q b))
 :hints (("Goal''" :cases ((< (* a q) (* a b))))))

(defthm n-over-1-is-n-nniq
 (implies (natp n)
	  (equal (nonnegative-integer-quotient n 1)
		 n)))

(defthm if-less-product-then-nniq-less-factor
 (implies (and (posp n) (posp b) (posp d)
	       (< n (* b d)))
	  (< (nonnegative-integer-quotient n d) b))
 :hints (("Goal" :cases ((<= (nonnegative-integer-quotient n d) (/ n d)))
	  :do-not-induct t)
	 ("Subgoal 1'" :use (:instance cancellation-argument-1
				       (q (nonnegative-integer-quotient n d))
				       (a d))
	  :in-theory (disable cancellation-argument-1))))

(in-theory (disable cancellation-argument-1
		    random-weird-equality-ordering-lemma))

(defthm coeff-acl2-count-less-ord
 (implies (posp coeff)
	  (< coeff (acl2-count (make-ord expt coeff rest))))
 :hints (("Goal" :in-theory (enable make-ord))))

(defthm make-ord-monotonic-3
 (implies (and (o-p ord1) (o-p ord2)
	       (o<= (o-first-expt ord1) (o-first-expt ord2))
	       (o<= (o-first-coeff ord1) (o-first-coeff ord2))
	       (o<= (o-rst ord1) (o-rst ord2)))
	  (o<= ord1 ord2)))

(defun dual-ord-struct-induction (ord1 ord2)
  (cond ((not (o-p ord1)) nil)
	((not (o-p ord2)) nil)
	((and (o-finp ord1) (o-finp ord2) nil))
	((o-finp ord1) nil)
	((o-finp ord2) nil)
	(t (let* ((expt1 (o-first-expt ord1))
		  (expt2 (o-first-expt ord2))
		  (coeff1 (o-first-coeff ord1))
		  (coeff2 (o-first-coeff ord2))
		  (rest1 (o-rst ord1))
		  (rest2 (o-rst ord2)))
	     (list (dual-ord-struct-induction expt1 expt2)
		   (dual-ord-struct-induction coeff1 coeff2)
		   (dual-ord-struct-induction rest1 rest2))))))

(defthm push-ord-max-int-through-make-ord
 (implies (and (< (ord-max-int ord) b)
	       (o-p ord))
	  (and (< (ord-max-int (o-first-expt ord)) b)
	       (< (ord-max-int (o-first-coeff ord)) b)
	       (< (ord-max-int (o-rst ord)) b)))
 :rule-classes (:rewrite :linear :forward-chaining))
  
(defthm b-to-the-pos-at-least-b
 (implies (and (posp b)
	       (posp power))
	  (<= b (expt b power))))

(defthm product-of-three-ordering-lemma-1
 (implies (and (< 1 a)
	       (< 1 b)
	       (< 0 c)
	       (rationalp a)
	       (rationalp b)
	       (rationalp c))
	  (< c (* (* a b) c)))
 :hints (("Goal" :in-theory (disable associativity-of-* commutativity-of-*)))
 :rule-classes
 ((:rewrite
   :corollary
   (implies (and (< 1 a)
		 (< 1 b)
		 (< 0 c)
		 (rationalp a)
		 (rationalp b)
		 (rationalp c))
	    (< c (* a b c))))))

(defthm product-of-three-ordering-lemma-1-weak
 (implies (and (<= 1 a)
	       (<= 1 b)
	       (< 0 c)
	       (rationalp a)
	       (rationalp b)
	       (rationalp c))
	  (<= c (* a b c)))
 :hints (("Goal" :cases ((and (equal a 1) (equal b 1))
			 (and (< 1 a) (equal b 1))
			 (and (equal a 1) (< 1 b))
			 (and (< 1 a) (< 1 b))))
	 ("Subgoal 1'" :use (:instance product-of-three-ordering-lemma-1)
	  :in-theory (disable product-of-three-ordering-lemma-1))))

(defthm increase-and-mult-by-gt-1-is-increase
 (implies (and (<= b b2)
	       (< 0 b)
	       (rationalp b) (rationalp b2)
	       (rationalp coeff)
	       (< 1 coeff))
	  (<= b (* (/ b2 b) coeff b)))
 :hints (("Goal" :use (:instance product-of-three-ordering-lemma-1-weak
				 (c b) (a (/ b2 b)) (b coeff))))
 :rule-classes
 ((:rewrite
   :corollary
 (implies (and (<= b b2)
	       (< 0 b)
	       (rationalp b) (rationalp b2)
	       (rationalp coeff)
	       (< 1 coeff))
	  (<= b (* b2 coeff))))))

(defthm increase-and-mult-by-gt-1-is-increase-c
 (implies (and (<= b b2)
	       (< 0 b)
	       (rationalp b) (rationalp b2)
	       (rationalp coeff)
	       (< 1 coeff))
	  (<= b (* coeff b2))))
  
(defthm non-last-digit-at-least-base
 (implies (and (posp b)
	       (posp coeff)
	       (posp power))
	  (<= b (* coeff (expt b power))))
 :hints (("Goal" :cases ((<= b (expt b power)))
	  :do-not-induct t)
	 ("Subgoal 1" :in-theory (disable b-to-the-pos-at-least-b))
	 ("Subgoal 1'" :use (:instance increase-and-mult-by-gt-1-is-increase-c
				       (b2 (expt b power))))))

(defthm ord-to-num-monotonic-case-expt-and-coeff-equal
 (implies (and (o-p ord1) (o-p ord2)
	       (o<= (o-first-expt ord2) (o-first-expt ord1))
	       (o<= (o-first-coeff ord2) (o-first-coeff ord1))
	       (< (ordinal-to-num b (o-rst ord1))
		  (ordinal-to-num b (o-rst ord2)))
	       (o< ord1 ord2))
	  (< (+ (ordinal-to-num b (o-rst ord1))
		(* (o-first-coeff ord1)
		   (expt b
			 (ordinal-to-num b (o-first-expt ord1)))))
	     (+ (ordinal-to-num b (o-rst ord2))
		(* (o-first-coeff ord2)
		   (expt b
			 (ordinal-to-num b (o-first-expt ord2))))))))

(defthm fc-from-ord-max-to-coeff-bound
 (implies (and (< (ord-max-int ord) b)
	       (o-p ord)
	       (posp b))
	  (< (o-first-coeff ord) b))
 :rule-classes (:rewrite :forward-chaining :linear))

(defthm fc-from-ord-max-to-second-expt-bound
 (implies (and (< (ord-max-int ord) b)
	       (o-p ord)
	       (posp b))
	  (< (ord-max-int (o-first-coeff (o-rst ord))) b))
 :rule-classes (:rewrite :forward-chaining))

(defthm expt-increasing-w-times-b
 (implies (and (< n (* b (expt b e1)))
	       (natp e1) (natp e2) (integerp b) (<= 2 b) (natp n)
	       (< e1 e2))
	  (< n (expt b e2)))
 :hints (("Goal" :cases ((equal e2 (+ 1 e1)) (< (+ 1 e1) e2)))
	 ("Subgoal 1" :use (:instance expt-is-increasing-for-base>1
				      (r b) (i (+ 1 e1)) (j e2))))
 :rule-classes (:rewrite :forward-chaining))
	       
(defthm ord-to-num-rest-less-than-expt-induct-step
 (implies (and (o-p ord) (not (o-finp ord))
	       (integerp b) (<= 2 b)
	       (< (ordinal-to-num b (o-first-expt (o-rst ord)))
		  (ordinal-to-num b (o-first-expt ord)))
	       (< (ordinal-to-num b (o-rst ord))
		  (* b (expt b (ordinal-to-num b (o-first-expt 
						  (o-rst ord)))))))
	  (< (ordinal-to-num b (o-rst ord))
	     (expt b (ordinal-to-num b (o-first-expt ord))))))

(defthmd random-linear-lemma-1
 (implies (and (posp exp) (natp c1)
	       (integerp c2) (< c1 c2)
	       (< rest exp))
	  (<= (+ exp (* c1 exp))
	      (* c2 exp)))
 :hints	(("Goal" :use (:instance *-preserves->=-for-nonnegatives
				 (x2 (+ 1 c1)) (x1 c2)
				 (y1 exp) (y2 exp)))))

(defthm one-digit-ordering-lemma
 (implies (and (natp exp) (natp rest) (natp coeff)
	       (integerp b) (<= 2 b) (< coeff b)
	       (< rest (expt b exp)))
	  (< (+ rest (* coeff (expt b exp)))
	     (* b (expt b exp))))
 :hints (("Goal" :use (:instance random-linear-lemma-1
				 (c1 coeff) (c2 b) (exp (expt b exp))))))

(defthm order-by-first-digit-lemma
 (implies (and (natp coeff1) (natp coeff2)
	       (natp rest1) (natp rest2)
	       (posp exp)
	       (< coeff1 coeff2)	       
	       (< rest1 exp)
	       (< rest2 exp))
	  (< (+ rest1 (* coeff1 exp))
	     (+ rest2 (* coeff2 exp))))
 :hints (("Goal" :use (:instance *-preserves->=-for-nonnegatives
				 (x2 (+ 1 coeff1)) (x1 coeff2)
				 (y1 exp) (y2 exp)))))

(defthm one-digit-lower-bound-lemma
 (implies (and (posp coeff)
	       (natp rest)
	       (< coeff b)
	       (integerp b) (<= 2 b)
	       (natp exp)
	       (< rest (expt b exp)))
	  (<= (expt b exp) (+ rest (* coeff (expt b exp)))))
 :hints (("Goal" :cases ((<= (expt b exp) (* coeff (expt b exp)))))))


(defthm order-by-num-digits-lemma
 (implies (and (posp coeff1) (posp coeff2)
	       (natp rest1) (natp rest2)
	       (< coeff1 b) (< coeff2 b)
	       (integerp b) (<= 2 b)
	       (natp exp1) (natp exp2)
	       (< rest1 (expt b exp1))
	       (< rest2 (expt b exp2))
	       (< exp1 exp2))
	  (< (+ rest1 (* coeff1 (expt b exp1)))
	     (+ rest2 (* coeff2 (expt b exp2)))))
 :hints (("Goal" :cases ((equal exp2 (+ 1 exp1)) (< (+ 1 exp1) exp2)))
	 ("Subgoal 2"
	  :cases ((not (and (< (+ rest1 (* coeff1 (expt b exp1)))
			       (expt b (+ 1 exp1)))
			    (<= (expt b exp2)
				(+ rest2 (* coeff2 (expt b exp2)))))))
	  :do-not-induct t)
	 ("Subgoal 2.1"
	  :use (:instance one-digit-lower-bound-lemma
			  (rest rest2) (coeff coeff2) (exp (+ 1 exp1))))
	 ("Subgoal 1"
	  :cases ((not (and (< (+ rest1 (* coeff1 (expt b exp1)))
			       (expt b (+ 1 exp1)))
			    (<= (expt b exp2)
				(+ rest2 (* coeff2 (expt b exp2))))
			    (< (expt b (+ 1 exp1)) (expt b exp2)))))
	  :do-not-induct t)
	 ("Subgoal 1.1"
	  :use (:instance expt-is-increasing-for-base>1
			  (r b) (i (+ 1 exp1)) (j exp2)))
	 ))

(defthm ord-to-num-monotonic-case-different-exponent
 (implies (and (o-p ord1) (o-p ord2)
	       (not (o-finp ord1))
	       (o< ord1 ord2)
	       (integerp b) (<= 2 b)
	       (< (o-first-coeff ord1) b)
	       (< (o-first-coeff ord2) b)
	       (< (ordinal-to-num b (o-first-expt ord1))
		  (ordinal-to-num b (o-first-expt ord2)))
	       (< (ordinal-to-num b (o-first-expt (o-rst ord1)))
		  (ordinal-to-num b (o-first-expt ord1)))
	       (< (ordinal-to-num b (o-first-expt (o-rst ord2)))
		  (ordinal-to-num b (o-first-expt ord2)))
	       (< (ordinal-to-num b (o-rst ord1))
		  (* b
		     (expt b
			   (ordinal-to-num b (o-first-expt (o-rst ord1))))))
	       (< (ordinal-to-num b (o-rst ord2))
		  (* b
		     (expt b
			   (ordinal-to-num b (o-first-expt (o-rst ord2)))))))
	  (< (+ (ordinal-to-num b (o-rst ord1))
		(* (o-first-coeff ord1)
		   (expt b
			 (ordinal-to-num b (o-first-expt ord1)))))
	     (+ (ordinal-to-num b (o-rst ord2))
		(* (o-first-coeff ord2)
		   (expt b
			 (ordinal-to-num b (o-first-expt ord2))))))))

(defun ord-to-num-on-structure (b ord)
  (cond ((not (o-p ord)) nil)
	((o-finp ord) t)
	(t (and (< (ordinal-to-num b (o-first-expt (o-rst ord)))
		   (ordinal-to-num b (o-first-expt ord)))
		(ord-to-num-on-structure b (o-first-expt ord))
		(ord-to-num-on-structure b (o-rst ord))))))

(defthm ord-to-num-bound-given-structure
 (implies (and (integerp b) (<= 2 b)
	       (o-p ord)
	       (ord-to-num-on-structure b ord)
	       (< (ord-max-int ord) b))
	  (< (ordinal-to-num b ord)
	     (* b (expt b (ordinal-to-num b (o-first-expt ord)))))))

(defthm ord-to-num-monotonic-case-same-exponent
 (implies (and (o-p ord1) (o-p ord2)
	       (not (o-finp ord1))
	       (o< ord1 ord2)
	       (integerp b) (<= 2 b)
	       (< (ord-max-int ord1) b)
	       (< (ord-max-int ord2) b)
	       (ord-to-num-on-structure b ord1)
	       (ord-to-num-on-structure b ord2)
	       (o<= (o-first-expt ord2) (o-first-expt ord1))
	       (< (o-first-coeff ord1) (o-first-coeff ord2)))
	  (< (+ (ordinal-to-num b (o-rst ord1))
		(* (o-first-coeff ord1)
		   (expt b
			 (ordinal-to-num b (o-first-expt ord1)))))
	     (+ (ordinal-to-num b (o-rst ord2))
		(* (o-first-coeff ord2)
		   (expt b
			 (ordinal-to-num b (o-first-expt ord2)))))))
 :hints (("Goal" :use ((:instance ord-to-num-rest-less-than-expt-induct-step
				  (ord ord1))
		       (:instance ord-to-num-rest-less-than-expt-induct-step
				  (ord ord2))))))

(defthm have-non-last-digit-then-at-least-base
 (implies (and (natp rest) (posp coeff) (posp exp)
	       (integerp b) (<= 2 b))
	  (<= b (+ rest (* coeff (expt b exp)))))
 :hints (("Goal" :cases ((<= b (* coeff (expt b exp)))))))

(defthm ord-to-num-of-infinite-at-least-base
 (implies (and (o-p ord)
	       (not (o-finp ord))
	       (integerp b) (<= 2 b))
	  (<= b (ordinal-to-num b ord))))

(defthm ord-to-num-monotonic-case-ord1-finite
 (implies (and (natp ord1)
	       (o-p ord2)
	       (integerp b) (<= 2 b)
	       (o< ord1 ord2)
	       (< ord1 b)
	       (< (ord-max-int ord2) b)
	       (ord-to-num-on-structure b ord2))
	  (< ord1 (ordinal-to-num b ord2)))
 :hints (("Goal" :cases ((o-finp ord2) (o<= 1 (o-first-expt ord2))))
	 ("Subgoal 1" :use (:instance ord-to-num-of-infinite-at-least-base
				      (ord ord2))
	  :in-theory (disable ord-to-num-of-infinite-at-least-base))))

(defthm ord-to-num-monotonic-case-different-exponent-2
 (implies (and (o-p ord1)
	       (o-p ord2)
	       (not (o-finp ord1))
	       (< (ordinal-to-num b (o-first-expt ord1))
		  (ordinal-to-num b (o-first-expt ord2)))
	       (integerp b) (<= 2 b)
	       (o< ord1 ord2)
	       (< (o-first-coeff ord1) b)
	       (< (o-first-coeff ord2) b)
	       (< (ord-max-int (o-rst ord1)) b)
	       (< (ord-max-int (o-rst ord2)) b)
	       (< (ordinal-to-num b (o-first-expt (o-rst ord1)))
		  (ordinal-to-num b (o-first-expt ord1)))
	       (ord-to-num-on-structure b (o-first-expt ord1))
	       (ord-to-num-on-structure b (o-rst ord1))
	       (< (ordinal-to-num b (o-first-expt (o-rst ord2)))
		  (ordinal-to-num b (o-first-expt ord2)))
	       (ord-to-num-on-structure b (o-first-expt ord2))
	       (ord-to-num-on-structure b (o-rst ord2)))
	  (< (+ (ordinal-to-num b (o-rst ord1))
		(* (o-first-coeff ord1)
		   (expt b (ordinal-to-num b (o-first-expt ord1)))))
	     (+ (ordinal-to-num b (o-rst ord2))
		(* (o-first-coeff ord2)
		   (expt b (ordinal-to-num b (o-first-expt ord2))))))))

(defthm ord-to-num-monotonic-given-structure
 (implies (and (integerp b) (<= 2 b)
	       (o-p ord1) (o-p ord2)
	       (o< ord1 ord2)
	       (< (ord-max-int ord1) b)
	       (< (ord-max-int ord2) b)
	       (ord-to-num-on-structure b ord1)
	       (ord-to-num-on-structure b ord2))
	  (< (ordinal-to-num b ord1) (ordinal-to-num b ord2)))
 :hints (("Goal" :induct (dual-ord-struct-induction ord1 ord2))))

(defun ordinal-structural-induction (ord)
  (cond ((not (o-p ord)) nil)
	((o-finp ord) nil)
	(t (list (ordinal-structural-induction (o-first-expt ord))
		 (ordinal-structural-induction (o-rst ord))))))

(defthm ord-structure-given-bound
 (implies (and (o-p ord)
	       (integerp b) (<= 2 b)
	       (< (ord-max-int ord) b))
	  (ord-to-num-on-structure b ord))
 :hints (("Goal" :induct (ordinal-structural-induction ord))))

(defthm ord-to-num-bound
 (implies (and (integerp b) (<= 2 b)
	       (o-p ord)
	       (< (ord-max-int ord) b))
	  (< (ordinal-to-num b ord)
	     (* b (expt b (ordinal-to-num b (o-first-expt ord)))))))

(defthm ord-to-num-monotonic
 (implies (and (integerp b) (<= 2 b)
	       (o-p ord1) (o-p ord2)
	       (o< ord1 ord2)
	       (< (ord-max-int ord1) b)
	       (< (ord-max-int ord2) b))
	  (< (ordinal-to-num b ord1) (ordinal-to-num b ord2))))

(defthmd ord-to-num-one-to-one
 (implies (and (o-p ord1) (< (ord-max-int ord1) b)
	       (o-p ord2) (< (ord-max-int ord2) b)
	       (integerp b) (<= 2 b)
	       (equal (ordinal-to-num b ord1) (ordinal-to-num b ord2)))
	  (equal (equal ord1 ord2) t))
 :hints (("Goal" :cases ((o< ord1 ord2) (equal ord1 ord2) (o< ord2 ord1)))
	 ("Subgoal 3" :use (:instance ord-to-num-monotonic))
	 ("Subgoal 1" :use (:instance ord-to-num-monotonic
				      (ord1 ord2) (ord2 ord1)))))

(defthm ord-max-of-hbb-make
 (implies (and (natp n)
	       (integerp b) (<= 2 b))
	  (< (ord-max-int (hered-base-b-ordinal-make b n)) b)))

(defthm hbb-ord-make-ord-to-num-identity
 (implies (and (o-p ord) (integerp b) (<= 2 b)
	       (< (ord-max-int ord) b))
	  (equal (hered-base-b-ordinal-make b (ordinal-to-num b ord))
		 ord))
 :hints (("Goal" :use (:instance ord-to-num-one-to-one
				 (ord1 (hered-base-b-ordinal-make
					b (ordinal-to-num b ord)))
				 (ord2 ord)))))

(defthm goodstein-ord-step-decreasing
 (implies (and (integerp b) (<= 2 b)
	       (o-p ord)
	       (o< 0 ord)
	       (< (ord-max-int ord) b))
	  (o< (goodstein-ord-step b ord) ord))
 :hints (("Goal" :use (:instance hbb-ord-make-monotonic
				 (n1 (+ -1 (ordinal-to-num b ord)))
				 (n2 (ordinal-to-num b ord))))))

(defthm goodstein-ord-step-is-o-p
 (implies (and (o-p ord) (integerp b) (<= 2 b) (o< 0 ord))
	  (o-p (goodstein-ord-step b ord))))

(in-theory (disable goodstein-ord-step))

(defun ord-transparent-count (o)
  (if (o-p o) o (acl2-count o)))

(defun goodstein-ord-step-count-help (ord count)  
  (declare (xargs :measure (ord-transparent-count ord)
		  :hints (("Goal" :do-not-induct t))))
  (cond ((not (natp count)) nil)
	((not (o-p ord)) nil)
	((not (< (ord-max-int ord) (+ 3 count))) nil)
	((equal ord 0) count)
	(t
	 (goodstein-ord-step-count-help (goodstein-ord-step (+ 3 count) ord)
					(+ 1 count)))))

(defun goodstein-ord-step-count (n)
  (goodstein-ord-step-count-help
   (hered-base-b-ordinal-make 2 n) 0))