Step
*
3
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 = u ∈ A
11. p2 ↓∈ bs
⊢ <p1, p2> ↓∈ bag-map(λx.<u, x>;bs)
BY
{ ((Using [`T',⌜B⌝] (BLemma `bag-member-map` )⋅ THEN Auto)⋅ THEN Reduce 0) }
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 = u ∈ A
11. p2 ↓∈ bs
⊢ ↓∃v:B. (v ↓∈ bs ∧ (<p1, p2> = <u, v> ∈ (A × B)))
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 = u
11. p2 \mdownarrow{}\mmember{} bs
\mvdash{} <p1, p2> \mdownarrow{}\mmember{} bag-map(\mlambda{}x.<u, x>bs)
By
Latex:
((Using [`T',\mkleeneopen{}B\mkleeneclose{}] (BLemma `bag-member-map` )\mcdot{} THEN Auto)\mcdot{} THEN Reduce 0)
Home
Index