---

Step * of Lemma nim-sum-0

∀[x:ℕ]. (nim-sum(x;0) = x ∈ ℤ)
BY
{ (Auto THEN RWO "nim-sum-com" 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbN{}].  (nim-sum(x;0)  =  x)


By

---

Latex:
(Auto  THEN  RWO  "nim-sum-com"  0  THEN  Reduce  0  THEN  Auto)

---

Home Index