---

Step * 1 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. n : ℕ
⊢ (((k)*atom(x)+atom(y)))^(0)[bag-rep(n;x)] = if (n =z 0) then k ↑r 0 else 0 fi  ∈ |r|
BY
{ TACTIC:((RWO "fps-exp-zero" 0⋅ THENA Auto)
          THEN RepUR ``fps-one fps-coeff`` 0
          THEN (RWO "bag-null-rep" 0 THENA Auto)
          THEN AutoSplit) }

---

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.  n  :  \mBbbN{}
\mvdash{}  (((k)*atom(x)+atom(y)))\^{}(0)[bag-rep(n;x)]  =  if  (n  =\msubz{}  0)  then  k  \muparrow{}r  0  else  0  fi 


By

---

Latex:
TACTIC:((RWO  "fps-exp-zero"  0\mcdot{}  THENA  Auto)
                THEN  RepUR  ``fps-one  fps-coeff``  0
                THEN  (RWO  "bag-null-rep"  0  THENA  Auto)
                THEN  AutoSplit)

---

Home Index