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

Information

namerelation-natural-def
version1.20
descriptionDefinition of relations over natural numbers
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2012-08-06
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

() = λp. p = λx.