---

Step * of Lemma bag-member-splits

No Annotations
∀[T:Type]. ∀[as,bs,cs:bag(T)].  uiff(<as, bs> ↓∈ bag-splits(cs);(as + bs) = cs ∈ bag(T))
BY
{ (Auto THEN Try ((Unhide THEN Auto))) }

1
1. T : Type
2. as : bag(T)
3. bs : bag(T)
4. cs : bag(T)
5. <as, bs> ↓∈ bag-splits(cs)
⊢ (as + bs) = cs ∈ bag(T)

2
1. T : Type
2. as : bag(T)
3. bs : bag(T)
4. cs : bag(T)
5. (as + bs) = cs ∈ bag(T)
⊢ <as, bs> ↓∈ bag-splits(cs)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[as,bs,cs:bag(T)].    uiff(<as,  bs>  \mdownarrow{}\mmember{}  bag-splits(cs);(as  +  bs)  =  cs)


By

---

Latex:
(Auto  THEN  Try  ((Unhide  THEN  Auto)))

---

Home Index