---

Step * 2 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)
⊢ Π(x∈{0} + [1, k)).f[x] = (f[0]*Π(x∈upto(k - 1)).f[x + 1]) ∈ PowerSeries(X;r)
BY
{ ((Assert (([1, k) ∈ bag(ℕk)) ∧ ({0} ∈ bag(ℕk))) ∧ (upto(k - 1) ∈ bag(ℕk - 1)) ∧ ({0} + [1, k) ∈ bag(ℕk)) BY
          Auto)
   THEN (InstLemma `fps-product-append` [⌜X⌝;⌜eq⌝;⌜r⌝;⌜ℕk⌝]⋅ THENA Auto)
   THEN (RWO "-1" 0 THENA Auto)
   THEN EqCD
   THEN Auto) }

1
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. k : ℕ+
6. f : ℕk ⟶ PowerSeries(X;r)
7. [1, k) ∈ bag(ℕk)
8. {0} ∈ bag(ℕk)
9. upto(k - 1) ∈ bag(ℕk - 1)
10. {0} + [1, k) ∈ bag(ℕk)
11. ∀[f:ℕk ⟶ PowerSeries(X;r)]. ∀[b,c:bag(ℕk)].  (Π(x∈b + c).f[x] = (Π(x∈b).f[x]*Π(x∈c).f[x]) ∈ PowerSeries(X;r))
⊢ Π(x∈{0}).f[x] = f[0] ∈ PowerSeries(X;r)

2
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. k : ℕ+
6. f : ℕk ⟶ PowerSeries(X;r)
7. [1, k) ∈ bag(ℕk)
8. {0} ∈ bag(ℕk)
9. upto(k - 1) ∈ bag(ℕk - 1)
10. {0} + [1, k) ∈ bag(ℕk)
11. ∀[f:ℕk ⟶ PowerSeries(X;r)]. ∀[b,c:bag(ℕk)].  (Π(x∈b + c).f[x] = (Π(x∈b).f[x]*Π(x∈c).f[x]) ∈ PowerSeries(X;r))
⊢ Π(x∈[1, k)).f[x] = Π(x∈upto(k - 1)).f[x + 1] ∈ PowerSeries(X;r)

---

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{}  \mPi{}(x\mmember{}\{0\}  +  [1,  k)).f[x]  =  (f[0]*\mPi{}(x\mmember{}upto(k  -  1)).f[x  +  1])


By

---

Latex:
((Assert  (([1,  k)  \mmember{}  bag(\mBbbN{}k))  \mwedge{}  (\{0\}  \mmember{}  bag(\mBbbN{}k)))
                \mwedge{}  (upto(k  -  1)  \mmember{}  bag(\mBbbN{}k  -  1))
                \mwedge{}  (\{0\}  +  [1,  k)  \mmember{}  bag(\mBbbN{}k))  BY
                Auto)
  THEN  (InstLemma  `fps-product-append`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}\mBbbN{}k\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  EqCD
  THEN  Auto)

---

Home Index