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

Information

Files

• Package tarball relation-well-founded-def-1.7.tgz
• Theory file relation-well-founded-def.thy (included in the package tarball)

Defined Constant

• Relation
  • Relation.wellFounded

Theorem

⊦ ∀<<.
    Relation.wellFounded << ⇔ ∀P. (∃x. P x) ⇒ ∃x. P x ∧ ∀y. << y x ⇒ ¬P y

Input Type Operators

• →
• bool

Input Constants

• =
• Data
  • Bool
    • ∀
    • ∧
    • ⇒
    • ∃
    • ~
    • T

Assumptions

⊦ T

⊦ (∀) = λP. P = λx. T