---

Step * 3 of Lemma nim-sum-rem2


1. x : ℕ
2. ∀x:ℕx. ∀[y:ℕ]. (nim-sum(x;y) rem 2 ~ if x rem 2=y rem 2 then 0 else 1)
3. y : ℕ
4. ¬(x = 0 ∈ ℤ)
5. x = (((x ÷ 2) * 2) + (x rem 2)) ∈ ℤ
6. 0 ≤ (x rem 2)
7. x rem 2 < 2
8. ¬(y = 0 ∈ ℤ)
9. nim-sum(x ÷ 2;y ÷ 2) rem 2 ~ if x ÷ 2 rem 2=y ÷ 2 rem 2 then 0 else 1
⊢ ((2 * nim-sum(x ÷ 2;y ÷ 2)) + if x rem 2=y rem 2 then 0 else 1 rem 2) = if x rem 2=y rem 2 then 0 else 1 ∈ ℤ
BY
{ AutoSplit }

1
1. x : {1...}
2. ∀x:ℕx. ∀[y:ℕ]. (nim-sum(x;y) rem 2 ~ if x rem 2=y rem 2 then 0 else 1)
3. y : ℕ
4. x rem 2 ≠ y rem 2
5. x = (((x ÷ 2) * 2) + (x rem 2)) ∈ ℤ
6. 0 ≤ (x rem 2)
7. x rem 2 < 2
8. ¬(y = 0 ∈ ℤ)
9. nim-sum(x ÷ 2;y ÷ 2) rem 2 ~ if x ÷ 2 rem 2=y ÷ 2 rem 2 then 0 else 1
⊢ ((2 * nim-sum(x ÷ 2;y ÷ 2)) + 1 rem 2) = 1 ∈ ℤ

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}
2.  \mforall{}x:\mBbbN{}x.  \mforall{}[y:\mBbbN{}].  (nim-sum(x;y)  rem  2  \msim{}  if  x  rem  2=y  rem  2  then  0  else  1)
3.  y  :  \mBbbN{}
4.  \mneg{}(x  =  0)
5.  x  =  (((x  \mdiv{}  2)  *  2)  +  (x  rem  2))
6.  0  \mleq{}  (x  rem  2)
7.  x  rem  2  <  2
8.  \mneg{}(y  =  0)
9.  nim-sum(x  \mdiv{}  2;y  \mdiv{}  2)  rem  2  \msim{}  if  x  \mdiv{}  2  rem  2=y  \mdiv{}  2  rem  2  then  0  else  1
\mvdash{}  ((2  *  nim-sum(x  \mdiv{}  2;y  \mdiv{}  2))  +  if  x  rem  2=y  rem  2  then  0  else  1  rem  2)
=  if  x  rem  2=y  rem  2  then  0  else  1


By

---

Latex:
AutoSplit

---

Home Index