---

Step * of Lemma bag-count-bag-lub

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:bag(T)]. ∀[x:T].  ((#x in bag-lub(eq;as;bs)) = imax((#x in as);(#x in bs)) ∈ ℤ)
BY
{ xxx(Auto
      THEN Unfold `bag-lub` 0
      THEN (RWO "bag-count-combine" 0 THENA Auto)
      THEN RWO "bag-sum-count" 0
      THEN Auto
      THEN (InstLemma `decidable__bag-member` [⌜T⌝;⌜x⌝;⌜bag-to-set(eq;as + bs)⌝]⋅ THENA Auto)
      THEN D -1)xxx }

1
1. T : Type
2. eq : EqDecider(T)
3. as : bag(T)
4. bs : bag(T)
5. x : T
6. x ↓∈ bag-to-set(eq;as + bs)
⊢ bag-sum([x1∈bag-to-set(eq;as + bs)|
           1 ≤z (#x in bag-rep(imax((#x1 in as);(#x1 in bs));x1))];x1.(#x in bag-rep(imax((#x1 in as);(#x1 in bs));x1)))
= imax((#x in as);(#x in bs))
∈ ℤ

2
1. T : Type
2. eq : EqDecider(T)
3. as : bag(T)
4. bs : bag(T)
5. x : T
6. ¬x ↓∈ bag-to-set(eq;as + bs)
⊢ bag-sum([x1∈bag-to-set(eq;as + bs)|
           1 ≤z (#x in bag-rep(imax((#x1 in as);(#x1 in bs));x1))];x1.(#x in bag-rep(imax((#x1 in as);(#x1 in bs));x1)))
= imax((#x in as);(#x in bs))
∈ ℤ

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[as,bs:bag(T)].  \mforall{}[x:T].
    ((\#x  in  bag-lub(eq;as;bs))  =  imax((\#x  in  as);(\#x  in  bs)))


By

---

Latex:
xxx(Auto
        THEN  Unfold  `bag-lub`  0
        THEN  (RWO  "bag-count-combine"  0  THENA  Auto)
        THEN  RWO  "bag-sum-count"  0
        THEN  Auto
        THEN  (InstLemma  `decidable\_\_bag-member`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}bag-to-set(eq;as  +  bs)\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  D  -1)xxx

---

Home Index