---

Step * of Lemma nim-sum-com

∀[x,y:ℕ].  (nim-sum(x;y) = nim-sum(y;x) ∈ ℤ)
BY
{ ((CompleteInductionOnNat THEN (D 0 THENA Auto))
   THEN (CaseNat 0 `x'
         THENL [(Computation THEN Auto)
               ; (CaseNat 0 `y' THENL [(Computation THEN Auto); (Unfold `nim-sum` 0 THEN Reduce 0)])]
   )
   THEN (InstLemma `div_rem_sum` [⌜x⌝;⌜2⌝]⋅ THENA Auto)
   THEN (InstLemma `rem_bounds_1` [⌜x⌝;⌜2⌝]⋅ THENA Auto)
   THEN (InstLemma `div_rem_sum` [⌜y⌝;⌜2⌝]⋅ THENA Auto)
   THEN (InstLemma `rem_bounds_1` [⌜y⌝;⌜2⌝]⋅ THENA Auto)) }

1
1. x : ℕ
2. ∀x:ℕx. ∀[y:ℕ]. (nim-sum(x;y) = nim-sum(y;x) ∈ ℤ)
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
= eval rx = y rem 2 in
  eval qx = y ÷ 2 in
  eval ry = x rem 2 in
  eval qy = x ÷ 2 in
  eval s = nim-sum(qx;qy) in
  eval d = if rx=ry then 0 else 1 in
    (2 * s) + d
∈ ℤ

---

Latex:

---

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


By

---

Latex:
((CompleteInductionOnNat  THEN  (D  0  THENA  Auto))
  THEN  (CaseNat  0  `x'
              THENL  [(Computation  THEN  Auto)
                          ;  (CaseNat  0  `y'  THENL  [(Computation  THEN  Auto);  (Unfold  `nim-sum`  0  THEN  Reduce  0)])]
  )
  THEN  (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index