---

Step * of Lemma play-item-reachable

∀g:SimpleGame. ∀n:ℕ. ∀s:win2strat(g;n). ∀moves:strat2play(g;n;s). ∀i:ℕ(2 * n) + 2.
  (moves[i] ∈ {p:Pos(g)| sg-reachable(g;InitialPos(g);p)} )
BY
{ (Intros
   THEN (Strat2PlayInvariant 4 THENA Auto)
   THEN (Strat2PlaySubtype 4 THENA Auto)
   THEN (MemTypeHD (-1) THENA Auto)
   THEN Fold `member` (-2)
   THEN MemTypeCD
   THEN Auto
   THEN (D 0 With ⌜seq-truncate(moves;i + 1)⌝  THENW Auto)
   THEN RWW "seq-len-truncate seq-truncate-item" 0
   THEN Auto
   THEN Try ((Fold `play-item` 0 THEN BackThruSomeHyp))) }

1
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])

---

Latex:

---

Latex:
\mforall{}g:SimpleGame.  \mforall{}n:\mBbbN{}.  \mforall{}s:win2strat(g;n).  \mforall{}moves:strat2play(g;n;s).  \mforall{}i:\mBbbN{}(2  *  n)  +  2.
    (moves[i]  \mmember{}  \{p:Pos(g)|  sg-reachable(g;InitialPos(g);p)\}  )


By

---

Latex:
(Intros
  THEN  (Strat2PlayInvariant  4  THENA  Auto)
  THEN  (Strat2PlaySubtype  4  THENA  Auto)
  THEN  (MemTypeHD  (-1)  THENA  Auto)
  THEN  Fold  `member`  (-2)
  THEN  MemTypeCD
  THEN  Auto
  THEN  (D  0  With  \mkleeneopen{}seq-truncate(moves;i  +  1)\mkleeneclose{}    THENW  Auto)
  THEN  RWW  "seq-len-truncate  seq-truncate-item"  0
  THEN  Auto
  THEN  Try  ((Fold  `play-item`  0  THEN  BackThruSomeHyp)))

---

Home Index