---

Step * of Lemma strat2play_subtype

∀[g:SimpleGame]. ∀[n:ℕ]. ∀[s:win2strat(g;n)].
  (strat2play(g;n;s) ⊆r {moves:sequence(Pos(g))| ((2 * n) + 2) ≤ ||moves||} )
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN Unfold `strat2play` -1
   THEN (SplitOnHypITE -1  THENA Auto)
   THEN ((DepIsectHD (-2) THEN MemTypeHD (-2) THEN All (Fold `member`) THEN Auto) ORELSE (D -2 THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[g:SimpleGame].  \mforall{}[n:\mBbbN{}].  \mforall{}[s:win2strat(g;n)].
    (strat2play(g;n;s)  \msubseteq{}r  \{moves:sequence(Pos(g))|  ((2  *  n)  +  2)  \mleq{}  ||moves||\}  )


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  Unfold  `strat2play`  -1
  THEN  (SplitOnHypITE  -1    THENA  Auto)
  THEN  ((DepIsectHD  (-2)  THEN  MemTypeHD  (-2)  THEN  All  (Fold  `member`)  THEN  Auto)
  ORELSE  (D  -2  THEN  Auto)
  ))

---

Home Index