---

Step * of Lemma KozenSilva-corollary1

∀[x,y:Atom].
  ∀[d:ℕ ⟶ ℕ]. ∀[k:ℕ].
    (Moessner(ℤ-rng;x;y;1;λi.if (i =z 0) then 0 else d (i - 1) fi ;k)
    = Π(i∈upto(k)).(((k - i)*atom(x)+atom(y)))^(d i)
    ∈ PowerSeries(ℤ-rng)) 
  supposing ¬(x = y ∈ Atom)
BY
{ (Auto
   THEN RWO "KozenSilva-corollary0" 0
   THEN Try ((GenConcl ⌜upto(k) = b ∈ bag(ℕk)⌝⋅ THENA Auto))
   THEN Auto
   THEN RepeatFor 4 ((EqCD THEN Auto))
   THEN RWO "rng_nat_op-int" 0
   THEN Auto) }

1
1. x : Atom
2. y : Atom
3. ¬(x = y ∈ Atom)
4. d : ℕ ⟶ ℕ
5. k : ℕ
6. b : bag(ℕk)
7. upto(k) = b ∈ bag(ℕk)
8. i : ℕk
⊢ ((k - i) * 1) = (k - i) ∈ |ℤ-rng|

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  RWO  "KozenSilva-corollary0"  0
  THEN  Try  ((GenConcl  \mkleeneopen{}upto(k)  =  b\mkleeneclose{}\mcdot{}  THENA  Auto))
  THEN  Auto
  THEN  RepeatFor  4  ((EqCD  THEN  Auto))
  THEN  RWO  "rng\_nat\_op-int"  0
  THEN  Auto)

---

Home Index