---

Step * of Lemma nim-sum-rem2

No Annotations
∀[x,y:ℕ].  (nim-sum(x;y) rem 2 ~ if x rem 2=y rem 2 then 0 else 1)
BY
{ (CompleteInductionOnNat
   THEN (D 0 THENA Auto)
   THEN (CaseNat 0 `x'
         THENL [Reduce 0
               ; (((InstLemma `div_rem_sum` [⌜x⌝;⌜2⌝]⋅ THENA Auto)
                   THEN (InstLemma `rem_bounds_1` [⌜x⌝;⌜2⌝]⋅ THENA Auto)
                   )
                  THEN (CaseNat 0 `y'
                        THENL [Reduce 0
                              ; (RW (AddrC [1] (UnfoldC `nim-sum`)) 0
                                 THEN Reduce 0
                                 THEN (InstHyp [⌜x ÷ 2⌝;⌜y ÷ 2⌝] 2⋅ THENA Auto)
                                 THEN Repeat ((CallByValueReduce 0⋅ THENA Auto))
                                 THEN Auto)]
                       )
                  )]
   )) }

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

2
1. x : ℕ
2. ∀x:ℕx. ∀[y:ℕ]. (nim-sum(x;y) rem 2 ~ if x rem 2=y rem 2 then 0 else 1)
3. y : ℕ
4. ¬(x = 0 ∈ ℤ)
5. x = (((x ÷ 2) * 2) + (x rem 2)) ∈ ℤ
6. (0 ≤ (x rem 2)) ∧ x rem 2 < 2
7. y = 0 ∈ ℤ
⊢ nim-sum(x;0) rem 2 ~ if x rem 2=0 then 0 else 1

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

---

Latex:

---

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


By

---

Latex:
(CompleteInductionOnNat
  THEN  (D  0  THENA  Auto)
  THEN  (CaseNat  0  `x'
              THENL  [Reduce  0
                          ;  (((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  (CaseNat  0  `y'
                                            THENL  [Reduce  0
                                                        ;  (RW  (AddrC  [1]  (UnfoldC  `nim-sum`))  0
                                                              THEN  Reduce  0
                                                              THEN  (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