---

Step * of Lemma bag-member-product

∀[A,B:Type]. ∀[as:bag(A)]. ∀[bs:bag(B)]. ∀[p:A × B].  uiff(p ↓∈ as × bs;fst(p) ↓∈ as ∧ snd(p) ↓∈ bs)
BY
{ ((UnivCD THENA Auto)
   THEN skip{(Unhide THENA Auto)}
   THEN (BagInd 3 THENA Auto)
   THEN Try (Folds ``empty-bag`` 0)
   THEN Try ((Subst' [u / v] ~ {u} + v 0 THENA (RepUR ``bag-append single-bag`` 0 THEN Auto)))
   THEN ((RWW "bag-product-empty bag-product-append bag-product-single" 0 THENA Auto)
         THEN Auto
         THEN skip{Unhide}
         THEN Auto
         THEN Try (OnMaybeHyp 6 (\h. Complete (BagMemberD h)))
         THEN DVar `p'
         THEN All Reduce)⋅) }

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) + v × bs
⊢ p1 ↓∈ {u} + 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> ↓∈ bag-map(λx.<u, x>;bs) + v × bs
⊢ p2 ↓∈ bs

3
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 ↓∈ {u} + v
11. p2 ↓∈ bs
⊢ <p1, p2> ↓∈ bag-map(λx.<u, x>;bs) + v × bs

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[as:bag(A)].  \mforall{}[bs:bag(B)].  \mforall{}[p:A  \mtimes{}  B].    uiff(p  \mdownarrow{}\mmember{}  as  \mtimes{}  bs;fst(p)  \mdownarrow{}\mmember{}  as  \mwedge{}  snd(p)  \mdownarrow{}\mmember{}  bs)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  skip\{(Unhide  THENA  Auto)\}
  THEN  (BagInd  3  THENA  Auto)
  THEN  Try  (Folds  ``empty-bag``  0)
  THEN  Try  ((Subst'  [u  /  v]  \msim{}  \{u\}  +  v  0  THENA  (RepUR  ``bag-append  single-bag``  0  THEN  Auto)))
  THEN  ((RWW  "bag-product-empty  bag-product-append  bag-product-single"  0  THENA  Auto)
              THEN  Auto
              THEN  skip\{Unhide\}
              THEN  Auto
              THEN  Try  (OnMaybeHyp  6  (\mbackslash{}h.  Complete  (BagMemberD  h)))
              THEN  DVar  `p'
              THEN  All  Reduce)\mcdot{})

---

Home Index