---

Step * 4 1 1 of Lemma strat2play-longer

.....assertion..... 
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)
⊢ (s play-truncate(seq-truncate(x;||moves||);2 * n)) = (s play-truncate(moves;2 * n)) ∈ Pos(g)
BY
{ (Unfold `play-truncate` 0 THEN (RWO "seq-truncate-truncate" 0 THENA Auto) THEN Fold `play-truncate` 0) }

1
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)
⊢ (s play-truncate(x;2 * n)) = (s play-truncate(moves;2 * n)) ∈ Pos(g)

---

Latex:

---

Latex:
.....assertion..... 
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
\mvdash{}  (s  play-truncate(seq-truncate(x;||moves||);2  *  n))  =  (s  play-truncate(moves;2  *  n))


By

---

Latex:
(Unfold  `play-truncate`  0
  THEN  (RWO  "seq-truncate-truncate"  0  THENA  Auto)
  THEN  Fold  `play-truncate`  0)

---

Home Index