Step
*
3
2
1
2
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||
22. Legal1(x[2 * n];x[(2 * n) + 1])
23. play-truncate(moves;2 * n) ∈ {moves:strat2play(g;n - 1;s)| ||moves|| = (2 * n) ∈ ℤ} 
24. seq-truncate(x;2 * n) ∈ strat2play(g;n - 1;s)
25. play-truncate(x;2 * n) = play-truncate(moves;2 * n) ∈ strat2play(g;n - 1;s)
⊢ (s play-truncate(x;2 * n)) = (s play-truncate(moves;2 * n)) ∈ Pos(g)
BY
{ (Assert s ∈ moves:{f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(g)| Legal2(moves[(2 * n) - 1];p)}  BY
         (Unfold `win2strat` 5
          THEN (SplitOnHypITE 5  THENA Auto)
          THEN Try ((Assert ⌜False⌝⋅ THEN Complete (Auto)))
          THEN DepIsectHD 5
          THEN Auto)) }
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)
21. ((2 * n) + 2) ≤ ||x||
22. Legal1(x[2 * n];x[(2 * n) + 1])
23. play-truncate(moves;2 * n) ∈ {moves:strat2play(g;n - 1;s)| ||moves|| = (2 * n) ∈ ℤ} 
24. seq-truncate(x;2 * n) ∈ strat2play(g;n - 1;s)
25. play-truncate(x;2 * n) = play-truncate(moves;2 * n) ∈ strat2play(g;n - 1;s)
26. s ∈ moves:{f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(g)| Legal2(moves[(2 * n) - 1];p)} 
⊢ (s play-truncate(x;2 * n)) = (s play-truncate(moves;2 * n)) ∈ Pos(g)
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||
22.  Legal1(x[2  *  n];x[(2  *  n)  +  1])
23.  play-truncate(moves;2  *  n)  \mmember{}  \{moves:strat2play(g;n  -  1;s)|  ||moves||  =  (2  *  n)\} 
24.  seq-truncate(x;2  *  n)  \mmember{}  strat2play(g;n  -  1;s)
25.  play-truncate(x;2  *  n)  =  play-truncate(moves;2  *  n)
\mvdash{}  (s  play-truncate(x;2  *  n))  =  (s  play-truncate(moves;2  *  n))
By
Latex:
(Assert  s  \mmember{}  moves:\{f:strat2play(g;n  -  1;s)|  ||f||  =  (2  *  n)\}    {}\mrightarrow{}  \{p:Pos(g)|  Legal2(moves[(2  *  n)  -  1\000C];p)\}    BY
              (Unfold  `win2strat`  5
                THEN  (SplitOnHypITE  5    THENA  Auto)
                THEN  Try  ((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Complete  (Auto)))
                THEN  DepIsectHD  5
                THEN  Auto))
Home
Index