---

Step * 1 2 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)
9. R[{} + as;cs + as]
⊢ R[as;as + cs]
BY
{ ((RWO "bag-empty-append" (-1) THEN Auto) THEN RWO "bag-append-comm" (-1) THEN Auto) }

---

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


By

---

Latex:
((RWO  "bag-empty-append"  (-1)  THEN  Auto)  THEN  RWO  "bag-append-comm"  (-1)  THEN  Auto)

---

Home Index