---

Step * of Lemma KozenSilva-lemma

∀[r:CRng]. ∀[x,y:Atom]. ∀[h:PowerSeries(r)]. ∀[n,m:ℕ].
  [([h]_n(y:=1)*Δ(x,y))]_m = ([h]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n)) ∈ PowerSeries(r) 
  supposing (n ≤ m) ∧ (¬(x = y ∈ Atom))
BY
{ Auto }

1
1. r : CRng
2. x : Atom
3. y : Atom
4. h : PowerSeries(r)
5. n : ℕ
6. m : ℕ
7. n ≤ m
8. ¬(x = y ∈ Atom)
⊢ [([h]_n(y:=1)*Δ(x,y))]_m = ([h]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n)) ∈ PowerSeries(r)

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[x,y:Atom].  \mforall{}[h:PowerSeries(r)].  \mforall{}[n,m:\mBbbN{}].
    [([h]\_n(y:=1)*\mDelta{}(x,y))]\_m  =  ([h]\_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))\^{}(m  -  n)) 
    supposing  (n  \mleq{}  m)  \mwedge{}  (\mneg{}(x  =  y))


By

---

Latex:
Auto

---

Home Index