Package relation-well-founded-thm: Properties of well-founded relations

Information

namerelation-well-founded-thm
version1.53
descriptionProperties of well-founded relations
authorJoe Leslie-Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2012-08-06
requiresbool
pair
relation-def
relation-thm
relation-well-founded-def
showData.Bool
Data.Pair
Relation

Files

Theorems

wellFounded empty

r. wellFounded r irreflexive r

r s. subrelation r s wellFounded s wellFounded r

r m. wellFounded r wellFounded (λx y. r (m x) (m y))

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

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

r s.
    wellFounded r wellFounded s
    wellFounded (λ(x1, y1) (x2, y2). r x1 x2 s y1 y2)

r s.
    wellFounded r wellFounded s
    wellFounded (λ(x1, y1) (x2, y2). r x1 x2 x1 = x2 s y1 y2)

r s.
    wellFounded r (a. wellFounded (s a))
    wellFounded (λ(x1, y1) (x2, y2). r x1 x2 x1 = x2 s x1 y1 y2)

Input Type Operators

Input Constants

Assumptions

¬

¬

t. t t

p. p

t. t ¬t

(¬) = λp. p

t. (x. t) t

t. (x. t) t

t. (λx. t x) = t

() = λp. p = λx.

t. ¬¬t t

t. ( t) t

t. t

t. t t

t. t t

t. t

t. t t

t. t

t. t t

t. t

t. t

x y. ¬empty x y

t. ( t) ¬t

t. t ¬t

() = λp q. p q p

t. (t ) (t )

p x. p x p ((select) p)

f y. (let x y in f x) = f y

t1 t2. t1 t2 t2 t1

t1 t2. t1 t2 t2 t1

r. irreflexive r x. ¬r x x

() = λp q. (λf. f p q) = λf. f

p. ¬(x. p x) x. ¬p x

p. ¬(x. p x) x. ¬p x

() = λp. q. (x. p x q) q

t1 t2. ¬(t1 t2) t1 ¬t2

t1 t2. ¬t1 ¬t2 t2 t1

p. (xy. p xy) x y. p (x, y)

() = λp q. r. (p r) (q r) r

f. fn. x y. fn (x, y) = f x y

p q. p (x. q x) x. p q x

p q. p (x. q x) x. p q x

p q. p (x. q x) x. p q x

p q. p (x. q x) x. p q x

p q. (x. p x) q x. p x q

p q. (x. p x) q x. p x q

t1 t2 t3. (t1 t2) t3 t1 t2 t3

p. (x. y. p x y) y. x. p x (y x)

r s. subrelation r s x y. r x y s x y

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