---

Step * 2 1 1 2 1 2 2 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)]. ∀[f:strat2play(g;n;s)].  (||f|| ∈ ℤ)
11. ∀[s:win2strat(g;n)]. ∀[f:strat2play(g;n;s)]. ∀[k:{(2 * n) + 2..||f|| + 1-}].
      (seq-truncate(f;k) ∈ strat2play(g;n;s))
⊢ Ax ∈ ∀[s:win2strat(g;n)]. ∀[f:strat2play(g;n;s)]. ∀[k:{(2 * n) + 2..||f|| + 1-}].
         (seq-truncate(f;k) ∈ strat2play(g;n;s))
BY
{ (Unfold `uall` 0 THEN (MemTypeCD THENA Auto) THEN D -4 With ⌜s⌝  THEN Auto) }

---

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.  \mforall{}[s:win2strat(g;n)].  \mforall{}[f:strat2play(g;n;s)].    (||f||  \mmember{}  \mBbbZ{})
11.  \mforall{}[s:win2strat(g;n)].  \mforall{}[f:strat2play(g;n;s)].  \mforall{}[k:\{(2  *  n)  +  2..||f||  +  1\msupminus{}\}].
            (seq-truncate(f;k)  \mmember{}  strat2play(g;n;s))
\mvdash{}  Ax  \mmember{}  \mforall{}[s:win2strat(g;n)].  \mforall{}[f:strat2play(g;n;s)].  \mforall{}[k:\{(2  *  n)  +  2..||f||  +  1\msupminus{}\}].
                  (seq-truncate(f;k)  \mmember{}  strat2play(g;n;s))


By

---

Latex:
(Unfold  `uall`  0  THEN  (MemTypeCD  THENA  Auto)  THEN  D  -4  With  \mkleeneopen{}s\mkleeneclose{}    THEN  Auto)

---

Home Index