---

Step * of Lemma fps-set-to-one-ucont

∀[r:CRng]. ∀y:Atom. ∀n:ℕ.  fps-ucont(Atom;AtomDeq;r;f.[f]_n(y:=1))
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN With ⌜b + bag-rep(n;y)⌝ (D 0)⋅
   THEN Auto
   THEN RepUR ``fps-set-to-one fps-coeff fps-restrict`` 0⋅
   THEN RepeatFor 3 (AutoSplit)
   THEN D (-4)
   THEN With ⌜bag-rep(#(b);y)⌝ (D 0)⋅
   THEN Auto') }

1
1. r : CRng
2. y : Atom
3. n : ℕ
4. b : bag(Atom)
5. ¬n < #(b)
6. ¬0 < (#y in b)
7. f : PowerSeries(r)
⊢ (b + bag-rep(n;y)) = ((b + bag-rep(n - #(b);y)) + bag-rep(#(b);y)) ∈ bag(Atom)

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}y:Atom.  \mforall{}n:\mBbbN{}.    fps-ucont(Atom;AtomDeq;r;f.[f]\_n(y:=1))


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  With  \mkleeneopen{}b  +  bag-rep(n;y)\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  RepUR  ``fps-set-to-one  fps-coeff  fps-restrict``  0\mcdot{}
  THEN  RepeatFor  3  (AutoSplit)
  THEN  D  (-4)
  THEN  With  \mkleeneopen{}bag-rep(\#(b);y)\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto')

---

Home Index