Package base: The standard theory library

Information

namebase
version1.204
descriptionThe standard theory library
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
homepagehttp://opentheory.gilith.com/?pkg=base
haskell-nameopentheory
haskell-int-filehaskell.int
haskell-src-filehaskell.art
haskell-test-filehaskell-test.art
haskell-equality-type"Data.List.list"
haskell-equality-type"Data.Option.option"
haskell-equality-type"Data.Pair.*"
haskell-equality-type"Data.Sum.+"
haskell-equality-type"Number.Natural.natural"
haskell-arbitrary-type"Data.List.list"
haskell-arbitrary-type"Data.Option.option"
haskell-arbitrary-type"Data.Pair.*"
haskell-arbitrary-type"Data.Sum.+"
haskell-arbitrary-type"Number.Natural.natural"
checksum9e9a1dac8ea5119d45a614701b3188851aab1481
showData.Bool
Data.List
Data.Option
Data.Pair
Data.Sum
Data.Unit
Function
Number.Natural
Number.Real
Relation
Set

Files

Defined Type Operators

Defined Constants

Theorems

null []

isNone none

even 0

irreflexive empty

irreflexive isSuc

reflexive universe

transitive empty

transitive universe

transitive (<)

wellFounded empty

wellFounded (<)

wellFounded isSuc

finite

finite universe

infinite universe

¬isSome none

¬odd 0

subrelation isSuc (<)

id = λx. x

¬(universe = )

const = λx y. x

empty = fromSet

universe = fromSet universe

¬

¬

length [] = 0

bit0 0 = 0

size = 0

concat [] = []

nubReverse [] = []

reverse [] = []

toSet [] =

bigIntersect = universe

bigUnion =

bigUnion universe = universe

transitiveClosure isSuc = (<)

map id = id

map id = id

a. isSome (some a)

a. isLeft (left a)

x. x = x

x. x universe

b. isRight (right b)

t. t t

v. v = ()

n. 0 n

n. n n

x. x x

l. finite (toSet l)

s. disjoint s

s. disjoint s

s. s

s. s universe

s. s s

p. all p []

m. wellFounded (measure m)

r. transitive (transitiveClosure r)

r. subrelation r r

p. p

(minimal n. ) = 0

fromPredicate (λx. ) =

fromPredicate (λx. ) = universe

l. all (λx. ) l

hasSize universe 2

finite universe finite universe

infinite universe infinite universe

factorial 0 = 1

zip [] [] = []

cross universe universe = universe

a. ¬isNone (some a)

a. ¬isRight (left a)

x. ¬member x []

x. ¬(x )

a. finite (insert a )

x. id x = x

b. ¬isLeft (right b)

t. t ¬t

m. ¬(m < 0)

n. ¬(n < n)

n. 0 < suc n

n. n < suc n

n. n suc n

s. ¬(universe s)

s. ¬(s )

s. ¬(s s)

p. ¬any p []

r. subrelation r (transitiveClosure r)

(¬) = λp. p

() = λp. p ((select) p)

x y. universe x y

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

(λp. p) = λp. p

() = λp. p = λx.

Combinator.w = λf x. f x x

unzip [] = ([], [])

a. ¬(some a = none)

a. destLeft (left a) = a

x. replicate x 0 = []

x. delete x =

x. insert x universe = universe

b. destRight (right b) = b

t. ¬¬t t

t. ( t) t

t. (t ) t

t. t

t. t t

t. t

t. t t

t. t t t

t. t

t. t t

t. t

t. t t

t. t

t. t t

t. t

t. t t t

n. ¬(factorial n = 0)

n. ¬(suc n = 0)

n. n n * n

n. even n odd n

n. pre (suc n) = n

n. 0 * n = 0

m. m * 0 = 0

n. 0 + n = n

m. m + 0 = m

m. m - 0 = m

n. n - n = 0

n. distance 0 n = n

n. distance n 0 = n

n. distance n n = 0

n. max 0 n = n

n. max n 0 = n

n. max n n = n

n. min 0 n = 0

n. min n 0 = 0

n. min n n = n

m. interval m 0 = []

n. id n = id

l. reverse (reverse l) = l

l. [] @ l = l

l. l @ [] = l

l. drop 0 l = l

l. take 0 l = []

s. \ s =

s. s \ = s

s. s \ universe =

s. s \ s =

s. image id s = s

s. s =

s. universe s = s

s. s =

s. s universe = s

s. s s = s

s. s = s

s. universe s = universe

s. s = s

s. s universe = universe

s. s s = s

s. cross s =

s. cross s =

f. f 0 = id

f. map f [] = []

f. map f none = none

f. image f =

x. Combinator.s const x = id

f. f id = f

f. id f = f

p. filter p [] = []

s. toSet (fromSet s) = s

r. wellFounded r irreflexive r

f. flip (flip f) = f

r. fromSet (toSet r) = r

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

flip = λf x y. f y x

x y. ¬empty x y

e. fn. fn () = e

e. ∃!fn. fn () = e

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

s. image (λx. x) s = s

universe = insert (insert )

size = fold (λx n. suc n) 0

t1 t2. (let x t2 in t1) = t1

x. hasSize (insert x ) 1

x. last (x :: []) = x

t. ( t) ¬t

t. (t ) ¬t

t. t ¬t

n. ¬(even n odd n)

n. even (2 * n)

n. bit1 n = suc (bit0 n)

n. ¬even n odd n

n. ¬odd n even n

m. m 0 = 1

m. m * 1 = m

n. n 1 = n

n. n div 1 = n

n. n mod 1 = 0

m. 1 * m = m

x. 0 + x = x

l. null l l = []

l. length (reverse l) = length l

l. nub (nub l) = nub l

l. nubReverse (nubReverse l) = nubReverse l

l. toSet (nub l) = toSet l

l. toSet (nubReverse l) = toSet l

l. toSet (reverse l) = toSet l

l. length (nub l) length l

l. length (nubReverse l) length l

l. size (toSet l) length l

l. drop (length l) l = []

l. take (length l) l = l

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

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

x. case none some x = x

s. infinite s ¬finite s

s. bigIntersect (insert s ) = s

s. bigUnion (insert s ) = s

f. f 1 = f

x. case left right x = x

f. zipWith f [] [] = []

f. injective f ¬surjective f

Combinator.s = λf g x. f x (g x)

x y. const x y = x

h t. ¬null (h :: t)

x s. x insert x s

x s. delete s x s

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

m n. m m + n

m n. m max m n

m n. n m + n

m n. n max m n

m n. min m n m

m n. min m n n

l. all (λx. ) l null l

s t. disjoint s (t \ s)

s t. s s t

s t. s t s

s t. disjoint (t \ s) s

s t. s \ t s

s t. s t s

s t. t s s

p. p () x. p x

() = λp q. p q p

finite universe finite universe finite universe

x. size (insert x ) = 1

t. (t ) (t )

n. odd (suc (2 * n))

n. n < 2 n

m. suc m = m + 1

n. even (suc n) ¬even n

n. odd (suc n) ¬odd n

m. m 0 m = 0

n. 1 n = 1

n. suc n - 1 = n

x. x 0 = 1

x. ~x + x = 0

x. 1 * x = x

l. nub l = reverse (nubReverse (reverse l))

l. length l = 0 null l

l. toSet l = null l

s. finite s hasSize s (size s)

s. rest s = delete s (choice s)

s. infinite s ¬(s = )

s. disjoint s s s =

s. hasSize s 0 s =

s. universe s s = universe

s. s s =

s. universe \ (universe \ s) = s

l. null (concat l) all null l

x. (fst x, snd x) = x

s. bigUnion (delete s ) = bigUnion s

s. bigUnion (insert s) = bigUnion s

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

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

a b. ¬(left a = right b)

a b. fst (a, b) = a

a b. snd (a, b) = b

x n. length (replicate x n) = n

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

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

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

x s. ¬(insert x s = )

b f. case b f none = b

b f. case b f [] = b

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

m n. ¬(m + n < m)

m n. ¬(n + m < m)

m n. length (interval m n) = n

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

r x. reflexive r r x x

r. reflexive r x. r x x

f b. foldr f b [] = b

f b. foldl f b [] = b

n. 0 < n ¬(n = 0)

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

l. length l = 0 l = []

l. toSet l = l = []

l. foldl (flip (::)) [] l = reverse l

s. finite s toSet (fromSet s) = s

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

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

s. bigIntersect s = fromSet (bigIntersect (image toSet s))

s. bigUnion s = fromSet (bigUnion (image toSet s))

x y. x = y y = x

x y. x = y y = x

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

x s. finite s finite (insert x s)

t1 t2. t1 t2 t2 t1

t1 t2. t1 t2 t2 t1

a b. (a b) a b

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

m n. max m n = max n m

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

m n. distance m (m + n) = n

m n. m + n - m = n

m n. m + n - n = m

m n. distance (m + n) m = n

m n. n * (m div n) m

x y. x > y y < x

x y. x y y x

x y. x * y = y * x

x y. x + y = y + x

x y. x y y x

s x. finite s finite (delete s x)

s x. finite (delete s x) finite s

s x. finite (insert x s) finite s

s t. finite s finite (s \ t)

s t. disjoint s t disjoint t s

s t. s t = t s

s t. s t = t s

s t. s t s t

s. (x. x s) s = universe

s. finite s a. ¬(a s)

f l. null (map f l) null l

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

f s. finite s finite (image f s)

p x. x fromPredicate p p x

p l. length (filter p l) length l

f x. Combinator.w f x = f x x

r x. irreflexive r ¬r x x

r. irreflexive r x. ¬r x x

= { x. x | }

universe = { x. x | }

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

n. n 2 = n * n

n. 2 * n = n + n

s. finite s length (fromSet s) = size s

s. ¬(s = ) choice s s

x n. null (replicate x n) n = 0

h t. length (h :: t) = suc (length t)

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

m n. ¬(m < n n m)

m n. ¬(m n n < m)

m n. isSuc m n suc m = n

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

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 y. x < y ¬(y x)

x y. x - y = x + ~y

l x. member x l x toSet l

l x. member x (nub l) member x l

l x. member x (nubReverse l) member x l

l x. member x (reverse l) member x l

l1 l2. foldr (::) l2 l1 = l1 @ l2

l1 l2. drop (length l1) (l1 @ l2) = l2

l1 l2. take (length l1) (l1 @ l2) = l1

l1 l2. zip l1 l2 = zipWith , l1 l2

x. x = none a. x = some a

s n. hasSize s n size s = n

s. singleton s x. s = insert x

s. s universe x. ¬(x s)

s. (x. x s) ¬(s = )

f a. map f (some a) = some (f a)

p. (b. p b) p p

p. (b. p b) p p

p. p p x. p x

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

n. even n n mod 2 = 0

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

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

n. ¬(n = 0) n 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

l. unzip l = (map fst l, map snd l)

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

() = λp. q. (x. p x q) q

x y. x insert y x = y

a b. some a = some b a = b

a b. left a = left b a = b

h t. toSet (h :: t) = insert h (toSet t)

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

x s. x s insert x s = s

x s. s \ insert x = delete s x

x s. insert x (insert x s) = insert x s

x s. delete (delete s x) x = delete s x

x s. insert x s = insert x s

a b. right a = right b a = b

p q. (q p) ¬p ¬q

t1 t2. ¬(t1 t2) t1 ¬t2

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

m n. suc m < suc n m < n

m n. suc m suc n m n

m n. fromNatural m fromNatural n m n

m n. m + n = m n = 0

m n. m + n = n m = 0

m n. distance m n = 0 m = n

m n. m + n m n = 0

m n. n + m m n = 0

m n. distance (suc m) (suc n) = distance m n

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

s x. insert x s x s

s t. disjoint s t s t =

s t. s t s t = s

s t. s t s t = t

s t. s \ t = s t

s t. s \ t = s disjoint s t

s t. t (s \ t) = t s

s t. s \ t \ t = s \ t

s t. s \ t t = s t

s t. finite t s t finite s

s t. infinite s s t infinite t

s u. bigIntersect (insert s u) = s bigIntersect u

s u. bigUnion (insert s u) = s bigUnion u

f l. reverse (map f l) = map f (reverse l)

f l. toSet (map f l) = image f (toSet l)

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

f s. image f s = s =

s t. s t bigIntersect t bigIntersect s

f g. f g bigUnion f bigUnion g

r s. subrelation r s wellFounded s wellFounded r

r s. subrelation r s toSet r toSet s

r s. toSet r = toSet s r = s

{ m. m | m < 0 } =

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

n. finite { m. m | m < n }

n. finite { m. m | m n }

n. odd n n mod 2 = 1

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

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

k. 1 < k log k 1 = 0

x. abs x = if 0 x then x else ~x

l. ¬null l head l :: tail l = l

s. finite s (size s = 0 s = )

f g a. case f g (left a) = f a

f g b. case f g (right b) = g b

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

f x y. flip f x y = f y x

x n. replicate x (suc n) = x :: replicate x n

h t. take 1 (h :: t) = h :: []

x s. disjoint s (insert x ) ¬(x s)

x s. delete s x = s ¬(x s)

x s. disjoint (insert x ) s ¬(x s)

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

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

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. m suc n = m * m n

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

m n. max (suc m) (suc n) = suc (max m n)

m n. min (suc m) (suc n) = suc (min m n)

m n. fromNatural m * fromNatural n = fromNatural (m * n)

m n. fromNatural m + fromNatural n = fromNatural (m + n)

m n. map suc (interval m n) = interval (suc m) n

n. even n m. n = 2 * m

x n. x suc n = x * x n

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

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

l1 l2. null (l1 @ l2) null l1 null l2

l1 l2. length (l1 @ l2) = length l1 + length l2

l1 l2. reverse (l1 @ l2) = reverse l2 @ reverse l1

l1 l2. toSet (l1 @ l2) = toSet l1 toSet l2

l1 l2. foldl (flip (::)) l2 l1 = reverse l1 @ l2

s t. finite (s t) finite s finite t

s t. finite s finite t finite (s t)

s t. infinite s finite t infinite (s \ t)

s t. finite s finite t finite (s t)

s t. bigIntersect (insert s (insert t )) = s t

s t. bigUnion (insert s (insert t )) = s t

s t. finite s finite t finite (cross s t)

f n. f suc n = f f n

f n. f suc n = f n f

f x. image f (insert x ) = insert (f x)

f s. finite s size (image f s) size s

f s. image f (bigUnion s) = bigUnion (image (image f) s)

f s. image f (bigIntersect s) bigIntersect (image (image f) s)

f g. map f map g = map (f g)

f g. map f map g = map (f g)

s t. bigIntersect (s t) = bigIntersect s bigIntersect t

s t. bigUnion (s t) = bigUnion s bigUnion t

r s. intersect r s = fromSet (toSet r toSet s)

r s. union r s = fromSet (toSet r toSet s)

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

p. (x. p x) a b. p (a, b)

p. (x. p x) a b. p (a, b)

p. (a b. p (a, b)) x. p x

a b. f. f = a f = b

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

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

n. ¬(n = 0) pre n = n - 1

n. hasSize { m. m | m < n } n

l. l = [] h t. l = h :: t

s t x. s t s insert x t

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

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

p a. (x. a = x p x) p a

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 l. ¬all p l any (λx. ¬p x) l

p l. ¬any p l all (λx. ¬p x) l

p l. ¬all (λx. ¬p x) l any p l

p l. ¬any (λx. ¬p x) l all p l

x. (a. x = left a) b. x = right b

p. p none (a. p (some a)) x. p x

f g x. Combinator.s f g x = f x (g x)

p. (f. p f) f. p (λa b. f (a, b))

p. (f. p f) f. p (λa b. f (a, b))

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

h t. last (h :: t) = if null t then h else last t

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

x s. x s insert x (delete s x) = s

m n. m n m < n m = n

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

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 (m n) odd m n = 0

m n. interval m (suc n) = m :: interval (suc m) n

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)

x y. x y y x x = y

l k. foldl (λn x. suc n) k l = length l + k

l k. foldr (λx n. suc n) k l = length l + k

s n. hasSize s n finite s size s = n

s t. s t t s s = t

s t. s (t \ s) = t s t

s t. t \ s s = t s t

s t. s t t s s = t

s t. bijections s t = injections s t surjections s t

s. finite s x. member x (fromSet s) x s

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

f. fn. a b. fn (a, b) = f a b

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

finite universe finite universe
  size universe = size universe size universe

{ s. s | s } = insert

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

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

k n. 1 < k m. n k m

n. size { m. m | m < n } = n

l. ¬null l length (tail l) = length l - 1

s. finite s a. x. x s x a

s. infinite s N. n. N n n s

f x n. map f (replicate x n) = replicate (f x) n

f s x. x s f x image f s

p l. (x. member x l p x) all p l

p l. (x. member x l p x) any p l

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

s x y. fromSet s x y (x, y) s

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

r x y. (x, y) toSet r r x y

p. (x y. p x y) y x. p x y

p. (x y. p x y) y x. p x y

x s. delete (insert x s) x = s ¬(x s)

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 (m n) even m ¬(n = 0)

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

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

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

k m. 1 < k log k (k m) = m

s t. s t s t ¬(s = t)

s t. s t s t ¬(t s)

a b. a b finite b size a < size b

a b. a b finite b size a size b

s t. image fst (cross s t) = if t = then else s

s t. image snd (cross s t) = if s = then else t

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

s. bigIntersect s = universe t. t s t = universe

s. bigUnion s = t. t s t =

p. (x y. p x y) z. p (fst z) (snd z)

p. (x y. p x y) z. p (fst z) (snd z)

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

x1 x2 l. last (x1 :: x2 :: l) = last (x2 :: l)

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

x y s. delete (delete s x) y = delete (delete s y) x

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

x s t. s insert x t delete s x t

x s t. insert x s t = insert x (s t)

a. { x. x | x = a } = insert a

p q r. p q r p q r

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

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

x y n. x y x n y n

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

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

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

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

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

a b n. b < a * n b div a < n

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

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

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

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

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

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

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

p m n. distance (m + p) (n + p) = distance 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

x y z. y z x + y x + z

x y z. x * (y * z) = x * y * z

x y z. x + (y + z) = x + y + z

x y z. x y y z x z

x. ¬(x = 0) inv x * x = 1

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

l1 l2 l3. l1 @ l2 @ l3 = (l1 @ l2) @ l3

l l1 l2. l @ l1 = l @ l2 l1 = l2

l l1 l2. l1 @ l = l2 @ l l1 = l2

l l1 l2. l @ l1 = l @ l2 l1 = l2

l l1 l2. l1 @ l = l2 @ l l1 = l2

l. ¬null l nth l (length l - 1) = last l

s c. image (λx. c) s = if s = then else insert c

s t x. disjoint (delete s x) t disjoint (delete t x) s

s t x. s \ insert x t = delete s x \ t

s t x. delete s x t = delete (s t) x

s t u. s t u s \ t u

s t u. s t u s \ u t

t u s. s \ t \ u = s \ (t u)

t u s. s \ t \ u = s \ u \ t

s t u. s t u = s (t u)

s t u. s t u = s (t u)

s t u. s t t u s u

s t u. s t t u s u

s t u. s t t u s u

s t u. s t t u s u

s t. s t x. x s x t

s t. (x. x s x t) s = t

s t. (x. x s x t) s = t

s. finite s finite { t. t | t s }

f n x. (f suc n) x = f ((f n) x)

f n x. (f suc n) x = (f n) (f x)

f m n. f (m * n) = (f m) n

f s t. s t image f s image f t

f g x. isLeft x case f g x = f (destLeft x)

f g x. isRight x case f g x = g (destRight x)

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

p l. all p l x. x toSet l p x

p l. any p l x. x toSet l p x

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

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

f g s. image (f g) s = image f (image g s)

p f l. all p (map f l) all (p f) l

p f l. any p (map f l) any (p f) l

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

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

f b l. foldr f b (reverse l) = foldl (flip f) b l

r s t. subrelation r s subrelation s t subrelation r t

r. (x. y. r x y) f. x. r x (f x)

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

f b l. foldl f b l = foldr (flip f) b (reverse l)

f b l. foldl f b (reverse l) = foldr (flip f) b l

x y. zip (x :: []) (y :: []) = (x, y) :: []

x n. toSet (replicate x n) = if n = 0 then else insert x

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

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

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

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

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

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

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

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

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

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

m n. max m n = 0 m = 0 n = 0

m n. hasSize universe m hasSize universe n hasSize universe (n m)

m n. distance (distance m n) (distance m (n + 1)) = 1

l1 l2. l1 @ l2 = [] l1 = [] l2 = []

xs ys. length xs = length ys map fst (zip xs ys) = xs

xs ys. length xs = length ys map snd (zip xs ys) = ys

s t. s t = s = t =

s t. cross s t = s = t =

s. finite s (finite (bigUnion s) t. t s finite t)

s. finite (bigUnion s) finite s t. t s finite t

p. (a. p (left a)) (b. p (right b)) x. p x

n. hasSize { m. m | m n } (n + 1)

s t. disjoint s t ¬x. x s x t

s t. disjoint s (bigUnion t) x. x t disjoint s x

t u. t bigIntersect u s. s u t s

s. finite s toSet (fromSet s) = s length (fromSet s) = size s

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

f x s. image f (insert x s) = insert (f x) (image f s)

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

p h t. all p (h :: t) p h all p t

p h t. any p (h :: t) p h any p t

p l x. member x (filter p l) member x l p x

p. p 0 (n. p n p (suc n)) n. p n

s x. x bigIntersect s t. t s x t

s x. x bigUnion s t. t s x t

f t. bigUnion f t s. s f s t

u s. (t. t u t s) bigIntersect u s

p l. (x. all (p x) l) all (λy. x. p x y) l

p l. (x. any (p x) l) any (λy. x. p x y) l

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

x s. x rest s x s ¬(x = choice s)

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

m n. distance m n = if m n then n - m else m - n

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

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

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

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

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

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

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

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

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

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

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

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

x y. ¬(y = 0) x / y = x * inv y

p x. x { y. y | p y } p x

l xs. unzip l = (xs, []) l = [] xs = []

l ys. unzip l = ([], ys) l = [] ys = []

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

r s. (x y. r x y s x y) r = s

x h t. member x (h :: t) x = h member x t

x y s. x insert y s x = y x s

x m n. replicate x (m + n) = replicate x m @ replicate x n

x s t. insert x s t x t s t

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 q) (p r)

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

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

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

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

m n x. m n take m (replicate x n) = replicate x m

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

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

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

m n p. m max n p m n m p

m n p. m min n p m n m p

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

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

m n p. max n p m n m p m

m n p. min n p m n m p m

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

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

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

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

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

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

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

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

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

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

n. size { m. m | m n } = n + 1

x y z. x * (y + z) = x * y + x * z

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

s t x. x s t x s x t

s t x. x s t x s x t

s t u. s t \ u s t disjoint s u

s t u. s t u s t s u

s t u. disjoint (s t) u disjoint s u disjoint t u

s t u. s t u s u t u

s t u. s (t u) = s t s u

s t u. s t u = (s t) (s u)

s t u. (s t) u = s u t u

s t u. s t u = (s u) (t u)

s t. ¬(s = t) x. x t ¬(x s)

s t u. cross s (t \ u) = cross s t \ cross s u

s t u. cross s (t u) = cross s t cross s u

s t u. cross s (t u) = cross s t cross s u

s t u. cross (t \ u) s = cross t s \ cross u s

s t u. cross (t u) s = cross t s cross u s

s t u. cross (t u) s = cross t s cross u s

f m n. f (m + n) = f m f n

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

f s t. image f (s t) = image f s image f t

f s t. image f (s t) image f s image f t

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

f. (ys. xs. map f xs = ys) y. x. f x = y

f. (t. s. image f s = t) y. x. f x = y

p l1 l2. all p (l1 @ l2) all p l1 all p l2

p l1 l2. any p (l1 @ l2) any p l1 any p l2

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

p l. all p l i. i < length l p (nth l i)

p l. any p l i. i < length l p (nth l i)

p f l. filter p (map f l) = map f (filter (p f) l)

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

h t.
    nubReverse (h :: t) =
    if member h t then nubReverse t else h :: nubReverse t

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. n m (odd (m - n) ¬(odd m odd n))

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

s x. s insert x s = s = insert x

s p. { x. x | x s p x } s

f s. { x. f x | x s } = image f s

p q l. all p (filter q l) all (λx. q x p x) l

p q l. any p (filter q l) any (λx. q x p x) l

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

p. (n. (m. m < n p m) p n) n. p n

r. toSet r = { x y. (x, y) | r x y }

s x y. bigIntersect s x y r. r s r x y

s x y. bigUnion s x y r. r s r x y

x n y. member y (replicate x n) y = x ¬(n = 0)

x s t. s delete t x s t ¬(x s)

x s t. disjoint (insert x s) t ¬(x t) disjoint s t

x s. ¬(x s) t. s insert x t s t

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

l. toSet l = image (nth l) { i. i | i < length l }

s x y. x delete s y x s ¬(x = y)

s x. x s t. s = insert x t ¬(x t)

s t x. x s \ t x s ¬(x t)

s t. s t x. ¬(x s) insert x s t

s. s = x t. s = insert x t ¬(x t)

f s t. finite t s image f t size s size t

f g. (x. y. g y = f x) h. f = g h

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

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

f x y. zipWith f (x :: []) (y :: []) = f x y :: []

f. (λx. f x) = λ(a, b). f (a, b)

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

a b c. (n. a * n b * n + c) a b

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

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

x y. 0 x 0 y 0 x * y

s t. finite s finite t size (s t) size s + size t

s t. finite t s t (size s = size t s = t)

a b. finite b a b size a = size b a = b

a b. finite b a b size b size a a = b

s t. finite s finite t size (cross s t) = size s * size t

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

p. p [] (h t. p t p (h :: t)) l. p l

f b h t. foldr f b (h :: t) = f h (foldr f b t)

r s x y. intersect r s x y r x y s x y

r s x y. union r s x y r x y s x y

f b h t. foldl f b (h :: t) = foldl f (f b h) t

h t n. n < length t nth (h :: t) (suc n) = nth t n

n h t. n length t drop (suc n) (h :: t) = drop n t

m n x. m n drop m (replicate x n) = replicate x (n - m)

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

m n p. p n m + n - (m + p) = n - 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. x n = 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. x n y n x y n = 0

n s. finite s n size s t. t s hasSize t n

s n. finite s n size s t. t s hasSize t n

s n. (finite s n size s) t. t s hasSize t n

a. finite a a = x s. a = insert x s finite s

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

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

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

s. bigIntersect s = universe \ bigUnion { t. universe \ t | t s }

s. bigUnion s = universe \ bigIntersect { t. universe \ t | t s }

x s.
    finite s size (insert x s) = if x s then size s else suc (size s)

y s f. y image f s x. y = f x x s

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

s t. finite s t s size (s \ t) = size s - size t

s p. finite s finite { x. x | x s p x }

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

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

f. (y. x. f x = y) p. (x. p (f x)) y. p y

f. (y. x. f x = y) p. (x. p (f x)) y. p y

p q l. all (λx. p x q x) l all p l all q l

p q l. all (λx. p x q x) l all p l all q l

s. bigIntersect s = { x. x | u. u s x u }

s. bigUnion s = { x. x | u. u s x u }

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

f b l1 l2. foldr f b (l1 @ l2) = foldr f (foldr f b l2) l1

f b l1 l2. foldl f b (l1 @ l2) = foldl f (foldl f b l1) l2

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

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

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

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. x n < y n x < y ¬(n = 0)

x y n. x < y ¬(n = 0) x n < 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

k m n. 1 < k k m n m log k n

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

l1 l2 n. length l1 = n length l2 = n length (zip l1 l2) = n

s t. s t s t a. a t ¬(a s)

f g. fn. (a. fn (left a) = f a) b. fn (right b) = g b

f. (λ(x, y). f x y) = λp. f (fst p) (snd p)

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

a b a' b'. (a, b) = (a', b') a = a' b = b'

x y s t. (x, y) cross s t x s y t

x s. insert x s = { y. y | y = x y s }

p1 p2 q1 q2. (p1 p2) (q1 q2) p1 q1 p2 q2

p1 p2 q1 q2. (p1 p2) (q1 q2) p1 q1 p2 q2

p1 p2 q1 q2. (p2 p1) (q1 q2) (p1 q1) p2 q2

m n p q. distance m p distance (m + n) (p + q) + distance n q

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 n p q. distance (m + n) (p + q) distance m p + distance n q

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

k m. 1 < k log k (k (m + 1) - 1) = m

s1 s2 t1 t2. cross s1 t1 cross s2 t2 = cross (s1 s2) (t1 t2)

s t. s t = { x. x | x s x t }

s t. s t = { x. x | x s x t }

s t. finite s finite t size (s t) = size s + size (t \ s)

s t m n. hasSize s m hasSize t n hasSize (cross s t) (m * n)

s t s' t'. s s' t t' cross s t cross s' t'

s t. finite (cross s t) s = t = finite s finite t

u s. u \ bigIntersect s = bigUnion { t. u \ t | t s }

s f. cross s (bigUnion f) = bigUnion { t. cross s t | t f }

f s t. s image f t u. u t s = image f u

p l. toSet (filter p l) = toSet l \ { x. x | ¬p x }

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

s t. t bigUnion s = bigUnion { x. t x | x s }

s t. t bigIntersect s = bigIntersect { x. t x | x s }

s t. bigUnion s \ t = bigUnion { x. x \ t | x s }

s t. bigUnion s t = bigUnion { x. x t | x s }

s t. bigIntersect s t = bigIntersect { x. x t | x s }

f t. cross (bigUnion f) t = bigUnion { s. cross s t | s f }

p. p (a s. ¬(a s) p (insert a s)) s. p s

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

p. (f. p f) f. p (λ(a, b). f a b)

p. (f. p f) f. p (λ(a, b). f a b)

n h t. n length t take (suc n) (h :: t) = h :: take n t

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

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

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

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

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

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

p h t. filter p (h :: t) = if p h then h :: filter p t else filter p t

x l. member x l l1 l2. ¬member x l1 l = l1 @ x :: l2

x s. finite s size (delete s x) = if x s then size s - 1 else size s

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

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

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

s x. delete s x = { y. y | y s ¬(y = x) }

s t. s \ t = { x. x | x s ¬(x t) }

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

t. { x y. (x, y) | x y t x } =

p. p (x s. p s p (insert x s)) a. finite a p a

p. ((a, b). p a b) a b. p a b

p. ((a, b). p a b) a b. p a b

x y s.
    delete (insert x s) y =
    if x = y then delete s y else insert x (delete s y)

x s t. insert x s t = if x t then insert x (s t) else s t

x s t. insert x s t = if x t then s t else insert x (s t)

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

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

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

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

a b n. ¬(n = 0) (a * n + b) div n = a + b div 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 l. m + n length l drop (m + n) l = drop m (drop n l)

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

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

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

s t x. insert x s \ t = if x t then s \ t else insert x (s \ t)

s. finite s size { t. t | t s } = 2 size s

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

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

l xs ys. unzip l = (xs, ys) length xs = length ys l = zip xs ys

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

p. (select (a, b). p a b) = select x. p (fst x) (snd x)

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

k n. 1 < k ¬(n = 0) n < k (log k n + 1)

l1 l1' l2 l2'. length l1 = length l1' l1 @ l2 = l1' @ l2' l1 = l1'

l1 l1' l2 l2'. length l2 = length l2' l1 @ l2 = l1' @ l2' l2 = l2'

s n. hasSize s n hasSize { t. t | t s } (2 n)

s t.
    finite s finite t (size (s t) = size s + size t disjoint s t)

s t. finite s finite t disjoint s t size (s t) = size s + size t

u s. u \ bigUnion s = u bigIntersect { t. u \ t | t s }

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

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) any p l any q l

p r. (x. p x y. r x y) f. x. p x r x (f x)

s t. (x. x s y. y t x y) bigUnion s bigUnion t

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

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

s x x'. (x s x' s) (x delete s x' x' delete s x)

s x x'. (x delete s x' x' delete s x) x s x' s

s n. hasSize s (suc n) ¬(s = ) a. a s hasSize (delete s a) n

f s. finite s finite { y. y | x. x s y = f x }

f s. image f s = { y. y | x. x s y = f x }

p f s. (y. y image f s p y) x. x s p (f x)

p f s. (y. y image f s p y) x. x s p (f x)

f s. finite s s bigUnion f g. finite g g f s bigUnion g

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

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

s t. finite s finite t size (s t) = size s + size t - size (s t)

s t. finite s finite t size (s t) + size (s t) = size s + size t

s t.
    finite s finite t size (s t) < size s + size t ¬disjoint s t

s. infinite s r. (m n. m < n r m < r n) image r universe = s

p. (b. n. p n b) a b. n. n * p n a * n + b

b p q r s. (p q) (r s) (if b then p else r) if b then q else s

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

n a b. ¬(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 n m. k m n n < k (m + 1) log k n = m

s t. cross s t = { x y. (x, y) | x s y t }

f g. (x y. g x = g y f x = f y) h. f = h g

f s. bigIntersect (image f s) = { y. y | x. x s y f x }

f s. bigUnion (image f s) = { y. y | x. x s y f x }

p f s. (t. t image f s p t) t. t s p (image f t)

p f s. (t. t image f s p t) t. t s p (image f t)

s n. hasSize s (suc n) a t. hasSize t n ¬(a t) s = insert a t

s t m n.
    hasSize s m hasSize t n disjoint s t hasSize (s t) (m + n)

s t m n. hasSize s m hasSize t n t s hasSize (s \ t) (m - n)

p f. { x. f x | p x } = image f { x. x | p x }

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

k n1 n2. 1 < k ¬(n1 = 0) n1 n2 log k n1 log k n2

k m n. 1 < k ¬(n = 0) n < k m log k n < m

n. { m. m | m < suc n } = insert n { m. m | m < n }

s t u. finite u disjoint s t s t = u size s + size t = size u

p a s. (x. x insert a s p x) p a x. x s p x

p a s. (x. x insert a s p x) p a x. x s p x

p s. (x. x bigUnion s p x) t x. t s x t p x

p s. (x. x bigUnion s p x) t x. t s x t p x

s f.
    s bigIntersect f =
    if f = then s else bigIntersect { t. s t | t f }

f s.
    bigIntersect f s =
    if f = then s else bigIntersect { t. t s | t f }

p a b. (a, b) { x y. (x, y) | p x y } p a b

p. { x. x | p x } = { a b. (a, b) | p (a, b) }

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

m n l. m + n length l take (m + n) l = take m l @ take n (drop m l)

n. { m. m | m < suc n } = insert 0 { m. suc m | m < n }

l1 l2.
    length l1 = length l2 (i. i < length l1 nth l1 i = nth l2 i)
    l1 = l2

x y xs ys.
    length xs = length ys zip (x :: xs) (y :: ys) = (x, y) :: zip xs ys

s x. ¬(s = ) (m. x. x s x m) x s x sup s

f s t.
    finite t t image f s s'. finite s' s' s t = image f s'

f s t.
    finite t t image f s s'. finite s' s' s t image f s'

s t. finite s finite t finite { x y. (x, y) | x s y t }

f g.
    cross (bigUnion f) (bigUnion g) =
    bigUnion { s t. cross s t | s f t g }

p x t. (s. s insert x t p s) s. s t p s p (insert x s)

p x t. (s. s insert x t p s) s. s t (p s p (insert x s))

x p m n. ¬(p = 0) x mod p m mod p n = x mod p min m n

s f.
    cross s (bigIntersect f) =
    if f = then cross s universe
    else bigIntersect { t. cross s t | t f }

p x y. p (distance x y) d. (x = y + d p d) (y = x + d p d)

p. (n. p n) (m. n. p n n m) m. p m n. p n n m

f s.
    cross (bigIntersect f) s =
    if f = then cross universe s
    else bigIntersect { t. cross t s | t f }

f. (l1 l2. map f l1 = map f l2 l1 = l2) x y. f x = f y x = y

f. (s t. image f s = image f t s = t) x y. f x = f y x = y

p f g. (x. p x y. g y = f x) h. x. p x f x = g (h x)

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

k p. 1 < k p 0 (n. ¬(n = 0) p (n div k) p n) n. p n

s t s' t'. cross s t cross s' t' s = t = s s' t t'

f.
    finite f
    bigUnion { t. t | t f u. u f ¬(t u) } = bigUnion f

p. ((a, b, c). p a b c) a b c. p a b c

p. ((a, b, c). p a b c) a b c. p a b c

p f q. (z. z { x. f x | p x } q z) x. p x q (f x)

p f q. (z. z { x. f x | p x } q z) x. p x q (f x)

p q. (b. i. p i q i + b) b n. i. n i p i q i + b

k n.
    1 < k ¬(n = 0) log k n = if n < k then 0 else log k (n div k) + 1

p t u. (s. s t u p s) t' u'. t' t u' u p (t' u')

p t u. (s. s t u p s) t' u'. t' t u' u p (t' u')

p.
    p (x s. p s ¬(x s) finite s p (insert x s))
    s. finite s p s

p s t. (z. z cross s t p z) x y. x s y t p (x, y)

p s t. (z. z cross s t p z) x y. x s y t p (x, y)

f s t.
    (x y. f x = f y x = y) image f (s t) = image f s image f t

f. (k. t. { x. x | f x t } = k) x y. f x = f y x = y

p f. bigIntersect { x. f x | p x } = { a. a | x. p x a f x }

p f. bigUnion { x. f x | p x } = { a. a | x. p x a f x }

p f s.
    (t. finite t t image f s p t)
    t. finite t t s p (image f t)

p f s.
    (t. finite t t image f s p t)
    t. finite t t s p (image f t)

f h1 h2 t1 t2.
    length t1 = length t2
    zipWith f (h1 :: t1) (h2 :: t2) = f h1 h2 :: zipWith f t1 t2

f s.
    (x y. x s y s f x = f y x = y)
    (finite (image f s) finite s)

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

f A. (x y. f x = f y x = y) finite A finite { x. x | f x A }

p s t. (x. x s t p x) (x. x s p x) x. x t p x

p s t. (x. x s t p x) (x. x s p x) x. x t p x

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

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

m n p q r s.
    distance m n r distance p q s
    distance m p distance n q + (r + s)

s f. finite s image f s = s x y. x s y s f x = f y x = y

f s a.
    (x. x s f x = f a x = a)
    image f (delete s a) = delete (image f s) (f a)

f s t. (y. y t x. f x = y) (x. f x t x s) image f s = t

unzip = foldr (λ(x, y) (xs, ys). (x :: xs, y :: ys)) ([], [])

l1 l2 k.
    k < length l1 + length l2
    nth (l1 @ l2) k =
    if k < length l1 then nth l1 k else nth l2 (k - length l1)

s m.
    ¬(s = ) (m. x. x s x m) (x. x s x m) sup s m

f.
    finite f ¬(f = ) (s t. s f t f s t t s)
    bigIntersect f f

f.
    finite f ¬(f = ) (s t. s f t f s t t s)
    bigUnion f f

x1 x2 y1 y2.
    length x1 = length y1 length x2 = length y2
    zip (x1 @ x2) (y1 @ y2) = zip x1 y1 @ zip x2 y2

l1 l2 n i.
    length l1 = n length l2 = n i < n
    nth (zip l1 l2) i = (nth l1 i, nth l2 i)

f. (y. x. f x = y) p. image f { x. x | p (f x) } = { x. x | p x }

p.
    (m. p m m) (m n. m n p m n p m (suc n)) m n. m n p m n

s t.
    finite s finite t
    size { x y. (x, y) | x s y t } = size s * size t

s n.
    hasSize s n
    f. (m. m < n f m s) x. x s ∃!m. m < n f m = x

f s.
    finite s
    (size (image f s) = size s x y. x s y s f x = f y x = y)

f s.
    (x y. x s y s f x = f y x = y) finite s
    size (image f s) = size s

h x y t xs ys.
    unzip (h :: t) = (x :: xs, y :: ys) h = (x, y) unzip t = (xs, ys)

p.
    p (s. finite s ¬(s = ) x. x s (p (delete s x) p s))
    s. finite s p s

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

k n m. 1 < k ¬(n = 0) (log k n = m k m n n < k (m + 1))

n l i.
    n length l i < length l
    nth l i = if i < n then nth (take n l) i else nth (drop n l) (i - n)

f s n.
    (x y. x s y s f x = f y x = y)
    (hasSize (image f s) n hasSize s n)

f s n.
    (x y. x s y s f x = f y x = y) hasSize s n
    hasSize (image f s) n

x n l1 l2.
    l1 @ l2 = replicate x n
    replicate x (length l1) = l1 replicate x (length l2) = l2
    length l1 + length l2 = n

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

d t.
    { f. f | (x. x f x t) x. ¬(x ) f x = d } =
    insert (λx. d)

k n1 n2.
    1 < k ¬(n1 = 0) ¬(n2 = 0)
    log k (n1 * n2) log k n1 + (log k n2 + 1)

s t m n.
    hasSize s m hasSize t n
    hasSize { x y. (x, y) | x s y t } (m * n)

f l1 l2 n i.
    length l1 = n length l2 = n i < n
    nth (zipWith f l1 l2) i = f (nth l1 i) (nth l2 i)

f s.
    (x y. x s y s f x = f y x = y) g. x. x s g (f x) = x

r s.
    wellFounded r wellFounded s
    wellFounded (λ(x1, y1) (x2, y2). r x1 x2 s 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)

f u v.
    (t. t v s. s u image f s = t)
    y. y v x. x u f x = y

f s.
    t.
      t s image f s = image f t
      x y. x t y t f x = f y x = y

f t.
    finite t (y. y t finite { x. x | f x = y })
    finite { x. x | f x t }

f s t.
    finite s (x. x s finite (t x))
    finite { x y. f x y | x s y t x }

p f q. (z. z { x y. f x y | p x y } q z) x y. p x y q (f x y)

p f q. (z. z { x y. f x y | p x y } q z) x y. p x y q (f x y)

p q. (a b. p a b) (a b. p a b q (a, b)) q (select (a, b). p a b)

n s u.
    s u finite s size s n (finite u n size u)
    t. s t t u hasSize t n

s1 t1 s2 t2.
    cross s1 t1 = cross s2 t2
    (s1 = t1 = ) (s2 = t2 = ) s1 = s2 t1 = t2

f s t.
    (y. y t x. x s f x = y)
    g. y. y t g y s f (g y) = y

f.
    (t t'. { x. x | f x t } = { x. x | f x t' } t = t')
    image f universe = universe

p f g.
    (x y. p x p y g x = g y f x = f y) h. x. p x f x = h (g x)

f x1 x2 y1 y2.
    length x1 = length y1 length x2 = length y2
    zipWith f (x1 @ x2) (y1 @ y2) = zipWith f x1 y1 @ zipWith f x2 y2

p f.
    bigIntersect { x y. f x y | p x y } =
    { a. a | x y. p x y a f x y }

p f.
    bigUnion { x y. f x y | p x y } = { a. a | x y. p x y a f x y }

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

f s t.
    (x y. x s y t f x = f y x = y)
    image f (s \ t) = image f s \ image f t

f s t.
    finite s (x. x s f x t) (y. y t ∃!x. x s f x = y)
    size t = size s

p.
    (x. p x) (m. x. p x x m)
    s. (x. p x x s) m. (x. p x x m) s m

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.
    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.
    (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) wellFounded r

p a b.
    p 0 0 = 0 (m n. p m n a * (m + n) + b)
    c. m n. p m n c * (m + n)

d s t.
    finite s finite t
    finite { f. f | (x. x s f x t) x. ¬(x s) f x = d }

s t f.
    finite s size s = size t image f s = t
    x y. x s y s f x = f y x = y

s t.
    surjections s t =
    { f. f | (x. x s f x t) x. x t y. y s f y = x }

p f s.
    (x y. x image f s y image f s p x y)
    x y. x s y s p (f x) (f y)

r s.
    wellFounded r wellFounded s
    wellFounded (λ(x1, y1) (x2, y2). r x1 x2 x1 = x2 s y1 y2)

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

f s.
    ¬(s = )
    (x y. x bigUnion s y bigUnion s f x = f y x = y)
    image f (bigIntersect s) = bigIntersect (image (image f) s)

a t.
    { s. s | s insert a t } =
    { s. s | s t } image (λs. insert a s) { s. s | s t }

f s a.
    (x y. x s y s f x = f y x = y) a s
    image f (delete s a) = delete (image f s) (f a)

f s t.
    s image f t
    u. u t (x y. x u y u f x = f y x = y) s = image f u

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

s t.
    finite s finite t size s size t
    f. image f s t x y. x s y s f x = f y x = y

s t m n.
    hasSize s m (x. x s finite (t x) size (t x) n)
    size (bigUnion { x. t x | x s }) m * n

f s t.
    (x y. x s y s f x = f y x = y) t s
    image f (s \ t) = image f s \ image f t

s t m n.
    hasSize s m (x. x s hasSize (t x) n)
    hasSize { x y. (x, y) | x s y t x } (m * n)

f g s.
    ¬(g = ) (t. t delete g s { x. x | f x image f t } t)
    image f (bigIntersect g) = bigIntersect (image (image f) g)

f s.
    finite s s bigUnion f ¬(f = )
    (t u. t f u f t u u t) t. t f s t

r s.
    wellFounded r (a. wellFounded (s a))
    wellFounded (λ(x1, y1) (x2, y2). r x1 x2 x1 = x2 s x1 y1 y2)

p f q.
    (z. z { w x y. f w x y | p w x y } q z)
    w x y. p w x y q (f w x y)

p f q.
    (z. z { w x y. f w x y | p w x y } q z)
    w x y. p w x y q (f w x y)

s t.
    injections s t =
    { f. f |
      (x. x s f x t) x y. x s y s f x = f y x = y }

f t s.
    (x y. x s y s f x = f y x = y) finite t
    finite { x. x | x s f x t }

f n.
    (t u. t f u f t u u t)
    (t. t f finite t size t n)
    finite (bigUnion f) size (bigUnion f) n

p f.
    bigIntersect { x y z. f x y z | p x y z } =
    { a. a | x y z. p x y z a f x y z }

p f.
    bigUnion { x y z. f x y z | p x y z } =
    { a. a | x y z. p x y z a f x y z }

d s t.
    finite s finite t
    size { f. f | (x. x s f x t) x. ¬(x s) f x = d } =
    size t size s

p f s.
    (t. t image f s p t)
    t. t s (x y. x t y t f x = f y x = y) p (image f t)

p f s.
    (t. t image f s p t)
    t. t s (x y. x t y t f x = f y x = y) p (image f t)

f s t.
    finite t (y. y t finite { x. x | x s f x = y })
    finite { x. x | x s f x t }

f u.
    (s t. s u t u image f s = image f t s = t)
    x y. x u y u f x = f y x = y

f s.
    bigIntersect { x. bigUnion (f x) | x s } =
    bigUnion { g. bigIntersect { x. g x | x s } | x. x s g x f x }

f s.
    bigUnion { x. bigIntersect (f x) | x s } =
    bigIntersect { g. bigUnion { x. g x | x s } | x. x s g x f x }

r s.
    finite s (x. ¬r x x) (x y z. r x y r y z r x z)
    (x. x s y. y s r x y) s =

d s t m n.
    hasSize s m hasSize t n
    hasSize { f. f | (x. x s f x t) x. ¬(x s) f x = d }
      (n m)

s t f g n.
    (x. x s f x t g (f x) = x)
    (y. y t g y s f (g y) = y) hasSize s n hasSize t n

s t f g.
    (x. x s f x t g (f x) = x)
    (y. y t g y s f (g y) = y) n. hasSize s n hasSize t n

g f b l1 l2.
    (s. g b s = s) (x s1 s2. g (f x s1) s2 = f x (g s1 s2))
    foldr f b (l1 @ l2) = g (foldr f b l1) (foldr f b l2)

g f b l1 l2.
    (s. g s b = s) (s1 s2 x. g s1 (f s2 x) = f (g s1 s2) x)
    foldl f b (l1 @ l2) = g (foldl f b l1) (foldl f b l2)

s f.
    finite s image f s s
    ((y. y s x. x s f x = y)
     x y. x s y s f x = f y x = y)

f s t.
    { x. x | f x image f s } s { x. x | f x image f t } t
    image f (s t) = image f s image f t

s t f g.
    (finite s finite t) (x. x s f x t g (f x) = x)
    (y. y t g y s f (g y) = y) size s = size t

s t.
    finite s finite t size s = size t
    f g.
      (x. x s f x t g (f x) = x)
      y. y t g y s f (g y) = y

s t a.
    { x y. (x, y) | x insert a s y t x } =
    image (, a) (t a) { x y. (x, y) | x s y t x }

s.
    { t. t | t s } =
    image (λp. { x. x | p x })
      { p. p | (x. x s p x universe) x. ¬(x s) (p x ) }

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

p f s.
    (t. finite t t image f s p t)
    t.
      finite t t s (x y. x t y t f x = f y x = y)
      p (image f t)

p f s.
    (t. finite t t image f s p t)
    t.
      finite t t s (x y. x t y t f x = f y x = y)
      p (image f t)

r.
    wellFounded r
    h s.
      (f g x.
         (z. r 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

r.
    wellFounded r
    h.
      (f g x. (z. r 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

r.
    (h.
       (f g x. (z. r 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 r

f s u.
    (t1 t2.
       t1 u t2 u
       { x. x | x s f x t1 } = { x. x | x s f x t2 }
       t1 = t2) u image f s

f g s u.
    ¬(g = ) (t. t g t u)
    (t. t delete g s { x. x | x u f x image f t } t)
    image f (bigIntersect g) = bigIntersect (image (image f) g)

s t f.
    finite s finite t size s = size t image f s t
    ((y. y t x. x s f x = y)
     x y. x s y s f x = f y x = y)

s t m n.
    hasSize s m (x. x s hasSize (t x) n)
    (x y. x s y s ¬(x = y) disjoint (t x) (t y))
    hasSize (bigUnion { x. t x | x s }) (m * n)

f b.
    (x y s. ¬(x = y) f x (f y s) = f y (f x s))
    fold f b = b
    x s.
      finite s
      fold f b (insert x s) =
      if x s then fold f b s else f x (fold f b s)

f s u.
    (k. k s t. t u { x. x | x s f x t } = k)
    image f s u x y. x s y s f x = f y x = y

f b.
    (x y s. ¬(x = y) f x (f y s) = f y (f x s))
    fold f b = b
    x s.
      finite s
      fold f b s =
      if x s then f x (fold f b (delete s x)) else fold f b (delete s x)

f g.
    cross (bigIntersect f) (bigIntersect g) =
    if f = then bigIntersect { t. cross universe t | t g }
    else if g = then bigIntersect { s. cross s universe | s f }
    else bigIntersect { s t. cross s t | s f t g }

s t.
    finite s finite t size s = size t
    f.
      (x. x s f x t) (y. y t x. x s f x = y)
      x y. x s y s f x = f y x = y

f s t u.
    { x. x | x u f x image f s } s t u
    { x. x | x u f x image f t } t s u
    image f (s t) = image f s image f t

(f. (λ(a, b). f (a, b)) = f) (f. (λ(a, b, c). f (a, b, c)) = f)
  f. (λ(a, b, c, d). f (a, b, c, d)) = f

f g b s.
    finite s (x. x s f x = g x)
    (x y s. ¬(x = y) f x (f y s) = f y (f x s))
    (x y s. ¬(x = y) g x (g y s) = g y (g x s))
    fold f b s = fold g b s

f s t.
    (x. x s f x t)
    ((x y. x s y s f x = f y x = y)
     (y. y t x. x s f x = y)
     g.
       (y. y t g y s) (y. y t f (g y) = y)
       x. x s g (f x) = x)

d a s t.
    { f. f |
      (x. x insert a s f x t) x. ¬(x insert a s) f x = d } =
    image (λ(b, g) x. if x = a then b else g x)
      (cross t { f. f | (x. x s f x t) x. ¬(x s) f x = d })

External Type Operators

External Constants

Assumptions

AXIOM OF EXTENSIONALITY

AXIOM OF CHOICE

AXIOM OF INFINITY