---

Step * 1 of Lemma nim-sum_wf


1. x : ℕ
2. ∀x:ℕx. ∀[y:ℕ]. (nim-sum(x;y) ∈ ℕ)
3. y : ℕ
4. ¬(x = 0 ∈ ℤ)
5. ¬(y = 0 ∈ ℤ)
6. x = (((x ÷ 2) * 2) + (x rem 2)) ∈ ℤ
7. (0 ≤ (x rem 2)) ∧ x rem 2 < 2
8. y = (((y ÷ 2) * 2) + (y rem 2)) ∈ ℤ
9. (0 ≤ (y rem 2)) ∧ y rem 2 < 2
⊢ eval rx = x rem 2 in
  eval qx = x ÷ 2 in
  eval ry = y rem 2 in
  eval qy = y ÷ 2 in
  eval s = nim-sum(qx;qy) in
  eval d = if rx=ry then 0 else 1 in
    (2 * s) + d ∈ ℕ
BY
{ ((InstHyp [⌜x ÷ 2⌝;⌜y ÷ 2⌝] 2⋅ THENA Auto) THEN Repeat ((CallByValueReduce 0⋅ THENA Auto)) THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}
2.  \mforall{}x:\mBbbN{}x.  \mforall{}[y:\mBbbN{}].  (nim-sum(x;y)  \mmember{}  \mBbbN{})
3.  y  :  \mBbbN{}
4.  \mneg{}(x  =  0)
5.  \mneg{}(y  =  0)
6.  x  =  (((x  \mdiv{}  2)  *  2)  +  (x  rem  2))
7.  (0  \mleq{}  (x  rem  2))  \mwedge{}  x  rem  2  <  2
8.  y  =  (((y  \mdiv{}  2)  *  2)  +  (y  rem  2))
9.  (0  \mleq{}  (y  rem  2))  \mwedge{}  y  rem  2  <  2
\mvdash{}  eval  rx  =  x  rem  2  in
    eval  qx  =  x  \mdiv{}  2  in
    eval  ry  =  y  rem  2  in
    eval  qy  =  y  \mdiv{}  2  in
    eval  s  =  nim-sum(qx;qy)  in
    eval  d  =  if  rx=ry  then  0  else  1  in
        (2  *  s)  +  d  \mmember{}  \mBbbN{}


By

---

Latex:
((InstHyp  [\mkleeneopen{}x  \mdiv{}  2\mkleeneclose{};\mkleeneopen{}y  \mdiv{}  2\mkleeneclose{}]  2\mcdot{}  THENA  Auto)
  THEN  Repeat  ((CallByValueReduce  0\mcdot{}  THENA  Auto))
  THEN  Auto)

---

Home Index