Package axiom-infinity: axiom-infinity

Information

nameaxiom-infinity
version1.1
descriptionaxiom-infinity
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-07-19
showData.Bool

Files

Theorem

f. Function.injective f ¬Function.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. Function.surjective f y. x. y = f x

() = λP. q. (x. P x q) q

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

let a o
      (let h
           let p r
               let p s
                   (let fo r = o s
                    λg.
                      (let hf
                       λi.
                         (λj. j h i) =
                         λk. k ((λd. d) = λd. d) ((λd. d) = λd. d)) g f)
                     (r = s) ∈
               p = (λq. (λd. d) = λd. d) ∈
           p = (λq. (λd. d) = λd. d) ∈
       λi. (λj. j h i) = λk. k ((λd. d) = λd. d) ((λd. d) = λd. d))
        (let t
             let p u
                 let v yu = o y
                 let b w
                     (let f
                          let p x
                              (let fv x
                               λg.
                                 (let hf
                                  λi.
                                    (λj. j h i) =
                                    λk.
                                      k ((λd. d) = λd. d)
                                        ((λd. d) = λd. d)) g f) w
                          p = (λq. (λd. d) = λd. d) ∈
                      λg.
                        (let hf
                         λi.
                           (λj. j h i) =
                           λk. k ((λd. d) = λd. d) ((λd. d) = λd. d)) g
                        f) w
                 b = (λc. (λd. d) = λd. d) ∈
             p = (λq. (λd. d) = λd. d) ∈
         (let ft
          λg.
            (let hf
             λi. (λj. j h i) = λk. k ((λd. d) = λd. d) ((λd. d) = λd. d))
              g f) (let b ddb = λc. (λd. d) = λd. d)) ∈
  let b e
      (let f
           let l n
               (let fa n
                λg.
                  (let hf
                   λi.
                     (λj. j h i) =
                     λk. k ((λd. d) = λd. d) ((λd. d) = λd. d)) g f) e
           l = (λm. (λd. d) = λd. d) ∈
       λg.
         (let hf
          λi. (λj. j h i) = λk. k ((λd. d) = λd. d) ((λd. d) = λd. d)) g
         f) e
  b = λc. (λd. d) = λd. d