---

Step * of Lemma implies-sg-win2

∀g:SimpleGame
  ((∃Good:Pos(g) ⟶ ℙ'
     ∃F:p:{p:Pos(g)| Good[p]}  ⟶ q:{q:Pos(g)| Legal1(p;q)}  ⟶ Pos(g)
      (Good[InitialPos(g)] ∧ (∀p:{p:Pos(g)| Good[p]} . ∀q:{q:Pos(g)| Legal1(p;q)} .  (Good[F[p;q]] ∧ Legal2(q;F[p;q]))))\000C)
  ⇒ win2(g))
BY
{ ((Auto THEN ExRepD)
   THEN (D 0 THENA Auto)
   THEN UseWitness ⌜λmoves.(F moves[||moves|| - 2] moves[||moves|| - 1])⌝⋅
   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@i'
2. Good : Pos(g) ⟶ ℙ'@i 2
3. F : p:{p:Pos(g)| Good[p]}  ⟶ q:{q:Pos(g)| Legal1(p;q)}  ⟶ Pos(g)@i 2
4. Good[InitialPos(g)]
5. ∀p:{p:Pos(g)| Good[p]} . ∀q:{q:Pos(g)| Legal1(p;q)} .  (Good[F[p;q]] ∧ Legal2(q;F[p;q]))
6. n : ℤ
7. 0 < n
8. λmoves.(F moves[||moves|| - 2] moves[||moves|| - 1]) ∈ win2strat(g;n - 1)
9. ¬(n = 0 ∈ ℤ)
10. moves : strat2play(g;n - 1;λmoves.(F moves[||moves|| - 2] moves[||moves|| - 1]))@i
11. ||moves|| = (2 * n) ∈ ℤ
⊢ F moves[(2 * n) - 2] moves[(2 * n) - 1] ∈ {p:Pos(g)| Legal2(moves[(2 * n) - 1];p)} 

---

Latex:

---

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


By

---

Latex:
((Auto  THEN  ExRepD)
  THEN  (D  0  THENA  Auto)
  THEN  UseWitness  \mkleeneopen{}\mlambda{}moves.(F  moves[||moves||  -  2]  moves[||moves||  -  1])\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