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

Information

namerelation-well-founded-def
version1.36
descriptionDefinition of well-founded relations
authorJoe Leslie-Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2012-12-02
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.