---

Step * of Lemma fps-set-to-one-one

∀[r:CRng]. ∀[y:Atom]. ∀[n:ℕ].  ([1]_n(y:=1) = if (n =z 0) then 1 else 0 fi  ∈ PowerSeries(r))
BY
{ (Auto
   THEN (BLemma `fps-ext` THEN Auto)
   THEN RepUR ``fps-one fps-zero fps-coeff fps-set-to-one`` 0
   THEN RepeatFor 2 (AutoSplit)) }

1
1. r : CRng
2. y : Atom
3. n : ℕ
4. b : bag(Atom)
5. 0 < (#y in b)
6. n = 0 ∈ ℤ
⊢ 0 = if bag-null(b) then 1 else 0 fi  ∈ |r|

2
1. r : CRng
2. y : Atom
3. n : ℕ
4. b : bag(Atom)
5. ¬0 < (#y in b)
6. n < #(b)
⊢ 0 = (if (n =z 0) then λb.if bag-null(b) then 1 else 0 fi  else λb.0 fi  b) ∈ |r|

3
1. r : CRng
2. y : Atom
3. n : ℕ
4. b : bag(Atom)
5. ¬n < #(b)
6. ¬0 < (#y in b)
⊢ if bag-null(b + bag-rep(n - #(b);y)) then 1 else 0 fi 
= (if (n =z 0) then λb.if bag-null(b) then 1 else 0 fi  else λb.0 fi  b)
∈ |r|

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[y:Atom].  \mforall{}[n:\mBbbN{}].    ([1]\_n(y:=1)  =  if  (n  =\msubz{}  0)  then  1  else  0  fi  )


By

---

Latex:
(Auto
  THEN  (BLemma  `fps-ext`  THEN  Auto)
  THEN  RepUR  ``fps-one  fps-zero  fps-coeff  fps-set-to-one``  0
  THEN  RepeatFor  2  (AutoSplit))

---

Home Index