---

Step * of Lemma KozenSilva-corollary0

∀[r:CRng]. ∀[x,y:Atom].
  ∀[d:ℕ ⟶ ℕ]. ∀[k:ℕ].
    (Moessner(r;x;y;1;λi.if (i =z 0) then 0 else d (i - 1) fi ;k)
    = Π(i∈upto(k)).((((k - i) ⋅r 1)*atom(x)+atom(y)))^(d i)
    ∈ PowerSeries(r)) 
  supposing ¬(x = y ∈ Atom)
BY
{ (((Auto THEN InstLemma `KozenSilva-theorem` [⌜r⌝;⌜x⌝;⌜y⌝;⌜1⌝;⌜λi.if (i =z 0) then 0 else d (i - 1) fi ⌝;⌜k⌝]⋅)
    THENA Auto
    )
   THEN Reduce (-1)
   THEN NthHypEq (-1)
   THEN EqCD
   THEN Auto
   THEN Thin (-1)) }

1
1. r : CRng
2. x : Atom
3. y : Atom
4. ¬(x = y ∈ Atom)
5. d : ℕ ⟶ ℕ
6. k : ℕ
⊢ Π(i∈upto(k)).((((k - i) ⋅r 1)*atom(x)+atom(y)))^(d i)
= ([1]_0(y:=((k ⋅r 1)*atom(x)+atom(y)))*Π(i∈upto(k)).((((k - i) ⋅r 1)*atom(x)+atom(y)))^(if (i + 1 =z 0)
  then 0
  else d ((i + 1) - 1)
  fi ))
∈ PowerSeries(r)

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[x,y:Atom].
    \mforall{}[d:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[k:\mBbbN{}].
        (Moessner(r;x;y;1;\mlambda{}i.if  (i  =\msubz{}  0)  then  0  else  d  (i  -  1)  fi  ;k)
        =  \mPi{}(i\mmember{}upto(k)).((((k  -  i)  \mcdot{}r  1)*atom(x)+atom(y)))\^{}(d  i)) 
    supposing  \mneg{}(x  =  y)


By

---

Latex:
(((Auto
      THEN  InstLemma  `KozenSilva-theorem`  [\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}\mlambda{}i.if  (i  =\msubz{}  0)  then  0  else  d  (i  -  1)  fi  \mkleeneclose{};
                \mkleeneopen{}k\mkleeneclose{}]\mcdot{}
      )
    THENA  Auto
    )
  THEN  Reduce  (-1)
  THEN  NthHypEq  (-1)
  THEN  EqCD
  THEN  Auto
  THEN  Thin  (-1))

---

Home Index