---

Step * 1 1 1 of Lemma bag-combine-no-repeats


1. T1 : Type
2. T2 : Type
3. f : T1 ⟶ bag(T2)
4. eq1 : EqDecider(T1)
5. eq2 : EqDecider(T2)
6. b1 : T1 List
7. ∀x,y:T1. ∀z:T2.  (z ↓∈ f[x] ⇒ z ↓∈ f[y] ⇒ (x = y ∈ T1))
8. ∀x:T1. ∀[x1:T2]. uiff(1 ≤ (#x1 in f[x]);(#x1 in f[x]) = 1 ∈ ℤ)
9. ∀[x:T1]. uiff(1 ≤ (#x in b1);(#x in b1) = 1 ∈ ℤ)
10. x : T2
⊢ 1 < bag-sum([x1∈b1|1 ≤z (#x in f[x1])];x1.(#x in f[x1])) ⇒ False
BY
{ (RepUR ``bag-sum bag-filter`` 0⋅
   THEN (GenConcl ⌜filter(λx1.1 ≤z (#x in f[x1]);b1) = L ∈ (T1 List)⌝⋅ THENA Auto)
   THEN D -2
   THEN Reduce 0) }

1
1. T1 : Type
2. T2 : Type
3. f : T1 ⟶ bag(T2)
4. eq1 : EqDecider(T1)
5. eq2 : EqDecider(T2)
6. b1 : T1 List
7. ∀x,y:T1. ∀z:T2.  (z ↓∈ f[x] ⇒ z ↓∈ f[y] ⇒ (x = y ∈ T1))
8. ∀x:T1. ∀[x1:T2]. uiff(1 ≤ (#x1 in f[x]);(#x1 in f[x]) = 1 ∈ ℤ)
9. ∀[x:T1]. uiff(1 ≤ (#x in b1);(#x in b1) = 1 ∈ ℤ)
10. x : T2
11. filter(λx1.1 ≤z (#x in f[x1]);b1) = [] ∈ (T1 List)
⊢ 1 < 0 ⇒ False

2
1. T1 : Type
2. T2 : Type
3. f : T1 ⟶ bag(T2)
4. eq1 : EqDecider(T1)
5. eq2 : EqDecider(T2)
6. b1 : T1 List
7. ∀x,y:T1. ∀z:T2.  (z ↓∈ f[x] ⇒ z ↓∈ f[y] ⇒ (x = y ∈ T1))
8. ∀x:T1. ∀[x1:T2]. uiff(1 ≤ (#x1 in f[x]);(#x1 in f[x]) = 1 ∈ ℤ)
9. ∀[x:T1]. uiff(1 ≤ (#x in b1);(#x in b1) = 1 ∈ ℤ)
10. x : T2
11. u : T1
12. v : T1 List
13. filter(λx1.1 ≤z (#x in f[x1]);b1) = [u / v] ∈ (T1 List)
⊢ 1 < accumulate (with value s and list item x1):
       (#x in f[x1]) + s
      over list:
        v
      with starting value:
       (#x in f[u]) + 0)
⇒ False

---

Latex:

---

Latex:

1.  T1  :  Type
2.  T2  :  Type
3.  f  :  T1  {}\mrightarrow{}  bag(T2)
4.  eq1  :  EqDecider(T1)
5.  eq2  :  EqDecider(T2)
6.  b1  :  T1  List
7.  \mforall{}x,y:T1.  \mforall{}z:T2.    (z  \mdownarrow{}\mmember{}  f[x]  {}\mRightarrow{}  z  \mdownarrow{}\mmember{}  f[y]  {}\mRightarrow{}  (x  =  y))
8.  \mforall{}x:T1.  \mforall{}[x1:T2].  uiff(1  \mleq{}  (\#x1  in  f[x]);(\#x1  in  f[x])  =  1)
9.  \mforall{}[x:T1].  uiff(1  \mleq{}  (\#x  in  b1);(\#x  in  b1)  =  1)
10.  x  :  T2
\mvdash{}  1  <  bag-sum([x1\mmember{}b1|1  \mleq{}z  (\#x  in  f[x1])];x1.(\#x  in  f[x1]))  {}\mRightarrow{}  False


By

---

Latex:
(RepUR  ``bag-sum  bag-filter``  0\mcdot{}
  THEN  (GenConcl  \mkleeneopen{}filter(\mlambda{}x1.1  \mleq{}z  (\#x  in  f[x1]);b1)  =  L\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  Reduce  0)

---

Home Index