Package base: The standard theory library

Information

namebase
version1.2
descriptionThe standard theory library
authorJoe Hurd <joe@gilith.com>
licenseMIT
show Data.Bool
Data.List
Data.Option
Data.Pair
Data.Sum
Data.Unit
Function
Number.Natural
Number.Numeral
Relation

Files

Defined Type Operators

Defined Constants

Axioms

t. (λx. t x) = t

f. injective f ¬surjective f

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

Theorems

T

wellFounded (<)

wellFounded (λx y. F)

id = λx. x

pre 0 = 0

map id = id

x. x = x

v. v = ()

n. 0 n

n. n n

m. wellFounded (measure m)

F p. p

l. all (λx. T) l

let = λf x. f x

1 = suc 0

x. id x = x

t. t ¬t

n. ¬(n < n)

n. 0 < factorial n

n. 0 < suc n

(¬) = λp. p F

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

a. x. x = a

a. ∃!x. x = a

t. (x. t) t

t. (x. t) t

t. (λx. t x) = t

f g. f = g

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

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

a'. ¬(none = some a')

x. destLeft (left x) = x

x. x = x T

y. destRight (right y) = y

n. ¬(factorial n = 0)

n. ¬(suc n = 0)

n. n n * n

n. even n odd n

n. 1 factorial n

n. pre (suc n) = n

m. m * 0 = 0

m. m + 0 = m

n. n - n = 0

l. reverse (reverse l) = l

l. l @ [] = l

e. fn. fn () = e

e. ∃!fn. fn () = e

l. map (λx. x) l = l

2 = suc 1

t1 t2. (λx. t1) t2 = t1

n. ¬(even n odd n)

n. even (2 * n)

n. bit0 n = n + n

n. bit1 n = suc (bit0 n)

n. ¬even n odd n

n. ¬odd n even n

n. n div 1 = n

n. exp n 1 = n

n. n mod 1 = 0

l. null l l = []

l. drop (length l) l = []

l. take (length l) l = l

l. case [] (::) l = l

x. case none some x = x

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

m n. m m + n

m n. n m + n

P. P () x. P x

() = λp q. p q p

t. (t T) (t F)

n. odd (suc (2 * n))

m. suc m = m + 1

n. bit1 n = suc (n + n)

n. exp 1 n = 1

n. suc n - 1 = n

l. null (concat l) all null l

x. (fst x, snd x) = x

x y. fst (x, y) = x

x y. snd (x, y) = y

h t. ¬(h :: t = [])

h t. tail (h :: t) = t

b t. (if b then t else t) = t

n x. length (replicate n x) = n

m n. length (interval m n) = n

t h. head (h :: t) = h

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

(¬T F) (¬F T)

n. 0 < n ¬(n = 0)

l. length l = 0 l = []

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

p. x y. p = (x, y)

x y. x = y y = x

x y. x = y y = x

t1 t2. t1 t2 t2 t1

t1 t2. t1 t2 t2 t1

a b. (a b) a b

n m. m > n n < m

n m. m n n m

m n. m * n = n * m

m n. m + n = n + m

m n. m = n m n

m n. m < n m n

m n. m < n n m

m n. m n n < m

m n. m n n m

m n. m - (m + n) = 0

m n. n - (m + n) = 0

m n. m + n - m = n

m n. m + n - n = m

m n. n * (m div n) m

l f. length (map f l) = length l

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

n. exp n 2 = n * n

n. 2 * n = n + n

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

f g. (f o g) = λx. f (g x)

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

m n. ¬(m < n n m)

m n. ¬(m n n < m)

m n. ¬(m < n) n m

m n. ¬(m n) n < m

m n. m < suc n m n

m n. suc m n m < n

m. m = 0 n. m = suc n

x. x = none a. x = some a

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

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

P. P F P T x. P x

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

n. even n n mod 2 = 0

n. ¬(n = 0) 0 div n = 0

n. ¬(n = 0) 0 mod n = 0

f. surjective f y. x. y = f x

P. (x. ¬P x) ¬x. P x

P. (x. ¬P x) ¬x. P x

P. ¬(x. P x) x. ¬P x

P. ¬(x. P x) x. ¬P x

() = λP. q. (x. P x q) q

a a'. some a = some a' a = a'

A B. (B A) ¬A ¬B

t1 t2. ¬(t1 t2) t1 ¬t2

t1 t2. ¬t1 ¬t2 t2 t1

m n. m < n m div n = 0

m n. m < n m mod n = m

m n. m n factorial m factorial n

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

m n. m < m + n 0 < n

m n. n < m + n 0 < m

m n. suc m = suc n m = n

m n. suc m < suc n m < n

m n. suc m suc n m n

m n. m + n = m n = 0

m n. m + n = n m = 0

m n. m - n = 0 m n

m n. pre (suc m - n) = m - n

m n. suc m - suc n = m - n

f l. map f l = [] l = []

n. odd n n mod 2 = 1

n. exp 0 n = if n = 0 then 1 else 0

n. ¬(n = 0) n div n = 1

m. 0 - m = 0 m - 0 = m

f. (id o f) = f (f o id) = f

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

m n. max m n = if m n then n else m

m n. min m n = if m n then m else n

m n. even (m * n) even m even n

m n. even (m + n) even m even n

m n. odd (m * n) odd m odd n

m n. m * suc n = m + m * n

m n. ¬(n = 0) m mod n < n

m n. ¬(n = 0) m div n m

m n. ¬(n = 0) m mod n m

n. even n m. n = 2 * m

l n. n < length l member (nth n l) l

l m. null (l @ m) null l null m

l m. length (l @ m) = length l + length m

l m. reverse (l @ m) = reverse m @ reverse l

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

P. (x y. P (x, y)) p. P p

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

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

a b. f. f F = a f T = b

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

x. x = [] a0 a1. x = a0 :: a1

P a. (x. a = x P x) P a

P l. ¬exists P l all (λx. ¬P x) l

P l. ¬all P l exists (λx. ¬P x) l

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

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

P a. (x. x = a P x) P a

P a. (x. a = x P x) P a

P a. (x. x = a P x) P a

P. P none (a. P (some a)) x. P x

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

(even 0 T) n. even (suc n) ¬even n

(odd 0 F) n. odd (suc n) ¬odd n

m n. m n m < n m = n

m n. n m m - n + n = m

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

m n. odd (m + n) ¬(odd m odd n)

m n. odd (exp m n) odd m n = 0

m n. m n n m m = n

n l. n length l length (take n l) = n

n. odd n m. n = suc (2 * m)

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

(null [] T) h t. null (h :: t) F

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

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

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

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

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

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

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

P l. (x. member x l P x) all P l

P l. (x. P x member x l) exists P l

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

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

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

bit0 0 = 0 n. bit0 (suc n) = suc (suc (bit0 n))

h t. last (h :: t) = if t = [] then h else last t

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

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

m n. m < n m n ¬(m = n)

m n. even (exp m n) even m ¬(n = 0)

m n. ¬(m = 0) m * n div m = n

m n. ¬(m = 0) m * n mod m = 0

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

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. (∃!x. P x) x. y. P y x = y

x y z. x = y y = z x = z

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

p q r. p q r p q r

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

p q r. p q r p q r

p q r. p q r q p r

n x i. i < n nth i (replicate n x) = x

x y n. x y exp x n exp y n

m n p. m * (n * p) = m * n * p

m n p. m + (n + p) = m + n + p

m n p. exp m (n * p) = exp (exp m n) p

m n p. m + n = m + p n = p

m n p. m + p = n + p m = n

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

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

m n p. m + n m + p n p

m n p. m + p n + p m n

m n p. m + n - (m + p) = n - p

m n p. m + p - (n + p) = m - n

m n p. (m * n + p) mod n = p mod n

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

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

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

m n p. m n n p m p

l. ¬(l = []) length (tail l) = length l - 1

l m n. l @ m @ n = (l @ m) @ n

P f l. all P (map f l) all (P o f) l

P f l. exists P (map f l) exists (P o f) l

f g l. map (g o f) l = map g (map f l)

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

f g h. (f o (g o h)) = (f o g o h)

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

P. (x. ∃!y. P x y) ∃!f. x. P x (f x)

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

b f g. (λx. if b then f x else g x) = if b then f else g

m n. 0 < m * n 0 < m 0 < n

m n. m * n = 0 m = 0 n = 0

m n. m + n = 0 m = 0 n = 0

l m. l @ m = [] l = [] m = []

p q. last (p @ q) = if q = [] then last p else last q

l m. head (l @ m) = if l = [] then head m else head l

P. (a. P (left a)) (a. P (right a)) x. P x

length [] = 0 h t. length (h :: t) = suc (length t)

l. ¬(l = []) last l = nth (length l - 1) l

P l x. member x (filter P l) P x member x l

f. injective f x1 x2. f x1 = f x2 x1 = x2

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

P l. (x. exists (P x) l) exists (λs. x. P x s) l

P l. (x. all (P x) l) all (λs. x. P x s) l

factorial 0 = 1 n. factorial (suc n) = suc n * factorial n

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

NONE' SOME'. fn. fn none = NONE' a. fn (some a) = SOME' a

m n. even (m - n) m n (even m even n)

m n. ¬(n = 0) (m div n = 0 m < n)

m n. ¬(n = 0) m mod n mod n = m mod n

n x. 0 < exp x n ¬(x = 0) n = 0

m n. exp m n = 0 m = 0 ¬(n = 0)

n l. n length l length (drop n l) = length l - n

n l. n length l take n l @ drop n l = l

concat [] = [] h t. concat (h :: t) = h @ concat t

x l1 l2. member x (l1 @ l2) member x l1 member x l2

b t1 t2. (if b then t1 else t2) (¬b t1) (b t2)

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

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

m n i. i < n nth i (interval m n) = m + i

m n p. m * (n + p) = m * n + m * p

m n p. m * (n - p) = m * n - m * p

m n p. exp m (n + p) = exp m n * exp m p

m n p. (m + n) * p = m * p + n * p

m n p. (m - n) * p = m * p - n * p

p m n. exp (m * n) p = exp m p * exp n p

P l1 l2. filter P (l1 @ l2) = filter P l1 @ filter P l2

P f l. filter P (map f l) = map f (filter (P o f) l)

P l1 l2. all P (l1 @ l2) all P l1 all P l2

f l1 l2. map f (l1 @ l2) = map f l1 @ map f l2

f. (m. l. map f l = m) y. x. f x = y

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

b f x y. f (if b then x else y) = if b then f x else f y

b f g x. (if b then f else g) x = if b then f x else g x

m n. odd (m - n) n < m ¬(odd m odd n)

x n. exp x n = 1 x = 1 n = 0

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

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

P g h. f. x. f x = if P x then f (g x) else h 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 Q x) (x. P x) x. Q x

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

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

l x. member x l i. i < length l x = nth i l

t. (λp. t p) = λ(x, y). t (x, y)

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

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

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

m n. ¬(n = 0) m div n * n + m mod n = m

m n. m * n = 1 m = 1 n = 1

P Q l. (x. P x Q x) all P l all Q l

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

P. P [] (a0 a1. P a1 P (a0 :: a1)) x. P x

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

reverse [] = [] l x. reverse (x :: l) = reverse l @ x :: []

m n p. m * n = m * p m = 0 n = p

m n p. m * p = n * p m = n p = 0

x y n. exp x n = exp y n x = y n = 0

m n p. m * n m * p m = 0 n p

m n p. m * p n * p m n p = 0

x y n. exp x n exp y n x y n = 0

f l i. i < length l nth i (map f l) = f (nth i l)

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

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

(m. m - 0 = m) m n. m - suc n = pre (m - n)

f g l. all (λx. f x = g x) l map f l = map g l

P Q l. all (λx. P x Q x) l all P l all Q l

P Q l. all P l all Q l all (λx. P x Q x) l

f y l. member y (map f l) x. member x l y = f x

cond = λt t1 t2. select x. ((t T) x = t1) ((t F) x = t2)

a b n. ¬(a = 0) (n b div a a * n b)

m n p. ¬(p = 0) m * (n div p) m * n div p

m n p. m * n < m * p ¬(m = 0) n < p

m n p. m * p < n * p m < n ¬(p = 0)

x y n. exp x n < exp y n x < y ¬(n = 0)

x y n. x < y ¬(n = 0) exp x n < exp y n

m n p. ¬(m = 0) n < p m * n < m * p

m n p. ¬(p = 0) m n m div p n div p

m n p. ¬(p = 0) p m n div m n div p

a b n. ¬(a = 0) b a * n b div a n

m n. ¬(n = 0) (m mod n = 0 q. m = q * n)

INL' INR'. fn. (a. fn (left a) = INL' a) a. fn (right a) = INR' a

(x. replicate 0 x = []) n x. replicate (suc n) x = x :: replicate n x

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

h1 h2 t1 t2. h1 :: t1 = h2 :: t2 h1 = h2 t1 = t2

x y a b. (x, y) = (a, b) x = a y = b

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

m n p q. m = n + q * p m mod p = n mod p

m n p q. m < n p < q m * p < n * q

m n p q. m < p n < q m + n < p + q

m n p q. m < p n q m + n < p + q

m n p q. m n p q m * p n * q

m n p q. m p n < q m + n < p + q

m n p q. m p n q m + n p + q

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

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

n h t. nth n (h :: t) = if n = 0 then h else nth (n - 1) t

n. (k m. odd m n = exp 2 k * m) ¬(n = 0)

(m. interval m 0 = [])
  m n. interval m (suc n) = m :: interval (suc m) n

(m. exp m 0 = 1) m n. exp m (suc n) = m * exp m n

l n. length l = suc n h t. l = h :: t length t = n

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

(l. drop 0 l = l) n h t. drop (suc n) (h :: t) = drop n t

NIL' CONS'.
    fn. fn [] = NIL' a0 a1. fn (a0 :: a1) = CONS' a0 a1 (fn a1)

m n p. ¬(n = 0) m * (p mod n) mod n = m * p mod n

m n p. ¬(n = 0) m mod n * p mod n = m * p mod n

m n p. ¬(n = 0) exp (m mod n) p mod n = exp m p mod n

m n p. ¬(m * p = 0) m * n div (m * p) = n div p

m n p. ¬(n * p = 0) m div n div p = m div (n * p)

m n p. ¬(n * p = 0) m mod (n * p) mod n = m mod n

m n p. ¬(p = 0) m + p n m div p < n div p

m n. (q. m = n * q) if n = 0 then m = 0 else m mod n = 0

n l i. n length l i < n nth i (take n l) = nth i l

P. (∃!x. P x) (x. P x) x x'. P x P x' x = x'

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

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

(b f. case b f none = b) b f a. case b f (some a) = f a

m n q r. m = q * n + r r < n m div n = q

m n q r. m = q * n + r r < n m mod n = r

P Q l. (x. member x l P x Q x) all P l all Q l

P Q l. (x. member x l P x Q x) exists P l exists Q l

f l1 l2 n. length l1 = n length l2 = n length (zipWith f l1 l2) = n

(l. [] @ l = l) h t l. (h :: t) @ l = h :: t @ l

a b n. ¬(a = 0) (b div a n b < a * (n + 1))

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

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

(l. take 0 l = []) n h t. take (suc n) (h :: t) = h :: take n t

(P. all P [] T) h P t. all P (h :: t) P h all P t

(P. exists P [] F) h P t. exists P (h :: t) P h exists P t

(f. map f [] = []) f h t. map f (h :: t) = f h :: map f t

(h. last (h :: []) = h) h k t. last (h :: k :: t) = last (k :: t)

b A B C D. (A B) (C D) (if b then A else C) if b then B else D

m n p. ¬(n = 0) m mod n * (p mod n) mod n = m * p mod n

a b n. ¬(n = 0) (a mod n + b mod n) mod n = (a + b) mod n

m n p. ¬(m * p = 0) m * n mod (m * p) = m * (n mod p)

m n p. ¬(n * p = 0) m div n mod p = m mod (n * p) div n

k l m.
    nth k (l @ m) = if k < length l then nth k l else nth (k - length l) m

(x. member x [] F) h x t. member x (h :: t) x = h member x t

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

(h t. nth 0 (h :: t) = h) h t n. nth (suc n) (h :: t) = nth n t

(b f. case b f [] = b) b f h t. case b f (h :: t) = f h t

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

l m.
    length l = length m (i. i < length l nth i l = nth i m) l = m

n l i.
    n length l i < length l - n nth i (drop n l) = nth (n + i) l

n. (even n m. n = 2 * m) (¬even n m. n = suc (2 * m))

P. (x. P x) (M. x. P x x M) m. P m x. P x x m

f. (l m. map f l = map f m l = m) x y. f x = f y x = y

m n q r. m = q * n + r r < n m div n = q m mod n = r

a b c d. ¬(b = 0) b * c < (a + 1) * d c div d a div b

(P. filter P [] = [])
  h P t. filter P (h :: t) = if P h then h :: filter P t else filter P t

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

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)

x m n.
    exp x m = exp x n if x = 0 then m = 0 n = 0 else x = 1 m = n

x m n.
    exp x m exp x n if x = 0 then m = 0 n = 0 else x = 1 m n

(f. zipWith f [] [] = [])
  f h1 h2 t1 t2.
    zipWith f (h1 :: t1) (h2 :: t2) = f h1 h2 :: zipWith f t1 t2

x m n. exp x m < exp x n 2 x m < n x = 0 ¬(m = 0) n = 0

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

a b c d. b * c < (a + 1) * d a * d < (c + 1) * b a div b = c div d

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

m n p.
    m * n = n * m m * n * p = m * (n * p) m * (n * p) = n * (m * p)

m n p.
    m + n = n + m m + n + p = m + (n + p) m + (n + p) = n + (m + p)

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

a b n.
    ¬(n = 0)
    ((a + b) mod n = a mod n + b mod n (a + b) div n = a div n + b div n)

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

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

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

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)

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)

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

(n. 0 * n = 0) (m. m * 0 = 0) (n. 1 * n = n) (m. m * 1 = m)
  (m n. suc m * n = m * n + n) m n. m * suc n = m + m * n

(n. ¬(n = 0) 0 < n) (n. ¬(n = 0) 1 n)
  (n. 0 < n ¬(n = 0)) (n. 0 < n 1 n) (n. 1 n 0 < n)
  n. 1 n ¬(n = 0)

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