---

Step * 1 1 of Lemma KozenSilva-corollary0

.....equality..... 
1. r : CRng
2. x : Atom
3. y : Atom
4. ¬(x = y ∈ Atom)
5. d : ℕ ⟶ ℕ
6. k : ℕ
7. b : bag(ℕk)
8. upto(k) = b ∈ bag(ℕk)
⊢ [1]_0(y:=((k ⋅r 1)*atom(x)+atom(y))) = 1 ∈ PowerSeries(r)
BY
{ xxx((InstLemma `fps-one-slice` [⌜Atom⌝]⋅ THENA Auto) THEN RWO  "-1" 0 THEN Auto)xxx }

---

Latex:

---

Latex:
.....equality..... 
1.  r  :  CRng
2.  x  :  Atom
3.  y  :  Atom
4.  \mneg{}(x  =  y)
5.  d  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
6.  k  :  \mBbbN{}
7.  b  :  bag(\mBbbN{}k)
8.  upto(k)  =  b
\mvdash{}  [1]\_0(y:=((k  \mcdot{}r  1)*atom(x)+atom(y)))  =  1


By

---

Latex:
xxx((InstLemma  `fps-one-slice`  [\mkleeneopen{}Atom\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  RWO    "-1"  0  THEN  Auto)xxx

---

Home Index