Package set: Set types

Information

nameset
version1.62
descriptionSet types
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
requiresbool
function
natural
pair
showData.Bool
Data.Pair
Function
Number.Natural
Set

Files

Defined Type Operator

Defined Constants

Theorems

finite

finite universe

infinite universe

¬(universe = )

size = 0

bigIntersect = universe

bigUnion =

x. x universe

s. disjoint s

s. disjoint s

s. s

s. s universe

s. s s

fromPredicate (λx. ) =

fromPredicate (λx. ) = universe

hasSize universe 2

x. ¬(x )

a. finite (insert a )

s. ¬(universe s)

s. ¬(s )

s. ¬(s s)

x. delete x =

x. insert x universe = universe

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

f. image f =

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

universe = insert (insert )

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

x. hasSize (insert x ) 1

s. infinite s ¬finite s

s. bigIntersect (insert s ) = s

s. bigUnion (insert s ) = s

x s. x insert x s

x s. delete s x s

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

finite universe finite universe finite universe

x. size (insert x ) = 1

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 =

x s. ¬(insert x s = )

x s. finite s finite (insert x s)

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 s. finite s finite (image f s)

p x. x fromPredicate p p x

= { x. x | }

universe = { x. x | }

s. ¬(s = ) choice s s

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

x y. x insert y x = y

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

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 s. image f s = s =

s t. s t bigIntersect t bigIntersect s

f g. f g bigUnion f bigUnion g

{ m. m | m < 0 } =

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

n. finite { m. m | m n }

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

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

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

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

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

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

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

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

s t x. s t s insert x t

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

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

finite universe finite universe
  size universe = size universe size universe

{ s. s | s } = insert

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

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

f s x. x s f x image f s

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

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. bigIntersect s = universe t. t s t = universe

s. bigUnion s = t. t s t =

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

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 s t. s t image f s image f t

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

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

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

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

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

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

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

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

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

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

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

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)

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. (t. s. image f s = t) y. x. f x = y

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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)

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

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

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 }

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

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

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

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

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

FINITE'.
    FINITE' (x s. FINITE' s FINITE' (insert x s))
    a. finite a FINITE' a

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)

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

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 s. (x y. f x = f y x = y) infinite s infinite (image f s)

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

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

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)

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

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

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

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

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. { m. m | m < suc n } = insert 0 { m. suc m | m < n }

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 s a.
    (x. f x = f a x = a)
    image f (delete s a) = delete (image f s) (f a)

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

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

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

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

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

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 s.
    (x y. x s y s f x = f y x = y)
    (finite (image f s) finite 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

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

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

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

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

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

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

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

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

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

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)

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

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

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.
    finite s (x. x s f x t) (y. y t ∃!x. x s f x = y)
    size t = size s

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 }

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

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

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)

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 A s.
    (x y. x s y s f x = f y x = y) finite A
    finite { x. x | x s f x A }

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

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 }

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

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)

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

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

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

id = λx. x

¬

¬

bit0 0 = 0

t. t t

n. 0 n

n. n n

p. p

t. t ¬t

m. ¬(m < 0)

n. ¬(n < n)

n. 0 < suc n

n. n < suc n

(¬) = λp. p

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

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

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

n. 0 * n = 0

n. 0 + n = n

m. m - 0 = m

n. n - n = 0

t. ( t) ¬t

t. (t ) ¬t

t. t ¬t

n. bit1 n = suc (bit0 n)

m. m 0 = 1

m n. m max m n

m n. n m + n

m n. n max m n

() = λp q. p q p

t. (t ) (t )

m. suc m = m + 1

m. m 0 m = 0

n. suc n - 1 = n

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

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

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

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

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

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

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

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 < suc n m n

m n. suc m n m < n

m. m = 0 n. m = suc n

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

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

t1 t2. ¬t1 ¬t2 t2 t1

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

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

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

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

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

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

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

m n. m suc n = m * m n

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

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

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

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

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

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

m n. m n n m m = n

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

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

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

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

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

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

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

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

m n p. m n n p m p

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

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

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

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. () 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 a' b'. (a, b) = (a', b') a = a' b = b'

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

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

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

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

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

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