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

Information

namenatural-distance-def
version1.37
descriptionDefinition of natural number distance
authorJoe Leslie-Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2012-08-06
requiresbool
natural-add
natural-order
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.