---

Step * 1 1 2 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)} )
⊢ [p∈parts|¬bbag-null(fst(p))] ∈ bag({p:bag(X) × bag(X)| #(snd(p)) < #(b1)} )
BY
{ xxx((DoSubsume THEN Auto) THEN SubtypeReasoning THEN Auto)xxx }

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 : {p:bag(X) × bag(X)| b1 = ((fst(p)) + (snd(p))) ∈ bag(X)} 
9. ↑¬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
\mvdash{}  [p\mmember{}parts|\mneg{}\msubb{}bag-null(fst(p))]  \mmember{}  bag(\{p:bag(X)  \mtimes{}  bag(X)|  \#(snd(p))  <  \#(b1)\}  )


By

---

Latex:
xxx((DoSubsume  THEN  Auto)  THEN  SubtypeReasoning  THEN  Auto)xxx

---

Home Index