---

Step * 1 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
11. filter(λx1.1 ≤z (#x in f[x1]);b1) = [] ∈ (T1 List)
⊢ 1 < 0 ⇒ False
BY
{ Auto }

---

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.  filter(\mlambda{}x1.1  \mleq{}z  (\#x  in  f[x1]);b1)  =  []
\mvdash{}  1  <  0  {}\mRightarrow{}  False


By

---

Latex:
Auto

---

Home Index