---

Step * of Lemma win2strat-strat2play-wf

∀[g:SimpleGame]. ∀[n:ℕ].
  ((win2strat(g;n) ∈ Type)
  ∧ (∀[s:win2strat(g;n)]. (strat2play(g;n;s) ∈ Type))
  ∧ (∀[s:win2strat(g;n)]. ∀[f:strat2play(g;n;s)].  (||f|| ∈ ℤ))
  ∧ (∀[s:win2strat(g;n)]. ∀[f:strat2play(g;n;s)]. ∀[k:{(2 * n) + 2..||f|| + 1-}].
       (play-truncate(f;k) ∈ strat2play(g;n;s))))
BY
{ (Unfolds ``play-len play-truncate`` 0 THEN RepeatFor 2 (Intro) THEN UseWitness ⌜<Ax, Ax, Ax, Ax>⌝⋅ THEN NatInd (-1)) }

1
.....basecase..... 
1. g : SimpleGame
2. n : ℤ
⊢ <Ax, Ax, Ax, Ax> ∈ (win2strat(g;0) ∈ Type)
  ∧ (∀[s:win2strat(g;0)]. (strat2play(g;0;s) ∈ Type))
  ∧ (∀[s:win2strat(g;0)]. ∀[f:strat2play(g;0;s)].  (||f|| ∈ ℤ))
  ∧ (∀[s:win2strat(g;0)]. ∀[f:strat2play(g;0;s)]. ∀[k:{(2 * 0) + 2..||f|| + 1-}].
       (seq-truncate(f;k) ∈ strat2play(g;0;s)))

2
.....upcase..... 
1. g : SimpleGame
2. n : ℤ
3. 0 < n
4. <Ax, Ax, Ax, Ax> ∈ (win2strat(g;n - 1) ∈ Type)
   ∧ (∀[s:win2strat(g;n - 1)]. (strat2play(g;n - 1;s) ∈ Type))
   ∧ (∀[s:win2strat(g;n - 1)]. ∀[f:strat2play(g;n - 1;s)].  (||f|| ∈ ℤ))
   ∧ (∀[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)))
⊢ <Ax, Ax, Ax, Ax> ∈ (win2strat(g;n) ∈ Type)
  ∧ (∀[s:win2strat(g;n)]. (strat2play(g;n;s) ∈ Type))
  ∧ (∀[s:win2strat(g;n)]. ∀[f:strat2play(g;n;s)].  (||f|| ∈ ℤ))
  ∧ (∀[s:win2strat(g;n)]. ∀[f:strat2play(g;n;s)]. ∀[k:{(2 * n) + 2..||f|| + 1-}].
       (seq-truncate(f;k) ∈ strat2play(g;n;s)))

---

Latex:

---

Latex:
\mforall{}[g:SimpleGame].  \mforall{}[n:\mBbbN{}].
    ((win2strat(g;n)  \mmember{}  Type)
    \mwedge{}  (\mforall{}[s:win2strat(g;n)].  (strat2play(g;n;s)  \mmember{}  Type))
    \mwedge{}  (\mforall{}[s:win2strat(g;n)].  \mforall{}[f:strat2play(g;n;s)].    (||f||  \mmember{}  \mBbbZ{}))
    \mwedge{}  (\mforall{}[s:win2strat(g;n)].  \mforall{}[f:strat2play(g;n;s)].  \mforall{}[k:\{(2  *  n)  +  2..||f||  +  1\msupminus{}\}].
              (play-truncate(f;k)  \mmember{}  strat2play(g;n;s))))


By

---

Latex:
(Unfolds  ``play-len  play-truncate``  0
  THEN  RepeatFor  2  (Intro)
  THEN  UseWitness  \mkleeneopen{}<Ax,  Ax,  Ax,  Ax>\mkleeneclose{}\mcdot{}
  THEN  NatInd  (-1))

---

Home Index