---

Step * 1 of Lemma truncate-strat2play

.....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-}
BY
{ ((Strat2PlaySubtype 4 THEN Auto)
   THEN (MemTypeHD (-1) THENA Auto)
   THEN Unfold `play-len` 0
   THEN (Assert (j + 1) ≤ n BY
               Auto)
   THEN Mul ⌜2⌝ (-1)⋅
   THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  g  :  SimpleGame
2.  n  :  \mBbbN{}
3.  s  :  win2strat(g;n)
4.  moves  :  strat2play(g;n;s)
5.  j  :  \mBbbN{}
6.  j  <  n
\mvdash{}  2  *  (j  +  1)  \mmember{}  \{(2  *  j)  +  2..||moves||  +  1\msupminus{}\}


By

---

Latex:
((Strat2PlaySubtype  4  THEN  Auto)
  THEN  (MemTypeHD  (-1)  THENA  Auto)
  THEN  Unfold  `play-len`  0
  THEN  (Assert  (j  +  1)  \mleq{}  n  BY
                          Auto)
  THEN  Mul  \mkleeneopen{}2\mkleeneclose{}  (-1)\mcdot{}
  THEN  Auto)

---

Home Index