Filtering...

limits

books/ordinals/limits

Included Books

ordinal-exponentiation top-with-meta
other
(in-package "ACL2")
include-book
(include-book "ordinal-exponentiation")
local
(local (include-book "top-with-meta"))
limit-+theorem
(defthm limit-+
  (implies (o-p a) (not (limitp (o+ a 1))))
  :hints (("goal" :in-theory (e/d (limitp) (natpart-o-rst)))))
local
(local (in-theory (disable o+)))
|limitp.b => a<b <=> a+1 < b|theorem
(defthm |limitp.b  =>  a<b   <=>  a+1 < b|
  (implies (and (limitp b) (o-p a))
    (equal (o< (o+ a 1) b) (o< a b))))
|limitp.b => c<b <=> a+c+1 < a+b|theorem
(defthm |limitp.b  =>   c<b  <=>  a+c+1 < a+b|
  (implies (and (limitp b) (o-p a) (o-p c))
    (equal (o< (o+ a c 1) (o+ a b)) (o< c b))))
|limitp.b & a < w^b => a < w^[fe.a +1] & [fe.a + 1] < w^b|encapsulate
(encapsulate nil
  (local (defthm |limitp.b &  a < w^b   =>   a < w^[fe.a +1]  &  [fe.a + 1] < w^b :l1|
      (implies (and (not (equal b 0))
          (o-p a)
          (o-p b)
          (o< a (o^ (omega) b)))
        (o< (o-first-expt a) b))
      :hints (("goal" :cases ((o-infp a))))
      :rule-classes :forward-chaining))
  (defthm |limitp.b &  a < w^b   =>   a < w^[fe.a +1]  &  [fe.a + 1] < w^b|
    (implies (and (limitp b) (o-p a) (o< a (o^ (omega) b)))
      (and (o< a (o^ (omega) (o+ (o-first-expt a) 1)))
        (o< (o^ (omega) (o+ (o-first-expt a) 1)) (o^ (omega) b))))
    :rule-classes ((:rewrite :match-free :all))))
o*-o-first-expt-equaltheorem
(defthm o*-o-first-expt-equal
  (implies (and (not (equal a 0))
      (not (equal b 0))
      (equal (o-first-expt a) (o-first-expt b))
      (limitp c)
      (o-p a)
      (o-p b))
    (equal (o* a c) (o* b c)))
  :rule-classes ((:forward-chaining :trigger-terms ((o* a c) (o* b c)))))