---

Step * of Lemma sub-bag-union-of-list

∀[T:Type]. ∀[x:bag(T)].  ∀bs:bag(T) List. ((x ∈ bs) ⇒ sub-bag(T;x;bag-union(bs)))
BY
{ (Auto
   THEN RepeatFor 2 (D -1)
   THEN With ⌜bag-union(firstn(i;bs)) + bag-union(nth_tl(i + 1;bs))⌝ (D 0)⋅
   THEN Auto
   THEN HypSubst' -1 0
   THEN Auto) }

1
1. T : Type
2. x : bag(T)
3. bs : bag(T) List
4. i : ℕ
5. i < ||bs||
6. x = bs[i] ∈ bag(T)
⊢ bag-union(bs) = (bs[i] + bag-union(firstn(i;bs)) + bag-union(nth_tl(i + 1;bs))) ∈ bag(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[x:bag(T)].    \mforall{}bs:bag(T)  List.  ((x  \mmember{}  bs)  {}\mRightarrow{}  sub-bag(T;x;bag-union(bs)))


By

---

Latex:
(Auto
  THEN  RepeatFor  2  (D  -1)
  THEN  With  \mkleeneopen{}bag-union(firstn(i;bs))  +  bag-union(nth\_tl(i  +  1;bs))\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  HypSubst'  -1  0
  THEN  Auto)

---

Home Index