---

Step * 1 1 of Lemma sub-bag-admissable

.....assertion..... 
1. [T] : Type
2. [R] : bag(T) ⟶ bag(T) ⟶ ℙ
3. ∀bs:bag(T). R[{};bs]
4. ∀as,bs,cs:bag(T).  (R[as;bs] ⇒ R[as + cs;bs + cs])
5. as : bag(T)
6. bs : bag(T)
7. cs : bag(T)
8. as + cs ∈ bag(T)
⊢ R[{} + as;cs + as]
BY
{ Auto }

---

Latex:

---

Latex:
.....assertion..... 
1.  [T]  :  Type
2.  [R]  :  bag(T)  {}\mrightarrow{}  bag(T)  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}bs:bag(T).  R[\{\};bs]
4.  \mforall{}as,bs,cs:bag(T).    (R[as;bs]  {}\mRightarrow{}  R[as  +  cs;bs  +  cs])
5.  as  :  bag(T)
6.  bs  :  bag(T)
7.  cs  :  bag(T)
8.  as  +  cs  \mmember{}  bag(T)
\mvdash{}  R[\{\}  +  as;cs  +  as]


By

---

Latex:
Auto

---

Home Index