Package axiom: Basic axioms

Information

nameaxiom
version1.3
descriptionBasic axioms
authorJoe Hurd <joe@gilith.com>
licenseMIT
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

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

let a d ← (λe. d e) = da = λb. (λc. c) = λc. c

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

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

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