---

Step * of Lemma win2strat-properties

∀g:SimpleGame. ∀n:ℕ+. ∀s:win2strat(g;n).
  ((s ∈ win2strat(g;n - 1))
  ∧ (s ∈ moves:{f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(g)| Legal2(moves[(2 * n) - 1];p)} ))
BY
{ (Intros THEN Unfold `win2strat` -1 THEN (SplitOnHypITE -1  THENA Auto) THEN Try (DepIsectHD (-2)) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}g:SimpleGame.  \mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}s:win2strat(g;n).
    ((s  \mmember{}  win2strat(g;n  -  1))
    \mwedge{}  (s  \mmember{}  moves:\{f:strat2play(g;n  -  1;s)|  ||f||  =  (2  *  n)\}    {}\mrightarrow{}  \{p:Pos(g)|  Legal2(moves[(2  *  n)  -  1];p\000C)\}  ))


By

---

Latex:
(Intros
  THEN  Unfold  `win2strat`  -1
  THEN  (SplitOnHypITE  -1    THENA  Auto)
  THEN  Try  (DepIsectHD  (-2))
  THEN  Auto)

---

Home Index