---

Step * 2 of Lemma fps-exp-linear-coeff


1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. x : X
5. y : X
6. ¬(x = y ∈ X)
7. r : CRng
8. k : |r|
9. m : ℤ
10. 0 < m
11. ∀[n:ℕ]. ((((k)*atom(x)+atom(y)))^(m - 1)[bag-rep(n;x)] = if (n =z m - 1) then k ↑r (m - 1) else 0 fi  ∈ |r|)
12. n : ℕ
⊢ (((k)*atom(x)+atom(y)))^(m)[bag-rep(n;x)] = if (n =z m) then k ↑r m else 0 fi  ∈ |r|
BY
{ (Subst ⌜m ~ (m - 1) + 1⌝ 0⋅
   THEN Auto
   THEN (RWO "fps-exp-add" 0 THENA Auto)
   THEN (RWO "fps-exp-one" 0 THENA Auto)
   THEN MoveToConcl (-2)
   THEN (GenConcl ⌜(((k)*atom(x)+atom(y)))^(m - 1) = f ∈ PowerSeries(X;r)⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN Auto
   THEN Subst ⌜(m - 1) + 1 ~ m⌝ 0⋅
   THEN Auto
   THEN RepUR ``fps-mul fps-coeff`` 0
   THEN Unfold `fps-coeff` (-1)) }

1
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. x : X
5. y : X
6. ¬(x = y ∈ X)
7. r : CRng
8. k : |r|
9. m : ℤ
10. 0 < m
11. n : ℕ
12. f : PowerSeries(X;r)
13. ∀[n:ℕ]. ((f bag-rep(n;x)) = if (n =z m - 1) then k ↑r (m - 1) else 0 fi  ∈ |r|)
⊢ Σ(p∈bag-partitions(eq;bag-rep(n;x))). * (f (fst(p))) (((k)*atom(x)+atom(y)) (snd(p)))
= if (n =z m) then k ↑r m else 0 fi 
∈ |r|

---

Latex:

---

Latex:

1.  X  :  Type
2.  valueall-type(X)
3.  eq  :  EqDecider(X)
4.  x  :  X
5.  y  :  X
6.  \mneg{}(x  =  y)
7.  r  :  CRng
8.  k  :  |r|
9.  m  :  \mBbbZ{}
10.  0  <  m
11.  \mforall{}[n:\mBbbN{}]
            ((((k)*atom(x)+atom(y)))\^{}(m  -  1)[bag-rep(n;x)]  =  if  (n  =\msubz{}  m  -  1)  then  k  \muparrow{}r  (m  -  1)  else  0  fi  )
12.  n  :  \mBbbN{}
\mvdash{}  (((k)*atom(x)+atom(y)))\^{}(m)[bag-rep(n;x)]  =  if  (n  =\msubz{}  m)  then  k  \muparrow{}r  m  else  0  fi 


By

---

Latex:
(Subst  \mkleeneopen{}m  \msim{}  (m  -  1)  +  1\mkleeneclose{}  0\mcdot{}
  THEN  Auto
  THEN  (RWO  "fps-exp-add"  0  THENA  Auto)
  THEN  (RWO  "fps-exp-one"  0  THENA  Auto)
  THEN  MoveToConcl  (-2)
  THEN  (GenConcl  \mkleeneopen{}(((k)*atom(x)+atom(y)))\^{}(m  -  1)  =  f\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  Auto
  THEN  Subst  \mkleeneopen{}(m  -  1)  +  1  \msim{}  m\mkleeneclose{}  0\mcdot{}
  THEN  Auto
  THEN  RepUR  ``fps-mul  fps-coeff``  0
  THEN  Unfold  `fps-coeff`  (-1))

---

Home Index