---

Step * of Lemma fps-support-degree-bound

∀[r:CRng]. ∀[f:PowerSeries(r)]. ∀[s:bag(Atom)].  (fps-support(r;f;s) ⇒ fps-degree-bound(r;f;#(s)))
BY
{ (Auto THEN UnfoldTopAb (-1) THEN UnfoldTopAb 0 THEN RepeatFor 2 (ParallelLast)) }

1
.....antecedent..... 
1. r : CRng
2. f : PowerSeries(r)
3. s : bag(Atom)
4. ∀[b:bag(Atom)]. f[b] = 0 ∈ |r| supposing ¬sub-bag(Atom;b;s)@i
5. b : bag(Atom)
6. #(s) < #(b)
⊢ ¬sub-bag(Atom;b;s)

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[f:PowerSeries(r)].  \mforall{}[s:bag(Atom)].    (fps-support(r;f;s)  {}\mRightarrow{}  fps-degree-bound(r;f;\#(s)))


By

---

Latex:
(Auto  THEN  UnfoldTopAb  (-1)  THEN  UnfoldTopAb  0  THEN  RepeatFor  2  (ParallelLast))

---

Home Index