---

Step * of Lemma strat2play-reachable

∀g:SimpleGame. ∀n:ℕ. ∀s:win2strat(g;n). ∀moves:strat2play(g;n;s).
  ((||moves|| ≤ ((2 * n) + 2)) ⇒ (moves ∈ sequence({p:Pos(g)| sg-reachable(g;InitialPos(g);p)} )))
BY
{ (InstLemma `play-item-reachable` []
   THEN RepeatFor 4 (ParallelLast')
   THEN (D 0 THENA Auto)
   THEN Strat2PlaySubtype (-3)
   THEN (Assert ∀i:ℕ(2 * n) + 2. (↓sg-reachable(g;InitialPos(g);moves[i])) BY
               (ParallelOp -3 THEN MemTypeHD (-1) THEN Auto))
   THEN (MoveToConcl (-1) THEN MoveToConcl (-2))
   THEN (GenConcl ⌜moves = xx ∈ {moves:sequence(Pos(g))| ((2 * n) + 2) ≤ ||moves||} ⌝⋅ THENA Auto)
   THEN All Thin) }

1
1. g : SimpleGame
2. n : ℕ
3. xx : {moves:sequence(Pos(g))| ((2 * n) + 2) ≤ ||moves||} 
⊢ (||xx|| ≤ ((2 * n) + 2))
⇒ (∀i:ℕ(2 * n) + 2. (↓sg-reachable(g;InitialPos(g);xx[i])))
⇒ (xx ∈ sequence({p:Pos(g)| sg-reachable(g;InitialPos(g);p)} ))

---

Latex:

---

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


By

---

Latex:
(InstLemma  `play-item-reachable`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  (D  0  THENA  Auto)
  THEN  Strat2PlaySubtype  (-3)
  THEN  (Assert  \mforall{}i:\mBbbN{}(2  *  n)  +  2.  (\mdownarrow{}sg-reachable(g;InitialPos(g);moves[i]))  BY
                          (ParallelOp  -3  THEN  MemTypeHD  (-1)  THEN  Auto))
  THEN  (MoveToConcl  (-1)  THEN  MoveToConcl  (-2))
  THEN  (GenConcl  \mkleeneopen{}moves  =  xx\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin)

---

Home Index