Package natural-distance-def: Definition of natural number distance

Information

namenatural-distance-def
version1.27
descriptionDefinition of natural number distance
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2012-05-18
requiresbool
showData.Bool
Number.Natural

Files

Defined Constant

Theorem

m n. distance m n = if m n then n - m else m - n

Input Type Operators

Input Constants

Assumptions

() = λp. p = λx.