---

Step * 1 8 of Lemma KozenSilva-lemma


1. r : CRng
2. x : Atom
3. y : Atom
4. h : PowerSeries(r)
5. n : ℕ
6. m : ℕ
7. n ≤ m
8. ¬(x = y ∈ Atom)
9. λ2h.[([h]_n(y:=1)*Δ(x,y))]_m
= λ2h.([h]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n))
∈ (PowerSeries(r) ⟶ PowerSeries(r))
⊢ [([h]_n(y:=1)*Δ(x,y))]_m = ([h]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n)) ∈ PowerSeries(r)
BY
{ xxx((ApFunToHypEquands `Z' ⌜Z[h]⌝ ⌜PowerSeries(r)⌝ (-1)⋅ THEN Auto)
      THEN RepUR ``so_apply so_lambda`` -1
      THEN Auto)xxx }

---

Latex:

---

Latex:

1.  r  :  CRng
2.  x  :  Atom
3.  y  :  Atom
4.  h  :  PowerSeries(r)
5.  n  :  \mBbbN{}
6.  m  :  \mBbbN{}
7.  n  \mleq{}  m
8.  \mneg{}(x  =  y)
9.  \mlambda{}\msubtwo{}h.[([h]\_n(y:=1)*\mDelta{}(x,y))]\_m  =  \mlambda{}\msubtwo{}h.([h]\_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))\^{}(m  -  n))
\mvdash{}  [([h]\_n(y:=1)*\mDelta{}(x,y))]\_m  =  ([h]\_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))\^{}(m  -  n))


By

---

Latex:
xxx((ApFunToHypEquands  `Z'  \mkleeneopen{}Z[h]\mkleeneclose{}  \mkleeneopen{}PowerSeries(r)\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto)
        THEN  RepUR  ``so\_apply  so\_lambda``  -1
        THEN  Auto)xxx

---

Home Index