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

Information

namerelation-well-founded-thm
version1.30
descriptionProperties of well-founded relations
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-11-27
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))

p g h. f. x. f x = if p x then f (g x) else h x

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

¬F T

¬T F

t. t t

F p. p

t. t ¬t

n. Number.Natural.< 0 (Number.Natural.suc n)

(¬) = λp. p F

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. F t F

t. T t t

t. t F F

t. t T t

t. F t T

t. T t t

t. t T T

t. F t t

t. T t T

t. t F t

t. t T T

m. Number.Natural.< m 0 F

x y. ¬empty x y

t. (F t) ¬t

t. (t F) ¬t

t. t F ¬t

() = λp q. p q p

t. (t T) (t F)

t1 t2. (if F then t1 else t2) = t2

t1 t2. (if T then t1 else t2) = t1

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

m. m = 0 n. m = Number.Natural.suc n

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

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

m n.
    Number.Natural.< (Number.Natural.suc m) (Number.Natural.suc n)
    Number.Natural.< m n

P. (p. P p) p1 p2. P (p1, p2)

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

PAIR'. fn. a0 a1. fn (a0, a1) = PAIR' a0 a1

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

m n.
    Number.Natural.< m (Number.Natural.suc n)
    m = n Number.Natural.< m n

P Q. (x. P x) Q x. P x Q

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 y y = x) (select) P = x

P. (x. y. P x y) y. x. P x (y x)

P. P 0 (n. P n P (Number.Natural.suc n)) n. P n

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

(∃!) = λP. () P x y. P x P y x = y

P Q. (x. P x Q x) (x. P x) x. Q x

P Q. (x. P x) (x. Q x) x. P x Q x

e f. ∃!fn. fn 0 = e n. fn (Number.Natural.suc n) = f (fn n) n

P c x y. P (if c then x else y) (c P x) (¬c P y)

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