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