---

Step * 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. bs : bag(T1)
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 bs);(#x in bs) = 1 ∈ ℤ)
10. x : T2
11. 1 < bag-sum([x1∈bs|1 ≤z (#x in f[x1])];x1.(#x in f[x1]))
⊢ False
BY
{ ((Assert ⌜0 = 1 ∈ ℤ⌝⋅ THEN Auto) THEN newQuotD (-6) THEN Assert ⌜False⌝⋅ THEN Auto THEN MoveToConcl  (-1)⋅) }

1
1. T1 : Type
2. T2 : Type
3. f : T1 ⟶ bag(T2)
4. eq1 : EqDecider(T1)
5. eq2 : EqDecider(T2)
6. istype(T1 List)
7. ∀as,b1:T1 List.  istype(permutation(T1;as;b1))
8. ∀as:T1 List. permutation(T1;as;as)
9. a : Base
10. b : Base
11. c : a = b ∈ pertype(λas,bs. ((as ∈ T1 List) ∧ (bs ∈ T1 List) ∧ permutation(T1;as;bs)))
12. a ∈ T1 List
13. b ∈ T1 List
14. permutation(T1;a;b)
15. ∀x,y:T1. ∀z:T2.  (z ↓∈ f[x] ⇒ z ↓∈ f[y] ⇒ (x = y ∈ T1))
16. ∀x:T1. ∀[x1:T2]. uiff(1 ≤ (#x1 in f[x]);(#x1 in f[x]) = 1 ∈ ℤ)
17. ∀[x:T1]. uiff(1 ≤ (#x in a);(#x in a) = 1 ∈ ℤ)
18. x : T2
⊢ 1 < bag-sum([x1∈a|1 ≤z (#x in f[x1])];x1.(#x in f[x1])) ⇒ False

---

Latex:

---

Latex:

1.  T1  :  Type
2.  T2  :  Type
3.  f  :  T1  {}\mrightarrow{}  bag(T2)
4.  eq1  :  EqDecider(T1)
5.  eq2  :  EqDecider(T2)
6.  bs  :  bag(T1)
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  bs);(\#x  in  bs)  =  1)
10.  x  :  T2
11.  1  <  bag-sum([x1\mmember{}bs|1  \mleq{}z  (\#x  in  f[x1])];x1.(\#x  in  f[x1]))
\mvdash{}  False


By

---

Latex:
((Assert  \mkleeneopen{}0  =  1\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  newQuotD  (-6)
  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  MoveToConcl
    (-1)\mcdot{})

---

Home Index