Package relation-natural-def: Definition of relations over natural numbers

Information

namerelation-natural-def
version1.7
descriptionDefinition of relations over natural numbers
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-12-02
requiresbool
showData.Bool
Number.Natural
Relation

Files

Defined Constants

Theorems

m n. isSuc m n suc m = n

m x y. measure m x y m x < m y

Input Type Operators

Input Constants

Assumptions

T

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