---

Step * 1 of Lemma sub-bag-admissable


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;as + cs]
BY
{ Assert ⌜R[{} + as;cs + as]⌝⋅ }

1
.....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]

2
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)
9. R[{} + as;cs + as]
⊢ R[as;as + cs]

---

Latex:

---

Latex:

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;as  +  cs]


By

---

Latex:
Assert  \mkleeneopen{}R[\{\}  +  as;cs  +  as]\mkleeneclose{}\mcdot{}

---

Home Index