Package natural-order-min-max-def: Definition of natural number min and max functions

Information

namenatural-order-min-max-def
version1.24
descriptionDefinition of natural number min and max functions
authorJoe Leslie-Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2012-07-28
requiresbool
natural-order-thm
showData.Bool
Number.Natural

Files

Defined Constants

Theorems

m n. max m n = if m n then n else m

m n. min m n = if m n then m else n

p. (n. p n) p ((minimal) p) m. m < (minimal) p ¬p m

Input Type Operators

Input Constants

Assumptions

() = λp. p ((select) p)

() = λp. p = λx.

() = λp q. p q p

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

p. (n. p n) n. p n m. m < n ¬p m