Package axiom: Standard axioms

Information

nameaxiom
version1.11
descriptionStandard axioms
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
requiresbool
function
showData.Bool
Function

Files

Theorems

t. (λx. t x) = t

f. injective f ¬surjective f

p x. p x p ((select) p)

Input Type Operators

Input Constants

Assumptions

p. p

(¬) = λp. p

(λp. p) = λp. p

() = λp. p = λx.

() = λp q. p q p

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

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

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

let a d (λe. d e) = d in a = λb. (λc. c) = λc. c

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

let a d
      let e g
          (let h d g in
           λi.
             (let j h in
              λk. (λl. l j k) = λm. m ((λc. c) = λc. c) ((λc. c) = λc. c))
               i h) (d ((select) d)) in
      e = (λf. (λc. c) = λc. c) in
  a = λb. (λc. c) = λc. c

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