Theory: bag

Parents

• pred_set

Types

Constants

• BAG_CARD_RELn  :('a -> num) -> num -> bool
• EMPTY_BAG  :'a -> num
• BAG_IN  :'a -> ('a -> num) -> bool
• BAG_INTER  :('a -> num) -> ('a -> num) -> 'a -> num
• FINITE_BAG  :('a -> num) -> bool
• BAG_INSERT  :'a -> ('a -> num) -> 'a -> num
• BAG_INN  :'a -> num -> ('a -> num) -> bool
• PSUB_BAG  :('a -> num) -> ('a -> num) -> bool
• BAG_DELETE  :('a -> num) -> 'a -> ('a -> num) -> bool
• BAG_CARD  :('a -> num) -> num
• BAG_DISJOINT  :('a -> num) -> ('a -> num) -> bool
• BAG_MERGE  :('a -> num) -> ('a -> num) -> 'a -> num
• BAG_DIFF  :('a -> num) -> ('a -> num) -> 'a -> num
• SING_BAG  :('a -> num) -> bool
• SUB_BAG  :('a -> num) -> ('a -> num) -> bool
• EL_BAG  :'a -> 'a -> num
• BAG_UNION  :('a -> num) -> ('a -> num) -> 'a -> num
• SET_OF_BAG  :('a -> num) -> 'a -> bool
• BAG_delta  :('a -> num) # ('a -> num) -> ('a -> num) -> 'a -> num
• BAG_OF_SET  :('a -> bool) -> 'a -> num

Definitions

BAG_CARD

|- !b. FINITE_BAG b ==> BAG_CARD_RELn b (BAG_CARD 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_DELETE

|- !b0 e b. BAG_DELETE b0 e b = (b0 = BAG_INSERT e b)

BAG_delta

|- !B1 B2 B3.
     BAG_delta (B1,B2) B3 =
     BAG_DIFF (BAG_UNION B3 (BAG_DIFF B2 B1)) (BAG_DIFF B1 B2)

BAG_DIFF

|- !b1 b2. BAG_DIFF b1 b2 = (\x. b1 x - b2 x)

BAG_DISJOINT

|- !b1 b2. BAG_DISJOINT b1 b2 = DISJOINT (SET_OF_BAG b1) (SET_OF_BAG b2)

BAG_IN

|- !e b. BAG_IN e b = BAG_INN e 1 b

BAG_INN

|- !e n b. BAG_INN e n b = b e >= n

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_OF_SET

|- !P. BAG_OF_SET P = (\x. (if x IN P then 1 else 0))

BAG_UNION

|- !b c. BAG_UNION b c = (\x. b x + c x)

EL_BAG

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

EMPTY_BAG

|- {||} = K 0

FINITE_BAG

|- !b.
     FINITE_BAG b = !P. P {||} /\ (!b. P b ==> !e. P (BAG_INSERT e b)) ==> P b

PSUB_BAG

|- !b1 b2. PSUB_BAG b1 b2 = SUB_BAG b1 b2 /\ ~(b1 = b2)

SET_OF_BAG

|- !b. SET_OF_BAG b = (\x. BAG_IN x b)

SING_BAG

|- !b. SING_BAG b = ?x. b = {|x|}

SUB_BAG

|- !b1 b2. SUB_BAG b1 b2 = !x n. BAG_INN x n b1 ==> BAG_INN x n b2

Theorems

ASSOC_BAG_UNION

|- !b1 b2 b3. BAG_UNION b1 (BAG_UNION b2 b3) = BAG_UNION (BAG_UNION b1 b2) b3

BAG_CARD_BAG_INN

|- !b. FINITE_BAG b ==> !n e. BAG_INN e n b ==> n <= BAG_CARD b

BAG_CARD_THM

|- (BAG_CARD {||} = 0) /\
   !b. FINITE_BAG b ==> !e. BAG_CARD (BAG_INSERT e b) = BAG_CARD b + 1

BAG_cases

|- !b. (b = {||}) \/ ?b0 e. b = BAG_INSERT e b0

BAG_DELETE_11

|- !b0 e1 e2 b1 b2.
     BAG_DELETE b0 e1 b1 /\ BAG_DELETE b0 e2 b2 ==> ((e1 = e2) = (b1 = b2))

BAG_DELETE_BAG_IN

|- !b0 b e. BAG_DELETE b0 e b ==> BAG_IN e b0

BAG_DELETE_BAG_IN_down

|- !b0 b e1 e2.
     BAG_DELETE b0 e1 b /\ ~(e1 = e2) /\ BAG_IN e2 b0 ==> BAG_IN e2 b

BAG_DELETE_BAG_IN_up

|- !b0 b e. BAG_DELETE b0 e b ==> !e'. BAG_IN e' b ==> BAG_IN e' b0

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

|- !e b. ~BAG_DELETE {||} 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_PSUB_BAG

|- !b0 e b. BAG_DELETE b0 e b ==> PSUB_BAG b b0

BAG_DELETE_SING

|- !b e. BAG_DELETE b e {||} ==> SING_BAG b

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

BAG_delta_eliminate

|- (!A BU BD X.
      SUB_BAG X A ==>
      (BAG_delta (A,BAG_DIFF (BAG_UNION A BU) BD) X =
       BAG_DIFF (BAG_UNION X BU) BD)) /\
   !A BU BD X.
     SUB_BAG X A ==>
     (BAG_delta (A,BAG_DIFF (BAG_UNION BU A) BD) X =
      BAG_DIFF (BAG_UNION BU X) BD)

BAG_DIFF_2L

|- !X Y Z. BAG_DIFF (BAG_DIFF X Y) Z = BAG_DIFF X (BAG_UNION Y Z)

BAG_DIFF_2R

|- !A B C'.
     SUB_BAG C' B ==>
     (BAG_DIFF A (BAG_DIFF B C') = BAG_DIFF (BAG_UNION A C') B)

BAG_DIFF_EMPTY

|- (!b. BAG_DIFF b b = {||}) /\ (!b. BAG_DIFF b {||} = b) /\
   (!b. BAG_DIFF {||} b = {||}) /\
   !b1 b2. SUB_BAG b1 b2 ==> (BAG_DIFF b1 b2 = {||})

BAG_DIFF_INSERT

|- !x b1 b2.
     ~BAG_IN x b1 ==>
     (BAG_DIFF (BAG_INSERT x b2) b1 = BAG_INSERT x (BAG_DIFF b2 b1))

BAG_DIFF_INSERT_same

|- !x b1 b2. BAG_DIFF (BAG_INSERT x b1) (BAG_INSERT x b2) = BAG_DIFF b1 b2

BAG_DIFF_UNION_eliminate

|- !b1 b2 b3.
     (BAG_DIFF (BAG_UNION b1 b2) (BAG_UNION b1 b3) = BAG_DIFF b2 b3) /\
     (BAG_DIFF (BAG_UNION b1 b2) (BAG_UNION b3 b1) = BAG_DIFF b2 b3) /\
     (BAG_DIFF (BAG_UNION b2 b1) (BAG_UNION b1 b3) = BAG_DIFF b2 b3) /\
     (BAG_DIFF (BAG_UNION b2 b1) (BAG_UNION b3 b1) = BAG_DIFF b2 b3)

BAG_DISJOINT_DIFF

|- !B1 B2. BAG_DISJOINT (BAG_DIFF B1 B2) (BAG_DIFF B2 B1)

BAG_DISJOINT_EMPTY

|- !b. BAG_DISJOINT b {||} /\ BAG_DISJOINT {||} b

BAG_EXTENSION

|- !b1 b2. (b1 = b2) = !n e. BAG_INN e n b1 = BAG_INN e n b2

BAG_IN_BAG_DELETE

|- !b e. BAG_IN e b ==> ?b'. BAG_DELETE b e b'

BAG_IN_BAG_INSERT

|- !b e1 e2. BAG_IN e1 (BAG_INSERT e2 b) = (e1 = e2) \/ BAG_IN e1 b

BAG_IN_BAG_UNION

|- !b1 b2 e. BAG_IN e (BAG_UNION b1 b2) = BAG_IN e b1 \/ BAG_IN e b2

BAG_INN_0

|- !b e. BAG_INN e 0 b

BAG_INN_BAG_DELETE

|- !b n e. BAG_INN e n b /\ n > 0 ==> ?b'. BAG_DELETE b e 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_UNION

|- !n e b1 b2.
     BAG_INN e n (BAG_UNION b1 b2) =
     ?m1 m2. (n = m1 + m2) /\ BAG_INN e m1 b1 /\ BAG_INN e m2 b2

BAG_INN_EMPTY_BAG

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

BAG_INN_LESS

|- !b e n m. BAG_INN e n b /\ m < n ==> BAG_INN e m b

BAG_INSERT_commutes

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

BAG_INSERT_DIFF

|- !x b. ~(BAG_INSERT x b = b)

BAG_INSERT_EQ_UNION

|- !e b1 b2 b.
     (BAG_INSERT e b = BAG_UNION b1 b2) ==> BAG_IN e b1 \/ BAG_IN e b2

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)

BAG_INSERT_UNION

|- !b e. BAG_INSERT e b = BAG_UNION (EL_BAG e) b

BAG_OF_EMPTY

|- SET_OF_BAG {||} = {}

BAG_UNION_DIFF

|- !X Y Z.
     SUB_BAG Z Y ==>
     (BAG_UNION X (BAG_DIFF Y Z) = BAG_DIFF (BAG_UNION X Y) Z) /\
     (BAG_UNION (BAG_DIFF Y Z) X = BAG_DIFF (BAG_UNION X Y) Z)

BAG_UNION_EMPTY

|- (!b. BAG_UNION b {||} = b) /\ (!b. BAG_UNION {||} b = b) /\
   !b1 b2. (BAG_UNION b1 b2 = {||}) = (b1 = {||}) /\ (b2 = {||})

BAG_UNION_INSERT

|- !e b1 b2.
     (BAG_UNION (BAG_INSERT e b1) b2 = BAG_INSERT e (BAG_UNION b1 b2)) /\
     (BAG_UNION b1 (BAG_INSERT e b2) = BAG_INSERT e (BAG_UNION b1 b2))

BAG_UNION_LEFT_CANCEL

|- !b b1 b2. (BAG_UNION b b1 = BAG_UNION b b2) = (b1 = b2)

BCARD_0

|- !b. FINITE_BAG b ==> ((BAG_CARD b = 0) = (b = {||}))

BCARD_SUC

|- !b.
     FINITE_BAG b ==>
     !n.
       (BAG_CARD b = SUC n) =
       ?b0 e. (b = BAG_INSERT e b0) /\ (BAG_CARD b0 = n)

C_BAG_INSERT_ONE_ONE

|- !x y b. (BAG_INSERT x b = BAG_INSERT y b) = (x = y)

COMM_BAG_UNION

|- !b1 b2. BAG_UNION b1 b2 = BAG_UNION b2 b1

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

EMPTY_BAG_alt

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

FINITE_BAG_DIFF

|- !b1. FINITE_BAG b1 ==> !b2. FINITE_BAG (BAG_DIFF b1 b2)

FINITE_BAG_DIFF_dual

|- !b1. FINITE_BAG b1 ==> !b2. FINITE_BAG (BAG_DIFF b2 b1) ==> FINITE_BAG b2

FINITE_BAG_INDUCT

|- !P.
     P {||} /\ (!b. P b ==> !e. P (BAG_INSERT e b)) ==>
     !b. FINITE_BAG b ==> P b

FINITE_BAG_INSERT

|- !b. FINITE_BAG b ==> !e. FINITE_BAG (BAG_INSERT e b)

FINITE_BAG_THM

|- FINITE_BAG {||} /\ !e b. FINITE_BAG (BAG_INSERT e b) = FINITE_BAG b

FINITE_BAG_UNION

|- !b1 b2. FINITE_BAG (BAG_UNION b1 b2) = FINITE_BAG b1 /\ FINITE_BAG b2

FINITE_EMPTY_BAG

|- FINITE_BAG {||}

FINITE_SUB_BAG

|- !b1. FINITE_BAG b1 ==> !b2. SUB_BAG b2 b1 ==> FINITE_BAG b2

IN_SET_OF_BAG

|- !x b. x IN SET_OF_BAG b = BAG_IN x b

MEMBER_NOT_EMPTY

|- !b. (?x. BAG_IN x b) = ~(b = {||})

move_BAG_UNION_over_eq

|- !X Y Z. (BAG_UNION X Y = Z) ==> (X = BAG_DIFF Z Y)

NOT_IN_BAG_DIFF

|- !x b1 b2. ~BAG_IN x b1 ==> (BAG_DIFF b1 (BAG_INSERT x b2) = BAG_DIFF b1 b2)

NOT_IN_EMPTY_BAG

|- !x. ~BAG_IN x {||}

NOT_IN_SUB_BAG_INSERT

|- !b1 b2 e. ~BAG_IN e b1 ==> (SUB_BAG b1 (BAG_INSERT e b2) = SUB_BAG b1 b2)

PSUB_BAG_ANTISYM

|- !b1 b2. ~(PSUB_BAG b1 b2 /\ PSUB_BAG b2 b1)

PSUB_BAG_IRREFL

|- !b. ~PSUB_BAG b b

PSUB_BAG_NOT_EQ

|- !b1 b2. PSUB_BAG b1 b2 ==> ~(b1 = b2)

PSUB_BAG_SUB_BAG

|- !b1 b2. PSUB_BAG b1 b2 ==> SUB_BAG b1 b2

PSUB_BAG_TRANS

|- !b1 b2 b3. PSUB_BAG b1 b2 /\ PSUB_BAG b2 b3 ==> PSUB_BAG b1 b3

SET_BAG_I

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

SET_OF_BAG_DIFF_SUBSET_down

|- !b1 b2. SET_OF_BAG b1 DIFF SET_OF_BAG b2 SUBSET SET_OF_BAG (BAG_DIFF b1 b2)

SET_OF_BAG_DIFF_SUBSET_up

|- !b1 b2. SET_OF_BAG (BAG_DIFF b1 b2) SUBSET SET_OF_BAG b1

SET_OF_BAG_INSERT

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

SET_OF_BAG_UNION

|- !b1 b2. SET_OF_BAG (BAG_UNION b1 b2) = SET_OF_BAG b1 UNION SET_OF_BAG b2

SET_OF_EL_BAG

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

SET_OF_EMPTY

|- BAG_OF_SET {} = {||}

SING_BAG_THM

|- !e. SING_BAG {|e|}

SING_EL_BAG

|- !e. SING_BAG (EL_BAG e)

STRONG_FINITE_BAG_INDUCT

|- !P.
     P {||} /\ (!b. FINITE_BAG b /\ P b ==> !e. P (BAG_INSERT e b)) ==>
     !b. FINITE_BAG b ==> P b

SUB_BAG_ANTISYM

|- !b1 b2. SUB_BAG b1 b2 /\ SUB_BAG b2 b1 ==> (b1 = b2)

SUB_BAG_BAG_DIFF

|- !X Y Y' Z W'.
     SUB_BAG (BAG_DIFF X Y) (BAG_DIFF Z W') ==>
     SUB_BAG (BAG_DIFF X (BAG_UNION Y Y')) (BAG_DIFF Z (BAG_UNION W' Y'))

SUB_BAG_BAG_IN

|- !x b1 b2. SUB_BAG (BAG_INSERT x b1) b2 ==> BAG_IN x b2

SUB_BAG_delta

|- (!A B0 B. SUB_BAG B0 A ==> SUB_BAG B (BAG_delta (B0,B) A)) /\
   !A B0 B. SUB_BAG A B0 ==> SUB_BAG (BAG_delta (B0,B) A) B

SUB_BAG_DIFF

|- (!b1 b2. SUB_BAG b1 b2 ==> !b3. SUB_BAG (BAG_DIFF b1 b3) b2) /\
   !b1 b2 b3 b4.
     SUB_BAG b2 b1 ==>
     SUB_BAG b4 b3 ==>
     (SUB_BAG (BAG_DIFF b1 b2) (BAG_DIFF b3 b4) =
      SUB_BAG (BAG_UNION b1 b4) (BAG_UNION b2 b3))

SUB_BAG_EL_BAG

|- !e b. SUB_BAG (EL_BAG e) b = BAG_IN e b

SUB_BAG_EMPTY

|- (!b. SUB_BAG {||} b) /\ !b. SUB_BAG b {||} = (b = {||})

SUB_BAG_EXISTS

|- !b1 b2. SUB_BAG b1 b2 = ?b. b2 = BAG_UNION b1 b

SUB_BAG_INSERT

|- !e b1 b2. SUB_BAG (BAG_INSERT e b1) (BAG_INSERT e b2) = SUB_BAG b1 b2

SUB_BAG_LEQ

|- !b1 b2. SUB_BAG b1 b2 = !x. b1 x <= b2 x

SUB_BAG_PSUB_BAG

|- !b1 b2. SUB_BAG b1 b2 = PSUB_BAG b1 b2 \/ (b1 = b2)

SUB_BAG_REFL

|- !b. SUB_BAG b b

SUB_BAG_SET

|- !b1 b2. SUB_BAG b1 b2 ==> SET_OF_BAG b1 SUBSET SET_OF_BAG b2

SUB_BAG_TRANS

|- !b1 b2 b3. SUB_BAG b1 b2 /\ SUB_BAG b2 b3 ==> SUB_BAG b1 b3

SUB_BAG_UNION

|- (!b1 b2. SUB_BAG b1 b2 ==> !b. SUB_BAG b1 (BAG_UNION b2 b)) /\
   (!b1 b2. SUB_BAG b1 b2 ==> !b. SUB_BAG b1 (BAG_UNION b b2)) /\
   (!b1 b2 b3.
      SUB_BAG b1 (BAG_UNION b2 b3) ==>
      !b. SUB_BAG b1 (BAG_UNION (BAG_UNION b2 b) b3)) /\
   (!b1 b2 b3.
      SUB_BAG b1 (BAG_UNION b2 b3) ==>
      !b. SUB_BAG b1 (BAG_UNION (BAG_UNION b b2) b3)) /\
   (!b1 b2 b3.
      SUB_BAG b1 (BAG_UNION b3 b2) ==>
      !b. SUB_BAG b1 (BAG_UNION b3 (BAG_UNION b2 b))) /\
   (!b1 b2 b3.
      SUB_BAG b1 (BAG_UNION b3 b2) ==>
      !b. SUB_BAG b1 (BAG_UNION b3 (BAG_UNION b b2))) /\
   (!b1 b2 b3 b4.
      SUB_BAG b1 b3 ==>
      SUB_BAG b2 b4 ==>
      SUB_BAG (BAG_UNION b1 b2) (BAG_UNION b3 b4)) /\
   (!b1 b2 b3 b4.
      SUB_BAG b1 b4 ==>
      SUB_BAG b2 b3 ==>
      SUB_BAG (BAG_UNION b1 b2) (BAG_UNION b3 b4)) /\
   (!b1 b2 b3 b4 b5.
      SUB_BAG b1 (BAG_UNION b3 b5) ==>
      SUB_BAG b2 b4 ==>
      SUB_BAG (BAG_UNION b1 b2) (BAG_UNION (BAG_UNION b3 b4) b5)) /\
   (!b1 b2 b3 b4 b5.
      SUB_BAG b1 (BAG_UNION b4 b5) ==>
      SUB_BAG b2 b3 ==>
      SUB_BAG (BAG_UNION b1 b2) (BAG_UNION (BAG_UNION b3 b4) b5)) /\
   (!b1 b2 b3 b4 b5.
      SUB_BAG b2 (BAG_UNION b3 b5) ==>
      SUB_BAG b1 b4 ==>
      SUB_BAG (BAG_UNION b1 b2) (BAG_UNION (BAG_UNION b3 b4) b5)) /\
   (!b1 b2 b3 b4 b5.
      SUB_BAG b2 (BAG_UNION b4 b5) ==>
      SUB_BAG b1 b3 ==>
      SUB_BAG (BAG_UNION b1 b2) (BAG_UNION (BAG_UNION b3 b4) b5)) /\
   (!b1 b2 b3 b4 b5.
      SUB_BAG b1 (BAG_UNION b5 b3) ==>
      SUB_BAG b2 b4 ==>
      SUB_BAG (BAG_UNION b2 b1) (BAG_UNION b5 (BAG_UNION b3 b4))) /\
   (!b1 b2 b3 b4 b5.
      SUB_BAG b1 (BAG_UNION b5 b4) ==>
      SUB_BAG b2 b3 ==>
      SUB_BAG (BAG_UNION b2 b1) (BAG_UNION b5 (BAG_UNION b3 b4))) /\
   (!b1 b2 b3 b4 b5.
      SUB_BAG b2 (BAG_UNION b5 b3) ==>
      SUB_BAG b1 b4 ==>
      SUB_BAG (BAG_UNION b2 b1) (BAG_UNION b5 (BAG_UNION b3 b4))) /\
   (!b1 b2 b3 b4 b5.
      SUB_BAG b2 (BAG_UNION b5 b4) ==>
      SUB_BAG b1 b3 ==>
      SUB_BAG (BAG_UNION b2 b1) (BAG_UNION b5 (BAG_UNION b3 b4))) /\
   (!b1 b2 b3 b4 b5.
      SUB_BAG (BAG_UNION b1 b2) b4 ==>
      SUB_BAG b3 b5 ==>
      SUB_BAG (BAG_UNION (BAG_UNION b1 b3) b2) (BAG_UNION b4 b5)) /\
   (!b1 b2 b3 b4 b5.
      SUB_BAG (BAG_UNION b1 b2) b5 ==>
      SUB_BAG b3 b4 ==>
      SUB_BAG (BAG_UNION (BAG_UNION b1 b3) b2) (BAG_UNION b4 b5)) /\
   (!b1 b2 b3 b4 b5.
      SUB_BAG (BAG_UNION b3 b2) b4 ==>
      SUB_BAG b1 b5 ==>
      SUB_BAG (BAG_UNION (BAG_UNION b1 b3) b2) (BAG_UNION b4 b5)) /\
   (!b1 b2 b3 b4 b5.
      SUB_BAG (BAG_UNION b3 b2) b5 ==>
      SUB_BAG b1 b4 ==>
      SUB_BAG (BAG_UNION (BAG_UNION b1 b3) b2) (BAG_UNION b4 b5)) /\
   (!b1 b2 b3 b4 b5.
      SUB_BAG (BAG_UNION b2 b1) b4 ==>
      SUB_BAG b3 b5 ==>
      SUB_BAG (BAG_UNION b2 (BAG_UNION b1 b3)) (BAG_UNION b5 b4)) /\
   (!b1 b2 b3 b4 b5.
      SUB_BAG (BAG_UNION b2 b1) b5 ==>
      SUB_BAG b3 b4 ==>
      SUB_BAG (BAG_UNION b2 (BAG_UNION b1 b3)) (BAG_UNION b5 b4)) /\
   (!b1 b2 b3 b4 b5.
      SUB_BAG (BAG_UNION b2 b3) b4 ==>
      SUB_BAG b1 b5 ==>
      SUB_BAG (BAG_UNION b2 (BAG_UNION b1 b3)) (BAG_UNION b5 b4)) /\
   !b1 b2 b3 b4 b5.
     SUB_BAG (BAG_UNION b2 b3) b5 ==>
     SUB_BAG b1 b4 ==>
     SUB_BAG (BAG_UNION b2 (BAG_UNION b1 b3)) (BAG_UNION b5 b4)

SUB_BAG_UNION_DIFF

|- !b1 b2 b3.
     SUB_BAG b1 b3 ==>
     (SUB_BAG b2 (BAG_DIFF b3 b1) = SUB_BAG (BAG_UNION b1 b2) b3)

SUB_BAG_UNION_down

|- !b1 b2 b3. SUB_BAG (BAG_UNION b1 b2) b3 ==> SUB_BAG b1 b3 /\ SUB_BAG b2 b3

SUB_BAG_UNION_eliminate

|- !b1 b2 b3.
     (SUB_BAG (BAG_UNION b1 b2) (BAG_UNION b1 b3) = SUB_BAG b2 b3) /\
     (SUB_BAG (BAG_UNION b1 b2) (BAG_UNION b3 b1) = SUB_BAG b2 b3) /\
     (SUB_BAG (BAG_UNION b2 b1) (BAG_UNION b1 b3) = SUB_BAG b2 b3) /\
     (SUB_BAG (BAG_UNION b2 b1) (BAG_UNION b3 b1) = SUB_BAG b2 b3)