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

Information

namenatural-distance-def
version1.39
descriptionDefinition of natural number distance
authorJoe Leslie-Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2012-12-02
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

External Type Operators

External Constants

Assumptions

() = λp. p = λx.