Step
*
2
of Lemma
bag-count-bag-lub
1. T : Type
2. eq : EqDecider(T)
3. as : bag(T)
4. bs : bag(T)
5. x : T
6. ¬x ↓∈ bag-to-set(eq;as + bs)
⊢ bag-sum([x1∈bag-to-set(eq;as + bs)|
1 ≤z (#x in bag-rep(imax((#x1 in as);(#x1 in bs));x1))];x1.(#x in bag-rep(imax((#x1 in as);(#x1 in bs));x1)))
= imax((#x in as);(#x in bs))
∈ ℤ
BY
{ (Subst ⌜[x1∈bag-to-set(eq;as + bs)|1 ≤z (#x in bag-rep(imax((#x1 in as);(#x1 in bs));x1))] = {} ∈ bag(T)⌝ 0⋅
THEN Auto
)⋅ }
1
.....equality.....
1. T : Type
2. eq : EqDecider(T)
3. as : bag(T)
4. bs : bag(T)
5. x : T
6. ¬x ↓∈ bag-to-set(eq;as + bs)
⊢ [x1∈bag-to-set(eq;as + bs)|1 ≤z (#x in bag-rep(imax((#x1 in as);(#x1 in bs));x1))] = {} ∈ bag(T)
2
1. T : Type
2. eq : EqDecider(T)
3. as : bag(T)
4. bs : bag(T)
5. x : T
6. ¬x ↓∈ bag-to-set(eq;as + bs)
⊢ bag-sum({};x1.(#x in bag-rep(imax((#x1 in as);(#x1 in bs));x1))) = imax((#x in as);(#x in bs)) ∈ ℤ
Latex:
Latex:
1. T : Type
2. eq : EqDecider(T)
3. as : bag(T)
4. bs : bag(T)
5. x : T
6. \mneg{}x \mdownarrow{}\mmember{} bag-to-set(eq;as + bs)
\mvdash{} bag-sum([x1\mmember{}bag-to-set(eq;as + bs)|
1 \mleq{}z (\#x in bag-rep(imax((\#x1 in as);
(\#x1 in bs));x1))];x1.(\#x in bag-rep(imax((\#x1 in as);
(\#x1 in bs));x1)))
= imax((\#x in as);(\#x in bs))
By
Latex:
(Subst \mkleeneopen{}[x1\mmember{}bag-to-set(eq;as + bs)|1 \mleq{}z (\#x in bag-rep(imax((\#x1 in as);(\#x1 in bs));x1))] = \{\}\mkleeneclose{} 0\mcdot{}
THEN Auto
)\mcdot{}
Home
Index