---

Step * 2 2 1 of Lemma KozenSilva-corollary2

.....equality..... 
1. x : Atom
2. y : Atom
3. ¬(x = y ∈ Atom)
4. k : ℤ
5. 0 < k
6. d : ℕ ⟶ ℕ
7. X : PowerSeries(ℤ-rng)
8. Π(i∈upto(k - 1)).(((k - 1 - i)*atom(x)+atom(y)))^(d (i + 1)) = X ∈ PowerSeries(ℤ-rng)
⊢ Σ(d i | i < k) ~ (d 0) + Σ(d (i + 1) | i < k - 1)
BY
{ TACTIC:((InstLemma `sum_split` [⌜k⌝;⌜λ2i.d i⌝;⌜1⌝]⋅ THENA Auto)
          THEN HypSubst' (-1) 0
          THEN EqCD
          THEN Auto
          THEN RepUR ``sum`` 0
          THEN Auto) }

---

Latex:

---

Latex:
.....equality..... 
1.  x  :  Atom
2.  y  :  Atom
3.  \mneg{}(x  =  y)
4.  k  :  \mBbbZ{}
5.  0  <  k
6.  d  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
7.  X  :  PowerSeries(\mBbbZ{}-rng)
8.  \mPi{}(i\mmember{}upto(k  -  1)).(((k  -  1  -  i)*atom(x)+atom(y)))\^{}(d  (i  +  1))  =  X
\mvdash{}  \mSigma{}(d  i  |  i  <  k)  \msim{}  (d  0)  +  \mSigma{}(d  (i  +  1)  |  i  <  k  -  1)


By

---

Latex:
TACTIC:((InstLemma  `sum\_split`  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i.d  i\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  HypSubst'  (-1)  0
                THEN  EqCD
                THEN  Auto
                THEN  RepUR  ``sum``  0
                THEN  Auto)

---

Home Index