---

Step * 3 1 of Lemma strat2play-longer


1. g : SimpleGame
2. n : ℤ
3. 0 < n
4. ∀[s:win2strat(g;n - 1)]. ∀[moves:strat2play(g;n - 1;s)]. ∀[x:sequence(Pos(g))].
     ((x ∈ strat2play(g;n - 1;s)) ∧ (seq-truncate(x;||moves||) = moves ∈ strat2play(g;n - 1;s))) supposing 
        ((seq-truncate(x;||moves||) = moves ∈ sequence(Pos(g))) and 
        (||moves|| ≤ ||x||))
5. s : win2strat(g;n)
6. moves : f:strat2play(g;n - 1;s) ⋂ {moves:sequence(Pos(g))| 
                                      (((2 * n) + 2) ≤ ||moves||)
                                      ∧ Legal1(moves[2 * n];moves[(2 * n) + 1])
                                      ∧ (moves[2 * n] = (s play-truncate(f;2 * n)) ∈ Pos(g))} 
7. moves ∈ strat2play(g;n - 1;s)
8. moves ∈ sequence(Pos(g))
9. ((2 * n) + 2) ≤ ||moves||
10. Legal1(moves[2 * n];moves[(2 * n) + 1])
11. moves[2 * n] = (s play-truncate(moves;2 * n)) ∈ Pos(g)
12. x : sequence(Pos(g))
13. moves ∈ {moves:sequence(Pos(g))| ((2 * n) + 2) ≤ ||moves||} 
14. ||moves|| ≤ ||x||
15. seq-truncate(x;||moves||) = moves ∈ sequence(Pos(g))
16. ∀i:ℕ||moves||. (x[i] = moves[i] ∈ Pos(g))
17. ¬(n = 0 ∈ ℤ)
18. ¬(n = 0 ∈ ℤ)
19. x ∈ strat2play(g;n - 1;s)
20. seq-truncate(x;||moves||) = moves ∈ strat2play(g;n - 1;s)
21. ((2 * n) + 2) ≤ ||x||
⊢ Legal1(x[2 * n];x[(2 * n) + 1])
BY
{ (RWO "16" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  SimpleGame
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  \mforall{}[s:win2strat(g;n  -  1)].  \mforall{}[moves:strat2play(g;n  -  1;s)].  \mforall{}[x:sequence(Pos(g))].
          ((x  \mmember{}  strat2play(g;n  -  1;s))  \mwedge{}  (seq-truncate(x;||moves||)  =  moves))  supposing 
                ((seq-truncate(x;||moves||)  =  moves)  and 
                (||moves||  \mleq{}  ||x||))
5.  s  :  win2strat(g;n)
6.  moves  :  f:strat2play(g;n  -  1;s)  \mcap{}  \{moves:sequence(Pos(g))| 
                                                                            (((2  *  n)  +  2)  \mleq{}  ||moves||)
                                                                            \mwedge{}  Legal1(moves[2  *  n];moves[(2  *  n)  +  1])
                                                                            \mwedge{}  (moves[2  *  n]  =  (s  play-truncate(f;2  *  n)))\} 
7.  moves  \mmember{}  strat2play(g;n  -  1;s)
8.  moves  \mmember{}  sequence(Pos(g))
9.  ((2  *  n)  +  2)  \mleq{}  ||moves||
10.  Legal1(moves[2  *  n];moves[(2  *  n)  +  1])
11.  moves[2  *  n]  =  (s  play-truncate(moves;2  *  n))
12.  x  :  sequence(Pos(g))
13.  moves  \mmember{}  \{moves:sequence(Pos(g))|  ((2  *  n)  +  2)  \mleq{}  ||moves||\} 
14.  ||moves||  \mleq{}  ||x||
15.  seq-truncate(x;||moves||)  =  moves
16.  \mforall{}i:\mBbbN{}||moves||.  (x[i]  =  moves[i])
17.  \mneg{}(n  =  0)
18.  \mneg{}(n  =  0)
19.  x  \mmember{}  strat2play(g;n  -  1;s)
20.  seq-truncate(x;||moves||)  =  moves
21.  ((2  *  n)  +  2)  \mleq{}  ||x||
\mvdash{}  Legal1(x[2  *  n];x[(2  *  n)  +  1])


By

---

Latex:
(RWO  "16"  0  THEN  Auto)

---

Home Index