---

Step * 1 of Lemma play-item-reachable


1. g : SimpleGame
2. n : ℕ
3. s : win2strat(g;n)
4. moves : strat2play(g;n;s)
5. i : ℕ(2 * n) + 2
6. moves[0] = InitialPos(g) ∈ Pos(g)
7. ∀i:ℕn + 1
     ((↓Legal1(moves[2 * i];moves[(2 * i) + 1]))
     ∧ (i < n
       ⇒ ((↓Legal2(moves[(2 * i) + 1];moves[2 * (i + 1)]))
          ∧ (moves[2 * (i + 1)] = (s play-truncate(moves;2 * (i + 1))) ∈ Pos(g)))))
8. moves ∈ sequence(Pos(g))
9. ((2 * n) + 2) ≤ ||moves||
10. 0 < i + 1
11. moves[0] = InitialPos(g) ∈ Pos(g)
12. moves[(i + 1) - 1] = moves[i] ∈ Pos(g)
13. ∀i@0:ℕ. ((2 * i@0) + 1 < i + 1 ⇒ (↓Legal1(moves[2 * i@0];moves[(2 * i@0) + 1])))
14. i@0 : ℕ+
15. 2 * i@0 < i + 1
⊢ ↓Legal2(moves[(2 * i@0) - 1];moves[2 * i@0])
BY
{ (RenameVar `j' (-2)
   THEN (D 7 With ⌜j - 1⌝  THENA Auto)
   THEN (RepeatFor 2 (D -1) THENA Auto)
   THEN D -1
   THEN NthHypSq (-2)
   THEN Unfold `play-item` 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  SimpleGame
2.  n  :  \mBbbN{}
3.  s  :  win2strat(g;n)
4.  moves  :  strat2play(g;n;s)
5.  i  :  \mBbbN{}(2  *  n)  +  2
6.  moves[0]  =  InitialPos(g)
7.  \mforall{}i:\mBbbN{}n  +  1
          ((\mdownarrow{}Legal1(moves[2  *  i];moves[(2  *  i)  +  1]))
          \mwedge{}  (i  <  n
              {}\mRightarrow{}  ((\mdownarrow{}Legal2(moves[(2  *  i)  +  1];moves[2  *  (i  +  1)]))
                    \mwedge{}  (moves[2  *  (i  +  1)]  =  (s  play-truncate(moves;2  *  (i  +  1)))))))
8.  moves  \mmember{}  sequence(Pos(g))
9.  ((2  *  n)  +  2)  \mleq{}  ||moves||
10.  0  <  i  +  1
11.  moves[0]  =  InitialPos(g)
12.  moves[(i  +  1)  -  1]  =  moves[i]
13.  \mforall{}i@0:\mBbbN{}.  ((2  *  i@0)  +  1  <  i  +  1  {}\mRightarrow{}  (\mdownarrow{}Legal1(moves[2  *  i@0];moves[(2  *  i@0)  +  1])))
14.  i@0  :  \mBbbN{}\msupplus{}
15.  2  *  i@0  <  i  +  1
\mvdash{}  \mdownarrow{}Legal2(moves[(2  *  i@0)  -  1];moves[2  *  i@0])


By

---

Latex:
(RenameVar  `j'  (-2)
  THEN  (D  7  With  \mkleeneopen{}j  -  1\mkleeneclose{}    THENA  Auto)
  THEN  (RepeatFor  2  (D  -1)  THENA  Auto)
  THEN  D  -1
  THEN  NthHypSq  (-2)
  THEN  Unfold  `play-item`  0
  THEN  Auto)

---

Home Index