---

Step * of Lemma nim-sum-div2

No Annotations
∀[x,y:ℕ].  (nim-sum(x;y) ÷ 2 ~ nim-sum(x ÷ 2;y ÷ 2))
BY
{ (CompleteInductionOnNat
   THEN (D 0 THENA Auto)
   THEN (CaseNat 0 `x'
         THENL [(Computation THEN Auto)
               ; (CaseNat 0 `y'
                  THENL [(Unfold `nim-sum` 0 THEN Reduce 0 THEN GenConclTerm ⌜x ÷ 2⌝⋅ THEN Auto)
                        ; (RW (AddrC [1] (UnfoldC `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 (InstHyp [⌜x ÷ 2⌝;⌜y ÷ 2⌝] 2⋅ THENA Auto)
   THEN Repeat ((CallByValueReduce 0⋅ THENA Auto))
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[x,y:\mBbbN{}].    (nim-sum(x;y)  \mdiv{}  2  \msim{}  nim-sum(x  \mdiv{}  2;y  \mdiv{}  2))


By

---

Latex:
(CompleteInductionOnNat
  THEN  (D  0  THENA  Auto)
  THEN  (CaseNat  0  `x'
              THENL  [(Computation  THEN  Auto)
                          ;  (CaseNat  0  `y'
                                THENL  [(Unfold  `nim-sum`  0  THEN  Reduce  0  THEN  GenConclTerm  \mkleeneopen{}x  \mdiv{}  2\mkleeneclose{}\mcdot{}  THEN  Auto)
                                            ;  (RW  (AddrC  [1]  (UnfoldC  `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  (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