| name | axiom-infinity |
| version | 1.1 |
| description | axiom-infinity |
| author | Joe Hurd <joe@gilith.com> |
| license | HOLLight |
| provenance | HOL Light theory extracted on 2011-07-19 |
| show | Data.Bool |
⊦ ∃f. Function.injective f ∧ ¬Function.surjective f
⊦ 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 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