---

Step * of Lemma play-truncate_wf

∀[g:SimpleGame]. ∀[n:ℕ]. ∀[s:win2strat(g;n)]. ∀[f:strat2play(g;n;s)]. ∀[k:{(2 * n) + 2..||f|| + 1-}].
  (play-truncate(f;k) ∈ {moves:strat2play(g;n;s)| ||moves|| = k ∈ ℤ} )
BY
{ (InstLemma `win2strat-strat2play-wf` [] THEN RepeatFor 2 (ParallelLast') THEN RepeatFor 3 (D -1)) }

1
1. [g] : SimpleGame
2. [n] : ℕ
3. win2strat(g;n) ∈ Type
4. ∀[s:win2strat(g;n)]. (strat2play(g;n;s) ∈ Type)
5. ∀[s:win2strat(g;n)]. ∀[f:strat2play(g;n;s)].  (||f|| ∈ ℤ)
6. ∀[s:win2strat(g;n)]. ∀[f:strat2play(g;n;s)]. ∀[k:{(2 * n) + 2..||f|| + 1-}].
     (play-truncate(f;k) ∈ strat2play(g;n;s))
⊢ ∀[s:win2strat(g;n)]. ∀[f:strat2play(g;n;s)]. ∀[k:{(2 * n) + 2..||f|| + 1-}].
    (play-truncate(f;k) ∈ {moves:strat2play(g;n;s)| ||moves|| = k ∈ ℤ} )

---

Latex:

---

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


By

---

Latex:
(InstLemma  `win2strat-strat2play-wf`  []  THEN  RepeatFor  2  (ParallelLast')  THEN  RepeatFor  3  (D  -1))

---

Home Index