Package relation-natural: Relations over natural numbers

Information

namerelation-natural
version1.4
descriptionRelations over natural numbers
authorJoe Hurd <joe@gilith.com>
licenseMIT
requiresbool
function
natural
set
relation-def
relation-thm
relation-well-founded
showData.Bool
Function
Number.Natural
Relation

Files

Defined Constants

Theorems

irreflexive isSuc

transitive (<)

wellFounded (<)

wellFounded isSuc

subrelation isSuc (<)

transitiveClosure isSuc = (<)

m. wellFounded (measure m)

m n. isSuc m n suc m = n

r. subrelation isSuc r transitive r subrelation (<) r

m x y. measure m x y m x < m y

r. wellFounded r ¬f. n. r (f (suc n)) (f n)

m a b. (y. measure m y a measure m y b) m a m b

r.
    wellFounded r
    h.
      (f g x. (z. r z x f z = g z) h f x = h g x)
      ∃!f. x. f x = h f x

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

Input Type Operators

Input Constants

Assumptions

T

Set.infinite Set.universe

¬F T

¬T F

x. Set.∈ x Set.universe

t. t t

F p. p

x. id x = x

t. t ¬t

n. ¬(n < n)

n. 0 < suc n

n. n < 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 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. m + 0 = m

r. wellFounded r irreflexive r

t. (F t) ¬t

t. t F ¬t

s. Set.infinite s ¬Set.finite s

() = λp q. p q p

t. (t T) (t F)

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

x y. x = y y = x

t1 t2. t1 t2 t2 t1

t1 t2. t1 t2 t2 t1

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

m n. ¬(m n) n < m

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

m n. m + suc n = suc (m + n)

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

r s. subrelation r s wellFounded s wellFounded r

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

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

f g. (x. f x = g x) f = g

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

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

r s.
    subrelation r s transitive s subrelation (transitiveClosure r) s

r s. subrelation r s subrelation s r r = s

m n. m < n d. n = m + suc d

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

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

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

m n p. m < n n < p m < p

m n p. m < n n p m < p

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

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

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

r s. subrelation r (bigIntersect s) t. Set.∈ t s subrelation r t

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

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

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

r.
    transitiveClosure r =
    bigIntersect { s. s | subrelation r s transitive s }

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

r. transitive r x y z. r x y r y z r x z

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

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

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

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)

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