---

Step * of Lemma Game-add-Game0

∀G:Game. 0 ⊕ G ≡ G
BY
{ (BLemma `Game-induction`
   THEN Auto
   THEN Unfold `Game-add` 0
   THEN (Subst' left-indices(0) ~ {k:ℤ| 0 ≤ k < 0}  0 THENA Computation)
   THEN (Subst' right-indices(0) ~ {k:ℤ| 0 ≤ k < 0}  0 THENA Computation)
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN RepUR ``left-indices right-indices left-move right-move mkGame Wsup`` 0
   THEN Folds ``left-indices left-move right-indices right-move`` 0
   THEN Auto
   THEN Try ((D -1
              THEN Auto
              THEN Reduce 0
              THEN (D 0 With ⌜y⌝  THEN Auto)
              THEN BackThruSomeHyp
              THEN RepUR ``left-option right-option`` 0
              THEN Auto))) }

1
1. G : Game@i'
2. ∀m:Game. ((left-option{i:l}(G;m) ∨ right-option{i:l}(G;m)) ⇒ 0 ⊕ m ≡ m)
3. i : left-indices(G)@i
⊢ ∃j:{k:ℤ| 0 ≤ k < 0}  + left-indices(G)
   left-move(G;i) ≡ case j of inl(a) => left-move(0;a) ⊕ G | inr(b) => 0 ⊕ left-move(G;b)

2
1. G : Game@i'
2. ∀m:Game. ((left-option{i:l}(G;m) ∨ right-option{i:l}(G;m)) ⇒ 0 ⊕ m ≡ m)
3. i : right-indices(G)@i
⊢ ∃j:{k:ℤ| 0 ≤ k < 0}  + right-indices(G)
   right-move(G;i) ≡ case j of inl(a) => right-move(0;a) ⊕ G | inr(b) => 0 ⊕ right-move(G;b)

---

Latex:

---

Latex:
\mforall{}G:Game.  0  \moplus{}  G  \mequiv{}  G


By

---

Latex:
(BLemma  `Game-induction`
  THEN  Auto
  THEN  Unfold  `Game-add`  0
  THEN  (Subst'  left-indices(0)  \msim{}  \{k:\mBbbZ{}|  0  \mleq{}  k  <  0\}    0  THENA  Computation)
  THEN  (Subst'  right-indices(0)  \msim{}  \{k:\mBbbZ{}|  0  \mleq{}  k  <  0\}    0  THENA  Computation)
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  RepUR  ``left-indices  right-indices  left-move  right-move  mkGame  Wsup``  0
  THEN  Folds  ``left-indices  left-move  right-indices  right-move``  0
  THEN  Auto
  THEN  Try  ((D  -1
                        THEN  Auto
                        THEN  Reduce  0
                        THEN  (D  0  With  \mkleeneopen{}y\mkleeneclose{}    THEN  Auto)
                        THEN  BackThruSomeHyp
                        THEN  RepUR  ``left-option  right-option``  0
                        THEN  Auto)))

---

Home Index