---

Step * of Lemma fps-pascal-slice

∀[r:CRng]. ∀[x,y:Atom]. ∀[n:ℕ].  ([Δ(x,y)]_n = ((<{x}>+<{y}>))^(n) ∈ PowerSeries(r))
BY
{ xxx(Auto
      THEN InstLemma `fps-geometric-slice1` [⌜Atom⌝;⌜AtomDeq⌝;⌜r⌝;⌜n⌝;⌜(<{x}>+<{y}>)⌝]⋅
      THEN Auto
      THEN Subst' [(<{x}>+<{y}>)]_1 = (<{x}>+<{y}>) ∈ PowerSeries(r) -1
      THEN Auto
      THEN Try ((Fold `fps-pascal` (-1) THEN Auto))
      THEN All Thin)xxx }

1
1. r : CRng
2. x : Atom
3. y : Atom
⊢ [(<{x}>+<{y}>)]_1 = (<{x}>+<{y}>) ∈ PowerSeries(r)

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[x,y:Atom].  \mforall{}[n:\mBbbN{}].    ([\mDelta{}(x,y)]\_n  =  ((<\{x\}>+<\{y\}>))\^{}(n))


By

---

Latex:
xxx(Auto
        THEN  InstLemma  `fps-geometric-slice1`  [\mkleeneopen{}Atom\mkleeneclose{};\mkleeneopen{}AtomDeq\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}(<\{x\}>+<\{y\}>)\mkleeneclose{}]\mcdot{}
        THEN  Auto
        THEN  Subst'  [(<\{x\}>+<\{y\}>)]\_1  =  (<\{x\}>+<\{y\}>)  -1
        THEN  Auto
        THEN  Try  ((Fold  `fps-pascal`  (-1)  THEN  Auto))
        THEN  All  Thin)xxx

---

Home Index