---

Step * 1 of Lemma KozenSilva-corollary0


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)
BY
{ xxx((GenConcl ⌜upto(k) = b ∈ bag(ℕk)⌝⋅ THENA Auto)
      THEN (Subst ⌜[1]_0(y:=((k ⋅r 1)*atom(x)+atom(y))) = 1 ∈ PowerSeries(r)⌝ 0⋅ THENA Auto)
      )xxx }

1
.....equality..... 
1. r : CRng
2. x : Atom
3. y : Atom
4. ¬(x = y ∈ Atom)
5. d : ℕ ⟶ ℕ
6. k : ℕ
7. b : bag(ℕk)
8. upto(k) = b ∈ bag(ℕk)
⊢ [1]_0(y:=((k ⋅r 1)*atom(x)+atom(y))) = 1 ∈ PowerSeries(r)

2
1. r : CRng
2. x : Atom
3. y : Atom
4. ¬(x = y ∈ Atom)
5. d : ℕ ⟶ ℕ
6. k : ℕ
7. b : bag(ℕk)
8. upto(k) = b ∈ bag(ℕk)
⊢ Π(i∈b).((((k - i) ⋅r 1)*atom(x)+atom(y)))^(d i)
= (1*Π(i∈b).((((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:

1.  r  :  CRng
2.  x  :  Atom
3.  y  :  Atom
4.  \mneg{}(x  =  y)
5.  d  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
6.  k  :  \mBbbN{}
\mvdash{}  \mPi{}(i\mmember{}upto(k)).((((k  -  i)  \mcdot{}r  1)*atom(x)+atom(y)))\^{}(d  i)
=  ([1]\_0(y:=((k  \mcdot{}r  1)*atom(x)+atom(y)))*\mPi{}(i\mmember{}upto(k)).((((k  -  i)  \mcdot{}r  1)*atom(x)
                                                                                                              +atom(y)))\^{}(if  (i  +  1  =\msubz{}  0)
    then  0
    else  d  ((i  +  1)  -  1)
    fi  ))


By

---

Latex:
xxx((GenConcl  \mkleeneopen{}upto(k)  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)
        THEN  (Subst  \mkleeneopen{}[1]\_0(y:=((k  \mcdot{}r  1)*atom(x)+atom(y)))  =  1\mkleeneclose{}  0\mcdot{}  THENA  Auto)
        )xxx

---

Home Index