---

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

.....assertion..... 
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
⊢ ∀[s:win2strat(g;n)]. (strat2play(g;n;s) ∈ Type)
BY
{ ((D 0 THENA Auto)
   THEN (Unfold `strat2play` 0 THEN Unfolds ``play-len play-truncate`` 0)
   THEN AutoSplit
   THEN Unfold `win2strat` -1
   THEN SplitOnHypITE -1 
   THEN Auto
   THEN DepIsectHD (-2)
   THEN D 6 With ⌜s⌝ 
   THEN Try (Trivial)
   THEN DepIsectWf
   THEN MemCD
   THEN Try (Trivial)
   THEN Unfold `play-item` 0) }

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)
⊢ {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:
.....assertion..... 
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
\mvdash{}  \mforall{}[s:win2strat(g;n)].  (strat2play(g;n;s)  \mmember{}  Type)


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (Unfold  `strat2play`  0  THEN  Unfolds  ``play-len  play-truncate``  0)
  THEN  AutoSplit
  THEN  Unfold  `win2strat`  -1
  THEN  SplitOnHypITE  -1 
  THEN  Auto
  THEN  DepIsectHD  (-2)
  THEN  D  6  With  \mkleeneopen{}s\mkleeneclose{} 
  THEN  Try  (Trivial)
  THEN  DepIsectWf
  THEN  MemCD
  THEN  Try  (Trivial)
  THEN  Unfold  `play-item`  0)

---

Home Index