---

Step * 1 of Lemma KozenSilva-corollary1


1. x : Atom
2. y : Atom
3. ¬(x = y ∈ Atom)
4. d : ℕ ⟶ ℕ
5. k : ℕ
6. b : bag(ℕk)
7. upto(k) = b ∈ bag(ℕk)
8. i : ℕk
⊢ ((k - i) * 1) = (k - i) ∈ |ℤ-rng|
BY
{ xxx(SymbComp 0 THEN Auto)xxx }

---

Latex:

---

Latex:

1.  x  :  Atom
2.  y  :  Atom
3.  \mneg{}(x  =  y)
4.  d  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
5.  k  :  \mBbbN{}
6.  b  :  bag(\mBbbN{}k)
7.  upto(k)  =  b
8.  i  :  \mBbbN{}k
\mvdash{}  ((k  -  i)  *  1)  =  (k  -  i)


By

---

Latex:
xxx(SymbComp  0  THEN  Auto)xxx

---

Home Index