Theory finite_set

⊢ ∀AB al bfs. FSET AB al bfs ⇔ ∃bl. LIST_REL AB al bl ∧ bfs = fset_ABS bl

⊢ fBIGUNION = (MAP fset_REP ∘ fset_REP ---> fset_ABS) FLAT

⊢ fCARD = (fset_REP ---> I) (LENGTH ∘ nub)

⊢ fDELETE = (I ---> fset_REP ---> fset_ABS) (λe. FILTER ($¬ ∘ $= e))

⊢ fDIFF =
  (fset_REP ---> fset_REP ---> fset_ABS)
    (λl1 l2. FILTER (λx. ¬MEM x l2) l1)

⊢ fEMPTY = fset_ABS []

⊢ fIMAGE = ((I ---> I) ---> fset_REP ---> fset_ABS) MAP

⊢ fINSERT = (I ---> fset_REP ---> fset_ABS) CONS

⊢ fINTER = (fset_REP ---> fset_REP ---> fset_ABS) (FILTER ∘ flip $IN ∘ set)

⊢ fIN = (I ---> fset_REP ---> I) (λx l. MEM x l)

⊢ ∀f s a0. fITSET f s a0 = @a. fITSETr f s a0 a

⊢ ∀s. fMAX_SET s = fITSET MAX s 0

⊢ ∀f s. fSUM_IMAGE f s = fITSET (λe a. f e + a) s 0

⊢ fUNION = (fset_REP ---> fset_REP ---> fset_ABS) $++

⊢ ∀s. fromSet s = ITSET fINSERT s fEMPTY

⊢ ∀l1 l2. fsequiv l1 l2 ⇔ set l1 = set l2

⊢ ∀r. fset_ABS r = fset_ABS_CLASS (fsequiv r)

⊢ ∀AB fs1 fs2. fset_REL AB fs1 fs2 ⇔ ∀a b. AB a b ⇒ (fIN a fs1 ⇔ fIN b fs2)

⊢ ∀a. fset_REP a = $@ (fset_REP_CLASS a)

⊢ ∃rep. TYPE_DEFINITION (λc. ∃r. fsequiv r r ∧ c = fsequiv r) rep

⊢ (∀a. fset_ABS_CLASS (fset_REP_CLASS a) = a) ∧
  ∀r. (λc. ∃r. fsequiv r r ∧ c = fsequiv r) r ⇔
      fset_REP_CLASS (fset_ABS_CLASS r) = r

⊢ ∀AB A B.
    rel_set AB A B ⇔
    (∀a. a ∈ A ⇒ ∃b. b ∈ B ∧ AB a b) ∧ ∀b. b ∈ B ⇒ ∃a. a ∈ A ∧ AB a b

⊢ ∀AB s fs.
    sfSETREL AB s fs ⇔
    (∀a. a ∈ s ⇒ ∃b. fIN b fs ∧ AB a b) ∧ ∀b. fIN b fs ⇒ ∃a. a ∈ s ∧ AB a b

⊢ ∀fs. toSet fs = {x | fIN x fs}

⊢ ∀fs. ∃r. fs = fset_ABS_CLASS (fsequiv r)

⊢ FUN_REL (rel_set (rel_set AB)) (rel_set AB) BIGUNION BIGUNION

⊢ CARD (toSet s) = fCARD s

⊢ fIN e s ⇔ ∃s0. s = fINSERT e s0 ∧ ¬fIN e s0

⊢ ∀e. fDELETE e fEMPTY = fEMPTY

⊢ ∀s1 s2. s1 = s2 ⇔ ∀e. fIN e s1 ⇔ fIN e s2

⊢ ∀s. FINITE (toSet s)

⊢ FUN_REL (LIST_REL (LIST_REL AB)) (LIST_REL AB) FLAT FLAT

⊢ FUN_REL FSET0 (FUN_REL FSET0 $<=>) fsequiv $=

⊢ FSET AB = FSET0 ∘ᵣ LIST_REL AB

⊢ right_unique AB ⇒ right_unique (FSET AB)

⊢ surj AB ⇒ surj (FSET AB)

⊢ FUN_REL D1 R1 ∘ᵣ FUN_REL D2 R2 ⊆ᵣ FUN_REL (D1 ∘ᵣ D2) (R1 ∘ᵣ R2)

⊢ D2 ⊆ᵣ D1 ∧ R1 ⊆ᵣ R2 ⇒ FUN_REL D1 R1 ⊆ᵣ FUN_REL D2 R2

⊢ ∀e s. fINSERT e (fDELETE e s) = fINSERT e s

⊢ fIN e (fBIGUNION fss) ⇔ ∃fs. fIN fs fss ∧ fIN e fs

⊢ ∀a b s. fIN a (fDELETE b s) ⇔ a ≠ b ∧ fIN a s

⊢ ∀e s1 s2. fIN e (fDIFF s1 s2) ⇔ fIN e s1 ∧ ¬fIN e s2

⊢ ∀f x s. fIN x (fIMAGE f s) ⇔ ∃y. fIN y s ∧ x = f y

⊢ ∀e1 e2 s. fIN e1 (fINSERT e2 s) ⇔ e1 = e2 ∨ fIN e1 s

⊢ ∀e s1 s2. fIN e (fINTER s1 s2) ⇔ fIN e s1 ∧ fIN e s2

⊢ ∀e s1 s2. fIN e (fUNION s1 s2) ⇔ fIN e s1 ∨ fIN e s2

⊢ FINITE s ⇒ (fIN e (fromSet s) ⇔ e ∈ s)

⊢ x ∈ toSet (fINSERT a s) ⇔ x = a ∨ x ∈ toSet s

⊢ Qt (LIST_REL fsequiv) (MAP fset_ABS) (MAP fset_REP) (LIST_REL FSET0)

⊢ LIST_REL FSET0 ll lfs ⇒ lfs = MAP fset_ABS ll

⊢ FUN_REL (LIST_REL AB) (rel_set AB) set set

⊢ FUN_REL (LIST_REL AB) (rel_set AB) set set

⊢ FUN_REL (FUN_REL AB CD) (FUN_REL (LIST_REL AB) (LIST_REL CD)) MAP MAP

⊢ FSET0 l fs ⇒ ∀a. MEM a l ⇔ fIN a fs

⊢ MEM x (fset_REP fs) ⇔ fIN x fs

⊢ bi_unique AB ⇒
  FUN_REL AB (FUN_REL (LIST_REL AB) $<=>) (λx l. MEM x l) (λx l. MEM x l)

⊢ ∀h t. fEMPTY ≠ fINSERT h t

⊢ ∀e. ¬fIN e fEMPTY

⊢ Qt R1 Abs1 Rep1 Tf1 ∧ Qt R2 Abs2 Rep2 Tf2 ⇒
  Qt (Tf1ᵀ ∘ᵣ R2 ∘ᵣ Tf1) (Abs2 ∘ Abs1) (Rep1 ∘ Rep2) (Tf2 ∘ᵣ Tf1)

⊢ RDOM (FSET AB) = (λal. ∀x. MEM x al ⇒ RDOM AB x)

⊢ RDOM (FUN_REL FSET0 $<=>) = (λlP. ∀l1 l2. lP l1 ∧ fsequiv l1 l2 ⇒ lP l2)

⊢ fset_REP_CLASS (fset_ABS_CLASS (fsequiv r)) = fsequiv r

⊢ fset_REP_CLASS fs1 = fset_REP_CLASS fs2 ⇔ fs1 = fs2

⊢ ∀fs. ∃x. fset_REP_CLASS fs x

⊢ R1 ⊆ᵣ R2 ⇒ R1 x y ⇒ R2 x y

⊢ R ⊆ᵣ R

⊢ bitotal AB ⇒ FUN_REL AB $<=> ⊆ᵣ rel_set AB

⊢ ∀r. fset_REP_CLASS (fset_ABS_CLASS (fsequiv r)) = fsequiv r

⊢ equalityp AB ⇒ equalityp (rel_set AB)

⊢ ∀a A. fIN a A ⇔ fINSERT a A = A

⊢ fBIGUNION (fset_ABS l) = FOLDL fUNION fEMPTY l

⊢ FUN_REL (FSET (FSET AB)) (FSET AB) FLAT fBIGUNION

⊢ ∀s. fCARD s = 0 ⇔ s = fEMPTY

⊢ fCARD fEMPTY = 0 ∧ ∀e s. fCARD (fINSERT e s) = 1 + fCARD (fDELETE e s)

⊢ FUN_REL FSET0 $= (LENGTH ∘ nub) fCARD

⊢ fDELETE a (fINSERT a A) = fDELETE a A

⊢ fDELETE e (fUNION A B) = fUNION (fDELETE e A) (fDELETE e B)

⊢ ∀e s. ¬fIN e s ⇒ fDELETE e s = s

⊢ FUN_REL $= (FUN_REL FSET0 FSET0) (λe. FILTER ($¬ ∘ $= e)) fDELETE

⊢ FUN_REL FSET0 (FUN_REL FSET0 FSET0) (λl1 l2. FILTER (λx. ¬MEM x l2) l1)
    fDIFF

⊢ FSET0 [] fEMPTY

⊢ (∀x y. f x = f y ⇔ x = y) ⇒ (fIMAGE f x = fIMAGE f y ⇔ x = y)

⊢ fIMAGE (f ∘ g) s = fIMAGE f (fIMAGE g s)

⊢ fIMAGE (λx. x) s = s ∧ fIMAGE I s = s

⊢ fIMAGE f (fUNION s1 s2) = fUNION (fIMAGE f s1) (fIMAGE f s2)

⊢ FUN_REL (FUN_REL AB CD) (FUN_REL (FSET AB) (FSET CD)) MAP fIMAGE

⊢ (∀f. fIMAGE f fEMPTY = fEMPTY) ∧
  ∀f e s. fIMAGE f (fINSERT e s) = fINSERT (f e) (fIMAGE f s)

⊢ ∀e1 e2 s. fINSERT e1 (fINSERT e2 s) = fINSERT e2 (fINSERT e1 s)

⊢ ∀e s. fINSERT e (fINSERT e s) = fINSERT e s

⊢ FUN_REL $= (FUN_REL FSET0 FSET0) CONS fINSERT

⊢ FUN_REL AB (FUN_REL (sfSETREL AB) (sfSETREL AB)) $INSERT fINSERT

⊢ fINTER a b = fINTER b a

⊢ ∀x. fINTER x fEMPTY = fEMPTY ∧ fINTER fEMPTY x = fEMPTY

⊢ ∀x. fINTER x x = x

⊢ fINTER (fINSERT a A) B =
  (if fIN a B then fINSERT a (fINTER A B) else fINTER A B) ∧
  fINTER A (fINSERT b B) =
  if fIN b A then fINSERT b (fINTER A B) else fINTER A B

⊢ FUN_REL FSET0 (FUN_REL FSET0 FSET0) (FILTER ∘ flip $IN ∘ set) fINTER

⊢ ∀e fs. fIN e fs ⇔ e ∈ toSet fs

⊢ ∀A e. fIN e A ⇒ e ≤ fMAX_SET A

⊢ fIN x (fset_ABS l) ⇔ MEM x l

⊢ bi_unique AB ⇒ FUN_REL AB (FUN_REL (FSET AB) $<=>) (λx l. MEM x l) fIN

⊢ bi_unique AB ⇒ FUN_REL AB (FUN_REL (sfSETREL AB) $<=>) $IN fIN

⊢ fITSET f fEMPTY a = a

⊢ (∀x y a. f x (f y a) = f y (f x a)) ⇒
  ∀e s a. fITSET f (fINSERT e s) a = f e (fITSET f (fDELETE e s) a)

⊢ (∀x y a. f x (f y a) = f y (f x a)) ⇒
  ∀e s a. fITSET f (fINSERT e s) a = fITSET f (fDELETE e s) (f e a)

⊢ ∀f a0 a1 a2.
    fITSETr f a0 a1 a2 ⇔
    a0 = fEMPTY ∧ a2 = a1 ∨
    ∃e s A1. a0 = fINSERT e s ∧ a2 = f e A1 ∧ fITSETr f s a1 A1 ∧ ¬fIN e s

⊢ (∀x y a. f x (f y a) = f y (f x a)) ⇒
  ∀s a0 a1 a2. fITSETr f s a0 a1 ∧ fITSETr f s a0 a2 ⇒ a1 = a2

⊢ ∀f fITSETr'.
    (∀A. fITSETr' fEMPTY A A) ∧
    (∀e s A0 A1.
       fITSETr' s A0 A1 ∧ ¬fIN e s ⇒ fITSETr' (fINSERT e s) A0 (f e A1)) ⇒
    ∀a0 a1 a2. fITSETr f a0 a1 a2 ⇒ fITSETr' a0 a1 a2

⊢ ∀f. (∀A. fITSETr f fEMPTY A A) ∧
      ∀e s A0 A1.
        fITSETr f s A0 A1 ∧ ¬fIN e s ⇒ fITSETr f (fINSERT e s) A0 (f e A1)

⊢ ∀f fITSETr'.
    (∀A. fITSETr' fEMPTY A A) ∧
    (∀e s A0 A1.
       fITSETr f s A0 A1 ∧ fITSETr' s A0 A1 ∧ ¬fIN e s ⇒
       fITSETr' (fINSERT e s) A0 (f e A1)) ⇒
    ∀a0 a1 a2. fITSETr f a0 a1 a2 ⇒ fITSETr' a0 a1 a2

⊢ ∀s f a0. ∃a. fITSETr f s a0 a

⊢ ∀A B. (∀e. fIN e A ⇒ fIN e B) ⇒ fMAX_SET A ≤ fMAX_SET B

⊢ fMAX_SET fEMPTY = 0 ∧ fMAX_SET (fINSERT e A) = MAX e (fMAX_SET A)

⊢ A ≠ fEMPTY ⇒ fIN (fMAX_SET A) A

⊢ ∀A B. (∀a. fIN a A ⇒ fIN a B) ⇒ fSUM_IMAGE f A ≤ fSUM_IMAGE f B

⊢ fSUM_IMAGE f fEMPTY = 0 ∧
  fSUM_IMAGE f (fINSERT e A) = f e + fSUM_IMAGE f (fDELETE e A)

⊢ ∀A B.
    fSUM_IMAGE f (fUNION A B) =
    fSUM_IMAGE f A + fSUM_IMAGE f B − fSUM_IMAGE f (fINTER A B)

⊢ ∀s1 s2 s3. fUNION s1 (fUNION s2 s3) = fUNION (fUNION s1 s2) s3

⊢ ∀s1 s2. fUNION s1 s2 = fUNION s2 s1

⊢ ∀s. fUNION fEMPTY s = s ∧ fUNION s fEMPTY = s

⊢ ∀s1 s2. fUNION s1 s2 = fEMPTY ⇔ s1 = fEMPTY ∧ s2 = fEMPTY

⊢ ∀s. fUNION s s = s

⊢ fUNION (fINSERT a A) B = fINSERT a (fUNION A B)

⊢ FUN_REL FSET0 (FUN_REL FSET0 FSET0) $++ fUNION

⊢ FUN_REL (sfSETREL AB) (FUN_REL (sfSETREL AB) (sfSETREL AB)) $UNION fUNION

⊢ fromSet ∅ = fEMPTY

⊢ FINITE s ⇒ fromSet (e INSERT s) = fINSERT e (fromSet s)

⊢ ∀l. fromSet (set l) = fset_ABS l

⊢ fromSet (toSet s) = s

⊢ EQUIV fsequiv

⊢ fsequiv l l

⊢ Qt fsequiv fset_ABS fset_REP FSET0

⊢ fset_ABS l1 = fset_ABS l2 ⇔ fsequiv l1 l2

⊢ fset_ABS (MAP f l) = fIMAGE f (fset_ABS l)

⊢ fset_ABS (fset_REP s) = s

⊢ (∀a. fset_ABS_CLASS (fset_REP_CLASS a) = a) ∧
  ∀c. (∃r. fsequiv r r ∧ c = fsequiv r) ⇔
      fset_REP_CLASS (fset_ABS_CLASS c) = c

⊢ ∀fs. ∃l. fset_ABS l = fs

⊢ QUOTIENT fsequiv fset_ABS fset_REP

⊢ fset_REP fs1 = fset_REP fs2 ⇔ fs1 = fs2

⊢ fset_REP fEMPTY = []

⊢ ∀s. s = fEMPTY ∨ ∃e s0. s = fINSERT e s0 ∧ ¬fIN e s0

⊢ ∀P. P fEMPTY ∧ (∀e s. P s ∧ ¬fIN e s ⇒ P (fINSERT e s)) ⇒ ∀s. P s

⊢ left_unique AB ⇒ left_unique (rel_set AB)

⊢ rel_set $= = $=

⊢ bi_unique AB ⇒ rel_set AB ⊆ᵣ FUN_REL AB $<=>

⊢ rel_set AB ∅ ∅

⊢ right_unique FSET0

⊢ right_unique AB ⇒ right_unique (rel_set AB)

⊢ ∀fss. toSet (fBIGUNION fss) = BIGUNION (toSet (fIMAGE toSet fss))

⊢ ∀f fs. toSet (fIMAGE f fs) = IMAGE f (toSet fs)

⊢ surj FSET0

⊢ surj AB ∧ right_unique AB ∧ surj CD ⇒ surj (FUN_REL AB CD)

⊢ ∀fs1 fs2. toSet fs1 = toSet fs2 ⇔ fs1 = fs2

⊢ Qt (λx y. FINITE x ∧ x = y) fromSet toSet (λs fs. s = toSet fs)

⊢ toSet fEMPTY = ∅

⊢ toSet (fIMAGE f s) = IMAGE f (toSet s)

⊢ toSet (fINSERT x s) = x INSERT toSet s

⊢ toSet (fUNION s1 s2) = toSet s1 ∪ toSet s2

⊢ FINITE s ⇒ toSet (fromSet s) = s

⊢ ∀l. toSet (fset_ABS l) = set l

⊢ FUN_REL (FSET AB) (rel_set AB) set toSet

⊢ bi_unique AB ⇒ FUN_REL (FSET AB) (FUN_REL AB $<=>) set toSet

⊢ total AB ⇒ total (FSET AB)