Theory "bag"

Signature

Definitions

EMPTY_BAG

|- {||} = K 0

BAG_INN

|- ∀e n b. BAG_INN e n b ⇔ b e ≥ n

SUB_BAG

|- ∀b1 b2. b1 ≤ b2 ⇔ ∀x n. BAG_INN x n b1 ⇒ BAG_INN x n b2

PSUB_BAG

|- ∀b1 b2. b1 < b2 ⇔ b1 ≤ b2 ∧ b1 ≠ b2

BAG_IN

|- ∀e b. e ⋲ b ⇔ BAG_INN e 1 b

BAG_UNION

|- ∀b c. b ⊎ c = (λx. b x + c x)

BAG_DIFF

|- ∀b1 b2. b1 − b2 = (λx. b1 x − b2 x)

BAG_INSERT

|- ∀e b. BAG_INSERT e b = (λx. if x = e then b e + 1 else b x)

BAG_INTER

|- ∀b1 b2. BAG_INTER b1 b2 = (λx. if b1 x < b2 x then b1 x else b2 x)

BAG_MERGE

|- ∀b1 b2. BAG_MERGE b1 b2 = (λx. if b1 x < b2 x then b2 x else b1 x)

BAG_DELETE

|- ∀b0 e b. BAG_DELETE b0 e b ⇔ (b0 = BAG_INSERT e b)

SING_BAG

|- ∀b. SING_BAG b ⇔ ∃x. b = {|x|}

EL_BAG

|- ∀e. EL_BAG e = {|e|}

SET_OF_BAG

|- ∀b. SET_OF_BAG b = (λx. x ⋲ b)

BAG_OF_SET

|- ∀P. BAG_OF_SET P = (λx. if x ∈ P then 1 else 0)

BAG_DISJOINT

|- ∀b1 b2. BAG_DISJOINT b1 b2 ⇔ DISJOINT (SET_OF_BAG b1) (SET_OF_BAG b2)

FINITE_BAG

|- ∀b. FINITE_BAG b ⇔ ∀P. P {||} ∧ (∀b. P b ⇒ ∀e. P (BAG_INSERT e b)) ⇒ P b

BAG_CARD_RELn

|- ∀b n.
     BAG_CARD_RELn b n ⇔
     ∀P. P {||} 0 ∧ (∀b n. P b n ⇒ ∀e. P (BAG_INSERT e b) (SUC n)) ⇒ P b n

BAG_CARD

|- ∀b. FINITE_BAG b ⇒ BAG_CARD_RELn b (BAG_CARD b)

BAG_FILTER_DEF

|- ∀P b. BAG_FILTER P b = (λe. if P e then b e else 0)

BAG_IMAGE_DEF

|- ∀f b.
     BAG_IMAGE f b =
     (λe.
        (let sb = BAG_FILTER (λe0. f e0 = e) b
         in
           if FINITE_BAG sb then BAG_CARD sb else 1))

BAG_CHOICE_DEF

|- ∀b. b ≠ {||} ⇒ BAG_CHOICE b ⋲ b

BAG_REST_DEF

|- ∀b. BAG_REST b = b − EL_BAG (BAG_CHOICE b)

ITBAG_tupled_primitive_def

|- ∀f.
     ITBAG_tupled f =
     WFREC
       (@R.
          WF R ∧
          ∀acc b.
            FINITE_BAG b ∧ b ≠ {||} ⇒
            R (BAG_REST b,f (BAG_CHOICE b) acc) (b,acc))
       (λITBAG_tupled a.
          case a of
            (b,acc) =>
              I
                (if FINITE_BAG b then
                   if b = {||} then acc
                   else ITBAG_tupled (BAG_REST b,f (BAG_CHOICE b) acc)
                 else ARB))

ITBAG_curried_def

|- ∀f x x1. ITBAG f x x1 = ITBAG_tupled f (x,x1)

BAG_GEN_SUM_def

|- ∀bag n. BAG_GEN_SUM bag n = ITBAG $+ bag n

BAG_GEN_PROD_def

|- ∀bag n. BAG_GEN_PROD bag n = ITBAG $* bag n

BAG_EVERY

|- ∀P b. BAG_EVERY P b ⇔ ∀e. e ⋲ b ⇒ P e

BAG_ALL_DISTINCT

|- ∀b. BAG_ALL_DISTINCT b ⇔ ∀e. b e ≤ 1

BIG_BAG_UNION_def

|- ∀sob. BIG_BAG_UNION sob = (λx. ∑ (λb. b x) sob)

mlt1_def

|- ∀r b1 b2.
     mlt1 r b1 b2 ⇔
     FINITE_BAG b1 ∧ FINITE_BAG b2 ∧
     ∃e rep res.
       (b1 = rep ⊎ res) ∧ (b2 = res ⊎ {|e|}) ∧ ∀e'. e' ⋲ rep ⇒ r e' e

dominates_def

|- ∀R s1 s2. dominates R s1 s2 ⇔ ∀x. x ∈ s1 ⇒ ∃y. y ∈ s2 ∧ R x y

bag_size_def

|- ∀eltsize b. bag_size eltsize b = ITBAG (λe acc. 1 + eltsize e + acc) b 0

Theorems

EMPTY_BAG_alt

|- {||} = (λx. 0)

BAG_cases

|- ∀b. (b = {||}) ∨ ∃b0 e. b = BAG_INSERT e b0

BAG_MERGE_IDEM

|- ∀b. BAG_MERGE b b = b

BAG_INN_0

|- ∀b e. BAG_INN e 0 b

BAG_INN_LESS

|- ∀b e n m. BAG_INN e n b ∧ m < n ⇒ BAG_INN e m b

BAG_IN_BAG_INSERT

|- ∀b e1 e2. e1 ⋲ BAG_INSERT e2 b ⇔ (e1 = e2) ∨ e1 ⋲ b

BAG_INN_BAG_INSERT

|- ∀b e1 e2.
     BAG_INN e1 n (BAG_INSERT e2 b) ⇔
     BAG_INN e1 (n − 1) b ∧ (e1 = e2) ∨ BAG_INN e1 n b

BAG_INN_BAG_INSERT_STRONG

|- ∀b n e1 e2.
     BAG_INN e1 n (BAG_INSERT e2 b) ⇔
     BAG_INN e1 (n − 1) b ∧ (e1 = e2) ∨ BAG_INN e1 n b ∧ e1 ≠ e2

BAG_UNION_EQ_LCANCEL1

|- (b = b ⊎ c) ⇔ (c = {||})

BAG_UNION_EQ_RCANCEL1

|- (b = c ⊎ b) ⇔ (c = {||})

BAG_IN_BAG_UNION

|- ∀b1 b2 e. e ⋲ b1 ⊎ b2 ⇔ e ⋲ b1 ∨ e ⋲ b2

BAG_INN_BAG_UNION

|- ∀n e b1 b2.
     BAG_INN e n (b1 ⊎ b2) ⇔
     ∃m1 m2. (n = m1 + m2) ∧ BAG_INN e m1 b1 ∧ BAG_INN e m2 b2

BAG_INN_BAG_MERGE

|- ∀n e b1 b2. BAG_INN e n (BAG_MERGE b1 b2) ⇔ BAG_INN e n b1 ∨ BAG_INN e n b2

BAG_IN_BAG_MERGE

|- ∀e b1 b2. e ⋲ BAG_MERGE b1 b2 ⇔ e ⋲ b1 ∨ e ⋲ b2

BAG_EXTENSION

|- ∀b1 b2. (b1 = b2) ⇔ ∀n e. BAG_INN e n b1 ⇔ BAG_INN e n b2

BAG_UNION_INSERT

|- ∀e b1 b2.
     (BAG_INSERT e b1 ⊎ b2 = BAG_INSERT e (b1 ⊎ b2)) ∧
     (b1 ⊎ BAG_INSERT e b2 = BAG_INSERT e (b1 ⊎ b2))

BAG_INSERT_DIFF

|- ∀x b. BAG_INSERT x b ≠ b

BAG_INSERT_NOT_EMPTY

|- ∀x b. BAG_INSERT x b ≠ {||}

BAG_INSERT_ONE_ONE

|- ∀b1 b2 x. (BAG_INSERT x b1 = BAG_INSERT x b2) ⇔ (b1 = b2)

C_BAG_INSERT_ONE_ONE

|- ∀x y b. (BAG_INSERT x b = BAG_INSERT y b) ⇔ (x = y)

BAG_INSERT_commutes

|- ∀b e1 e2. BAG_INSERT e1 (BAG_INSERT e2 b) = BAG_INSERT e2 (BAG_INSERT e1 b)

BAG_DECOMPOSE

|- ∀e b. e ⋲ b ⇒ ∃b'. b = BAG_INSERT e b'

BAG_UNION_LEFT_CANCEL

|- ∀b b1 b2. (b ⊎ b1 = b ⊎ b2) ⇔ (b1 = b2)

COMM_BAG_UNION

|- ∀b1 b2. b1 ⊎ b2 = b2 ⊎ b1

BAG_UNION_RIGHT_CANCEL

|- ∀b b1 b2. (b1 ⊎ b = b2 ⊎ b) ⇔ (b1 = b2)

ASSOC_BAG_UNION

|- ∀b1 b2 b3. b1 ⊎ (b2 ⊎ b3) = b1 ⊎ b2 ⊎ b3

BAG_UNION_EMPTY

|- (∀b. b ⊎ {||} = b) ∧ (∀b. {||} ⊎ b = b) ∧
   ∀b1 b2. (b1 ⊎ b2 = {||}) ⇔ (b1 = {||}) ∧ (b2 = {||})

BAG_DELETE_EMPTY

|- ∀e b. ¬BAG_DELETE {||} e b

BAG_DELETE_commutes

|- ∀b0 b1 b2 e1 e2.
     BAG_DELETE b0 e1 b1 ∧ BAG_DELETE b1 e2 b2 ⇒
     ∃b'. BAG_DELETE b0 e2 b' ∧ BAG_DELETE b' e1 b2

BAG_DELETE_11

|- ∀b0 e1 e2 b1 b2.
     BAG_DELETE b0 e1 b1 ∧ BAG_DELETE b0 e2 b2 ⇒ ((e1 = e2) ⇔ (b1 = b2))

BAG_INN_BAG_DELETE

|- ∀b n e. BAG_INN e n b ∧ n > 0 ⇒ ∃b'. BAG_DELETE b e b'

BAG_IN_BAG_DELETE

|- ∀b e. e ⋲ b ⇒ ∃b'. BAG_DELETE b e b'

BAG_DELETE_INSERT

|- ∀x y b1 b2.
     BAG_DELETE (BAG_INSERT x b1) y b2 ⇒
     (x = y) ∧ (b1 = b2) ∨ (∃b3. BAG_DELETE b1 y b3) ∧ x ≠ y

BAG_DELETE_BAG_IN_up

|- ∀b0 b e. BAG_DELETE b0 e b ⇒ ∀e'. e' ⋲ b ⇒ e' ⋲ b0

BAG_DELETE_BAG_IN_down

|- ∀b0 b e1 e2. BAG_DELETE b0 e1 b ∧ e1 ≠ e2 ∧ e2 ⋲ b0 ⇒ e2 ⋲ b

BAG_DELETE_BAG_IN

|- ∀b0 b e. BAG_DELETE b0 e b ⇒ e ⋲ b0

BAG_DELETE_concrete

|- ∀b0 b e.
     BAG_DELETE b0 e b ⇔
     b0 e > 0 ∧ (b = (λx. if x = e then b0 e − 1 else b0 x))

BAG_UNION_DIFF_eliminate

|- (b ⊎ c − c = b) ∧ (c ⊎ b − c = b)

BAG_INSERT_EQUAL

|- (BAG_INSERT a M = BAG_INSERT b N) ⇔
   (M = N) ∧ (a = b) ∨ ∃k. (M = BAG_INSERT b k) ∧ (N = BAG_INSERT a k)

BAG_DELETE_TWICE

|- ∀b0 e1 e2 b1 b2.
     BAG_DELETE b0 e1 b1 ∧ BAG_DELETE b0 e2 b2 ∧ b1 ≠ b2 ⇒
     ∃b. BAG_DELETE b1 e2 b ∧ BAG_DELETE b2 e1 b

SING_BAG_THM

|- ∀e. SING_BAG {|e|}

EL_BAG_11

|- ∀x y. (EL_BAG x = EL_BAG y) ⇒ (x = y)

EL_BAG_INSERT_squeeze

|- ∀x b y. (EL_BAG x = BAG_INSERT y b) ⇒ (x = y) ∧ (b = {||})

SING_EL_BAG

|- ∀e. SING_BAG (EL_BAG e)

BAG_INSERT_UNION

|- ∀b e. BAG_INSERT e b = EL_BAG e ⊎ b

BAG_INSERT_EQ_UNION

|- ∀e b1 b2 b. (BAG_INSERT e b = b1 ⊎ b2) ⇒ e ⋲ b1 ∨ e ⋲ b2

BAG_DELETE_SING

|- ∀b e. BAG_DELETE b e {||} ⇒ SING_BAG b

NOT_IN_EMPTY_BAG

|- ∀x. ¬(x ⋲ {||})

BAG_INN_EMPTY_BAG

|- ∀e n. BAG_INN e n {||} ⇔ (n = 0)

MEMBER_NOT_EMPTY

|- ∀b. (∃x. x ⋲ b) ⇔ b ≠ {||}

SUB_BAG_LEQ

|- b1 ≤ b2 ⇔ ∀x. b1 x ≤ b2 x

SUB_BAG_EMPTY

|- (∀b. {||} ≤ b) ∧ ∀b. b ≤ {||} ⇔ (b = {||})

SUB_BAG_REFL

|- ∀b. b ≤ b

PSUB_BAG_IRREFL

|- ∀b. ¬(b < b)

SUB_BAG_ANTISYM

|- ∀b1 b2. b1 ≤ b2 ∧ b2 ≤ b1 ⇒ (b1 = b2)

PSUB_BAG_ANTISYM

|- ∀b1 b2. ¬(b1 < b2 ∧ b2 < b1)

SUB_BAG_TRANS

|- ∀b1 b2 b3. b1 ≤ b2 ∧ b2 ≤ b3 ⇒ b1 ≤ b3

PSUB_BAG_TRANS

|- ∀b1 b2 b3. b1 < b2 ∧ b2 < b3 ⇒ b1 < b3

PSUB_BAG_SUB_BAG

|- ∀b1 b2. b1 < b2 ⇒ b1 ≤ b2

PSUB_BAG_NOT_EQ

|- ∀b1 b2. b1 < b2 ⇒ b1 ≠ b2

BAG_DIFF_EMPTY

|- (∀b. b − b = {||}) ∧ (∀b. b − {||} = b) ∧ (∀b. {||} − b = {||}) ∧
   ∀b1 b2. b1 ≤ b2 ⇒ (b1 − b2 = {||})

BAG_DIFF_EMPTY_simple

|- (∀b. b − b = {||}) ∧ (∀b. b − {||} = b) ∧ ∀b. {||} − b = {||}

BAG_DIFF_EQ_EMPTY

|- (b − c = {||}) ⇔ b ≤ c

BAG_DIFF_INSERT_same

|- ∀x b1 b2. BAG_INSERT x b1 − BAG_INSERT x b2 = b1 − b2

BAG_DIFF_INSERT

|- ∀x b1 b2. ¬(x ⋲ b1) ⇒ (BAG_INSERT x b2 − b1 = BAG_INSERT x (b2 − b1))

NOT_IN_BAG_DIFF

|- ∀x b1 b2. ¬(x ⋲ b1) ⇒ (b1 − BAG_INSERT x b2 = b1 − b2)

BAG_IN_DIFF_I

|- e ⋲ b1 ∧ ¬(e ⋲ b2) ⇒ e ⋲ b1 − b2

BAG_IN_DIFF_E

|- e ⋲ b1 − b2 ⇒ e ⋲ b1

BAG_UNION_DIFF

|- ∀X Y Z. Z ≤ Y ⇒ (X ⊎ (Y − Z) = X ⊎ Y − Z) ∧ (Y − Z ⊎ X = X ⊎ Y − Z)

BAG_DIFF_2L

|- ∀X Y Z. X − Y − Z = X − (Y ⊎ Z)

BAG_DIFF_2R

|- ∀A B C. C ≤ B ⇒ (A − (B − C) = A ⊎ C − B)

SUB_BAG_BAG_DIFF

|- ∀X Y Y' Z W. X − Y ≤ Z − W ⇒ X − (Y ⊎ Y') ≤ Z − (W ⊎ Y')

BAG_DIFF_UNION_eliminate

|- ∀b1 b2 b3.
     (b1 ⊎ b2 − (b1 ⊎ b3) = b2 − b3) ∧ (b1 ⊎ b2 − (b3 ⊎ b1) = b2 − b3) ∧
     (b2 ⊎ b1 − (b1 ⊎ b3) = b2 − b3) ∧ (b2 ⊎ b1 − (b3 ⊎ b1) = b2 − b3)

SUB_BAG_UNION_eliminate

|- ∀b1 b2 b3.
     (b1 ⊎ b2 ≤ b1 ⊎ b3 ⇔ b2 ≤ b3) ∧ (b1 ⊎ b2 ≤ b3 ⊎ b1 ⇔ b2 ≤ b3) ∧
     (b2 ⊎ b1 ≤ b1 ⊎ b3 ⇔ b2 ≤ b3) ∧ (b2 ⊎ b1 ≤ b3 ⊎ b1 ⇔ b2 ≤ b3)

move_BAG_UNION_over_eq

|- ∀X Y Z. (X ⊎ Y = Z) ⇒ (X = Z − Y)

SUB_BAG_UNION

|- (∀b1 b2. b1 ≤ b2 ⇒ ∀b. b1 ≤ b2 ⊎ b) ∧ (∀b1 b2. b1 ≤ b2 ⇒ ∀b. b1 ≤ b ⊎ b2) ∧
   (∀b1 b2 b3. b1 ≤ b2 ⊎ b3 ⇒ ∀b. b1 ≤ b2 ⊎ b ⊎ b3) ∧
   (∀b1 b2 b3. b1 ≤ b2 ⊎ b3 ⇒ ∀b. b1 ≤ b ⊎ b2 ⊎ b3) ∧
   (∀b1 b2 b3. b1 ≤ b3 ⊎ b2 ⇒ ∀b. b1 ≤ b3 ⊎ (b2 ⊎ b)) ∧
   (∀b1 b2 b3. b1 ≤ b3 ⊎ b2 ⇒ ∀b. b1 ≤ b3 ⊎ (b ⊎ b2)) ∧
   (∀b1 b2 b3 b4. b1 ≤ b3 ⇒ b2 ≤ b4 ⇒ b1 ⊎ b2 ≤ b3 ⊎ b4) ∧
   (∀b1 b2 b3 b4. b1 ≤ b4 ⇒ b2 ≤ b3 ⇒ b1 ⊎ b2 ≤ b3 ⊎ b4) ∧
   (∀b1 b2 b3 b4 b5. b1 ≤ b3 ⊎ b5 ⇒ b2 ≤ b4 ⇒ b1 ⊎ b2 ≤ b3 ⊎ b4 ⊎ b5) ∧
   (∀b1 b2 b3 b4 b5. b1 ≤ b4 ⊎ b5 ⇒ b2 ≤ b3 ⇒ b1 ⊎ b2 ≤ b3 ⊎ b4 ⊎ b5) ∧
   (∀b1 b2 b3 b4 b5. b2 ≤ b3 ⊎ b5 ⇒ b1 ≤ b4 ⇒ b1 ⊎ b2 ≤ b3 ⊎ b4 ⊎ b5) ∧
   (∀b1 b2 b3 b4 b5. b2 ≤ b4 ⊎ b5 ⇒ b1 ≤ b3 ⇒ b1 ⊎ b2 ≤ b3 ⊎ b4 ⊎ b5) ∧
   (∀b1 b2 b3 b4 b5. b1 ≤ b5 ⊎ b3 ⇒ b2 ≤ b4 ⇒ b2 ⊎ b1 ≤ b5 ⊎ (b3 ⊎ b4)) ∧
   (∀b1 b2 b3 b4 b5. b1 ≤ b5 ⊎ b4 ⇒ b2 ≤ b3 ⇒ b2 ⊎ b1 ≤ b5 ⊎ (b3 ⊎ b4)) ∧
   (∀b1 b2 b3 b4 b5. b2 ≤ b5 ⊎ b3 ⇒ b1 ≤ b4 ⇒ b2 ⊎ b1 ≤ b5 ⊎ (b3 ⊎ b4)) ∧
   (∀b1 b2 b3 b4 b5. b2 ≤ b5 ⊎ b4 ⇒ b1 ≤ b3 ⇒ b2 ⊎ b1 ≤ b5 ⊎ (b3 ⊎ b4)) ∧
   (∀b1 b2 b3 b4 b5. b1 ⊎ b2 ≤ b4 ⇒ b3 ≤ b5 ⇒ b1 ⊎ b3 ⊎ b2 ≤ b4 ⊎ b5) ∧
   (∀b1 b2 b3 b4 b5. b1 ⊎ b2 ≤ b5 ⇒ b3 ≤ b4 ⇒ b1 ⊎ b3 ⊎ b2 ≤ b4 ⊎ b5) ∧
   (∀b1 b2 b3 b4 b5. b3 ⊎ b2 ≤ b4 ⇒ b1 ≤ b5 ⇒ b1 ⊎ b3 ⊎ b2 ≤ b4 ⊎ b5) ∧
   (∀b1 b2 b3 b4 b5. b3 ⊎ b2 ≤ b5 ⇒ b1 ≤ b4 ⇒ b1 ⊎ b3 ⊎ b2 ≤ b4 ⊎ b5) ∧
   (∀b1 b2 b3 b4 b5. b2 ⊎ b1 ≤ b4 ⇒ b3 ≤ b5 ⇒ b2 ⊎ (b1 ⊎ b3) ≤ b5 ⊎ b4) ∧
   (∀b1 b2 b3 b4 b5. b2 ⊎ b1 ≤ b5 ⇒ b3 ≤ b4 ⇒ b2 ⊎ (b1 ⊎ b3) ≤ b5 ⊎ b4) ∧
   (∀b1 b2 b3 b4 b5. b2 ⊎ b3 ≤ b4 ⇒ b1 ≤ b5 ⇒ b2 ⊎ (b1 ⊎ b3) ≤ b5 ⊎ b4) ∧
   ∀b1 b2 b3 b4 b5. b2 ⊎ b3 ≤ b5 ⇒ b1 ≤ b4 ⇒ b2 ⊎ (b1 ⊎ b3) ≤ b5 ⊎ b4

SUB_BAG_EL_BAG

|- ∀e b. EL_BAG e ≤ b ⇔ e ⋲ b

SUB_BAG_INSERT

|- ∀e b1 b2. BAG_INSERT e b1 ≤ BAG_INSERT e b2 ⇔ b1 ≤ b2

SUB_BAG_INSERT_I

|- ∀b c e. b ≤ c ⇒ b ≤ BAG_INSERT e c

NOT_IN_SUB_BAG_INSERT

|- ∀b1 b2 e. ¬(e ⋲ b1) ⇒ (b1 ≤ BAG_INSERT e b2 ⇔ b1 ≤ b2)

SUB_BAG_BAG_IN

|- ∀x b1 b2. BAG_INSERT x b1 ≤ b2 ⇒ x ⋲ b2

SUB_BAG_EXISTS

|- ∀b1 b2. b1 ≤ b2 ⇔ ∃b. b2 = b1 ⊎ b

SUB_BAG_UNION_DIFF

|- ∀b1 b2 b3. b1 ≤ b3 ⇒ (b2 ≤ b3 − b1 ⇔ b1 ⊎ b2 ≤ b3)

SUB_BAG_UNION_down

|- ∀b1 b2 b3. b1 ⊎ b2 ≤ b3 ⇒ b1 ≤ b3 ∧ b2 ≤ b3

SUB_BAG_DIFF

|- (∀b1 b2. b1 ≤ b2 ⇒ ∀b3. b1 − b3 ≤ b2) ∧
   ∀b1 b2 b3 b4. b2 ≤ b1 ⇒ b4 ≤ b3 ⇒ (b1 − b2 ≤ b3 − b4 ⇔ b1 ⊎ b4 ≤ b2 ⊎ b3)

SUB_BAG_PSUB_BAG

|- ∀b1 b2. b1 ≤ b2 ⇔ b1 < b2 ∨ (b1 = b2)

BAG_DELETE_PSUB_BAG

|- ∀b0 e b. BAG_DELETE b0 e b ⇒ b < b0

SET_OF_EMPTY

|- BAG_OF_SET ∅ = {||}

BAG_IN_BAG_OF_SET

|- ∀P p. p ⋲ BAG_OF_SET P ⇔ p ∈ P

BAG_OF_EMPTY

|- SET_OF_BAG {||} = ∅

SET_BAG_I

|- ∀s. SET_OF_BAG (BAG_OF_SET s) = s

SUB_BAG_SET

|- ∀b1 b2. b1 ≤ b2 ⇒ SET_OF_BAG b1 ⊆ SET_OF_BAG b2

SET_OF_BAG_UNION

|- ∀b1 b2. SET_OF_BAG (b1 ⊎ b2) = SET_OF_BAG b1 ∪ SET_OF_BAG b2

SET_OF_BAG_MERGE

|- ∀b1 b2. SET_OF_BAG (BAG_MERGE b1 b2) = SET_OF_BAG b1 ∪ SET_OF_BAG b2

SET_OF_BAG_INSERT

|- ∀e b. SET_OF_BAG (BAG_INSERT e b) = e INSERT SET_OF_BAG b

SET_OF_EL_BAG

|- ∀e. SET_OF_BAG (EL_BAG e) = {e}

SET_OF_BAG_DIFF_SUBSET_down

|- ∀b1 b2. SET_OF_BAG b1 DIFF SET_OF_BAG b2 ⊆ SET_OF_BAG (b1 − b2)

SET_OF_BAG_DIFF_SUBSET_up

|- ∀b1 b2. SET_OF_BAG (b1 − b2) ⊆ SET_OF_BAG b1

IN_SET_OF_BAG

|- ∀x b. x ∈ SET_OF_BAG b ⇔ x ⋲ b

SET_OF_BAG_EQ_EMPTY

|- ∀b. ((∅ = SET_OF_BAG b) ⇔ (b = {||})) ∧ ((SET_OF_BAG b = ∅) ⇔ (b = {||}))

BAG_DISJOINT_EMPTY

|- ∀b. BAG_DISJOINT b {||} ∧ BAG_DISJOINT {||} b

BAG_DISJOINT_DIFF

|- ∀B1 B2. BAG_DISJOINT (B1 − B2) (B2 − B1)

BAG_DISJOINT_BAG_IN

|- ∀b1 b2. BAG_DISJOINT b1 b2 ⇔ ∀e. ¬(e ⋲ b1) ∨ ¬(e ⋲ b2)

BAG_DISJOINT_BAG_INSERT

|- (∀b1 b2 e1.
      BAG_DISJOINT (BAG_INSERT e1 b1) b2 ⇔ ¬(e1 ⋲ b2) ∧ BAG_DISJOINT b1 b2) ∧
   ∀b1 b2 e2.
     BAG_DISJOINT b1 (BAG_INSERT e2 b2) ⇔ ¬(e2 ⋲ b1) ∧ BAG_DISJOINT b1 b2

BAG_DISJOINT_BAG_UNION

|- (BAG_DISJOINT b1 (b2 ⊎ b3) ⇔ BAG_DISJOINT b1 b2 ∧ BAG_DISJOINT b1 b3) ∧
   (BAG_DISJOINT (b1 ⊎ b2) b3 ⇔ BAG_DISJOINT b1 b3 ∧ BAG_DISJOINT b2 b3)

FINITE_EMPTY_BAG

|- FINITE_BAG {||}

FINITE_BAG_INSERT

|- ∀b. FINITE_BAG b ⇒ ∀e. FINITE_BAG (BAG_INSERT e b)

FINITE_BAG_INDUCT

|- ∀P. P {||} ∧ (∀b. P b ⇒ ∀e. P (BAG_INSERT e b)) ⇒ ∀b. FINITE_BAG b ⇒ P b

STRONG_FINITE_BAG_INDUCT

|- ∀P.
     P {||} ∧ (∀b. FINITE_BAG b ∧ P b ⇒ ∀e. P (BAG_INSERT e b)) ⇒
     ∀b. FINITE_BAG b ⇒ P b

FINITE_BAG_THM

|- FINITE_BAG {||} ∧ ∀e b. FINITE_BAG (BAG_INSERT e b) ⇔ FINITE_BAG b

FINITE_BAG_DIFF

|- ∀b1. FINITE_BAG b1 ⇒ ∀b2. FINITE_BAG (b1 − b2)

FINITE_BAG_DIFF_dual

|- ∀b1. FINITE_BAG b1 ⇒ ∀b2. FINITE_BAG (b2 − b1) ⇒ FINITE_BAG b2

FINITE_BAG_UNION

|- ∀b1 b2. FINITE_BAG (b1 ⊎ b2) ⇔ FINITE_BAG b1 ∧ FINITE_BAG b2

FINITE_SUB_BAG

|- ∀b1. FINITE_BAG b1 ⇒ ∀b2. b2 ≤ b1 ⇒ FINITE_BAG b2

BAG_CARD_EMPTY

|- BAG_CARD {||} = 0

BCARD_0

|- ∀b. FINITE_BAG b ⇒ ((BAG_CARD b = 0) ⇔ (b = {||}))

BAG_CARD_THM

|- (BAG_CARD {||} = 0) ∧
   ∀b. FINITE_BAG b ⇒ ∀e. BAG_CARD (BAG_INSERT e b) = BAG_CARD b + 1

BAG_CARD_UNION

|- ∀b1 b2.
     FINITE_BAG b1 ∧ FINITE_BAG b2 ⇒
     (BAG_CARD (b1 ⊎ b2) = BAG_CARD b1 + BAG_CARD b2)

BCARD_SUC

|- ∀b.
     FINITE_BAG b ⇒
     ∀n.
       (BAG_CARD b = SUC n) ⇔ ∃b0 e. (b = BAG_INSERT e b0) ∧ (BAG_CARD b0 = n)

BAG_CARD_BAG_INN

|- ∀b. FINITE_BAG b ⇒ ∀n e. BAG_INN e n b ⇒ n ≤ BAG_CARD b

SUB_BAG_DIFF_EQ

|- ∀b1 b2. b1 ≤ b2 ⇒ (b2 = b1 ⊎ (b2 − b1))

SUB_BAG_CARD

|- ∀b1 b2. FINITE_BAG b2 ∧ b1 ≤ b2 ⇒ BAG_CARD b1 ≤ BAG_CARD b2

BAG_CARD_DIFF

|- ∀b. FINITE_BAG b ⇒ ∀c. c ≤ b ⇒ (BAG_CARD (b − c) = BAG_CARD b − BAG_CARD c)

BAG_FILTER_EMPTY

|- BAG_FILTER P {||} = {||}

BAG_FILTER_BAG_INSERT

|- BAG_FILTER P (BAG_INSERT e b) =
   if P e then BAG_INSERT e (BAG_FILTER P b) else BAG_FILTER P b

FINITE_BAG_FILTER

|- ∀b. FINITE_BAG b ⇒ FINITE_BAG (BAG_FILTER P b)

BAG_INN_BAG_FILTER

|- BAG_INN e n (BAG_FILTER P b) ⇔ (n = 0) ∨ P e ∧ BAG_INN e n b

BAG_IN_BAG_FILTER

|- e ⋲ BAG_FILTER P b ⇔ P e ∧ e ⋲ b

BAG_FILTER_FILTER

|- BAG_FILTER P (BAG_FILTER Q b) = BAG_FILTER (λa. P a ∧ Q a) b

BAG_FILTER_SUB_BAG

|- ∀P b. BAG_FILTER P b ≤ b

SET_OF_BAG_EQ_INSERT

|- ∀b e s.
     (e INSERT s = SET_OF_BAG b) ⇔
     ∃b0 eb.
       (b = eb ⊎ b0) ∧ (s = SET_OF_BAG b0) ∧ (∀e'. e' ⋲ eb ⇒ (e' = e)) ∧
       (e ∉ s ⇒ e ⋲ eb)

FINITE_SET_OF_BAG

|- ∀b. FINITE (SET_OF_BAG b) ⇔ FINITE_BAG b

BAG_IMAGE_EMPTY

|- ∀f. BAG_IMAGE f {||} = {||}

BAG_IMAGE_FINITE_INSERT

|- ∀b f e.
     FINITE_BAG b ⇒
     (BAG_IMAGE f (BAG_INSERT e b) = BAG_INSERT (f e) (BAG_IMAGE f b))

BAG_IMAGE_FINITE_UNION

|- ∀b1 b2 f.
     FINITE_BAG b1 ∧ FINITE_BAG b2 ⇒
     (BAG_IMAGE f (b1 ⊎ b2) = BAG_IMAGE f b1 ⊎ BAG_IMAGE f b2)

BAG_IMAGE_FINITE

|- ∀b. FINITE_BAG b ⇒ FINITE_BAG (BAG_IMAGE f b)

BAG_IMAGE_COMPOSE

|- ∀f g b. FINITE_BAG b ⇒ (BAG_IMAGE (f o g) b = BAG_IMAGE f (BAG_IMAGE g b))

BAG_IMAGE_FINITE_I

|- ∀b. FINITE_BAG b ⇒ (BAG_IMAGE I b = b)

BAG_IN_FINITE_BAG_IMAGE

|- FINITE_BAG b ⇒ (x ⋲ BAG_IMAGE f b ⇔ ∃y. (f y = x) ∧ y ⋲ b)

BAG_IMAGE_EQ_EMPTY

|- FINITE_BAG b ⇒ ((BAG_IMAGE f b = {||}) ⇔ (b = {||}))

BAG_INSERT_CHOICE_REST

|- ∀b. b ≠ {||} ⇒ (b = BAG_INSERT (BAG_CHOICE b) (BAG_REST b))

BAG_CHOICE_SING

|- BAG_CHOICE {|x|} = x

BAG_REST_SING

|- BAG_REST {|x|} = {||}

SUB_BAG_REST

|- ∀b. BAG_REST b ≤ b

PSUB_BAG_REST

|- ∀b. b ≠ {||} ⇒ BAG_REST b < b

SUB_BAG_UNION_MONO

|- (∀x y. x ≤ x ⊎ y) ∧ ∀x y. x ≤ y ⊎ x

PSUB_BAG_CARD

|- ∀b1 b2. FINITE_BAG b2 ∧ b1 < b2 ⇒ BAG_CARD b1 < BAG_CARD b2

EL_BAG_BAG_INSERT

|- ({|x|} = BAG_INSERT y b) ⇔ (x = y) ∧ (b = {||})

EL_BAG_SUB_BAG

|- {|x|} ≤ b ⇔ x ⋲ b

ITBAG_IND

|- ∀P.
     (∀b acc.
        (FINITE_BAG b ∧ b ≠ {||} ⇒ P (BAG_REST b) (f (BAG_CHOICE b) acc)) ⇒
        P b acc) ⇒
     ∀v v1. P v v1

ITBAG_THM

|- ∀b f acc.
     FINITE_BAG b ⇒
     (ITBAG f b acc =
      if b = {||} then acc else ITBAG f (BAG_REST b) (f (BAG_CHOICE b) acc))

ITBAG_EMPTY

|- ∀f acc. ITBAG f {||} acc = acc

ITBAG_INSERT

|- ∀f acc.
     FINITE_BAG b ⇒
     (ITBAG f (BAG_INSERT x b) acc =
      ITBAG f (BAG_REST (BAG_INSERT x b))
        (f (BAG_CHOICE (BAG_INSERT x b)) acc))

COMMUTING_ITBAG_INSERT

|- ∀f b.
     (∀x y z. f x (f y z) = f y (f x z)) ∧ FINITE_BAG b ⇒
     ∀x a. ITBAG f (BAG_INSERT x b) a = ITBAG f b (f x a)

COMMUTING_ITBAG_RECURSES

|- ∀f e b a.
     (∀x y z. f x (f y z) = f y (f x z)) ∧ FINITE_BAG b ⇒
     (ITBAG f (BAG_INSERT e b) a = f e (ITBAG f b a))

BAG_GEN_SUM_EMPTY

|- ∀n. BAG_GEN_SUM {||} n = n

BAG_GEN_PROD_EMPTY

|- ∀n. BAG_GEN_PROD {||} n = n

BAG_GEN_SUM_TAILREC

|- ∀b.
     FINITE_BAG b ⇒
     ∀x a. BAG_GEN_SUM (BAG_INSERT x b) a = BAG_GEN_SUM b (x + a)

BAG_GEN_SUM_REC

|- ∀b.
     FINITE_BAG b ⇒ ∀x a. BAG_GEN_SUM (BAG_INSERT x b) a = x + BAG_GEN_SUM b a

BAG_GEN_PROD_TAILREC

|- ∀b.
     FINITE_BAG b ⇒
     ∀x a. BAG_GEN_PROD (BAG_INSERT x b) a = BAG_GEN_PROD b (x * a)

BAG_GEN_PROD_REC

|- ∀b.
     FINITE_BAG b ⇒
     ∀x a. BAG_GEN_PROD (BAG_INSERT x b) a = x * BAG_GEN_PROD b a

BAG_GEN_PROD_EQ_1

|- ∀b. FINITE_BAG b ⇒ ∀e. (BAG_GEN_PROD b e = 1) ⇒ (e = 1)

BAG_GEN_PROD_ALL_ONES

|- ∀b. FINITE_BAG b ⇒ (BAG_GEN_PROD b 1 = 1) ⇒ ∀x. x ⋲ b ⇒ (x = 1)

BAG_GEN_PROD_POSITIVE

|- ∀b. FINITE_BAG b ⇒ (∀x. x ⋲ b ⇒ 0 < x) ⇒ 0 < BAG_GEN_PROD b 1

BAG_EVERY_THM

|- (∀P. BAG_EVERY P {||}) ∧
   ∀P e b. BAG_EVERY P (BAG_INSERT e b) ⇔ P e ∧ BAG_EVERY P b

BAG_EVERY_UNION

|- BAG_EVERY P (b1 ⊎ b2) ⇔ BAG_EVERY P b1 ∧ BAG_EVERY P b2

BAG_EVERY_MERGE

|- BAG_EVERY P (BAG_MERGE b1 b2) ⇔ BAG_EVERY P b1 ∧ BAG_EVERY P b2

BAG_EVERY_SET

|- BAG_EVERY P b ⇔ SET_OF_BAG b ⊆ {x | P x}

BAG_FILTER_EQ_EMPTY

|- (BAG_FILTER P b = {||}) ⇔ BAG_EVERY ($~ o P) b

SET_OF_BAG_IMAGE

|- SET_OF_BAG (BAG_IMAGE f b) = IMAGE f (SET_OF_BAG b)

BAG_IMAGE_FINITE_RESTRICTED_I

|- ∀b. FINITE_BAG b ∧ BAG_EVERY (λe. f e = e) b ⇒ (BAG_IMAGE f b = b)

BAG_ALL_DISTINCT_THM

|- BAG_ALL_DISTINCT {||} ∧
   ∀e b. BAG_ALL_DISTINCT (BAG_INSERT e b) ⇔ ¬(e ⋲ b) ∧ BAG_ALL_DISTINCT b

BAG_ALL_DISTINCT_BAG_MERGE

|- ∀b1 b2.
     BAG_ALL_DISTINCT (BAG_MERGE b1 b2) ⇔
     BAG_ALL_DISTINCT b1 ∧ BAG_ALL_DISTINCT b2

BAG_ALL_DISTINCT_BAG_UNION

|- ∀b1 b2.
     BAG_ALL_DISTINCT (b1 ⊎ b2) ⇔
     BAG_ALL_DISTINCT b1 ∧ BAG_ALL_DISTINCT b2 ∧ BAG_DISJOINT b1 b2

BAG_ALL_DISTINCT_DIFF

|- ∀b1 b2. BAG_ALL_DISTINCT b1 ⇒ BAG_ALL_DISTINCT (b1 − b2)

BAG_ALL_DISTINCT_DELETE

|- BAG_ALL_DISTINCT b ⇔ ∀e. e ⋲ b ⇒ ¬(e ⋲ b − {|e|})

BAG_ALL_DISTINCT_SET

|- BAG_ALL_DISTINCT b ⇔ (BAG_OF_SET (SET_OF_BAG b) = b)

BAG_ALL_DISTINCT_BAG_OF_SET

|- BAG_ALL_DISTINCT (BAG_OF_SET s)

BAG_IN_BAG_DIFF_ALL_DISTINCT

|- ∀b1 b2 e. BAG_ALL_DISTINCT b1 ⇒ (e ⋲ b1 − b2 ⇔ e ⋲ b1 ∧ ¬(e ⋲ b2))

SUB_BAG_ALL_DISTINCT

|- ∀b1 b2. BAG_ALL_DISTINCT b1 ⇒ (b1 ≤ b2 ⇔ ∀x. x ⋲ b1 ⇒ x ⋲ b2)

BAG_ALL_DISTINCT_BAG_INN

|- ∀b n e. BAG_ALL_DISTINCT b ⇒ (BAG_INN e n b ⇔ (n = 0) ∨ (n = 1) ∧ e ⋲ b)

BAG_ALL_DISTINCT_EXTENSION

|- ∀b1 b2.
     BAG_ALL_DISTINCT b1 ∧ BAG_ALL_DISTINCT b2 ⇒
     ((b1 = b2) ⇔ ∀x. x ⋲ b1 ⇔ x ⋲ b2)

NOT_BAG_IN

|- ∀b x. (b x = 0) ⇔ ¬(x ⋲ b)

BAG_UNION_EQ_LEFT

|- ∀b c d. (b ⊎ c = b ⊎ d) ⇒ (c = d)

BAG_IN_DIVIDES

|- ∀b x a. FINITE_BAG b ∧ x ⋲ b ⇒ divides x (BAG_GEN_PROD b a)

BAG_GEN_PROD_UNION_LEM

|- ∀b1.
     FINITE_BAG b1 ⇒
     ∀b2 a b.
       FINITE_BAG b2 ⇒
       (BAG_GEN_PROD (b1 ⊎ b2) (a * b) =
        BAG_GEN_PROD b1 a * BAG_GEN_PROD b2 b)

BAG_GEN_PROD_UNION

|- ∀b1 b2.
     FINITE_BAG b1 ∧ FINITE_BAG b2 ⇒
     (BAG_GEN_PROD (b1 ⊎ b2) 1 = BAG_GEN_PROD b1 1 * BAG_GEN_PROD b2 1)

BIG_BAG_UNION_EMPTY

|- BIG_BAG_UNION ∅ = {||}

BIG_BAG_UNION_INSERT

|- FINITE sob ⇒
   (BIG_BAG_UNION (b INSERT sob) = b ⊎ BIG_BAG_UNION (sob DELETE b))

BIG_BAG_UNION_DELETE

|- FINITE sob ⇒
   (BIG_BAG_UNION (sob DELETE b) =
    if b ∈ sob then BIG_BAG_UNION sob − b else BIG_BAG_UNION sob)

BIG_BAG_UNION_ITSET_BAG_UNION

|- ∀sob. FINITE sob ⇒ (BIG_BAG_UNION sob = ITSET $⊎ sob {||})

FINITE_BIG_BAG_UNION

|- ∀sob.
     FINITE sob ∧ (∀b. b ∈ sob ⇒ FINITE_BAG b) ⇒
     FINITE_BAG (BIG_BAG_UNION sob)

BAG_IN_BIG_BAG_UNION

|- FINITE P ⇒ (e ⋲ BIG_BAG_UNION P ⇔ ∃b. e ⋲ b ∧ b ∈ P)

BIG_BAG_UNION_EQ_EMPTY_BAG

|- ∀sob. FINITE sob ⇒ ((BIG_BAG_UNION sob = {||}) ⇔ ∀b. b ∈ sob ⇒ (b = {||}))

BIG_BAG_UNION_UNION

|- FINITE s1 ∧ FINITE s2 ⇒
   (BIG_BAG_UNION (s1 ∪ s2) =
    BIG_BAG_UNION s1 ⊎ BIG_BAG_UNION s2 − BIG_BAG_UNION (s1 ∩ s2))

BIG_BAG_UNION_EQ_ELEMENT

|- FINITE sob ∧ b ∈ sob ⇒
   ((BIG_BAG_UNION sob = b) ⇔ ∀b'. b' ∈ sob ⇒ (b' = b) ∨ (b' = {||}))

BAG_NOT_LESS_EMPTY

|- ¬mlt1 r b {||}

NOT_mlt_EMPTY

|- ¬mlt R b {||}

BAG_LESS_ADD

|- mlt1 r N (M0 ⊎ {|a|}) ⇒
   (∃M. mlt1 r M M0 ∧ (N = M ⊎ {|a|})) ∨
   ∃KK. (∀b. b ⋲ KK ⇒ r b a) ∧ (N = M0 ⊎ KK)

mlt1_all_accessible

|- WF R ⇒ ∀M. WFP (mlt1 R) M

WF_mlt1

|- WF R ⇒ WF (mlt1 R)

TC_mlt1_FINITE_BAG

|- ∀b1 b2. mlt R b1 b2 ⇒ FINITE_BAG b1 ∧ FINITE_BAG b2

TC_mlt1_UNION2_I

|- ∀b2 b1. FINITE_BAG b2 ∧ FINITE_BAG b1 ∧ b2 ≠ {||} ⇒ mlt R b1 (b1 ⊎ b2)

TC_mlt1_UNION1_I

|- ∀b2 b1. FINITE_BAG b2 ∧ FINITE_BAG b1 ∧ b1 ≠ {||} ⇒ mlt R b2 (b1 ⊎ b2)

mlt_NOT_REFL

|- WF R ⇒ ¬mlt R a a

mlt_INSERT_CANCEL_I

|- ∀a b. mlt R a b ⇒ mlt R (BAG_INSERT e a) (BAG_INSERT e b)

mlt1_INSERT_CANCEL

|- WF R ⇒ (mlt1 R (BAG_INSERT e a) (BAG_INSERT e b) ⇔ mlt1 R a b)

dominates_EMPTY

|- dominates R ∅ b

dominates_SUBSET

|- transitive R ∧ FINITE Y ∧ dominates R Y X ∧ X ⊆ Y ∧ X ≠ ∅ ⇒
   ∃x. x ∈ X ∧ R x x

mlt_dominates_thm1

|- transitive R ⇒
   ∀b1 b2.
     mlt R b1 b2 ⇔
     FINITE_BAG b1 ∧ FINITE_BAG b2 ∧
     ∃x y. x ≠ {||} ∧ x ≤ b2 ∧ (b1 = b2 − x ⊎ y) ∧ bdominates R y x

dominates_DIFF

|- WF R ∧ transitive R ∧ dominates R x y ∧ FINITE i ∧ i ⊆ x ∧ i ⊆ y ⇒
   dominates R (x DIFF i) (y DIFF i)

BAG_INSERT_SUB_BAG_E

|- BAG_INSERT e b ≤ c ⇒ e ⋲ c ∧ b ≤ c

bdominates_BAG_DIFF

|- WF R ∧ transitive R ∧ bdominates R x y ∧ FINITE_BAG i ∧ i ≤ x ∧ i ≤ y ⇒
   bdominates R (x − i) (y − i)

BAG_INTER_SUB_BAG

|- BAG_INTER b1 b2 ≤ b1 ∧ BAG_INTER b1 b2 ≤ b2

BAG_INTER_FINITE

|- FINITE_BAG b1 ∨ FINITE_BAG b2 ⇒ FINITE_BAG (BAG_INTER b1 b2)

mlt_dominates_thm2

|- WF R ∧ transitive R ⇒
   ∀b1 b2.
     mlt R b1 b2 ⇔
     FINITE_BAG b1 ∧ FINITE_BAG b2 ∧
     ∃x y.
       x ≠ {||} ∧ x ≤ b2 ∧ BAG_DISJOINT x y ∧ (b1 = b2 − x ⊎ y) ∧
       bdominates R y x

BAG_DIFF_INSERT_SUB_BAG

|- c ≤ b ⇒ (BAG_INSERT e b − c = BAG_INSERT e (b − c))

mlt_INSERT_CANCEL

|- transitive R ∧ WF R ⇒ (mlt R (BAG_INSERT e a) (BAG_INSERT e b) ⇔ mlt R a b)

mlt_UNION_RCANCEL_I

|- mlt R a b ∧ FINITE_BAG c ⇒ mlt R (a ⊎ c) (b ⊎ c)

mlt_UNION_RCANCEL

|- WF R ∧ transitive R ⇒ (mlt R (a ⊎ c) (b ⊎ c) ⇔ mlt R a b ∧ FINITE_BAG c)

mlt_UNION_LCANCEL_I

|- mlt R a b ∧ FINITE_BAG c ⇒ mlt R (c ⊎ a) (c ⊎ b)

mlt_UNION_LCANCEL

|- WF R ∧ transitive R ⇒ (mlt R (c ⊎ a) (c ⊎ b) ⇔ mlt R a b ∧ FINITE_BAG c)

mlt_UNION_CANCEL_EQN

|- WF R ⇒
   (mlt R b1 (b1 ⊎ b2) ⇔ FINITE_BAG b1 ∧ FINITE_BAG b2 ∧ b2 ≠ {||}) ∧
   (mlt R b1 (b2 ⊎ b1) ⇔ FINITE_BAG b1 ∧ FINITE_BAG b2 ∧ b2 ≠ {||})

mlt_UNION_EMPTY_EQN

|- T

SUB_BAG_SING

|- b ≤ {|e|} ⇔ (b = {||}) ∨ (b = {|e|})

SUB_BAG_DIFF_simple

|- b − c ≤ b

mltLT_SING0

|- mlt $< {|0|} b ⇔ FINITE_BAG b ∧ b ≠ {|0|} ∧ b ≠ {||}

BAG_SIZE_EMPTY

|- bag_size eltsize {||} = 0

BAG_SIZE_INSERT

|- FINITE_BAG b ⇒
   (bag_size eltsize (BAG_INSERT e b) = 1 + eltsize e + bag_size eltsize b)