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

Information

namenatural-min-max
version1.0
descriptionnatural-min-max
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-02-19
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