| name | axiom |
| version | 1.3 |
| description | Basic axioms |
| author | Joe Hurd <joe@gilith.com> |
| license | MIT |
| show | Data.Bool Function |
⊦ ∀t. (λx. t x) = t
⊦ ∃f. injective f ∧ ¬surjective f
⊦ ∀p x. p x ⇒ p ((select) p)
⊦ 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) = d ∈ 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 ∈
λi.
(let j ← h ∈
λ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 f ← o r = o s ∈
λg.
(let h ← f ∈
λ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 y ← u = o y ∈
let b w ←
(let f ←
let p x ←
(let f ← v x ∈
λg.
(let h ← f ∈
λ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 h ← f ∈
λ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 f ← t ∈
λg.
(let h ← f ∈
λi. (λj. j h i) = λk. k ((λd. d) = λd. d) ((λd. d) = λd. d))
g ⇔ f) (let b d ← d ∈ b = λc. (λd. d) = λd. d)) ∈
let b e ←
(let f ←
let l n ←
(let f ← a n ∈
λg.
(let h ← f ∈
λ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 h ← f ∈
λi. (λj. j h i) = λk. k ((λd. d) = λd. d) ((λd. d) = λd. d)) g ⇔
f) e ∈
b = λc. (λd. d) = λd. d