---

Step * of Lemma Game-induction

∀[P:Game ⟶ ℙ']
  ((∀g:Game. ((∀m:Game. ((left-option{i:l}(g;m) ∨ right-option{i:l}(g;m)) ⇒ P[m])) ⇒ P[g])) ⇒ {∀g:Game. P[g]})
BY
{ (Unfold `guard` 0
   THEN Auto
   THEN MoveToConcl  (-1)
   THEN (InstLemma `W-induction` [⌜parm{i'}⌝;⌜GameA{i:l}()⌝;⌜λ2LR.GameB(LR)⌝]⋅ THENA Auto)
   THEN Fold `Game` (-1)
   THEN (D -1 With ⌜P⌝  THENA Auto)
   THEN (D -1 THENM Trivial)) }

1
.....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)])

---

Latex:

---

Latex:
\mforall{}[P:Game  {}\mrightarrow{}  \mBbbP{}']
    ((\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]))
    {}\mRightarrow{}  \{\mforall{}g:Game.  P[g]\})


By

---

Latex:
(Unfold  `guard`  0
  THEN  Auto
  THEN  MoveToConcl    (-1)
  THEN  (InstLemma  `W-induction`  [\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}GameA\{i:l\}()\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}LR.GameB(LR)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Fold  `Game`  (-1)
  THEN  (D  -1  With  \mkleeneopen{}P\mkleeneclose{}    THENA  Auto)
  THEN  (D  -1  THENM  Trivial))

---

Home Index