---

Step * 1 1 2 1 1 3 2 1 1 of Lemma respond-implies-win2


1. g : SimpleGame
2. m : p:{p:Pos(g)| Legal1(InitialPos(g);p)}  ⟶ {q:Pos(g)| Legal2(p;q)} 
3. s : ∀p:{p:Pos(g)| Legal1(InitialPos(g);p)} . ∀[n:ℕ]. win2strat(g@m p;n)
4. n : ℤ
5. 0 < n
6. λmoves.if (||moves|| =z 2) then m moves[1] else s moves[1] seq-tl(seq-tl(moves)) fi  ∈ win2strat(g;n - 1)
7. ¬(n = 0 ∈ ℤ)
8. moves : strat2play(g;n - 1;λmoves.if (||moves|| =z 2) then m moves[1] else s moves[1] seq-tl(seq-tl(moves)) fi )
9. ||moves|| = (2 * n) ∈ ℤ
10. moves[1] ∈ {p:Pos(g)| Legal1(InitialPos(g);p)} 
11. 2 ≤ n
12. 4 ≤ (2 * n)
13. s moves[1] ∈ win2strat(g@m moves[1];n - 1 - 1)
14. s moves[1] ∈ moves@0:{f:strat2play(g@m moves[1];n - 1 - 1;s moves[1])| ||f|| = (2 * (n - 1)) ∈ ℤ}  ⟶ {p:Pos(g@m mov\000Ces[1])| 
                                                                                     Legal2(moves@0[(2 * (n - 1)) 
                                                                                     - 1];p)} 
15. seq-tl(seq-tl(moves)) ∈ {f:strat2play(g@m moves[1];n - 1 - 1;s moves[1])| ||f|| = (2 * (n - 1)) ∈ ℤ} 
16. (s moves[1] seq-tl(seq-tl(moves)))
= (s moves[1] seq-tl(seq-tl(moves)))
∈ {p:Pos(g@m moves[1])| Legal2(seq-tl(seq-tl(moves))[(2 * (n - 1)) - 1];p)} 
17. x : Pos(g@m moves[1])
18. Legal2(seq-tl(seq-tl(moves))[(2 * (n - 1)) - 1];x)
⊢ x ∈ Pos(g)
BY
{ All Thin }

1
1. g : SimpleGame
2. m : p:{p:Pos(g)| Legal1(InitialPos(g);p)}  ⟶ {q:Pos(g)| Legal2(p;q)} 
3. s : ∀p:{p:Pos(g)| Legal1(InitialPos(g);p)} . ∀[n:ℕ]. win2strat(g@m p;n)
4. n : ℤ
5. moves : strat2play(g;n - 1;λmoves.if (||moves|| =z 2) then m moves[1] else s moves[1] seq-tl(seq-tl(moves)) fi )
6. x : Pos(g@m moves[1])
⊢ x ∈ Pos(g)

---

Latex:

---

Latex:

1.  g  :  SimpleGame
2.  m  :  p:\{p:Pos(g)|  Legal1(InitialPos(g);p)\}    {}\mrightarrow{}  \{q:Pos(g)|  Legal2(p;q)\} 
3.  s  :  \mforall{}p:\{p:Pos(g)|  Legal1(InitialPos(g);p)\}  .  \mforall{}[n:\mBbbN{}].  win2strat(g@m  p;n)
4.  n  :  \mBbbZ{}
5.  0  <  n
6.  \mlambda{}moves.if  (||moves||  =\msubz{}  2)  then  m  moves[1]  else  s  moves[1]  seq-tl(seq-tl(moves))  fi 
      \mmember{}  win2strat(g;n  -  1)
7.  \mneg{}(n  =  0)
8.  moves  :  strat2play(g;n  -  1;\mlambda{}moves.if  (||moves||  =\msubz{}  2)
                                                                          then  m  moves[1]
                                                                          else  s  moves[1]  seq-tl(seq-tl(moves))
                                                                          fi  )
9.  ||moves||  =  (2  *  n)
10.  moves[1]  \mmember{}  \{p:Pos(g)|  Legal1(InitialPos(g);p)\} 
11.  2  \mleq{}  n
12.  4  \mleq{}  (2  *  n)
13.  s  moves[1]  \mmember{}  win2strat(g@m  moves[1];n  -  1  -  1)
14.  s  moves[1]  \mmember{}  moves@0:\{f:strat2play(g@m  moves[1];n  -  1  -  1;s  moves[1])|  ||f||  =  (2  *  (n  -  1))\} 
        {}\mrightarrow{}  \{p:Pos(g@m  moves[1])|  Legal2(moves@0[(2  *  (n  -  1))  -  1];p)\} 
15.  seq-tl(seq-tl(moves))  \mmember{}  \{f:strat2play(g@m  moves[1];n  -  1  -  1;s  moves[1])| 
                                                          ||f||  =  (2  *  (n  -  1))\} 
16.  (s  moves[1]  seq-tl(seq-tl(moves)))  =  (s  moves[1]  seq-tl(seq-tl(moves)))
17.  x  :  Pos(g@m  moves[1])
18.  Legal2(seq-tl(seq-tl(moves))[(2  *  (n  -  1))  -  1];x)
\mvdash{}  x  \mmember{}  Pos(g)


By

---

Latex:
All  Thin

---

Home Index