Package axiom-infinity: Axiom of Infinity

Information

nameaxiom-infinity
version1.5
descriptionAxiom of Infinity
authorJoe Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2011-12-18
requiresbool
function
showData.Bool
Function

Files

Theorem

f. injective f ¬surjective f

Input Type Operators

Input Constants

Assumptions

T

F p. p

(¬) = λp. p F

T (λp. p) = λp. p

() = λp. p = λx. T

() = λp q. p q p

() = λp q. (λf. f p q) = λf. f T T

f. surjective f y. x. y = f x

() = λp. q. (x. p x q) q

f. injective f x1 x2. f x1 = f x2 x1 = x2

let a o
      (let h
           let p r
               let p s
                   (let f o r = o s in
                    λg.
                      (let h f in
                       λi.
                         (λj. j h i) =
                         λk. k ((λd. d) = λd. d) ((λd. d) = λd. d)) g f)
                     (r = s) in
               p = (λq. (λd. d) = λd. d) in
           p = (λq. (λd. d) = λd. d) in
       λi. (λj. j h i) = λk. k ((λd. d) = λd. d) ((λd. d) = λd. d))
        (let t
             let p u
                 let v y u = o y in
                 let b w
                     (let f
                          let p x
                              (let f v x in
                               λg.
                                 (let h f in
                                  λi.
                                    (λj. j h i) =
                                    λk.
                                      k ((λd. d) = λd. d)
                                        ((λd. d) = λd. d)) g f) w in
                          p = (λq. (λd. d) = λd. d) in
                      λg.
                        (let h f in
                         λi.
                           (λj. j h i) =
                           λk. k ((λd. d) = λd. d) ((λd. d) = λd. d)) g
                        f) w in
                 b = (λc. (λd. d) = λd. d) in
             p = (λq. (λd. d) = λd. d) in
         (let f t in
          λg.
            (let h f in
             λi. (λj. j h i) = λk. k ((λd. d) = λd. d) ((λd. d) = λd. d))
              g f) (let b d d in b = λc. (λd. d) = λd. d)) in
  let b e
      (let f
           let l n
               (let f a n in
                λg.
                  (let h f in
                   λi.
                     (λj. j h i) =
                     λk. k ((λd. d) = λd. d) ((λd. d) = λd. d)) g f) e in
           l = (λm. (λd. d) = λd. d) in
       λg.
         (let h f in
          λi. (λj. j h i) = λk. k ((λd. d) = λd. d) ((λd. d) = λd. d)) g
         f) e in
  b = λc. (λd. d) = λd. d