---

Step * 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. 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
BY
{ (MoveToConcl (-2)
   THEN (GenConcl ⌜a = b1 ∈ (T1 List)⌝⋅ THENA Auto)
   THEN ThinVar `a'
   THEN ThinVar `b'
   THEN (D 0 THENA Auto)
   THEN RepeatFor 3 (Thin 6)
   THEN PromoteHyp (-2) 6
   THEN PromoteHyp (-1) (-2)) }

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
⊢ 1 < bag-sum([x1∈b1|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.  istype(T1  List)
7.  \mforall{}as,b1:T1  List.    istype(permutation(T1;as;b1))
8.  \mforall{}as:T1  List.  permutation(T1;as;as)
9.  a  :  Base
10.  b  :  Base
11.  c  :  a  =  b
12.  a  \mmember{}  T1  List
13.  b  \mmember{}  T1  List
14.  permutation(T1;a;b)
15.  \mforall{}x,y:T1.  \mforall{}z:T2.    (z  \mdownarrow{}\mmember{}  f[x]  {}\mRightarrow{}  z  \mdownarrow{}\mmember{}  f[y]  {}\mRightarrow{}  (x  =  y))
16.  \mforall{}x:T1.  \mforall{}[x1:T2].  uiff(1  \mleq{}  (\#x1  in  f[x]);(\#x1  in  f[x])  =  1)
17.  \mforall{}[x:T1].  uiff(1  \mleq{}  (\#x  in  a);(\#x  in  a)  =  1)
18.  x  :  T2
\mvdash{}  1  <  bag-sum([x1\mmember{}a|1  \mleq{}z  (\#x  in  f[x1])];x1.(\#x  in  f[x1]))  {}\mRightarrow{}  False


By

---

Latex:
(MoveToConcl  (-2)
  THEN  (GenConcl  \mkleeneopen{}a  =  b1\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinVar  `a'
  THEN  ThinVar  `b'
  THEN  (D  0  THENA  Auto)
  THEN  RepeatFor  3  (Thin  6)
  THEN  PromoteHyp  (-2)  6
  THEN  PromoteHyp  (-1)  (-2))

---

Home Index