---

Step * 1 1 2 1 of Lemma fps-div-coeff_wf


1. X : Type
2. eq : EqDecider(X)
3. b1 : bag(X)
4. valueall-type(X)
5. parts : bag({p:bag(X) × bag(X)| b1 = ((fst(p)) + (snd(p))) ∈ bag(X)} )
6. bag-partitions(eq;b1) = parts ∈ bag({p:bag(X) × bag(X)| b1 = ((fst(p)) + (snd(p))) ∈ bag(X)} )
7. [p∈parts|¬bbag-null(fst(p))]
= [p∈parts|¬bbag-null(fst(p))]
∈ bag({p:{p:bag(X) × bag(X)| b1 = ((fst(p)) + (snd(p))) ∈ bag(X)} | ↑¬bbag-null(fst(p))} )
8. p : {p:bag(X) × bag(X)| b1 = ((fst(p)) + (snd(p))) ∈ bag(X)} 
9. ↑¬bbag-null(fst(p))
⊢ #(snd(p)) < #(b1)
BY
{ D -2 }

1
1. X : Type
2. eq : EqDecider(X)
3. b1 : bag(X)
4. valueall-type(X)
5. parts : bag({p:bag(X) × bag(X)| b1 = ((fst(p)) + (snd(p))) ∈ bag(X)} )
6. bag-partitions(eq;b1) = parts ∈ bag({p:bag(X) × bag(X)| b1 = ((fst(p)) + (snd(p))) ∈ bag(X)} )
7. [p∈parts|¬bbag-null(fst(p))]
= [p∈parts|¬bbag-null(fst(p))]
∈ bag({p:{p:bag(X) × bag(X)| b1 = ((fst(p)) + (snd(p))) ∈ bag(X)} | ↑¬bbag-null(fst(p))} )
8. p : bag(X) × bag(X)
9. b1 = ((fst(p)) + (snd(p))) ∈ bag(X)
10. ↑¬bbag-null(fst(p))
⊢ #(snd(p)) < #(b1)

---

Latex:

---

Latex:

1.  X  :  Type
2.  eq  :  EqDecider(X)
3.  b1  :  bag(X)
4.  valueall-type(X)
5.  parts  :  bag(\{p:bag(X)  \mtimes{}  bag(X)|  b1  =  ((fst(p))  +  (snd(p)))\}  )
6.  bag-partitions(eq;b1)  =  parts
7.  [p\mmember{}parts|\mneg{}\msubb{}bag-null(fst(p))]  =  [p\mmember{}parts|\mneg{}\msubb{}bag-null(fst(p))]
8.  p  :  \{p:bag(X)  \mtimes{}  bag(X)|  b1  =  ((fst(p))  +  (snd(p)))\} 
9.  \muparrow{}\mneg{}\msubb{}bag-null(fst(p))
\mvdash{}  \#(snd(p))  <  \#(b1)


By

---

Latex:
D  -2

---

Home Index