Package relation-well-founded: Well-founded relations

Information

namerelation-well-founded
version1.10
descriptionWell-founded relations
authorJoe Hurd <joe@gilith.com>
licenseMIT
show Data.Bool
Data.Pair
Number.Natural
Relation

Files

Defined Constant

Theorems

wellFounded (<)

wellFounded (λx y. F)

<< x. wellFounded << ¬<< x x

<< m. wellFounded << wellFounded (λx x'. << (m x) (m x'))

<<. wellFounded << ¬s. n. << (s (suc n)) (s n)

<< <<<. (x y. << x y <<< x y) wellFounded <<< wellFounded <<

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

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

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

H.
    (f g n. (m. m < n f m = g m) H f n = H g n) f. n. f n = H f n

<< <<<.
    wellFounded << wellFounded <<<
    wellFounded (λ(x1, y1) (x2, y2). << x1 x2 <<< y1 y2)

<<.
    wellFounded <<
    H.
      (f g x. (z. << z x f z = g z) H f x = H g x)
      f. x. f x = H f x

<<.
    wellFounded <<
    H.
      (f g x. (z. << z x f z = g z) H f x = H g x)
      ∃!f. x. f x = H f x

<<.
    (H.
       (f g x. (z. << z x f z = g z) H f x = H g x)
       f. x. f x = H f x) wellFounded <<

R S.
    wellFounded R wellFounded S
    wellFounded (λ(r1, s1) (r2, s2). R r1 r2 r1 = r2 S s1 s2)

<<.
    (x. ¬<< x x) (x y z. << x y << y z << x z)
    (x. Set.finite { y. y | << y x }) wellFounded <<

R S.
    wellFounded R (a. wellFounded (S a))
    wellFounded (λ(r1, s1) (r2, s2). R r1 r2 r1 = r2 S r1 s1 s2)

<<.
    wellFounded <<
    H S.
      (f g x.
         (z. << z x f z = g z S z (f z))
         H f x = H g x S x (H f x)) f. x. f x = H f x

<<.
    wellFounded <<
    H.
      (f g x. (z. << z x f z = g z) H f x = H g x)
      f g. (x. f x = H f x) (x. g x = H g x) f = g

<<.
    (H.
       (f g x. (z. << z x (f z g z)) (H f x H g x))
       f g. (x. f x H f x) (x. g x H g x) f = g)
    wellFounded <<

Input Type Operators

Input Constants

Assumptions

T

Set.infinite Set.universe

x. Set.∈ x Set.universe

F p. p

x. Function.id x = x

n. 0 < suc n

(~) = λp. p F

() = λP. P ((select) P)

t. (x. t) t

t. (λx. t x) = t

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

x. x = x T

s. Set.infinite s ¬Set.finite s

() = λp q. p q p

t. (t T) (t F)

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

(¬T F) (¬F T)

f y. (let xyf x) = f y

x y. x = y y = x

s x. Set.finite (Set.insert x s) Set.finite s

() = λ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

s t. Set.finite t Set.⊆ s t Set.finite s

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

f g. f = g x. f x = g x

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

m n. m < n n < m m = n

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

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

P Q. (x. P Q x) P x. 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. 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

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

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

s t. Set.⊆ s t x. Set.∈ x s Set.∈ x t

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

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

P. P 0 (n. P n P (suc n)) n. P n

(t. ¬¬t t) (¬T F) (¬F T)

p x. Set.∈ x { y. y | p y } p x

x y s. Set.∈ x (Set.insert y s) x = y Set.∈ x s

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

P. (n. (m. m < n P m) P n) n. P n

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

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

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

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 (suc n) = f (fn n) n

P. (n. P n) n. P n m. m < n ¬P m

A B C D. (A B) (C D) A C B D

A B C D. (B A) (C D) (A C) B D

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

(m. m < 0 F) m n. m < suc n m = n m < n

f s.
    (x y. f x = f y x = y) Set.infinite s
    Set.infinite (Set.image f s)

P f s. (y. Set.∈ y (Set.image f s) P y) x. Set.∈ x s P (f x)

t1 t2. (¬(t1 t2) ¬t1 ¬t2) (¬(t1 t2) ¬t1 ¬t2)

t. ((T t) t) ((t T) t) ((F t) ¬t) ((t F) ¬t)

t. (T t t) (t T t) (F t F) (t F F) (t t t)

t. (T t T) (t T T) (F t t) (t F t) (t t t)

t. (T t t) (t T T) (F t T) (t t T) (t F ¬t)

R.
    (x y z. R x y R y z R x z) (n. R n (suc n))
    m n. m < n R m n

p q r.
    (p q q p) ((p q) r p q r) (p q r q p r)
    (p p p) (p p q p q)