---

Step * 1 of Lemma bag-member-product


1. A : Type
2. B : Type
3. bs : bag(B)
4. p1 : A
5. p2 : B
6. u : A
7. v : A List
8. p1 ↓∈ v ∧ p2 ↓∈ bs supposing <p1, p2> ↓∈ v × bs
9. <p1, p2> ↓∈ v × bs supposing p1 ↓∈ v ∧ p2 ↓∈ bs
10. <p1, p2> ↓∈ bag-map(λx.<u, x>;bs) + v × bs
⊢ p1 ↓∈ {u} + v
BY
{ (BagMemberD 0 THEN BagMemberD (-1) THEN ParallelLast THEN RepeatFor 2 (D -1)) }

1
1. A : Type
2. B : Type
3. bs : bag(B)
4. p1 : A
5. p2 : B
6. u : A
7. v : A List
8. p1 ↓∈ v ∧ p2 ↓∈ bs supposing <p1, p2> ↓∈ v × bs
9. <p1, p2> ↓∈ v × bs supposing p1 ↓∈ v ∧ p2 ↓∈ bs
10. <p1, p2> ↓∈ bag-map(λx.<u, x>;bs)
⊢ ↓p1 ↓∈ {u} ∨ p1 ↓∈ v

2
1. A : Type
2. B : Type
3. bs : bag(B)
4. p1 : A
5. p2 : B
6. u : A
7. v : A List
8. p1 ↓∈ v ∧ p2 ↓∈ bs supposing <p1, p2> ↓∈ v × bs
9. <p1, p2> ↓∈ v × bs supposing p1 ↓∈ v ∧ p2 ↓∈ bs
10. <p1, p2> ↓∈ v × bs
⊢ ↓p1 ↓∈ {u} ∨ p1 ↓∈ v

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  bs  :  bag(B)
4.  p1  :  A
5.  p2  :  B
6.  u  :  A
7.  v  :  A  List
8.  p1  \mdownarrow{}\mmember{}  v  \mwedge{}  p2  \mdownarrow{}\mmember{}  bs  supposing  <p1,  p2>  \mdownarrow{}\mmember{}  v  \mtimes{}  bs
9.  <p1,  p2>  \mdownarrow{}\mmember{}  v  \mtimes{}  bs  supposing  p1  \mdownarrow{}\mmember{}  v  \mwedge{}  p2  \mdownarrow{}\mmember{}  bs
10.  <p1,  p2>  \mdownarrow{}\mmember{}  bag-map(\mlambda{}x.<u,  x>bs)  +  v  \mtimes{}  bs
\mvdash{}  p1  \mdownarrow{}\mmember{}  \{u\}  +  v


By

---

Latex:
(BagMemberD  0  THEN  BagMemberD  (-1)  THEN  ParallelLast  THEN  RepeatFor  2  (D  -1))

---

Home Index