---

Step * of Lemma fps-single-bag-rep

∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X]. ∀[n:ℕ].  (<bag-rep(n;x)> = (atom(x))^(n) ∈ PowerSeries(X;r)) 
  supposing valueall-type(X)
BY
{ (xxxAutoxxx THEN NatInd (-1) THEN Try ((RWO "fps-exp-zero" 0 THEN Auto THEN Unfold `bag-rep` 0 THEN Reduce 0))) }

1
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. x : X
6. n : ℤ
⊢ <{}> = 1 ∈ PowerSeries(X;r)

2
.....upcase..... 
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. x : X
6. n : ℤ
7. 0 < n
8. <bag-rep(n - 1;x)> = (atom(x))^(n - 1) ∈ PowerSeries(X;r)
⊢ <bag-rep(n;x)> = (atom(x))^(n) ∈ PowerSeries(X;r)

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[x:X].  \mforall{}[n:\mBbbN{}].    (<bag-rep(n;x)>  =  (atom(x))\^{}(n)) 
    supposing  valueall-type(X)


By

---

Latex:
(xxxAutoxxx
  THEN  NatInd  (-1)
  THEN  Try  ((RWO  "fps-exp-zero"  0  THEN  Auto  THEN  Unfold  `bag-rep`  0  THEN  Reduce  0)))

---

Home Index