---

Step * 1 1 of Lemma Game-induction


1. [P] : Game ⟶ ℙ'
2. ∀g:Game. ((∀m:Game. ((left-option{i:l}(g;m) ∨ right-option{i:l}(g;m)) ⇒ P[m])) ⇒ P[g])
3. a : GameA{i:l}()
4. f : GameB(a) ⟶ Game
5. Wsup(a;f) ∈ Game
6. ∀b:GameB(a). P[f b]
7. m : Game
8. left-option{i:l}(Wsup(a;f);m) ∨ right-option{i:l}(Wsup(a;f);m)
⊢ P[m]
BY
{ ((D -1
    THENL [RepUR ``Wsup left-option left-indices left-move`` -1
          ; RepUR ``Wsup right-option right-indices right-move`` -1]
   )
   THEN ExRepD
   ) }

1
1. [P] : Game ⟶ ℙ'
2. ∀g:Game. ((∀m:Game. ((left-option{i:l}(g;m) ∨ right-option{i:l}(g;m)) ⇒ P[m])) ⇒ P[g])
3. a : GameA{i:l}()
4. f : GameB(a) ⟶ Game
5. Wsup(a;f) ∈ Game
6. ∀b:GameB(a). P[f b]
7. m : Game
8. x : fst(a)
9. m = (f (inl x)) ∈ Game
⊢ P[m]

2
1. [P] : Game ⟶ ℙ'
2. ∀g:Game. ((∀m:Game. ((left-option{i:l}(g;m) ∨ right-option{i:l}(g;m)) ⇒ P[m])) ⇒ P[g])
3. a : GameA{i:l}()
4. f : GameB(a) ⟶ Game
5. Wsup(a;f) ∈ Game
6. ∀b:GameB(a). P[f b]
7. m : Game
8. x : snd(a)
9. m = (f (inr x )) ∈ Game
⊢ P[m]

---

Latex:

---

Latex:

1.  [P]  :  Game  {}\mrightarrow{}  \mBbbP{}'
2.  \mforall{}g:Game.  ((\mforall{}m:Game.  ((left-option\{i:l\}(g;m)  \mvee{}  right-option\{i:l\}(g;m))  {}\mRightarrow{}  P[m]))  {}\mRightarrow{}  P[g])
3.  a  :  GameA\{i:l\}()
4.  f  :  GameB(a)  {}\mrightarrow{}  Game
5.  Wsup(a;f)  \mmember{}  Game
6.  \mforall{}b:GameB(a).  P[f  b]
7.  m  :  Game
8.  left-option\{i:l\}(Wsup(a;f);m)  \mvee{}  right-option\{i:l\}(Wsup(a;f);m)
\mvdash{}  P[m]


By

---

Latex:
((D  -1
    THENL  [RepUR  ``Wsup  left-option  left-indices  left-move``  -1
                ;  RepUR  ``Wsup  right-option  right-indices  right-move``  -1]
  )
  THEN  ExRepD
  )

---

Home Index