---

Step * of Lemma bag-member-parts

∀[T:Type]
  ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[L:bag(T) List+].
    uiff(L ↓∈ bag-parts(eq;bs);(bag-union(L) = bs ∈ bag(T)) ∧ (∀x∈L.¬(x = {} ∈ bag(T)))) 
  supposing valueall-type(T)
BY
{ ((UnivCD THENA Auto)
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN Assert ⌜∀n:ℕ. ∀bs:bag(T).
                  ((#(bs) ≤ n)
                  ⇒ (∀L:bag(T) List+
                        uiff(L ↓∈ bag-parts(eq;bs);(bag-union(L) = bs ∈ bag(T)) ∧ (∀x∈L.¬(x = {} ∈ bag(T))))))⌝⋅
   THEN Try (((D 0 THENA Auto) THEN InstHyp [⌜#(bs)⌝;⌜bs⌝] (-2)⋅ THEN Auto))
   THEN CompleteInductionOnNat) }

1
1. T : Type
2. valueall-type(T)
3. eq : EqDecider(T)
4. n : ℕ
5. ∀n:ℕn. ∀bs:bag(T).
     ((#(bs) ≤ n)
     ⇒ (∀L:bag(T) List+. uiff(L ↓∈ bag-parts(eq;bs);(bag-union(L) = bs ∈ bag(T)) ∧ (∀x∈L.¬(x = {} ∈ bag(T))))))
⊢ ∀bs:bag(T)
    ((#(bs) ≤ n)
    ⇒ (∀L:bag(T) List+. uiff(L ↓∈ bag-parts(eq;bs);(bag-union(L) = bs ∈ bag(T)) ∧ (∀x∈L.¬(x = {} ∈ bag(T))))))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}[eq:EqDecider(T)].  \mforall{}[bs:bag(T)].  \mforall{}[L:bag(T)  List\msupplus{}].
        uiff(L  \mdownarrow{}\mmember{}  bag-parts(eq;bs);(bag-union(L)  =  bs)  \mwedge{}  (\mforall{}x\mmember{}L.\mneg{}(x  =  \{\}))) 
    supposing  valueall-type(T)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}bs:bag(T).
                                ((\#(bs)  \mleq{}  n)
                                {}\mRightarrow{}  (\mforall{}L:bag(T)  List\msupplus{}
                                            uiff(L  \mdownarrow{}\mmember{}  bag-parts(eq;bs);(bag-union(L)  =  bs)  \mwedge{}  (\mforall{}x\mmember{}L.\mneg{}(x  =  \{\})))))\mkleeneclose{}\mcdot{}
  THEN  Try  (((D  0  THENA  Auto)  THEN  InstHyp  [\mkleeneopen{}\#(bs)\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto))
  THEN  CompleteInductionOnNat)

---

Home Index