Theory "pred_set"

Signature

Definitions

GSPECIFICATION

|- ∀f v. v ∈ GSPEC f ⇔ ∃x. (v,T) = f x

EMPTY_DEF

|- ∅ = (λx. F)

UNIV_DEF

|- 𝕌(:α) = (λx. T)

SUBSET_DEF

|- ∀s t. s ⊆ t ⇔ ∀x. x ∈ s ⇒ x ∈ t

PSUBSET_DEF

|- ∀s t. s ⊂ t ⇔ s ⊆ t ∧ s ≠ t

UNION_DEF

|- ∀s t. s ∪ t = {x | x ∈ s ∨ x ∈ t}

INTER_DEF

|- ∀s t. s ∩ t = {x | x ∈ s ∧ x ∈ t}

DISJOINT_DEF

|- ∀s t. DISJOINT s t ⇔ (s ∩ t = ∅)

DIFF_DEF

|- ∀s t. s DIFF t = {x | x ∈ s ∧ x ∉ t}

INSERT_DEF

|- ∀x s. x INSERT s = {y | (y = x) ∨ y ∈ s}

DELETE_DEF

|- ∀s x. s DELETE x = s DIFF {x}

CHOICE_DEF

|- ∀s. s ≠ ∅ ⇒ CHOICE s ∈ s

REST_DEF

|- ∀s. REST s = s DELETE CHOICE s

SING_DEF

|- ∀s. SING s ⇔ ∃x. s = {x}

IMAGE_DEF

|- ∀f s. IMAGE f s = {f x | x ∈ s}

INJ_DEF

|- ∀f s t.
     INJ f s t ⇔
     (∀x. x ∈ s ⇒ f x ∈ t) ∧ ∀x y. x ∈ s ∧ y ∈ s ⇒ (f x = f y) ⇒ (x = y)

SURJ_DEF

|- ∀f s t.
     SURJ f s t ⇔ (∀x. x ∈ s ⇒ f x ∈ t) ∧ ∀x. x ∈ t ⇒ ∃y. y ∈ s ∧ (f y = x)

BIJ_DEF

|- ∀f s t. BIJ f s t ⇔ INJ f s t ∧ SURJ f s t

LINV_DEF

|- ∀f s t. INJ f s t ⇒ ∀x. x ∈ s ⇒ (LINV f s (f x) = x)

RINV_DEF

|- ∀f s t. SURJ f s t ⇒ ∀x. x ∈ t ⇒ (f (RINV f s x) = x)

FINITE_DEF

|- ∀s. FINITE s ⇔ ∀P. P ∅ ∧ (∀s. P s ⇒ ∀e. P (e INSERT s)) ⇒ P s

REL_RESTRICT_DEF

|- ∀R s x y. REL_RESTRICT R s x y ⇔ x ∈ s ∧ y ∈ s ∧ R x y

CARD_DEF

|- (CARD ∅ = 0) ∧
   ∀s.
     FINITE s ⇒ ∀x. CARD (x INSERT s) = if x ∈ s then CARD s else SUC (CARD s)

BIGUNION

|- ∀P. BIGUNION P = {x | ∃s. s ∈ P ∧ x ∈ s}

BIGINTER

|- ∀P. BIGINTER P = {x | ∀s. s ∈ P ⇒ x ∈ s}

CROSS_DEF

|- ∀P Q. P × Q = {p | FST p ∈ P ∧ SND p ∈ Q}

COMPL_DEF

|- ∀P. COMPL P = 𝕌(:α) DIFF P

count_def

|- ∀n. count n = {m | m < n}

ITSET_tupled_primitive_def

|- ∀f.
     ITSET_tupled f =
     WFREC
       (@R. WF R ∧ ∀b s. FINITE s ∧ s ≠ ∅ ⇒ R (REST s,f (CHOICE s) b) (s,b))
       (λITSET_tupled a.
          case a of
            (s,b) =>
              I
                (if FINITE s then
                   if s = ∅ then b else ITSET_tupled (REST s,f (CHOICE s) b)
                 else ARB))

ITSET_curried_def

|- ∀f x x1. ITSET f x x1 = ITSET_tupled f (x,x1)

SUM_IMAGE_DEF

|- ∀f s. ∑ f s = ITSET (λe acc. f e + acc) s 0

SUM_SET_DEF

|- SUM_SET = ∑ I

PROD_IMAGE_DEF

|- ∀f s. Π f s = ITSET (λe acc. f e * acc) s 1

PROD_SET_DEF

|- PROD_SET = Π I

MAX_SET_DEF

|- ∀s.
     FINITE s ⇒
     (s ≠ ∅ ⇒ MAX_SET s ∈ s ∧ ∀y. y ∈ s ⇒ y ≤ MAX_SET s) ∧
     ((s = ∅) ⇒ (MAX_SET s = 0))

MIN_SET_DEF

|- MIN_SET = $LEAST

POW_DEF

|- ∀set. POW set = {s | s ⊆ set}

equiv_on_def

|- ∀R s.
     R equiv_on s ⇔
     (∀x. x ∈ s ⇒ R x x) ∧ (∀x y. x ∈ s ∧ y ∈ s ⇒ (R x y ⇔ R y x)) ∧
     ∀x y z. x ∈ s ∧ y ∈ s ∧ z ∈ s ∧ R x y ∧ R y z ⇒ R x z

partition_def

|- ∀R s. partition R s = {t | ∃x. x ∈ s ∧ (t = {y | y ∈ s ∧ R x y})}

pairwise_def

|- ∀P s. pairwise P s ⇔ ∀e1 e2. e1 ∈ s ∧ e2 ∈ s ⇒ P e1 e2

chooser_def

|- (∀s. chooser s 0 = CHOICE s) ∧ ∀s n. chooser s (SUC n) = chooser (REST s) n

countable_def

|- ∀s. countable s ⇔ ∃f. INJ f s 𝕌(:num)

num_to_pair_def

|- ∀n. num_to_pair n = (nfst n,nsnd n)

pair_to_num_def

|- ∀m n. pair_to_num (m,n) = m ⊗ n

Theorems

SPECIFICATION

|- ∀P x. x ∈ P ⇔ P x

IN_ABS

|- ∀x P. x ∈ (λx. P x) ⇔ P x

ABS_applied

|- T

EXTENSION

|- ∀s t. (s = t) ⇔ ∀x. x ∈ s ⇔ x ∈ t

NOT_EQUAL_SETS

|- ∀s t. s ≠ t ⇔ ∃x. x ∈ t ⇔ x ∉ s

NUM_SET_WOP

|- ∀s. (∃n. n ∈ s) ⇔ ∃n. n ∈ s ∧ ∀m. m ∈ s ⇒ n ≤ m

GSPECIFICATION_applied

|- ∀f v. GSPEC f v ⇔ ∃x. (v,T) = f x

SET_MINIMUM

|- ∀s M. (∃x. x ∈ s) ⇔ ∃x. x ∈ s ∧ ∀y. y ∈ s ⇒ M x ≤ M y

NOT_IN_EMPTY

|- ∀x. x ∉ ∅

MEMBER_NOT_EMPTY

|- ∀s. (∃x. x ∈ s) ⇔ s ≠ ∅

EMPTY_applied

|- ∅ x ⇔ F

IN_UNIV

|- ∀x. x ∈ 𝕌(:α)

UNIV_NOT_EMPTY

|- 𝕌(:α) ≠ ∅

EMPTY_NOT_UNIV

|- ∅ ≠ 𝕌(:α)

EQ_UNIV

|- (∀x. x ∈ s) ⇔ (s = 𝕌(:α))

SUBSET_TRANS

|- ∀s t u. s ⊆ t ∧ t ⊆ u ⇒ s ⊆ u

SUBSET_REFL

|- ∀s. s ⊆ s

SUBSET_ANTISYM

|- ∀s t. s ⊆ t ∧ t ⊆ s ⇒ (s = t)

EMPTY_SUBSET

|- ∀s. ∅ ⊆ s

SUBSET_EMPTY

|- ∀s. s ⊆ ∅ ⇔ (s = ∅)

SUBSET_UNIV

|- ∀s. s ⊆ 𝕌(:α)

UNIV_SUBSET

|- ∀s. 𝕌(:α) ⊆ s ⇔ (s = 𝕌(:α))

PSUBSET_TRANS

|- ∀s t u. s ⊂ t ∧ t ⊂ u ⇒ s ⊂ u

PSUBSET_IRREFL

|- ∀s. ¬(s ⊂ s)

NOT_PSUBSET_EMPTY

|- ∀s. ¬(s ⊂ ∅)

NOT_UNIV_PSUBSET

|- ∀s. ¬(𝕌(:α) ⊂ s)

PSUBSET_UNIV

|- ∀s. s ⊂ 𝕌(:α) ⇔ ∃x. x ∉ s

IN_UNION

|- ∀s t x. x ∈ s ∪ t ⇔ x ∈ s ∨ x ∈ t

UNION_applied

|- ∀s t x. (s ∪ t) x ⇔ x ∈ s ∨ x ∈ t

UNION_ASSOC

|- ∀s t u. s ∪ (t ∪ u) = s ∪ t ∪ u

UNION_IDEMPOT

|- ∀s. s ∪ s = s

UNION_COMM

|- ∀s t. s ∪ t = t ∪ s

SUBSET_UNION

|- (∀s t. s ⊆ s ∪ t) ∧ ∀s t. s ⊆ t ∪ s

UNION_SUBSET

|- ∀s t u. s ∪ t ⊆ u ⇔ s ⊆ u ∧ t ⊆ u

SUBSET_UNION_ABSORPTION

|- ∀s t. s ⊆ t ⇔ (s ∪ t = t)

UNION_EMPTY

|- (∀s. ∅ ∪ s = s) ∧ ∀s. s ∪ ∅ = s

UNION_UNIV

|- (∀s. 𝕌(:α) ∪ s = 𝕌(:α)) ∧ ∀s. s ∪ 𝕌(:α) = 𝕌(:α)

EMPTY_UNION

|- ∀s t. (s ∪ t = ∅) ⇔ (s = ∅) ∧ (t = ∅)

IN_INTER

|- ∀s t x. x ∈ s ∩ t ⇔ x ∈ s ∧ x ∈ t

INTER_applied

|- ∀s t x. (s ∩ t) x ⇔ x ∈ s ∧ x ∈ t

INTER_ASSOC

|- ∀s t u. s ∩ (t ∩ u) = s ∩ t ∩ u

INTER_IDEMPOT

|- ∀s. s ∩ s = s

INTER_COMM

|- ∀s t. s ∩ t = t ∩ s

INTER_SUBSET

|- (∀s t. s ∩ t ⊆ s) ∧ ∀s t. t ∩ s ⊆ s

SUBSET_INTER

|- ∀s t u. s ⊆ t ∩ u ⇔ s ⊆ t ∧ s ⊆ u

SUBSET_INTER_ABSORPTION

|- ∀s t. s ⊆ t ⇔ (s ∩ t = s)

INTER_EMPTY

|- (∀s. ∅ ∩ s = ∅) ∧ ∀s. s ∩ ∅ = ∅

INTER_UNIV

|- (∀s. 𝕌(:α) ∩ s = s) ∧ ∀s. s ∩ 𝕌(:α) = s

UNION_OVER_INTER

|- ∀s t u. s ∩ (t ∪ u) = s ∩ t ∪ s ∩ u

INTER_OVER_UNION

|- ∀s t u. s ∪ t ∩ u = (s ∪ t) ∩ (s ∪ u)

IN_DISJOINT

|- ∀s t. DISJOINT s t ⇔ ¬∃x. x ∈ s ∧ x ∈ t

DISJOINT_SYM

|- ∀s t. DISJOINT s t ⇔ DISJOINT t s

DISJOINT_EMPTY

|- ∀s. DISJOINT ∅ s ∧ DISJOINT s ∅

DISJOINT_EMPTY_REFL

|- ∀s. (s = ∅) ⇔ DISJOINT s s

DISJOINT_EMPTY_REFL_RWT

|- ∀s. DISJOINT s s ⇔ (s = ∅)

DISJOINT_UNION

|- ∀s t u. DISJOINT (s ∪ t) u ⇔ DISJOINT s u ∧ DISJOINT t u

DISJOINT_UNION_BOTH

|- ∀s t u.
     (DISJOINT (s ∪ t) u ⇔ DISJOINT s u ∧ DISJOINT t u) ∧
     (DISJOINT u (s ∪ t) ⇔ DISJOINT s u ∧ DISJOINT t u)

DISJOINT_SUBSET

|- ∀s t u. DISJOINT s t ∧ u ⊆ t ⇒ DISJOINT s u

IN_DIFF

|- ∀s t x. x ∈ s DIFF t ⇔ x ∈ s ∧ x ∉ t

DIFF_applied

|- ∀s t x. (s DIFF t) x ⇔ x ∈ s ∧ x ∉ t

DIFF_EMPTY

|- ∀s. s DIFF ∅ = s

EMPTY_DIFF

|- ∀s. ∅ DIFF s = ∅

DIFF_UNIV

|- ∀s. s DIFF 𝕌(:α) = ∅

DIFF_DIFF

|- ∀s t. s DIFF t DIFF t = s DIFF t

DIFF_EQ_EMPTY

|- ∀s. s DIFF s = ∅

DIFF_SUBSET

|- ∀s t. s DIFF t ⊆ s

UNION_DIFF

|- s ⊆ t ⇒ (s ∪ (t DIFF s) = t) ∧ (t DIFF s ∪ s = t)

DIFF_UNION

|- ∀x y z. x DIFF (y ∪ z) = x DIFF y DIFF z

DIFF_COMM

|- ∀x y z. x DIFF y DIFF z = x DIFF z DIFF y

DIFF_SAME_UNION

|- ∀x y. (x ∪ y DIFF x = y DIFF x) ∧ (x ∪ y DIFF y = x DIFF y)

IN_INSERT

|- ∀x y s. x ∈ y INSERT s ⇔ (x = y) ∨ x ∈ s

INSERT_applied

|- ∀x y s. (y INSERT s) x ⇔ (x = y) ∨ x ∈ s

COMPONENT

|- ∀x s. x ∈ x INSERT s

SET_CASES

|- ∀s. (s = ∅) ∨ ∃x t. (s = x INSERT t) ∧ x ∉ t

DECOMPOSITION

|- ∀s x. x ∈ s ⇔ ∃t. (s = x INSERT t) ∧ x ∉ t

ABSORPTION

|- ∀x s. x ∈ s ⇔ (x INSERT s = s)

ABSORPTION_RWT

|- ∀x s. x ∈ s ⇒ (x INSERT s = s)

INSERT_INSERT

|- ∀x s. x INSERT x INSERT s = x INSERT s

INSERT_COMM

|- ∀x y s. x INSERT y INSERT s = y INSERT x INSERT s

INSERT_UNIV

|- ∀x. x INSERT 𝕌(:α) = 𝕌(:α)

NOT_INSERT_EMPTY

|- ∀x s. x INSERT s ≠ ∅

NOT_EMPTY_INSERT

|- ∀x s. ∅ ≠ x INSERT s

INSERT_UNION

|- ∀x s t. (x INSERT s) ∪ t = if x ∈ t then s ∪ t else x INSERT s ∪ t

INSERT_UNION_EQ

|- ∀x s t. (x INSERT s) ∪ t = x INSERT s ∪ t

INSERT_INTER

|- ∀x s t. (x INSERT s) ∩ t = if x ∈ t then x INSERT s ∩ t else s ∩ t

DISJOINT_INSERT

|- ∀x s t. DISJOINT (x INSERT s) t ⇔ DISJOINT s t ∧ x ∉ t

DISJOINT_INSERT'

|- ∀x s t. DISJOINT t (x INSERT s) ⇔ DISJOINT t s ∧ x ∉ t

INSERT_SUBSET

|- ∀x s t. x INSERT s ⊆ t ⇔ x ∈ t ∧ s ⊆ t

SUBSET_INSERT

|- ∀x s. x ∉ s ⇒ ∀t. s ⊆ x INSERT t ⇔ s ⊆ t

INSERT_DIFF

|- ∀s t x. (x INSERT s) DIFF t = if x ∈ t then s DIFF t else x INSERT s DIFF t

UNIV_BOOL

|- 𝕌(:bool) = {T; F}

IN_DELETE

|- ∀s x y. x ∈ s DELETE y ⇔ x ∈ s ∧ x ≠ y

DELETE_applied

|- ∀s x y. (s DELETE y) x ⇔ x ∈ s ∧ x ≠ y

DELETE_NON_ELEMENT

|- ∀x s. x ∉ s ⇔ (s DELETE x = s)

DELETE_NON_ELEMENT_RWT

|- ∀x s. x ∉ s ⇒ (s DELETE x = s)

IN_DELETE_EQ

|- ∀s x x'. (x ∈ s ⇔ x' ∈ s) ⇔ (x ∈ s DELETE x' ⇔ x' ∈ s DELETE x)

EMPTY_DELETE

|- ∀x. ∅ DELETE x = ∅

DELETE_DELETE

|- ∀x s. s DELETE x DELETE x = s DELETE x

DELETE_COMM

|- ∀x y s. s DELETE x DELETE y = s DELETE y DELETE x

DELETE_SUBSET

|- ∀x s. s DELETE x ⊆ s

SUBSET_DELETE

|- ∀x s t. s ⊆ t DELETE x ⇔ x ∉ s ∧ s ⊆ t

SUBSET_INSERT_DELETE

|- ∀x s t. s ⊆ x INSERT t ⇔ s DELETE x ⊆ t

DIFF_INSERT

|- ∀s t x. s DIFF (x INSERT t) = s DELETE x DIFF t

PSUBSET_INSERT_SUBSET

|- ∀s t. s ⊂ t ⇔ ∃x. x ∉ s ∧ x INSERT s ⊆ t

PSUBSET_MEMBER

|- ∀s t. s ⊂ t ⇔ s ⊆ t ∧ ∃y. y ∈ t ∧ y ∉ s

DELETE_INSERT

|- ∀x y s.
     (x INSERT s) DELETE y = if x = y then s DELETE y else x INSERT s DELETE y

INSERT_DELETE

|- ∀x s. x ∈ s ⇒ (x INSERT s DELETE x = s)

DELETE_INTER

|- ∀s t x. (s DELETE x) ∩ t = s ∩ t DELETE x

DISJOINT_DELETE_SYM

|- ∀s t x. DISJOINT (s DELETE x) t ⇔ DISJOINT (t DELETE x) s

CHOICE_NOT_IN_REST

|- ∀s. CHOICE s ∉ REST s

CHOICE_INSERT_REST

|- ∀s. s ≠ ∅ ⇒ (CHOICE s INSERT REST s = s)

REST_SUBSET

|- ∀s. REST s ⊆ s

REST_PSUBSET

|- ∀s. s ≠ ∅ ⇒ REST s ⊂ s

SING

|- ∀x. SING {x}

SING_EMPTY

|- SING ∅ ⇔ F

SING_INSERT

|- SING (x INSERT s) ⇔ (s = ∅) ∨ (s = {x})

SING_UNION

|- SING (s ∪ t) ⇔
   SING s ∧ (t = ∅) ∨ SING t ∧ (s = ∅) ∨ SING s ∧ SING t ∧ (s = t)

IN_SING

|- ∀x y. x ∈ {y} ⇔ (x = y)

SING_applied

|- ∀x y. {y} x ⇔ (x = y)

NOT_SING_EMPTY

|- ∀x. {x} ≠ ∅

NOT_EMPTY_SING

|- ∀x. ∅ ≠ {x}

EQUAL_SING

|- ∀x y. ({x} = {y}) ⇔ (x = y)

DISJOINT_SING_EMPTY

|- ∀x. DISJOINT {x} ∅

INSERT_SING_UNION

|- ∀s x. x INSERT s = {x} ∪ s

SING_DELETE

|- ∀x. {x} DELETE x = ∅

DELETE_EQ_SING

|- ∀s x. x ∈ s ⇒ ((s DELETE x = ∅) ⇔ (s = {x}))

CHOICE_SING

|- ∀x. CHOICE {x} = x

REST_SING

|- ∀x. REST {x} = ∅

SING_IFF_EMPTY_REST

|- ∀s. SING s ⇔ s ≠ ∅ ∧ (REST s = ∅)

IN_IMAGE

|- ∀y s f. y ∈ IMAGE f s ⇔ ∃x. (y = f x) ∧ x ∈ s

IMAGE_applied

|- ∀y s f. IMAGE f s y ⇔ ∃x. (y = f x) ∧ x ∈ s

IMAGE_IN

|- ∀x s. x ∈ s ⇒ ∀f. f x ∈ IMAGE f s

IMAGE_EMPTY

|- ∀f. IMAGE f ∅ = ∅

IMAGE_ID

|- ∀s. IMAGE (λx. x) s = s

IMAGE_COMPOSE

|- ∀f g s. IMAGE (f o g) s = IMAGE f (IMAGE g s)

IMAGE_INSERT

|- ∀f x s. IMAGE f (x INSERT s) = f x INSERT IMAGE f s

IMAGE_EQ_EMPTY

|- ∀s f. (IMAGE f s = ∅) ⇔ (s = ∅)

IMAGE_DELETE

|- ∀f x s. x ∉ s ⇒ (IMAGE f (s DELETE x) = IMAGE f s)

IMAGE_UNION

|- ∀f s t. IMAGE f (s ∪ t) = IMAGE f s ∪ IMAGE f t

IMAGE_SUBSET

|- ∀s t. s ⊆ t ⇒ ∀f. IMAGE f s ⊆ IMAGE f t

IMAGE_INTER

|- ∀f s t. IMAGE f (s ∩ t) ⊆ IMAGE f s ∩ IMAGE f t

IMAGE_11

|- (∀x y. (f x = f y) ⇔ (x = y)) ⇒ ((IMAGE f s1 = IMAGE f s2) ⇔ (s1 = s2))

IMAGE_CONG

|- ∀f s f' s'.
     (s = s') ∧ (∀x. x ∈ s' ⇒ (f x = f' x)) ⇒ (IMAGE f s = IMAGE f' s')

INJ_IFF

|- INJ f s t ⇔
   (∀x. x ∈ s ⇒ f x ∈ t) ∧ ∀x y. x ∈ s ∧ y ∈ s ⇒ ((f x = f y) ⇔ (x = y))

INJ_ID

|- ∀s. INJ (λx. x) s s

INJ_COMPOSE

|- ∀f g s t u. INJ f s t ∧ INJ g t u ⇒ INJ (g o f) s u

INJ_EMPTY

|- ∀f. (∀s. INJ f ∅ s) ∧ ∀s. INJ f s ∅ ⇔ (s = ∅)

INJ_DELETE

|- ∀s t f. INJ f s t ⇒ ∀e. e ∈ s ⇒ INJ f (s DELETE e) (t DELETE f e)

INJ_INSERT

|- ∀f x s t.
     INJ f (x INSERT s) t ⇔
     INJ f s t ∧ f x ∈ t ∧ ∀y. y ∈ s ∧ (f x = f y) ⇒ (x = y)

INJ_SUBSET

|- ∀f s t s0 t0. INJ f s t ∧ s0 ⊆ s ∧ t ⊆ t0 ⇒ INJ f s0 t0

SURJ_ID

|- ∀s. SURJ (λx. x) s s

SURJ_COMPOSE

|- ∀f g s t u. SURJ f s t ∧ SURJ g t u ⇒ SURJ (g o f) s u

SURJ_EMPTY

|- ∀f. (∀s. SURJ f ∅ s ⇔ (s = ∅)) ∧ ∀s. SURJ f s ∅ ⇔ (s = ∅)

IMAGE_SURJ

|- ∀f s t. SURJ f s t ⇔ (IMAGE f s = t)

SURJ_IMAGE

|- SURJ f s (IMAGE f s)

SURJ_INJ_INV

|- SURJ f s t ⇒ ∃g. INJ g t s ∧ ∀y. y ∈ t ⇒ (f (g y) = y)

BIJ_ID

|- ∀s. BIJ (λx. x) s s

BIJ_EMPTY

|- ∀f. (∀s. BIJ f ∅ s ⇔ (s = ∅)) ∧ ∀s. BIJ f s ∅ ⇔ (s = ∅)

BIJ_COMPOSE

|- ∀f g s t u. BIJ f s t ∧ BIJ g t u ⇒ BIJ (g o f) s u

BIJ_DELETE

|- ∀s t f. BIJ f s t ⇒ ∀e. e ∈ s ⇒ BIJ f (s DELETE e) (t DELETE f e)

BIJ_LINV_INV

|- ∀f s t. BIJ f s t ⇒ ∀x. x ∈ t ⇒ (f (LINV f s x) = x)

BIJ_LINV_BIJ

|- ∀f s t. BIJ f s t ⇒ BIJ (LINV f s) t s

BIJ_IFF_INV

|- ∀f s t.
     BIJ f s t ⇔
     (∀x. x ∈ s ⇒ f x ∈ t) ∧
     ∃g.
       (∀x. x ∈ t ⇒ g x ∈ s) ∧ (∀x. x ∈ s ⇒ (g (f x) = x)) ∧
       ∀x. x ∈ t ⇒ (f (g x) = x)

BIJ_INSERT

|- BIJ f (e INSERT s) t ⇔
   e ∉ s ∧ f e ∈ t ∧ BIJ f s (t DELETE f e) ∨ e ∈ s ∧ BIJ f s t

FINITE_EMPTY

|- FINITE ∅

FINITE_INDUCT

|- ∀P.
     P ∅ ∧ (∀s. FINITE s ∧ P s ⇒ ∀e. e ∉ s ⇒ P (e INSERT s)) ⇒
     ∀s. FINITE s ⇒ P s

FINITE_INSERT

|- ∀x s. FINITE (x INSERT s) ⇔ FINITE s

FINITE_DELETE

|- ∀x s. FINITE (s DELETE x) ⇔ FINITE s

FINITE_REST

|- ∀s. FINITE s ⇒ FINITE (REST s)

FINITE_UNION

|- ∀s t. FINITE (s ∪ t) ⇔ FINITE s ∧ FINITE t

INTER_FINITE

|- ∀s. FINITE s ⇒ ∀t. FINITE (s ∩ t)

SUBSET_FINITE

|- ∀s. FINITE s ⇒ ∀t. t ⊆ s ⇒ FINITE t

SUBSET_FINITE_I

|- ∀s t. FINITE s ∧ t ⊆ s ⇒ FINITE t

PSUBSET_FINITE

|- ∀s. FINITE s ⇒ ∀t. t ⊂ s ⇒ FINITE t

FINITE_DIFF

|- ∀s. FINITE s ⇒ ∀t. FINITE (s DIFF t)

FINITE_DIFF_down

|- ∀P Q. FINITE (P DIFF Q) ∧ FINITE Q ⇒ FINITE P

FINITE_SING

|- ∀x. FINITE {x}

SING_FINITE

|- ∀s. SING s ⇒ FINITE s

IMAGE_FINITE

|- ∀s. FINITE s ⇒ ∀f. FINITE (IMAGE f s)

FINITELY_INJECTIVE_IMAGE_FINITE

|- ∀f. (∀x. FINITE {y | x = f y}) ⇒ ∀s. FINITE (IMAGE f s) ⇔ FINITE s

INJECTIVE_IMAGE_FINITE

|- ∀f. (∀x y. (f x = f y) ⇔ (x = y)) ⇒ ∀s. FINITE (IMAGE f s) ⇔ FINITE s

FINITE_INJ

|- ∀f s t. INJ f s t ∧ FINITE t ⇒ FINITE s

REL_RESTRICT_EMPTY

|- REL_RESTRICT R ∅ = REMPTY

REL_RESTRICT_SUBSET

|- s1 ⊆ s2 ⇒ REL_RESTRICT R s1 RSUBSET REL_RESTRICT R s2

CARD_EMPTY

|- CARD ∅ = 0

CARD_INSERT

|- ∀s.
     FINITE s ⇒ ∀x. CARD (x INSERT s) = if x ∈ s then CARD s else SUC (CARD s)

CARD_EQ_0

|- ∀s. FINITE s ⇒ ((CARD s = 0) ⇔ (s = ∅))

CARD_DELETE

|- ∀s. FINITE s ⇒ ∀x. CARD (s DELETE x) = if x ∈ s then CARD s − 1 else CARD s

CARD_INTER_LESS_EQ

|- ∀s. FINITE s ⇒ ∀t. CARD (s ∩ t) ≤ CARD s

CARD_UNION

|- ∀s.
     FINITE s ⇒ ∀t. FINITE t ⇒ (CARD (s ∪ t) + CARD (s ∩ t) = CARD s + CARD t)

CARD_UNION_EQN

|- ∀s t. FINITE s ∧ FINITE t ⇒ (CARD (s ∪ t) = CARD s + CARD t − CARD (s ∩ t))

CARD_SUBSET

|- ∀s. FINITE s ⇒ ∀t. t ⊆ s ⇒ CARD t ≤ CARD s

CARD_PSUBSET

|- ∀s. FINITE s ⇒ ∀t. t ⊂ s ⇒ CARD t < CARD s

SUBSET_EQ_CARD

|- ∀s. FINITE s ⇒ ∀t. FINITE t ∧ (CARD s = CARD t) ∧ s ⊆ t ⇒ (s = t)

CARD_SING

|- ∀x. CARD {x} = 1

SING_IFF_CARD1

|- ∀s. SING s ⇔ (CARD s = 1) ∧ FINITE s

CARD_DIFF

|- ∀t. FINITE t ⇒ ∀s. FINITE s ⇒ (CARD (s DIFF t) = CARD s − CARD (s ∩ t))

CARD_DIFF_EQN

|- ∀s. FINITE s ⇒ (CARD (s DIFF t) = CARD s − CARD (s ∩ t))

LESS_CARD_DIFF

|- ∀t. FINITE t ⇒ ∀s. FINITE s ⇒ CARD t < CARD s ⇒ 0 < CARD (s DIFF t)

BIJ_FINITE

|- ∀f s t. BIJ f s t ∧ FINITE s ⇒ FINITE t

FINITE_BIJ_CARD_EQ

|- ∀S. FINITE S ⇒ ∀t f. BIJ f S t ∧ FINITE t ⇒ (CARD S = CARD t)

CARD_INJ_IMAGE

|- ∀f s.
     (∀x y. (f x = f y) ⇔ (x = y)) ∧ FINITE s ⇒ (CARD (IMAGE f s) = CARD s)

FINITE_COMPLETE_INDUCTION

|- ∀P. (∀x. (∀y. y ⊂ x ⇒ P y) ⇒ FINITE x ⇒ P x) ⇒ ∀x. FINITE x ⇒ P x

INJ_CARD

|- ∀f s t. INJ f s t ∧ FINITE t ⇒ CARD s ≤ CARD t

PHP

|- ∀f s t. FINITE t ∧ CARD t < CARD s ⇒ ¬INJ f s t

INFINITE_DEF

|- T

NOT_IN_FINITE

|- INFINITE 𝕌(:α) ⇔ ∀s. FINITE s ⇒ ∃x. x ∉ s

INFINITE_INHAB

|- ∀P. INFINITE P ⇒ ∃x. x ∈ P

IMAGE_11_INFINITE

|- ∀f. (∀x y. (f x = f y) ⇒ (x = y)) ⇒ ∀s. INFINITE s ⇒ INFINITE (IMAGE f s)

INFINITE_SUBSET

|- ∀s. INFINITE s ⇒ ∀t. s ⊆ t ⇒ INFINITE t

IN_INFINITE_NOT_FINITE

|- ∀s t. INFINITE s ∧ FINITE t ⇒ ∃x. x ∈ s ∧ x ∉ t

INFINITE_UNIV

|- INFINITE 𝕌(:α) ⇔ ∃f. (∀x y. (f x = f y) ⇒ (x = y)) ∧ ∃y. ∀x. f x ≠ y

INFINITE_NUM_UNIV

|- INFINITE 𝕌(:num)

FINITE_PSUBSET_INFINITE

|- ∀s. INFINITE s ⇔ ∀t. FINITE t ⇒ t ⊆ s ⇒ t ⊂ s

FINITE_PSUBSET_UNIV

|- INFINITE 𝕌(:α) ⇔ ∀s. FINITE s ⇒ s ⊂ 𝕌(:α)

INFINITE_DIFF_FINITE

|- ∀s t. INFINITE s ∧ FINITE t ⇒ s DIFF t ≠ ∅

FINITE_ISO_NUM

|- ∀s.
     FINITE s ⇒
     ∃f.
       (∀n m. n < CARD s ∧ m < CARD s ⇒ (f n = f m) ⇒ (n = m)) ∧
       (s = {f n | n < CARD s})

FINITE_WEAK_ENUMERATE

|- ∀s. FINITE s ⇔ ∃f b. ∀e. e ∈ s ⇔ ∃n. n < b ∧ (e = f n)

FINITE_WF_noloops

|- ∀s. FINITE s ⇒ (WF (REL_RESTRICT R s) ⇔ irreflexive (REL_RESTRICT R s)⁺)

FINITE_StrongOrder_WF

|- ∀R s. FINITE s ∧ StrongOrder (REL_RESTRICT R s) ⇒ WF (REL_RESTRICT R s)

IN_BIGUNION

|- ∀x sos. x ∈ BIGUNION sos ⇔ ∃s. x ∈ s ∧ s ∈ sos

BIGUNION_applied

|- ∀x sos. BIGUNION sos x ⇔ ∃s. x ∈ s ∧ s ∈ sos

BIGUNION_EMPTY

|- BIGUNION ∅ = ∅

BIGUNION_EQ_EMPTY

|- ∀P.
     ((BIGUNION P = ∅) ⇔ (P = ∅) ∨ (P = {∅})) ∧
     ((∅ = BIGUNION P) ⇔ (P = ∅) ∨ (P = {∅}))

BIGUNION_SING

|- ∀x. BIGUNION {x} = x

BIGUNION_UNION

|- ∀s1 s2. BIGUNION (s1 ∪ s2) = BIGUNION s1 ∪ BIGUNION s2

DISJOINT_BIGUNION

|- (∀s t. DISJOINT (BIGUNION s) t ⇔ ∀s'. s' ∈ s ⇒ DISJOINT s' t) ∧
   ∀s t. DISJOINT t (BIGUNION s) ⇔ ∀s'. s' ∈ s ⇒ DISJOINT t s'

BIGUNION_INSERT

|- ∀s P. BIGUNION (s INSERT P) = s ∪ BIGUNION P

BIGUNION_SUBSET

|- ∀X P. BIGUNION P ⊆ X ⇔ ∀Y. Y ∈ P ⇒ Y ⊆ X

FINITE_BIGUNION

|- ∀P. FINITE P ∧ (∀s. s ∈ P ⇒ FINITE s) ⇒ FINITE (BIGUNION P)

FINITE_BIGUNION_EQ

|- ∀P. FINITE (BIGUNION P) ⇔ FINITE P ∧ ∀s. s ∈ P ⇒ FINITE s

SUBSET_BIGUNION_I

|- x ∈ P ⇒ x ⊆ BIGUNION P

CARD_BIGUNION_SAME_SIZED_SETS

|- ∀n s.
     FINITE s ∧ (∀e. e ∈ s ⇒ FINITE e ∧ (CARD e = n)) ∧
     (∀e1 e2. e1 ∈ s ∧ e2 ∈ s ∧ e1 ≠ e2 ⇒ DISJOINT e1 e2) ⇒
     (CARD (BIGUNION s) = CARD s * n)

IN_BIGINTER

|- x ∈ BIGINTER B ⇔ ∀P. P ∈ B ⇒ x ∈ P

BIGINTER_applied

|- BIGINTER B x ⇔ ∀P. P ∈ B ⇒ x ∈ P

BIGINTER_INSERT

|- ∀P B. BIGINTER (P INSERT B) = P ∩ BIGINTER B

BIGINTER_EMPTY

|- BIGINTER ∅ = 𝕌(:α)

BIGINTER_INTER

|- ∀P Q. BIGINTER {P; Q} = P ∩ Q

BIGINTER_SING

|- ∀P. BIGINTER {P} = P

SUBSET_BIGINTER

|- ∀X P. X ⊆ BIGINTER P ⇔ ∀Y. Y ∈ P ⇒ X ⊆ Y

DISJOINT_BIGINTER

|- ∀X Y P.
     Y ∈ P ∧ DISJOINT Y X ⇒ DISJOINT X (BIGINTER P) ∧ DISJOINT (BIGINTER P) X

BIGINTER_UNION

|- ∀s1 s2. BIGINTER (s1 ∪ s2) = BIGINTER s1 ∩ BIGINTER s2

IN_CROSS

|- ∀P Q x. x ∈ P × Q ⇔ FST x ∈ P ∧ SND x ∈ Q

CROSS_applied

|- ∀P Q x. (P × Q) x ⇔ FST x ∈ P ∧ SND x ∈ Q

CROSS_EMPTY

|- ∀P. (P × ∅ = ∅) ∧ (∅ × P = ∅)

CROSS_EMPTY_EQN

|- (s × t = ∅) ⇔ (s = ∅) ∨ (t = ∅)

CROSS_INSERT_LEFT

|- ∀P Q x. (x INSERT P) × Q = {x} × Q ∪ P × Q

CROSS_INSERT_RIGHT

|- ∀P Q x. P × (x INSERT Q) = P × {x} ∪ P × Q

FINITE_CROSS

|- ∀P Q. FINITE P ∧ FINITE Q ⇒ FINITE (P × Q)

CROSS_SINGS

|- ∀x y. {x} × {y} = {(x,y)}

CARD_SING_CROSS

|- ∀x P. FINITE P ⇒ (CARD ({x} × P) = CARD P)

CARD_CROSS

|- ∀P Q. FINITE P ∧ FINITE Q ⇒ (CARD (P × Q) = CARD P * CARD Q)

CROSS_SUBSET

|- ∀P Q P0 Q0. P0 × Q0 ⊆ P × Q ⇔ (P0 = ∅) ∨ (Q0 = ∅) ∨ P0 ⊆ P ∧ Q0 ⊆ Q

FINITE_CROSS_EQ

|- ∀P Q. FINITE (P × Q) ⇔ (P = ∅) ∨ (Q = ∅) ∨ FINITE P ∧ FINITE Q

CROSS_UNIV

|- 𝕌(:α # β) = 𝕌(:α) × 𝕌(:β)

INFINITE_PAIR_UNIV

|- FINITE 𝕌(:α # β) ⇔ FINITE 𝕌(:α) ∧ FINITE 𝕌(:β)

SUM_UNIV

|- 𝕌(:α + β) = IMAGE INL 𝕌(:α) ∪ IMAGE INR 𝕌(:β)

INJ_INL

|- (∀x. x ∈ s ⇒ INL x ∈ t) ⇒ INJ INL s t

INJ_INR

|- (∀x. x ∈ s ⇒ INR x ∈ t) ⇒ INJ INR s t

IN_COMPL

|- ∀x s. x ∈ COMPL s ⇔ x ∉ s

COMPL_applied

|- ∀x s. COMPL s x ⇔ x ∉ s

COMPL_COMPL

|- ∀s. COMPL (COMPL s) = s

COMPL_CLAUSES

|- ∀s. (COMPL s ∩ s = ∅) ∧ (COMPL s ∪ s = 𝕌(:α))

COMPL_SPLITS

|- ∀p q. p ∩ q ∪ COMPL p ∩ q = q

INTER_UNION_COMPL

|- ∀s t. s ∩ t = COMPL (COMPL s ∪ COMPL t)

COMPL_EMPTY

|- COMPL ∅ = 𝕌(:α)

COMPL_INTER

|- (x ∩ COMPL x = ∅) ∧ (COMPL x ∩ x = ∅)

COMPL_UNION

|- COMPL (s ∪ t) = COMPL s ∩ COMPL t

IN_COUNT

|- ∀m n. m ∈ count n ⇔ m < n

COUNT_applied

|- ∀m n. count n m ⇔ m < n

COUNT_ZERO

|- count 0 = ∅

COUNT_SUC

|- ∀n. count (SUC n) = n INSERT count n

FINITE_COUNT

|- ∀n. FINITE (count n)

CARD_COUNT

|- ∀n. CARD (count n) = n

COUNT_11

|- (count n1 = count n2) ⇔ (n1 = n2)

ITSET_ind

|- ∀P.
     (∀s b. (FINITE s ∧ s ≠ ∅ ⇒ P (REST s) (f (CHOICE s) b)) ⇒ P s b) ⇒
     ∀v v1. P v v1

ITSET_def

|- ∀s f b.
     ITSET f s b =
     if FINITE s then if s = ∅ then b else ITSET f (REST s) (f (CHOICE s) b)
     else ARB

ITSET_IND

|- ∀P.
     (∀s b. (FINITE s ∧ s ≠ ∅ ⇒ P (REST s) (f (CHOICE s) b)) ⇒ P s b) ⇒
     ∀v v1. P v v1

ITSET_THM

|- ∀s f b.
     FINITE s ⇒
     (ITSET f s b = if s = ∅ then b else ITSET f (REST s) (f (CHOICE s) b))

ITSET_EMPTY

|- ∀f b. ITSET f ∅ b = b

ITSET_INSERT

|- ∀s.
     FINITE s ⇒
     ∀f x b.
       ITSET f (x INSERT s) b =
       ITSET f (REST (x INSERT s)) (f (CHOICE (x INSERT s)) b)

COMMUTING_ITSET_INSERT

|- ∀f s.
     (∀x y z. f x (f y z) = f y (f x z)) ∧ FINITE s ⇒
     ∀x b. ITSET f (x INSERT s) b = ITSET f (s DELETE x) (f x b)

COMMUTING_ITSET_RECURSES

|- ∀f e s b.
     (∀x y z. f x (f y z) = f y (f x z)) ∧ FINITE s ⇒
     (ITSET f (e INSERT s) b = f e (ITSET f (s DELETE e) b))

SUM_IMAGE_THM

|- ∀f.
     (∑ f ∅ = 0) ∧
     ∀e s. FINITE s ⇒ (∑ f (e INSERT s) = f e + ∑ f (s DELETE e))

SUM_IMAGE_SING

|- ∀f e. ∑ f {e} = f e

SUM_IMAGE_SUBSET_LE

|- ∀f s t. FINITE s ∧ t ⊆ s ⇒ ∑ f t ≤ ∑ f s

SUM_IMAGE_IN_LE

|- ∀f s e. FINITE s ∧ e ∈ s ⇒ f e ≤ ∑ f s

SUM_IMAGE_DELETE

|- ∀f s.
     FINITE s ⇒ ∀e. ∑ f (s DELETE e) = if e ∈ s then ∑ f s − f e else ∑ f s

SUM_IMAGE_UNION

|- ∀f s t. FINITE s ∧ FINITE t ⇒ (∑ f (s ∪ t) = ∑ f s + ∑ f t − ∑ f (s ∩ t))

SUM_IMAGE_lower_bound

|- ∀s. FINITE s ⇒ ∀n. (∀x. x ∈ s ⇒ n ≤ f x) ⇒ CARD s * n ≤ ∑ f s

SUM_IMAGE_upper_bound

|- ∀s. FINITE s ⇒ ∀n. (∀x. x ∈ s ⇒ f x ≤ n) ⇒ ∑ f s ≤ CARD s * n

SUM_SAME_IMAGE

|- ∀P.
     FINITE P ⇒
     ∀f p. p ∈ P ∧ (∀q. q ∈ P ⇒ (f p = f q)) ⇒ (∑ f P = CARD P * f p)

SUM_IMAGE_CONG

|- (s1 = s2) ∧ (∀x. x ∈ s2 ⇒ (f1 x = f2 x)) ⇒ (∑ f1 s1 = ∑ f2 s2)

SUM_IMAGE_ZERO

|- ∀s. FINITE s ⇒ ((∑ f s = 0) ⇔ ∀x. x ∈ s ⇒ (f x = 0))

ABS_DIFF_SUM_IMAGE

|- ∀s. FINITE s ⇒ ABS_DIFF (∑ f s) (∑ g s) ≤ ∑ (λx. ABS_DIFF (f x) (g x)) s

SUM_IMAGE_MONO_LESS_EQ

|- ∀s. FINITE s ⇒ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒ ∑ f s ≤ ∑ g s

SUM_IMAGE_MONO_LESS

|- ∀s.
     FINITE s ⇒
     (∃x. x ∈ s ∧ f x < g x) ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒
     ∑ f s < ∑ g s

SUM_SET_THM

|- (SUM_SET ∅ = 0) ∧
   ∀x s. FINITE s ⇒ (SUM_SET (x INSERT s) = x + SUM_SET (s DELETE x))

SUM_SET_EMPTY

|- SUM_SET ∅ = 0

SUM_SET_SING

|- ∀n. SUM_SET {n} = n

SUM_SET_SUBSET_LE

|- ∀s t. FINITE t ∧ s ⊆ t ⇒ SUM_SET s ≤ SUM_SET t

SUM_SET_IN_LE

|- ∀x s. FINITE s ∧ x ∈ s ⇒ x ≤ SUM_SET s

SUM_SET_DELETE

|- ∀s.
     FINITE s ⇒
     ∀e. SUM_SET (s DELETE e) = if e ∈ s then SUM_SET s − e else SUM_SET s

SUM_SET_UNION

|- ∀s t.
     FINITE s ∧ FINITE t ⇒
     (SUM_SET (s ∪ t) = SUM_SET s + SUM_SET t − SUM_SET (s ∩ t))

PROD_IMAGE_THM

|- ∀f.
     (Π f ∅ = 1) ∧
     ∀e s. FINITE s ⇒ (Π f (e INSERT s) = f e * Π f (s DELETE e))

PROD_SET_THM

|- (PROD_SET ∅ = 1) ∧
   ∀x s. FINITE s ⇒ (PROD_SET (x INSERT s) = x * PROD_SET (s DELETE x))

PROD_SET_EMPTY

|- PROD_SET ∅ = 1

PROD_SET_IMAGE_REDUCTION

|- ∀f s x.
     FINITE (IMAGE f s) ∧ f x ∉ IMAGE f s ⇒
     (PROD_SET (IMAGE f (x INSERT s)) = f x * PROD_SET (IMAGE f s))

MAX_SET_THM

|- (MAX_SET ∅ = 0) ∧
   ∀e s. FINITE s ⇒ (MAX_SET (e INSERT s) = MAX e (MAX_SET s))

MAX_SET_REWRITES

|- (MAX_SET ∅ = 0) ∧ (MAX_SET {e} = e)

MAX_SET_ELIM

|- ∀P Q.
     FINITE P ∧ ((P = ∅) ⇒ Q 0) ∧ (∀x. (∀y. y ∈ P ⇒ y ≤ x) ∧ x ∈ P ⇒ Q x) ⇒
     Q (MAX_SET P)

MIN_SET_ELIM

|- ∀P Q. P ≠ ∅ ∧ (∀x. (∀y. y ∈ P ⇒ x ≤ y) ∧ x ∈ P ⇒ Q x) ⇒ Q (MIN_SET P)

MIN_SET_THM

|- (∀e. MIN_SET {e} = e) ∧
   ∀s e1 e2. MIN_SET (e1 INSERT e2 INSERT s) = MIN e1 (MIN_SET (e2 INSERT s))

MIN_SET_LEM

|- ∀s. s ≠ ∅ ⇒ MIN_SET s ∈ s ∧ ∀x. x ∈ s ⇒ MIN_SET s ≤ x

SUBSET_MIN_SET

|- ∀I J n. I ≠ ∅ ∧ J ≠ ∅ ∧ I ⊆ J ⇒ MIN_SET J ≤ MIN_SET I

SUBSET_MAX_SET

|- ∀I J. FINITE I ∧ FINITE J ∧ I ⊆ J ⇒ MAX_SET I ≤ MAX_SET J

MIN_SET_LEQ_MAX_SET

|- ∀s. s ≠ ∅ ∧ FINITE s ⇒ MIN_SET s ≤ MAX_SET s

MIN_SET_UNION

|- ∀A B.
     FINITE A ∧ FINITE B ∧ A ≠ ∅ ∧ B ≠ ∅ ⇒
     (MIN_SET (A ∪ B) = MIN (MIN_SET A) (MIN_SET B))

MAX_SET_UNION

|- ∀A B. FINITE A ∧ FINITE B ⇒ (MAX_SET (A ∪ B) = MAX (MAX_SET A) (MAX_SET B))

IN_POW

|- ∀set e. e ∈ POW set ⇔ e ⊆ set

UNIV_FUN_TO_BOOL

|- 𝕌(:α -> bool) = POW 𝕌(:α)

SUBSET_POW

|- ∀s1 s2. s1 ⊆ s2 ⇒ POW s1 ⊆ POW s2

SUBSET_INSERT_RIGHT

|- ∀e s1 s2. s1 ⊆ s2 ⇒ s1 ⊆ e INSERT s2

SUBSET_DELETE_BOTH

|- ∀s1 s2 x. s1 ⊆ s2 ⇒ s1 DELETE x ⊆ s2 DELETE x

POW_EMPTY

|- ∀s. POW s ≠ ∅

POW_INSERT

|- ∀e s. POW (e INSERT s) = IMAGE ($INSERT e) (POW s) ∪ POW s

POW_EQNS

|- (POW ∅ = {∅}) ∧
   ∀e s. POW (e INSERT s) = (let ps = POW s in IMAGE ($INSERT e) ps ∪ ps)

FINITE_POW

|- ∀s. FINITE s ⇒ FINITE (POW s)

CARD_POW

|- ∀s. FINITE s ⇒ (CARD (POW s) = 2 ** CARD s)

GSPEC_ETA

|- {x | P x} = P

GSPEC_F

|- {x | F} = ∅

GSPEC_T

|- {x | T} = 𝕌(:α)

GSPEC_ID

|- {x | x ∈ y} = y

GSPEC_EQ

|- {x | x = y} = {y}

GSPEC_EQ2

|- {x | y = x} = {y}

GSPEC_F_COND

|- ∀f. (∀x. ¬SND (f x)) ⇒ (GSPEC f = ∅)

GSPEC_AND

|- ∀P Q. {x | P x ∧ Q x} = {x | P x} ∩ {x | Q x}

GSPEC_OR

|- ∀P Q. {x | P x ∨ Q x} = {x | P x} ∪ {x | Q x}

BIGUNION_partition

|- R equiv_on s ⇒ (BIGUNION (partition R s) = s)

EMPTY_NOT_IN_partition

|- R equiv_on s ⇒ ∅ ∉ partition R s

partition_elements_disjoint

|- R equiv_on s ⇒
   ∀t1 t2. t1 ∈ partition R s ∧ t2 ∈ partition R s ∧ t1 ≠ t2 ⇒ DISJOINT t1 t2

partition_elements_interrelate

|- R equiv_on s ⇒ ∀t. t ∈ partition R s ⇒ ∀x y. x ∈ t ∧ y ∈ t ⇒ R x y

partition_SUBSET

|- ∀R s t. t ∈ partition R s ⇒ t ⊆ s

FINITE_partition

|- ∀R s. FINITE s ⇒ FINITE (partition R s) ∧ ∀t. t ∈ partition R s ⇒ FINITE t

partition_CARD

|- ∀R s. R equiv_on s ∧ FINITE s ⇒ (CARD s = ∑ CARD (partition R s))

pairwise_UNION

|- pairwise R (s1 ∪ s2) ⇔
   pairwise R s1 ∧ pairwise R s2 ∧ ∀x y. x ∈ s1 ∧ y ∈ s2 ⇒ R x y ∧ R y x

pairwise_SUBSET

|- ∀R s t. pairwise R t ∧ s ⊆ t ⇒ pairwise R s

KoenigsLemma

|- ∀R.
     (∀x. FINITE {y | R x y}) ⇒
     ∀x. INFINITE {y | R^* x y} ⇒ ∃f. (f 0 = x) ∧ ∀n. R (f n) (f (SUC n))

KoenigsLemma_WF

|- ∀R. (∀x. FINITE {y | R x y}) ∧ WF (inv R) ⇒ ∀x. FINITE {y | R^* x y}

SET_EQ_SUBSET

|- ∀s1 s2. (s1 = s2) ⇔ s1 ⊆ s2 ∧ s2 ⊆ s1

PSUBSET_EQN

|- ∀s1 s2. s1 ⊂ s2 ⇔ s1 ⊆ s2 ∧ ¬(s2 ⊆ s1)

PSUBSET_SUBSET_TRANS

|- ∀s t u. s ⊂ t ∧ t ⊆ u ⇒ s ⊂ u

SUBSET_PSUBSET_TRANS

|- ∀s t u. s ⊆ t ∧ t ⊂ u ⇒ s ⊂ u

CROSS_EQNS

|- ∀s1 s2.
     (∅ × s2 = ∅) ∧ ((a INSERT s1) × s2 = IMAGE (λy. (a,y)) s2 ∪ s1 × s2)

count_EQN

|- ∀n. count n = if n = 0 then ∅ else (let p = PRE n in p INSERT count p)

UNIQUE_MEMBER_SING

|- ∀x s. x ∈ s ∧ (∀y. y ∈ s ⇒ (x = y)) ⇔ (s = {x})

inj_surj

|- ∀f s t. INJ f s t ⇒ (s = ∅) ∨ ∃f'. SURJ f' t s

infinite_rest

|- ∀s. INFINITE s ⇒ INFINITE (REST s)

chooser_def_compute

|- (∀s. chooser s 0 = CHOICE s) ∧
   (∀s n.
      chooser s (NUMERAL (BIT1 n)) =
      chooser (REST s) (NUMERAL (BIT1 n) − 1)) ∧
   ∀s n. chooser s (NUMERAL (BIT2 n)) = chooser (REST s) (NUMERAL (BIT1 n))

infinite_num_inj

|- ∀s. INFINITE s ⇔ ∃f. INJ f 𝕌(:num) s

countable_image_nats

|- countable (IMAGE f 𝕌(:num))

countable_surj

|- ∀s. countable s ⇔ (s = ∅) ∨ ∃f. SURJ f 𝕌(:num) s

num_countable

|- countable 𝕌(:num)

subset_countable

|- ∀s t. countable s ∧ t ⊆ s ⇒ countable t

image_countable

|- ∀f s. countable s ⇒ countable (IMAGE f s)

finite_countable

|- ∀s. FINITE s ⇒ countable s

pair_to_num_formula

|- ∀x y. pair_to_num (x,y) = (x + y + 1) * (x + y) DIV 2 + y

pair_to_num_inv

|- (∀x. pair_to_num (num_to_pair x) = x) ∧
   ∀x y. num_to_pair (pair_to_num (x,y)) = (x,y)

cross_countable

|- ∀s t. countable s ∧ countable t ⇒ countable (s × t)

inter_countable

|- ∀s t. countable s ∨ countable t ⇒ countable (s ∩ t)

inj_countable

|- ∀f s t. countable t ∧ INJ f s t ⇒ countable s

bigunion_countable

|- ∀s. countable s ∧ (∀x. x ∈ s ⇒ countable x) ⇒ countable (BIGUNION s)

union_countable

|- ∀s t. countable s ∧ countable t ⇒ countable (s ∪ t)

union_countable_IFF

|- countable (s ∪ t) ⇔ countable s ∧ countable t

inj_image_countable_IFF

|- INJ f s (IMAGE f s) ⇒ (countable (IMAGE f s) ⇔ countable s)

pow_no_surj

|- ∀s. ¬∃f. SURJ f s (POW s)

infinite_pow_uncountable

|- ∀s. INFINITE s ⇒ ¬countable (POW s)

countable_Usum

|- countable 𝕌(:α + β) ⇔ countable 𝕌(:α) ∧ countable 𝕌(:β)

countable_EMPTY

|- countable ∅

countable_INSERT

|- countable (x INSERT s) ⇔ countable s

cross_countable_IFF

|- countable (s × t) ⇔ (s = ∅) ∨ (t = ∅) ∨ countable s ∧ countable t

countable_Uprod

|- countable 𝕌(:α # β) ⇔ countable 𝕌(:α) ∧ countable 𝕌(:β)

IMAGE_BIGUNION

|- ∀f M. IMAGE f (BIGUNION M) = BIGUNION (IMAGE (IMAGE f) M)

SUBSET_DIFF

|- ∀s1 s2 s3. s1 ⊆ s2 DIFF s3 ⇔ s1 ⊆ s2 ∧ DISJOINT s1 s3

INTER_SUBSET_EQN

|- ((A ∩ B = A) ⇔ A ⊆ B) ∧ ((A ∩ B = B) ⇔ B ⊆ A)

PSUBSET_SING

|- ∀s x. x ⊂ {s} ⇔ (x = ∅)

INTER_UNION

|- ((A ∪ B) ∩ A = A) ∧ ((B ∪ A) ∩ A = A) ∧ (A ∩ (A ∪ B) = A) ∧
   (A ∩ (B ∪ A) = A)

UNION_DELETE

|- ∀A B x. A ∪ B DELETE x = A DELETE x ∪ (B DELETE x)

DELETE_SUBSET_INSERT

|- ∀s e s2. s DELETE e ⊆ s2 ⇔ s ⊆ e INSERT s2

IN_INSERT_EXPAND

|- ∀x y P. x ∈ y INSERT P ⇔ (x = y) ∨ x ≠ y ∧ x ∈ P

FINITE_INTER

|- ∀s1 s2. FINITE s1 ∨ FINITE s2 ⇒ FINITE (s1 ∩ s2)

INSERT_EQ_SING

|- ∀s x y. (x INSERT s = {y}) ⇔ (x = y) ∧ s ⊆ {y}

CARD_UNION_LE

|- FINITE s ∧ FINITE t ⇒ CARD (s ∪ t) ≤ CARD s + CARD t

IMAGE_SUBSET_gen

|- ∀f s u t. s ⊆ u ∧ IMAGE f u ⊆ t ⇒ IMAGE f s ⊆ t

CARD_REST

|- ∀s. FINITE s ∧ s ≠ ∅ ⇒ (CARD (REST s) = CARD s − 1)

SUBSET_DIFF_EMPTY

|- ∀s t. (s DIFF t = ∅) ⇔ s ⊆ t

DIFF_INTER_SUBSET

|- ∀r s t. r ⊆ s ⇒ (r DIFF s ∩ t = r DIFF t)

UNION_DIFF_2

|- ∀s t. s ∪ (s DIFF t) = s

count_add

|- ∀n m. count (n + m) = count n ∪ IMAGE ($+ n) (count m)

IMAGE_EQ_SING

|- (IMAGE f s = {z}) ⇔ s ≠ ∅ ∧ ∀x. x ∈ s ⇒ (f x = z)

count_add1

|- ∀n. count (n + 1) = n INSERT count n

compl_insert

|- ∀s x. COMPL (x INSERT s) = COMPL s DELETE x

in_max_set

|- ∀s. FINITE s ⇒ ∀x. x ∈ s ⇒ x ≤ MAX_SET s