---

Step * 1 of Lemma bag-append-no-repeats


1. T : Type
2. as : bag(T)
3. bs : bag(T)
4. bag-no-repeats(T;as) ∧ bag-no-repeats(T;bs) ∧ (∀z:T. (z ↓∈ as ⇒ (¬z ↓∈ bs)))
⊢ bag-no-repeats(T;as + bs)
BY
{ (BLemma `bag-append-no-repeats1` THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  as  :  bag(T)
3.  bs  :  bag(T)
4.  bag-no-repeats(T;as)  \mwedge{}  bag-no-repeats(T;bs)  \mwedge{}  (\mforall{}z:T.  (z  \mdownarrow{}\mmember{}  as  {}\mRightarrow{}  (\mneg{}z  \mdownarrow{}\mmember{}  bs)))
\mvdash{}  bag-no-repeats(T;as  +  bs)


By

---

Latex:
(BLemma  `bag-append-no-repeats1`  THEN  Auto)\mcdot{}

---

Home Index