---

Step * 1 1 2 1 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 : bag(X) × bag(X)
9. b1 = ((fst(p)) + (snd(p))) ∈ bag(X)
10. ↑¬bbag-null(fst(p))
⊢ #(snd(p)) < #(b1)
BY
{ xxx((HypSubst (-2) 0 THEN Auto)
      THEN RWO "bag-size-append" 0
      THEN Auto
      THEN RWO "null-bag-size" (-1)
      THEN Auto
      THEN RW assert_pushdownC (-1)
      THEN Auto')xxx }

---

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  :  bag(X)  \mtimes{}  bag(X)
9.  b1  =  ((fst(p))  +  (snd(p)))
10.  \muparrow{}\mneg{}\msubb{}bag-null(fst(p))
\mvdash{}  \#(snd(p))  <  \#(b1)


By

---

Latex:
xxx((HypSubst  (-2)  0  THEN  Auto)
        THEN  RWO  "bag-size-append"  0
        THEN  Auto
        THEN  RWO  "null-bag-size"  (-1)
        THEN  Auto
        THEN  RW  assert\_pushdownC  (-1)
        THEN  Auto')xxx

---

Home Index