---

Step * of Lemma good-sg-win2

∀g:SimpleGame
  ((∃Good:Pos(g) ⟶ ℙ'
     (Good[InitialPos(g)] ∧ (∀p:Pos(g). ∀q:{q:Pos(g)| Legal1(p;q)} . ∀gd:Good[p].  ∃r:{r:Pos(g)| Legal2(q;r)} . Good[r])\000C))
  ⇒ win2(g))
BY
{ ((Auto THEN ExRepD)
   THEN RenameVar `g0' (-2)⋅
   THEN (Skolemize (-1) `F' THENA Auto)
   THEN RenameVar `G' (-1)
   THEN (D 0 THENA Auto)
   THEN UseWitness ⌜λmoves.(F moves[||moves|| - 2] moves[||moves|| - 1] goodAux(g0;G;moves))⌝⋅
   THEN NatInd (-1)
   THEN Unfold `win2strat` 0
   THEN (SplitOnConclITE THENA Auto)
   THEN Try (Trivial)
   THEN Try ((D -1 THEN Fold `member` 0 THEN Auto))
   THEN DepIsectCD
   THEN Try (Trivial)
   THEN (MemCD THENA Auto)
   THEN D -1
   THEN HypSubst' (-1) 0) }

1
1. g : SimpleGame
2. Good : Pos(g) ⟶ ℙ'
3. g0 : Good[InitialPos(g)]
4. ∀p:Pos(g). ∀q:{q:Pos(g)| Legal1(p;q)} . ∀gd:Good[p].  ∃r:{r:Pos(g)| Legal2(q;r)} . Good[r]
5. F : p:Pos(g) ⟶ q:{q:Pos(g)| Legal1(p;q)}  ⟶ gd:Good[p] ⟶ {r:Pos(g)| Legal2(q;r)} 
6. G : ∀p:Pos(g). ∀q:{q:Pos(g)| Legal1(p;q)} . ∀gd:Good[p].  Good[F p q gd]
7. n : ℤ
8. 0 < n
9. λmoves.(F moves[||moves|| - 2] moves[||moves|| - 1] goodAux(g0;G;moves)) ∈ win2strat(g;n - 1)
10. ¬(n = 0 ∈ ℤ)
11. moves : strat2play(g;n - 1;λmoves.(F moves[||moves|| - 2] moves[||moves|| - 1] goodAux(g0;G;moves)))
12. ||moves|| = (2 * n) ∈ ℤ
⊢ F moves[(2 * n) - 2] moves[(2 * n) - 1] goodAux(g0;G;moves) ∈ {p:Pos(g)| Legal2(moves[(2 * n) - 1];p)} 

---

Latex:

---

Latex:
\mforall{}g:SimpleGame
    ((\mexists{}Good:Pos(g)  {}\mrightarrow{}  \mBbbP{}'
          (Good[InitialPos(g)]
          \mwedge{}  (\mforall{}p:Pos(g).  \mforall{}q:\{q:Pos(g)|  Legal1(p;q)\}  .  \mforall{}gd:Good[p].    \mexists{}r:\{r:Pos(g)|  Legal2(q;r)\}  .  Good[r]))\000C)
    {}\mRightarrow{}  win2(g))


By

---

Latex:
((Auto  THEN  ExRepD)
  THEN  RenameVar  `g0'  (-2)\mcdot{}
  THEN  (Skolemize  (-1)  `F'  THENA  Auto)
  THEN  RenameVar  `G'  (-1)
  THEN  (D  0  THENA  Auto)
  THEN  UseWitness  \mkleeneopen{}\mlambda{}moves.(F  moves[||moves||  -  2]  moves[||moves||  -  1]  goodAux(g0;G;moves))\mkleeneclose{}\mcdot{}
  THEN  NatInd  (-1)
  THEN  Unfold  `win2strat`  0
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  Try  (Trivial)
  THEN  Try  ((D  -1  THEN  Fold  `member`  0  THEN  Auto))
  THEN  DepIsectCD
  THEN  Try  (Trivial)
  THEN  (MemCD  THENA  Auto)
  THEN  D  -1
  THEN  HypSubst'  (-1)  0)

---

Home Index