---

Step * 1 of Lemma Game-induction

.....antecedent..... 
1. [P] : Game ⟶ ℙ'
2. ∀g:Game. ((∀m:Game. ((left-option{i:l}(g;m) ∨ right-option{i:l}(g;m)) ⇒ P[m])) ⇒ P[g])
⊢ ∀a:GameA{i:l}(). ∀f:GameB(a) ⟶ Game.  ((∀b:GameB(a). P[f b]) ⇒ P[Wsup(a;f)])
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN (InstLemma `Wsup_wf` [⌜parm{i'}⌝;⌜GameA{i:l}()⌝;⌜λ2LR.GameB(LR)⌝;⌜a⌝;⌜f⌝]⋅ THENA Auto)
   THEN Fold `Game`  (-1)
   THEN Auto
   THEN BHyp 2 
   THEN Auto) }

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. left-option{i:l}(Wsup(a;f);m) ∨ right-option{i:l}(Wsup(a;f);m)
⊢ P[m]

---

Latex:

---

Latex:
.....antecedent..... 
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])
\mvdash{}  \mforall{}a:GameA\{i:l\}().  \mforall{}f:GameB(a)  {}\mrightarrow{}  Game.    ((\mforall{}b:GameB(a).  P[f  b])  {}\mRightarrow{}  P[Wsup(a;f)])


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (InstLemma  `Wsup\_wf`  [\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}GameA\{i:l\}()\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}LR.GameB(LR)\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Fold  `Game`    (-1)
  THEN  Auto
  THEN  BHyp  2 
  THEN  Auto)

---

Home Index