---

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


1. g : SimpleGame
2. n : ℤ
3. n ≠ 0
4. 0 < n
5. win2strat(g;n - 1) ∈ 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 : 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)} 
10. s ∈ win2strat(g;n - 1)
11. s ∈ moves:{f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(g)| Legal2(moves[(2 * n) - 1];p)} 
12. ¬(n = 0 ∈ ℤ)
13. strat2play(g;n - 1;s) ∈ Type
14. f : strat2play(g;n - 1;s)
15. f ∈ {moves:sequence(Pos(g))| (2 * n) ≤ ||moves||} 
⊢ {moves:sequence(Pos(g))| 
   (((2 * n) + 2) ≤ ||moves||)
   ∧ Legal1(moves[2 * n];moves[(2 * n) + 1])
   ∧ (moves[2 * n] = (s seq-truncate(f;2 * n)) ∈ Pos(g))}  ∈ Type
BY
{ (All (Unfolds ``play-len play-truncate``)
   THEN (Assert ||f|| ∈ ℤ BY
               Auto)
   THEN (Assert seq-truncate(f;2 * n) ∈ {f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ}  BY
               ((MemTypeCD THEN Auto) THEN (MemTypeHD (-2) THENA Auto) THEN BackThruSomeHyp))) }

1
1. g : SimpleGame
2. n : ℤ
3. n ≠ 0
4. 0 < n
5. win2strat(g;n - 1) ∈ 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 : 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)} 
10. s ∈ win2strat(g;n - 1)
11. s ∈ moves:{f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(g)| Legal2(moves[(2 * n) - 1];p)} 
12. ¬(n = 0 ∈ ℤ)
13. strat2play(g;n - 1;s) ∈ Type
14. f : strat2play(g;n - 1;s)
15. f ∈ {moves:sequence(Pos(g))| (2 * n) ≤ ||moves||} 
16. ||f|| ∈ ℤ
17. seq-truncate(f;2 * n) ∈ {f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ} 
⊢ {moves:sequence(Pos(g))| 
   (((2 * n) + 2) ≤ ||moves||)
   ∧ Legal1(moves[2 * n];moves[(2 * n) + 1])
   ∧ (moves[2 * n] = (s seq-truncate(f;2 * n)) ∈ Pos(g))}  ∈ Type

---

Latex:

---

Latex:

1.  g  :  SimpleGame
2.  n  :  \mBbbZ{}
3.  n  \mneq{}  0
4.  0  <  n
5.  win2strat(g;n  -  1)  \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.  s  :  s:win2strat(g;n  -  1)  \mcap{}  moves:\{f:strat2play(g;n  -  1;s)|  ||f||  =  (2  *  n)\}    {}\mrightarrow{}  \{p:Pos(g)|  Legal2\000C(moves[(2  *  n)  -  1];p)\} 
10.  s  \mmember{}  win2strat(g;n  -  1)
11.  s  \mmember{}  moves:\{f:strat2play(g;n  -  1;s)|  ||f||  =  (2  *  n)\}    {}\mrightarrow{}  \{p:Pos(g)|  Legal2(moves[(2  *  n)  -  1];p)\000C\} 
12.  \mneg{}(n  =  0)
13.  strat2play(g;n  -  1;s)  \mmember{}  Type
14.  f  :  strat2play(g;n  -  1;s)
15.  f  \mmember{}  \{moves:sequence(Pos(g))|  (2  *  n)  \mleq{}  ||moves||\} 
\mvdash{}  \{moves:sequence(Pos(g))| 
      (((2  *  n)  +  2)  \mleq{}  ||moves||)
      \mwedge{}  Legal1(moves[2  *  n];moves[(2  *  n)  +  1])
      \mwedge{}  (moves[2  *  n]  =  (s  seq-truncate(f;2  *  n)))\}    \mmember{}  Type


By

---

Latex:
(All  (Unfolds  ``play-len  play-truncate``)
  THEN  (Assert  ||f||  \mmember{}  \mBbbZ{}  BY
                          Auto)
  THEN  (Assert  seq-truncate(f;2  *  n)  \mmember{}  \{f:strat2play(g;n  -  1;s)|  ||f||  =  (2  *  n)\}    BY
                          ((MemTypeCD  THEN  Auto)  THEN  (MemTypeHD  (-2)  THENA  Auto)  THEN  BackThruSomeHyp)))

---

Home Index