---

Step * 1 1 1 2 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
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
BY
{ (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. u : T1
12. filter(λx1.1 ≤z (#x in f[x1]);b1) = [u] ∈ (T1 List)
⊢ 1 < (#x in f[u]) + 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. u1 : T1
13. v : T1 List
14. filter(λx1.1 ≤z (#x in f[x1]);b1) = [u; [u1 / 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[u1]) + (#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
11.  u  :  T1
12.  v  :  T1  List
13.  filter(\mlambda{}x1.1  \mleq{}z  (\#x  in  f[x1]);b1)  =  [u  /  v]
\mvdash{}  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)
{}\mRightarrow{}  False


By

---

Latex:
(D  (-2)  THEN  Reduce  0)

---

Home Index