Package relation-well-founded-def: Definition of well-founded relations

Information

namerelation-well-founded-def
version1.38
descriptionDefinition of well-founded relations
authorJoe Leslie-Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2014-10-30
checksum8dac1adb31a0915d7cf32d96dd58e8b7505c72cd
requiresbool
showData.Bool
Relation

Files

Defined Constant

Theorem

r. wellFounded r p. (x. p x) x. p x y. r y x ¬p y

External Type Operators

External Constants

Assumptions

() = λp. p = λx.