---

Step * 1 1 of Lemma nim-sum-assoc

.....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
∈ ℤ
BY
{ ((GenConcl ⌜(x rem 2) = r ∈ ℕ2⌝⋅ THENA Auto)
   THEN IntSegCases (-2)
   THEN ThinVar `r'
   THEN ((GenConcl ⌜(y rem 2) = r ∈ ℕ2⌝⋅ THENA Auto) THEN IntSegCases (-2) THEN ThinVar `r')
   THEN (GenConcl ⌜(z rem 2) = r ∈ ℕ2⌝⋅ THENA Auto)
   THEN IntSegCases (-2)
   THEN ThinVar `r'
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
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)
6.  x  =  (((x  \mdiv{}  2)  *  2)  +  (x  rem  2))
7.  0  \mleq{}  (x  rem  2)
8.  x  rem  2  <  2
9.  \mforall{}[y,z:\mBbbN{}].    (nim-sum(x  \mdiv{}  2;nim-sum(y;z))  =  nim-sum(nim-sum(x  \mdiv{}  2;y);z))
\mvdash{}  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


By

---

Latex:
((GenConcl  \mkleeneopen{}(x  rem  2)  =  r\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  IntSegCases  (-2)
  THEN  ThinVar  `r'
  THEN  ((GenConcl  \mkleeneopen{}(y  rem  2)  =  r\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  IntSegCases  (-2)  THEN  ThinVar  `r')
  THEN  (GenConcl  \mkleeneopen{}(z  rem  2)  =  r\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  IntSegCases  (-2)
  THEN  ThinVar  `r'
  THEN  Reduce  0
  THEN  Auto)

---

Home Index