---

Step * 1 2 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. fps-ucont(Atom;AtomDeq;r;f.[([f]_n(y:=1)*Δ(x,y))]_m)
⊢ fps-ucont(Atom;AtomDeq;r;f.([f]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n)))
BY
{ xxx(InstLemma `fps-ucont-composition` [⌜Atom⌝;⌜AtomDeq⌝;⌜r⌝;⌜λ2f.(f*((atom(x)+atom(y)))^(m - n))⌝;
      ⌜λ2f.[f]_n(y:=(atom(x)+atom(y)))⌝]⋅
      THEN Auto
      THEN Try ((BLemma `fps-mul-ucont` THEN Auto))
      THEN RepUR ``compose so_apply so_lambda`` (-1)
      THEN Auto
      THEN Auto')⋅xxx }

1
.....antecedent..... 
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. fps-ucont(Atom;AtomDeq;r;f.[([f]_n(y:=1)*Δ(x,y))]_m)
⊢ fps-ucont(Atom;AtomDeq;r;f.[f]_n(y:=(atom(x)+atom(y))))

---

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.  fps-ucont(Atom;AtomDeq;r;f.[([f]\_n(y:=1)*\mDelta{}(x,y))]\_m)
\mvdash{}  fps-ucont(Atom;AtomDeq;r;f.([f]\_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))\^{}(m  -  n)))


By

---

Latex:
xxx(InstLemma  `fps-ucont-composition`  [\mkleeneopen{}Atom\mkleeneclose{};\mkleeneopen{}AtomDeq\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}f.(f*((atom(x)+atom(y)))\^{}(m  -  n))\mkleeneclose{};
        \mkleeneopen{}\mlambda{}\msubtwo{}f.[f]\_n(y:=(atom(x)+atom(y)))\mkleeneclose{}]\mcdot{}
        THEN  Auto
        THEN  Try  ((BLemma  `fps-mul-ucont`  THEN  Auto))
        THEN  RepUR  ``compose  so\_apply  so\_lambda``  (-1)
        THEN  Auto
        THEN  Auto')\mcdot{}xxx

---

Home Index