---

Step * 1 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. x : fst(a)
9. m = (f (inl x)) ∈ Game
⊢ P[m]
BY
{ (InstHyp [⌜inl x⌝] (-4)⋅ THEN Auto) }

---

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.  x  :  fst(a)
9.  m  =  (f  (inl  x))
\mvdash{}  P[m]


By

---

Latex:
(InstHyp  [\mkleeneopen{}inl  x\mkleeneclose{}]  (-4)\mcdot{}  THEN  Auto)

---

Home Index