---

Step * 3 1 1 of Lemma bag-partitions-cons


1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. x : X
5. b : bag(X)
6. x2 : bag(X)
7. x3 : bag(X)
8. (↓∃v:bag(X) × bag(X)
      ((v ↓∈ bag-partitions(eq;b) ∧ (↑((#x in snd(v)) =z 0))) ∧ (<x2, x3> = <x.fst(v), snd(v)> ∈ (bag(X) × bag(X)))))
↓∨ (↓∃v:bag(X) × bag(X). (v ↓∈ bag-partitions(eq;b) ∧ (<x2, x3> = <fst(v), x.snd(v)> ∈ (bag(X) × bag(X)))))
9. ∀x:bag(X) × bag(X). ∀as,bs:bag(bag(X) × bag(X)).  (x ↓∈ as + bs ⇐⇒ x ↓∈ as ↓∨ x ↓∈ bs)
10. ∀x:bag(X) × bag(X). ∀f:(bag(X) × bag(X)) ⟶ (bag(X) × bag(X)). ∀bs:bag(bag(X) × bag(X)).
      uiff(x ↓∈ bag-map(f;bs);↓∃v:bag(X) × bag(X). (v ↓∈ bs ∧ (x = (f v) ∈ (bag(X) × bag(X)))))
⊢ (x2 + x3) = x.b ∈ bag(X)
BY
{ (RepeatFor 3 (D -3) THEN ExRepD THEN (EqHD (-3) THEN All Reduce THEN Auto) THEN RWO "-3 -4" 0 THEN Auto) }

1
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. x : X
5. b : bag(X)
6. x2 : bag(X)
7. x3 : bag(X)
8. v : bag(X) × bag(X)
9. v ↓∈ bag-partitions(eq;b)
10. ↑((#x in snd(v)) =z 0)
11. x2 = x.fst(v) ∈ bag(X)
12. x3 = (snd(v)) ∈ bag(X)
13. ∀x:bag(X) × bag(X). ∀as,bs:bag(bag(X) × bag(X)).  (x ↓∈ as + bs ⇐⇒ x ↓∈ as ↓∨ x ↓∈ bs)
14. ∀x:bag(X) × bag(X). ∀f:(bag(X) × bag(X)) ⟶ (bag(X) × bag(X)). ∀bs:bag(bag(X) × bag(X)).
      uiff(x ↓∈ bag-map(f;bs);↓∃v:bag(X) × bag(X). (v ↓∈ bs ∧ (x = (f v) ∈ (bag(X) × bag(X)))))
⊢ (x.fst(v) + (snd(v))) = x.b ∈ bag(X)

2
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. x : X
5. b : bag(X)
6. x2 : bag(X)
7. x3 : bag(X)
8. v : bag(X) × bag(X)
9. v ↓∈ bag-partitions(eq;b)
10. x2 = (fst(v)) ∈ bag(X)
11. x3 = x.snd(v) ∈ bag(X)
12. ∀x:bag(X) × bag(X). ∀as,bs:bag(bag(X) × bag(X)).  (x ↓∈ as + bs ⇐⇒ x ↓∈ as ↓∨ x ↓∈ bs)
13. ∀x:bag(X) × bag(X). ∀f:(bag(X) × bag(X)) ⟶ (bag(X) × bag(X)). ∀bs:bag(bag(X) × bag(X)).
      uiff(x ↓∈ bag-map(f;bs);↓∃v:bag(X) × bag(X). (v ↓∈ bs ∧ (x = (f v) ∈ (bag(X) × bag(X)))))
⊢ ((fst(v)) + x.snd(v)) = x.b ∈ bag(X)

---

Latex:

---

Latex:

1.  X  :  Type
2.  valueall-type(X)
3.  eq  :  EqDecider(X)
4.  x  :  X
5.  b  :  bag(X)
6.  x2  :  bag(X)
7.  x3  :  bag(X)
8.  (\mdownarrow{}\mexists{}v:bag(X)  \mtimes{}  bag(X)
            ((v  \mdownarrow{}\mmember{}  bag-partitions(eq;b)  \mwedge{}  (\muparrow{}((\#x  in  snd(v))  =\msubz{}  0)))  \mwedge{}  (<x2,  x3>  =  <x.fst(v),  snd(v)>)))
\mdownarrow{}\mvee{}  (\mdownarrow{}\mexists{}v:bag(X)  \mtimes{}  bag(X).  (v  \mdownarrow{}\mmember{}  bag-partitions(eq;b)  \mwedge{}  (<x2,  x3>  =  <fst(v),  x.snd(v)>)))
9.  \mforall{}x:bag(X)  \mtimes{}  bag(X).  \mforall{}as,bs:bag(bag(X)  \mtimes{}  bag(X)).    (x  \mdownarrow{}\mmember{}  as  +  bs  \mLeftarrow{}{}\mRightarrow{}  x  \mdownarrow{}\mmember{}  as  \mdownarrow{}\mvee{}  x  \mdownarrow{}\mmember{}  bs)
10.  \mforall{}x:bag(X)  \mtimes{}  bag(X).  \mforall{}f:(bag(X)  \mtimes{}  bag(X))  {}\mrightarrow{}  (bag(X)  \mtimes{}  bag(X)).  \mforall{}bs:bag(bag(X)  \mtimes{}  bag(X)).
            uiff(x  \mdownarrow{}\mmember{}  bag-map(f;bs);\mdownarrow{}\mexists{}v:bag(X)  \mtimes{}  bag(X).  (v  \mdownarrow{}\mmember{}  bs  \mwedge{}  (x  =  (f  v))))
\mvdash{}  (x2  +  x3)  =  x.b


By

---

Latex:
(RepeatFor  3  (D  -3)
  THEN  ExRepD
  THEN  (EqHD  (-3)  THEN  All  Reduce  THEN  Auto)
  THEN  RWO  "-3  -4"  0
  THEN  Auto)

---

Home Index