---

Step * 2 1 1 2 1 2 1 1 of Lemma win2strat-strat2play-wf


1. g : SimpleGame
2. n : ℤ
3. 0 < n
4. win2strat(g;n - 1) ∈ Type
5. ∀[s:win2strat(g;n - 1)]. (strat2play(g;n - 1;s) ∈ Type)
6. ∀[s:win2strat(g;n - 1)]. ∀[f:strat2play(g;n - 1;s)].  (||f|| ∈ ℤ)
7. ∀[s:win2strat(g;n - 1)]. ∀[f:strat2play(g;n - 1;s)]. ∀[k:{(2 * (n - 1)) + 2..||f|| + 1-}].
     (seq-truncate(f;k) ∈ strat2play(g;n - 1;s))
8. win2strat(g;n) ∈ Type
9. ∀[s:win2strat(g;n)]. (strat2play(g;n;s) ∈ Type)
10. s : win2strat(g;n)
11. strat2play(g;n;s) ∈ Type
12. ∀[f:strat2play(g;n;s)]. (||f|| ∈ ℤ)
13. f : strat2play(g;n;s)
14. k : {(2 * n) + 2..||f|| + 1-}
⊢ seq-truncate(f;k) ∈ strat2play(g;n;s)
BY
{ ((Assert s ∈ win2strat(g;n) BY
          Declaration)
   THEN (Unfold `win2strat` 10 THEN (SplitOnHypITE 10  THENA Auto))
   THEN (DepIsectHD 10 ORELSE Auto)
   THEN (Assert f ∈ strat2play(g;n;s) BY
               Declaration)
   THEN Unfold `strat2play` -5
   THEN (SplitOnHypITE -5  THENA Auto)
   THEN ((DepIsectHD (-6) THEN MemTypeHD (-6) THEN Auto) ORELSE Auto)
   THEN Unfold `strat2play` 0
   THEN (SplitOnConclITE THENA Auto)
   THEN (DepIsectCD ORELSE Auto)) }

1
1. g : SimpleGame
2. n : ℤ
3. 0 < n
4. win2strat(g;n - 1) ∈ Type
5. ∀[s:win2strat(g;n - 1)]. (strat2play(g;n - 1;s) ∈ Type)
6. ∀[s:win2strat(g;n - 1)]. ∀[f:strat2play(g;n - 1;s)].  (||f|| ∈ ℤ)
7. ∀[s:win2strat(g;n - 1)]. ∀[f:strat2play(g;n - 1;s)]. ∀[k:{(2 * (n - 1)) + 2..||f|| + 1-}].
     (seq-truncate(f;k) ∈ strat2play(g;n - 1;s))
8. win2strat(g;n) ∈ Type
9. ∀[s:win2strat(g;n)]. (strat2play(g;n;s) ∈ Type)
10. s : s:win2strat(g;n - 1) ⋂ moves:{f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(g)| Legal2(moves[(2 * n) \000C- 1];p)} 
11. s ∈ win2strat(g;n - 1)
12. s ∈ moves:{f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(g)| Legal2(moves[(2 * n) - 1];p)} 
13. strat2play(g;n;s) ∈ Type
14. ∀[f:strat2play(g;n;s)]. (||f|| ∈ ℤ)
15. f : 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))} 
16. f ∈ strat2play(g;n - 1;s)
17. f = f ∈ sequence(Pos(g))
18. ((2 * n) + 2) ≤ ||f||
19. Legal1(f[2 * n];f[(2 * n) + 1])
20. f[2 * n] = (s play-truncate(f;2 * n)) ∈ Pos(g)
21. k : {(2 * n) + 2..||f|| + 1-}
22. s ∈ win2strat(g;n)
23. ¬(n = 0 ∈ ℤ)
24. f ∈ strat2play(g;n;s)
25. ¬(n = 0 ∈ ℤ)
26. ¬(n = 0 ∈ ℤ)
⊢ seq-truncate(f;k) ∈ strat2play(g;n - 1;s)

2
1. g : SimpleGame
2. n : ℤ
3. 0 < n
4. win2strat(g;n - 1) ∈ Type
5. ∀[s:win2strat(g;n - 1)]. (strat2play(g;n - 1;s) ∈ Type)
6. ∀[s:win2strat(g;n - 1)]. ∀[f:strat2play(g;n - 1;s)].  (||f|| ∈ ℤ)
7. ∀[s:win2strat(g;n - 1)]. ∀[f:strat2play(g;n - 1;s)]. ∀[k:{(2 * (n - 1)) + 2..||f|| + 1-}].
     (seq-truncate(f;k) ∈ strat2play(g;n - 1;s))
8. win2strat(g;n) ∈ Type
9. ∀[s:win2strat(g;n)]. (strat2play(g;n;s) ∈ Type)
10. s : s:win2strat(g;n - 1) ⋂ moves:{f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(g)| Legal2(moves[(2 * n) \000C- 1];p)} 
11. s ∈ win2strat(g;n - 1)
12. s ∈ moves:{f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(g)| Legal2(moves[(2 * n) - 1];p)} 
13. strat2play(g;n;s) ∈ Type
14. ∀[f:strat2play(g;n;s)]. (||f|| ∈ ℤ)
15. f : 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))} 
16. f ∈ strat2play(g;n - 1;s)
17. f = f ∈ sequence(Pos(g))
18. ((2 * n) + 2) ≤ ||f||
19. Legal1(f[2 * n];f[(2 * n) + 1])
20. f[2 * n] = (s play-truncate(f;2 * n)) ∈ Pos(g)
21. k : {(2 * n) + 2..||f|| + 1-}
22. s ∈ win2strat(g;n)
23. ¬(n = 0 ∈ ℤ)
24. f ∈ strat2play(g;n;s)
25. ¬(n = 0 ∈ ℤ)
26. ¬(n = 0 ∈ ℤ)
⊢ seq-truncate(f;k) ∈ {moves:sequence(Pos(g))| 
                       (((2 * n) + 2) ≤ ||moves||)
                       ∧ Legal1(moves[2 * n];moves[(2 * n) + 1])
                       ∧ (moves[2 * n] = (s play-truncate(seq-truncate(f;k);2 * n)) ∈ Pos(g))} 

---

Latex:

---

Latex:

1.  g  :  SimpleGame
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  win2strat(g;n  -  1)  \mmember{}  Type
5.  \mforall{}[s:win2strat(g;n  -  1)].  (strat2play(g;n  -  1;s)  \mmember{}  Type)
6.  \mforall{}[s:win2strat(g;n  -  1)].  \mforall{}[f:strat2play(g;n  -  1;s)].    (||f||  \mmember{}  \mBbbZ{})
7.  \mforall{}[s:win2strat(g;n  -  1)].  \mforall{}[f:strat2play(g;n  -  1;s)].  \mforall{}[k:\{(2  *  (n  -  1))  +  2..||f||  +  1\msupminus{}\}].
          (seq-truncate(f;k)  \mmember{}  strat2play(g;n  -  1;s))
8.  win2strat(g;n)  \mmember{}  Type
9.  \mforall{}[s:win2strat(g;n)].  (strat2play(g;n;s)  \mmember{}  Type)
10.  s  :  win2strat(g;n)
11.  strat2play(g;n;s)  \mmember{}  Type
12.  \mforall{}[f:strat2play(g;n;s)].  (||f||  \mmember{}  \mBbbZ{})
13.  f  :  strat2play(g;n;s)
14.  k  :  \{(2  *  n)  +  2..||f||  +  1\msupminus{}\}
\mvdash{}  seq-truncate(f;k)  \mmember{}  strat2play(g;n;s)


By

---

Latex:
((Assert  s  \mmember{}  win2strat(g;n)  BY
                Declaration)
  THEN  (Unfold  `win2strat`  10  THEN  (SplitOnHypITE  10    THENA  Auto))
  THEN  (DepIsectHD  10  ORELSE  Auto)
  THEN  (Assert  f  \mmember{}  strat2play(g;n;s)  BY
                          Declaration)
  THEN  Unfold  `strat2play`  -5
  THEN  (SplitOnHypITE  -5    THENA  Auto)
  THEN  ((DepIsectHD  (-6)  THEN  MemTypeHD  (-6)  THEN  Auto)  ORELSE  Auto)
  THEN  Unfold  `strat2play`  0
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  (DepIsectCD  ORELSE  Auto))

---

Home Index