---

Step * of Lemma bag-induction

∀[T:Type]. ∀[P:bag(T) ⟶ ℙ].  ((∀x:T. P[[x]]) ⇒ (∀bs:bag({b:bag(T)| P[b]} ). P[bag-union(bs)]) ⇒ (∀b:bag(T). P[b]))
BY
{ (Auto THEN Try ((SubsumeC ⌜T List⌝⋅ THEN Auto THEN BLemma `list-subtype-bag` THEN Auto))) }

1
1. [T] : Type
2. [P] : bag(T) ⟶ ℙ
3. ∀x:T. P[[x]]
4. ∀bs:bag({b:bag(T)| P[b]} ). P[bag-union(bs)]
5. b : bag(T)
⊢ P[b]

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:bag(T)  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}x:T.  P[[x]])  {}\mRightarrow{}  (\mforall{}bs:bag(\{b:bag(T)|  P[b]\}  ).  P[bag-union(bs)])  {}\mRightarrow{}  (\mforall{}b:bag(T).  P[b]))


By

---

Latex:
(Auto  THEN  Try  ((SubsumeC  \mkleeneopen{}T  List\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  BLemma  `list-subtype-bag`  THEN  Auto)))

---

Home Index