---

Step * of Lemma nim-sum-rec

∀[x,y:ℕ].  (nim-sum(x;y) ~ (2 * nim-sum(x ÷ 2;y ÷ 2)) + if x rem 2=y rem 2 then 0 else 1)
BY
{ (Intros
   THEN (Assert nim-sum(x;y) = ((2 * nim-sum(x ÷ 2;y ÷ 2)) + if x rem 2=y rem 2 then 0 else 1) ∈ ℤ BY
               ((InstLemma `div_rem_sum` [⌜nim-sum(x;y)⌝;⌜2⌝]⋅ THENA Auto) THEN NthHypEqTrans (-1) THEN EqCD THEN Auto))
   ) }

1
1. [x] : ℕ
2. [y] : ℕ
3. nim-sum(x;y) = ((2 * nim-sum(x ÷ 2;y ÷ 2)) + if x rem 2=y rem 2 then 0 else 1) ∈ ℤ
⊢ nim-sum(x;y) ~ (2 * nim-sum(x ÷ 2;y ÷ 2)) + if x rem 2=y rem 2 then 0 else 1

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbN{}].    (nim-sum(x;y)  \msim{}  (2  *  nim-sum(x  \mdiv{}  2;y  \mdiv{}  2))  +  if  x  rem  2=y  rem  2  then  0  else  1)


By

---

Latex:
(Intros
  THEN  (Assert  nim-sum(x;y)  =  ((2  *  nim-sum(x  \mdiv{}  2;y  \mdiv{}  2))  +  if  x  rem  2=y  rem  2  then  0  else  1)  BY
                          ((InstLemma  `div\_rem\_sum`  [\mkleeneopen{}nim-sum(x;y)\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  NthHypEqTrans  (-1)
                            THEN  EqCD
                            THEN  Auto))
  )

---

Home Index