---

Step * of Lemma Moessner-aux_wf

∀[r:CRng]. ∀[x,y:Atom]. ∀[h:PowerSeries(r)]. ∀[d:ℕ ⟶ ℕ]. ∀[k:ℕ].  (Moessner-aux(r;x;y;h;d;k) ∈ PowerSeries(r))
BY
{ (InductionOnNat
   THEN RecUnfold `Moessner-aux` 0
   THEN AutoSplit
   THEN Auto
   THEN MemTypeCD
   THEN Auto
   THEN BLemma `non_neg_sum`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[x,y:Atom].  \mforall{}[h:PowerSeries(r)].  \mforall{}[d:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[k:\mBbbN{}].
    (Moessner-aux(r;x;y;h;d;k)  \mmember{}  PowerSeries(r))


By

---

Latex:
(InductionOnNat
  THEN  RecUnfold  `Moessner-aux`  0
  THEN  AutoSplit
  THEN  Auto
  THEN  MemTypeCD
  THEN  Auto
  THEN  BLemma  `non\_neg\_sum`
  THEN  Auto)

---

Home Index