---

Step * 2 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)) ∧ x rem 2 < 2
7. y = 0 ∈ ℤ
⊢ nim-sum(x;0) rem 2 ~ if x rem 2=0 then 0 else 1
BY
{ ((RWO  "nim-sum-0" 0 THENA Auto)
   THEN (GenConcl ⌜(x rem 2) = r ∈ ℕ2⌝⋅ THENA Auto)
   THEN IntSegCases (-2)
   THEN Reduce 0
   THEN Auto) }

---

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))  \mwedge{}  x  rem  2  <  2
7.  y  =  0
\mvdash{}  nim-sum(x;0)  rem  2  \msim{}  if  x  rem  2=0  then  0  else  1


By

---

Latex:
((RWO    "nim-sum-0"  0  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(x  rem  2)  =  r\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  IntSegCases  (-2)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index