---

Step * of Lemma bag-parts_wf

No Annotations
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)].  (bag-parts(eq;bs) ∈ bag(bag(T) List+)) supposing valueall-type(T)
BY
{ (Auto THEN MoveToConcl (-1) THEN Assert ⌜∀n:ℕ. ∀bs:bag(T).  ((#(bs) ≤ n) ⇒ (bag-parts(eq;bs) ∈ bag(bag(T) List+)))⌝⋅)
⋅ }

1
.....assertion..... 
1. T : Type
2. valueall-type(T)
3. eq : EqDecider(T)
⊢ ∀n:ℕ. ∀bs:bag(T).  ((#(bs) ≤ n) ⇒ (bag-parts(eq;bs) ∈ bag(bag(T) List+)))

2
1. T : Type
2. valueall-type(T)
3. eq : EqDecider(T)
4. ∀n:ℕ. ∀bs:bag(T).  ((#(bs) ≤ n) ⇒ (bag-parts(eq;bs) ∈ bag(bag(T) List+)))
⊢ ∀bs:bag(T). (bag-parts(eq;bs) ∈ bag(bag(T) List+))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type]
    \mforall{}[eq:EqDecider(T)].  \mforall{}[bs:bag(T)].    (bag-parts(eq;bs)  \mmember{}  bag(bag(T)  List\msupplus{})) 
    supposing  valueall-type(T)


By

---

Latex:
(Auto
  THEN  MoveToConcl  (-1)
  THEN  Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}bs:bag(T).    ((\#(bs)  \mleq{}  n)  {}\mRightarrow{}  (bag-parts(eq;bs)  \mmember{}  bag(bag(T)  List\msupplus{})))\mkleeneclose{}\mcdot{})\mcdot{}

---

Home Index