Package natural-min-max-def: natural-min-max-def

Information

namenatural-min-max-def
version1.4
descriptionnatural-min-max-def
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-09-21
showData.Bool

Files

Defined Constants

Theorems

m n. Number.Natural.max m n = if Number.Natural.≤ m n then n else m

m n. Number.Natural.min m n = if Number.Natural.≤ m n then m else n

P.
    (n. P n)
    P (Number.Natural.minimal P)
    m. Number.Natural.< m (Number.Natural.minimal P) ¬P m

Input Type Operators

Input Constants

Assumptions

T

() = λP. P ((select) P)

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

x. x = x T

() = λp q. p q p

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

P. (n. P n) n. P n m. Number.Natural.< m n ¬P m