---

Step * 2 1 1 1 of Lemma bag-member-combine


1. A : Type
2. B : Type
3. f : A ⟶ bag(B)
4. b : B
5. n : ℕ
6. ∀n:ℕn. ∀bs:bag(A).  ((#(bs) ≤ n) ⇒ uiff(b ↓∈ ⋃x∈bs.f[x];↓∃x:A. (x ↓∈ bs ∧ b ↓∈ f[x])))
7. bs : bag(A)
8. x : A
9. bs' : bag(A)
10. bs = ({x} + bs') ∈ bag(A)
11. #(bs) ≤ n
12. #(bs) = (#(bs') + 1) ∈ ℤ
13. uiff(b ↓∈ ⋃x∈bs'.f[x];↓∃x:A. (x ↓∈ bs' ∧ b ↓∈ f[x]))
⊢ uiff(b ↓∈ f[x] + ⋃x∈bs'.f[x];↓∃x@0:A. (x@0 ↓∈ {x} + bs' ∧ b ↓∈ f[x@0]))
BY
{ ((RWO "bag-member-append" 0 THEN Auto) THEN Unfold `sq_or` 0 THEN RepeatFor 2 (D -1)⋅) }

1
1. A : Type
2. B : Type
3. f : A ⟶ bag(B)
4. b : B
5. n : ℕ
6. ∀n:ℕn. ∀bs:bag(A).  ((#(bs) ≤ n) ⇒ uiff(b ↓∈ ⋃x∈bs.f[x];↓∃x:A. (x ↓∈ bs ∧ b ↓∈ f[x])))
7. bs : bag(A)
8. x : A
9. bs' : bag(A)
10. bs = ({x} + bs') ∈ bag(A)
11. #(bs) ≤ n
12. #(bs) = (#(bs') + 1) ∈ ℤ
13. ↓∃x:A. (x ↓∈ bs' ∧ b ↓∈ f[x]) supposing b ↓∈ ⋃x∈bs'.f[x]
14. b ↓∈ ⋃x∈bs'.f[x] supposing ↓∃x:A. (x ↓∈ bs' ∧ b ↓∈ f[x])
15. b ↓∈ f[x]
⊢ ↓∃x@0:A. ((↓x@0 ↓∈ {x} ∨ x@0 ↓∈ bs') ∧ b ↓∈ f[x@0])

2
1. A : Type
2. B : Type
3. f : A ⟶ bag(B)
4. b : B
5. n : ℕ
6. ∀n:ℕn. ∀bs:bag(A).  ((#(bs) ≤ n) ⇒ uiff(b ↓∈ ⋃x∈bs.f[x];↓∃x:A. (x ↓∈ bs ∧ b ↓∈ f[x])))
7. bs : bag(A)
8. x : A
9. bs' : bag(A)
10. bs = ({x} + bs') ∈ bag(A)
11. #(bs) ≤ n
12. #(bs) = (#(bs') + 1) ∈ ℤ
13. ↓∃x:A. (x ↓∈ bs' ∧ b ↓∈ f[x]) supposing b ↓∈ ⋃x∈bs'.f[x]
14. b ↓∈ ⋃x∈bs'.f[x] supposing ↓∃x:A. (x ↓∈ bs' ∧ b ↓∈ f[x])
15. b ↓∈ ⋃x∈bs'.f[x]
⊢ ↓∃x@0:A. ((↓x@0 ↓∈ {x} ∨ x@0 ↓∈ bs') ∧ b ↓∈ f[x@0])

3
1. A : Type
2. B : Type
3. f : A ⟶ bag(B)
4. b : B
5. n : ℕ
6. ∀n:ℕn. ∀bs:bag(A).  ((#(bs) ≤ n) ⇒ uiff(b ↓∈ ⋃x∈bs.f[x];↓∃x:A. (x ↓∈ bs ∧ b ↓∈ f[x])))
7. bs : bag(A)
8. x : A
9. bs' : bag(A)
10. bs = ({x} + bs') ∈ bag(A)
11. #(bs) ≤ n
12. #(bs) = (#(bs') + 1) ∈ ℤ
13. ↓∃x:A. (x ↓∈ bs' ∧ b ↓∈ f[x]) supposing b ↓∈ ⋃x∈bs'.f[x]
14. b ↓∈ ⋃x∈bs'.f[x] supposing ↓∃x:A. (x ↓∈ bs' ∧ b ↓∈ f[x])
15. x@0 : A
16. (x@0 ↓∈ {x} ↓∨ x@0 ↓∈ bs') ∧ b ↓∈ f[x@0]
⊢ ↓b ↓∈ f[x] ∨ b ↓∈ ⋃x∈bs'.f[x]

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  A  {}\mrightarrow{}  bag(B)
4.  b  :  B
5.  n  :  \mBbbN{}
6.  \mforall{}n:\mBbbN{}n.  \mforall{}bs:bag(A).    ((\#(bs)  \mleq{}  n)  {}\mRightarrow{}  uiff(b  \mdownarrow{}\mmember{}  \mcup{}x\mmember{}bs.f[x];\mdownarrow{}\mexists{}x:A.  (x  \mdownarrow{}\mmember{}  bs  \mwedge{}  b  \mdownarrow{}\mmember{}  f[x])))
7.  bs  :  bag(A)
8.  x  :  A
9.  bs'  :  bag(A)
10.  bs  =  (\{x\}  +  bs')
11.  \#(bs)  \mleq{}  n
12.  \#(bs)  =  (\#(bs')  +  1)
13.  uiff(b  \mdownarrow{}\mmember{}  \mcup{}x\mmember{}bs'.f[x];\mdownarrow{}\mexists{}x:A.  (x  \mdownarrow{}\mmember{}  bs'  \mwedge{}  b  \mdownarrow{}\mmember{}  f[x]))
\mvdash{}  uiff(b  \mdownarrow{}\mmember{}  f[x]  +  \mcup{}x\mmember{}bs'.f[x];\mdownarrow{}\mexists{}x@0:A.  (x@0  \mdownarrow{}\mmember{}  \{x\}  +  bs'  \mwedge{}  b  \mdownarrow{}\mmember{}  f[x@0]))


By

---

Latex:
((RWO  "bag-member-append"  0  THEN  Auto)  THEN  Unfold  `sq\_or`  0  THEN  RepeatFor  2  (D  -1)\mcdot{})

---

Home Index