Package natural-distance-def: natural-distance-def

Information

namenatural-distance-def
version1.8
descriptionnatural-distance-def
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-07-18
showData.Bool

Files

Defined Constant

Theorem

m n.
    Number.Natural.distance m n =
    if Number.Natural.≤ m n then Number.Natural.- n m
    else Number.Natural.- m n

Input Type Operators

Input Constants

Assumptions

T

() = λp. p = λx. T