Package set-finite-def: set-finite-def

Information

nameset-finite-def
version1.9
descriptionset-finite-def
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-07-18
showData.Bool

Files

Defined Constants

Theorems

s. Set.infinite s ¬Set.finite s

Set.finite Set.∅ x s. Set.finite s Set.finite (Set.insert x s)

a. Set.finite a a = Set.∅ x s. a = Set.insert x s Set.finite s

FINITE'.
    FINITE' Set.∅ (x s. FINITE' s FINITE' (Set.insert x s))
    a. Set.finite a FINITE' a

Input Type Operators

Input Constants

Assumptions

T

() = λp. p = λx. T

() = λp q. p q p

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

() = λP. q. (x. P x q) q

() = λp q. r. (p r) (q r) r

P Q. (x. P x Q x) (x. P x) x. Q x

A B C D. (A B) (C D) A C B D

A B C D. (A B) (C D) A C B D