| 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 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