---

Step * of Lemma bag-null-bag-union

∀[T:Type]. ∀[bbs:bag(bag(T))].  ↑bag-null(bag-union(bbs)) supposing ∀bs:bag(T). (bs ↓∈ bbs ⇒ (↑bag-null(bs)))
BY
{ ... }

1
1. T : Type
2. u : bag(T)
3. v : bag(T) List
4. (∀bs:bag(T). (bs ↓∈ v ⇒ (↑bag-null(bs)))) ⇒ (↑bag-null(bag-union(v)))
5. ∀bs:bag(T). (bs ↓∈ u.v ⇒ (↑bag-null(bs)))
6. u = {} ∈ bag(T)
⊢ ↑bag-null(bag-union(v))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[bbs:bag(bag(T))].
    \muparrow{}bag-null(bag-union(bbs))  supposing  \mforall{}bs:bag(T).  (bs  \mdownarrow{}\mmember{}  bbs  {}\mRightarrow{}  (\muparrow{}bag-null(bs)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (BagToList  (-1)  THENA  Auto)
  THEN  ListInd  (-1)
  THEN  Try  (Fold  `empty-bag`  0)
  THEN  Try  (Fold  `cons-bag`  0)
  THEN  Reduce  0
  THEN  (UnivCD  THENA  Auto)
  THEN  (RWO  "bag-null-append"  0  THENA  Auto)
  THEN  RW  assert\_pushdownC  0
  THEN  Auto
  THEN  (RWO  "assert-bag-null<"  0  THENA  Auto)
  THEN  Try  (Complete  ((BackThruSomeHyp  THEN  BagMemberD  0  THEN  D  0  THEN  Auto  THEN  OrLeft  THEN  Auto)))
  THEN  skip\{(BHyp  (-2)
                        THEN  Auto
                        THEN  BHyp  (-3)
                        THEN  Auto
                        THEN  BagMemberD  0
                        THEN  D  0
                        THEN  Auto
                        THEN  OrRight
                        THEN  Auto)\})

---

Home Index