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