---

Step * 1 1 of Lemma fps-product-upto


1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. k : ℕ+
6. f : ℕk ⟶ PowerSeries(X;r)
⊢ [0, k) ~ [0 / [1, k)]
BY
{ (RW (AddrC [1] RecUnfoldTopAbC) 0 THEN Reduce 0 THEN AutoSplit) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  valueall-type(X)
3.  eq  :  EqDecider(X)
4.  r  :  CRng
5.  k  :  \mBbbN{}\msupplus{}
6.  f  :  \mBbbN{}k  {}\mrightarrow{}  PowerSeries(X;r)
\mvdash{}  [0,  k)  \msim{}  [0  /  [1,  k)]


By

---

Latex:
(RW  (AddrC  [1]  RecUnfoldTopAbC)  0  THEN  Reduce  0  THEN  AutoSplit)

---

Home Index