---

Step * 1 of Lemma nim-sum-assoc


1. x : ℕ
2. ∀x:ℕx. ∀[y,z:ℕ].  (nim-sum(x;nim-sum(y;z)) = nim-sum(nim-sum(x;y);z) ∈ ℤ)
3. y : ℕ
4. z : ℕ
5. ¬(x = 0 ∈ ℤ)
⊢ nim-sum(x;nim-sum(y;z)) = nim-sum(nim-sum(x;y);z) ∈ ℤ
BY
{ ((InstLemma `div_rem_sum` [⌜x⌝;⌜2⌝]⋅ THENA Auto)
   THEN (InstLemma `rem_bounds_1` [⌜x⌝;⌜2⌝]⋅ THENA Auto)
   THEN (InstHyp [⌜x ÷ 2⌝] 2⋅ THENA Auto)
   THEN (RWO "nim-sum-rec" 0⋅ THEN Auto)
   THEN (RWO "nim-sum-div2 nim-sum-rem2" 0 THENA Auto)
   THEN EqCD
   THEN Auto) }

1
.....subterm..... T:t
2:n
1. x : ℕ
2. ∀x:ℕx. ∀[y,z:ℕ].  (nim-sum(x;nim-sum(y;z)) = nim-sum(nim-sum(x;y);z) ∈ ℤ)
3. y : ℕ
4. z : ℕ
5. ¬(x = 0 ∈ ℤ)
6. x = (((x ÷ 2) * 2) + (x rem 2)) ∈ ℤ
7. 0 ≤ (x rem 2)
8. x rem 2 < 2
9. ∀[y,z:ℕ].  (nim-sum(x ÷ 2;nim-sum(y;z)) = nim-sum(nim-sum(x ÷ 2;y);z) ∈ ℤ)
⊢ if x rem 2=if y rem 2=z rem 2 then 0 else 1 then 0 else 1
= if if x rem 2=y rem 2 then 0 else 1=z rem 2 then 0 else 1
∈ ℤ

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}
2.  \mforall{}x:\mBbbN{}x.  \mforall{}[y,z:\mBbbN{}].    (nim-sum(x;nim-sum(y;z))  =  nim-sum(nim-sum(x;y);z))
3.  y  :  \mBbbN{}
4.  z  :  \mBbbN{}
5.  \mneg{}(x  =  0)
\mvdash{}  nim-sum(x;nim-sum(y;z))  =  nim-sum(nim-sum(x;y);z)


By

---

Latex:
((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  (InstHyp  [\mkleeneopen{}x  \mdiv{}  2\mkleeneclose{}]  2\mcdot{}  THENA  Auto)
  THEN  (RWO  "nim-sum-rec"  0\mcdot{}  THEN  Auto)
  THEN  (RWO  "nim-sum-div2  nim-sum-rem2"  0  THENA  Auto)
  THEN  EqCD
  THEN  Auto)

---

Home Index