Package relation-well-founded-def: relation-well-founded-def

Information

namerelation-well-founded-def
version1.9
descriptionrelation-well-founded-def
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-09-21
showData.Bool

Files

Defined Constant

Theorem

<<.
    Relation.wellFounded << P. (x. P x) x. P x y. << y x ¬P y

Input Type Operators

Input Constants

Assumptions

T

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