---

Step * 1 1 1 1 2 2 1 1 1 1 1 1 1 2 1 1 1 of Lemma win2-iff


1. g : SimpleGame
2. s : ∀[n:ℕ]. win2strat(g;n)
3. n : ℤ
4. x : Pos(g)
5. v : strat2play(g;n;s)
6. [%3] : ||v|| = (2 * (n + 1)) ∈ ℤ
7. 1 ≤ n
8. Legal2(v[(2 * (n + 1)) - 1];x)
9. ∀i:ℕ(2 * n) + 1
     ((((i mod 2) = 0 ∈ ℤ) ⇒ (↓Legal1(v[i];v[i + 1]))) ∧ (((i mod 2) = 1 ∈ ℤ) ⇒ (↓Legal2(v[i];v[i + 1]))))
⊢ sg-reachable(g;v[2];x)
BY
{ (OnVar `v' Strat2PlaySubtype THEN (MemTypeHD  (-1) THENA Auto) THEN Thin (-1) THEN Fold `member` (-1)) }

1
1. g : SimpleGame
2. s : ∀[n:ℕ]. win2strat(g;n)
3. n : ℤ
4. x : Pos(g)
5. v : strat2play(g;n;s)
6. [%3] : ||v|| = (2 * (n + 1)) ∈ ℤ
7. 1 ≤ n
8. Legal2(v[(2 * (n + 1)) - 1];x)
9. ∀i:ℕ(2 * n) + 1
     ((((i mod 2) = 0 ∈ ℤ) ⇒ (↓Legal1(v[i];v[i + 1]))) ∧ (((i mod 2) = 1 ∈ ℤ) ⇒ (↓Legal2(v[i];v[i + 1]))))
10. v ∈ sequence(Pos(g))
⊢ sg-reachable(g;v[2];x)

---

Latex:

---

Latex:

1.  g  :  SimpleGame
2.  s  :  \mforall{}[n:\mBbbN{}].  win2strat(g;n)
3.  n  :  \mBbbZ{}
4.  x  :  Pos(g)
5.  v  :  strat2play(g;n;s)
6.  [\%3]  :  ||v||  =  (2  *  (n  +  1))
7.  1  \mleq{}  n
8.  Legal2(v[(2  *  (n  +  1))  -  1];x)
9.  \mforall{}i:\mBbbN{}(2  *  n)  +  1
          ((((i  mod  2)  =  0)  {}\mRightarrow{}  (\mdownarrow{}Legal1(v[i];v[i  +  1])))  \mwedge{}  (((i  mod  2)  =  1)  {}\mRightarrow{}  (\mdownarrow{}Legal2(v[i];v[i  +  1]))))
\mvdash{}  sg-reachable(g;v[2];x)


By

---

Latex:
(OnVar  `v'  Strat2PlaySubtype
  THEN  (MemTypeHD    (-1)  THENA  Auto)
  THEN  Thin  (-1)
  THEN  Fold  `member`  (-1))

---

Home Index