Package relation-well-founded: Well-founded relations

Information

namerelation-well-founded
version1.50
descriptionWell-founded relations
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
requiresbool
pair
relation-def
relation-thm
showData.Bool
Data.Pair
Relation

Files

Defined Constant

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. 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)

External Type Operators

External 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. (x. p x) a b. p (a, b)

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

f. fn. a b. fn (a, b) = f a b

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

r. (x. y. r x y) f. x. r x (f x)

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