Package relation: Basic theory of relations

Information

namerelation
version1.0
descriptionBasic theory of relations
authorJoe Hurd <joe@gilith.com>
licenseMIT
show Data.Bool
Data.Pair
Number.Natural
Relation

Files

Defined Constants

Theorems

wellFounded (<)

wellFounded (λx y. F)

m. wellFounded (measure m)

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

m. measure m = λx y. m x < m y

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

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

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

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

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

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

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

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

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)

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

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

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

<< P G H.
    wellFounded <<
    (f g x.
       (z. << z x f z = g z)
       (P f x P g x) G f x = G g x H f x = H g x)
    (f g x. (z. << z x f z = g z) H f x = H g x)
    (f x y. P f x << y (G f x) << y x)
    f. x. f x = (if P f x then f (G f x) else H f x)

Input Type Operators

Input Constants

Assumptions

T

n. n n

F p. p

x. Function.id x = x

t. t ¬t

n. ¬(n < n)

n. Number.Numeral.zero < suc n

(¬) = λp. p F

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

a. x. x = a

t. (x. t) t

t. (λx. t x) = t

() = λP. P = λx. T

x. x = x T

() = λp q. p q p

t. (t T) (t F)

P x. P x P ((select) P)

(¬T F) (¬F T)

f y. (λx. f x) y = f y

x y. x = y y = x

m n. ¬(m n) n < m

m. m = Number.Numeral.zero n. m = suc n

P. (b. P b) P T P F

() = λ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. suc m < suc n m < n

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

m n. m n d. n = m + d

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

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

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

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

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

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

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

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

p q r. p q r p q r

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

P x. (y. P y y = x) (select) P = x

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 Number.Numeral.zero (n. P n P (suc n)) n. P n

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

(∃!) = λ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 Number.Numeral.zero = 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. (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 < Number.Numeral.zero F) m n. m < suc n m = n m < n

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

(m. m Number.Numeral.zero m = Number.Numeral.zero)
  m n. m suc n m = suc n m n

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)

(n. Number.Numeral.zero + n = n) (m. m + Number.Numeral.zero = m)
  (m n. suc m + n = suc (m + n)) m n. m + suc n = suc (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)