---

Step * 2 of Lemma Game-add-Game0


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)
BY
{ ((D 0 With ⌜inr i ⌝  THEN Auto)
   THEN Reduce 0
   THEN BLemma `eq-Game_inversion`
   THEN Auto
   THEN BackThruSomeHyp
   THEN RepUR ``left-option right-option`` 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  G  :  Game@i'
2.  \mforall{}m:Game.  ((left-option\{i:l\}(G;m)  \mvee{}  right-option\{i:l\}(G;m))  {}\mRightarrow{}  0  \moplus{}  m  \mequiv{}  m)
3.  i  :  right-indices(G)@i
\mvdash{}  \mexists{}j:\{k:\mBbbZ{}|  0  \mleq{}  k  <  0\}    +  right-indices(G)
      right-move(G;i)  \mequiv{}  case  j  of  inl(a)  =>  right-move(0;a)  \moplus{}  G  |  inr(b)  =>  0  \moplus{}  right-move(G;b)


By

---

Latex:
((D  0  With  \mkleeneopen{}inr  i  \mkleeneclose{}    THEN  Auto)
  THEN  Reduce  0
  THEN  BLemma  `eq-Game\_inversion`
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  RepUR  ``left-option  right-option``  0
  THEN  Auto)

---

Home Index