---

Step * of Lemma truncate-strat2play

∀[g:SimpleGame]. ∀[n:ℕ]. ∀[s:win2strat(g;n)]. ∀[moves:strat2play(g;n;s)]. ∀[j:ℕ].
  play-truncate(moves;2 * (j + 1)) ∈ strat2play(g;j;s) supposing j < n
BY
{ (Intros THEN Unhide THEN InstLemma `play-truncate_wf` [⌜g⌝;⌜j⌝;⌜s⌝;⌜moves⌝;⌜2 * (j + 1)⌝]⋅ THEN Auto) }

1
.....wf..... 
1. g : SimpleGame
2. n : ℕ
3. s : win2strat(g;n)
4. moves : strat2play(g;n;s)
5. j : ℕ
6. j < n
⊢ 2 * (j + 1) ∈ {(2 * j) + 2..||moves|| + 1-}

---

Latex:

---

Latex:
\mforall{}[g:SimpleGame].  \mforall{}[n:\mBbbN{}].  \mforall{}[s:win2strat(g;n)].  \mforall{}[moves:strat2play(g;n;s)].  \mforall{}[j:\mBbbN{}].
    play-truncate(moves;2  *  (j  +  1))  \mmember{}  strat2play(g;j;s)  supposing  j  <  n


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  InstLemma  `play-truncate\_wf`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}moves\mkleeneclose{};\mkleeneopen{}2  *  (j  +  1)\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index