---

Step * of Lemma strat2play-invariant-type

∀g:SimpleGame. ∀n:ℕ. ∀s:win2strat(g;n). ∀moves:strat2play(g;n;s).
  (∀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))))) ∈ ℙ)
BY
{ (Auto
   THEN (InstLemma `win2strat-properties` [⌜g⌝;⌜i + 1⌝;⌜s⌝]⋅ THENA Auto)
   THEN (Assert ⌜play-truncate(moves;2 * (i + 1)) ∈ {f:strat2play(g;(i + 1) - 1;s)| ||f|| = (2 * (i + 1)) ∈ ℤ} ⌝⋅ THENM \000CAuto)) }

1
.....assertion..... 
1. g : SimpleGame
2. n : ℕ
3. s : win2strat(g;n)
4. moves : strat2play(g;n;s)
5. i : ℕn + 1
6. Legal1(moves[2 * i];moves[(2 * i) + 1])
7. i < n
8. Legal2(moves[(2 * i) + 1];moves[2 * (i + 1)])
9. (s ∈ win2strat(g;(i + 1) - 1))
∧ (s ∈ moves:{f:strat2play(g;(i + 1) - 1;s)| ||f|| = (2 * (i + 1)) ∈ ℤ}  ⟶ {p:Pos(g)| Legal2(moves[(2 * (i + 1)) - 1];p\000C)} )
⊢ play-truncate(moves;2 * (i + 1)) ∈ {f:strat2play(g;(i + 1) - 1;s)| ||f|| = (2 * (i + 1)) ∈ ℤ} 

---

Latex:

---

Latex:
\mforall{}g:SimpleGame.  \mforall{}n:\mBbbN{}.  \mforall{}s:win2strat(g;n).  \mforall{}moves:strat2play(g;n;s).
    (\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)))))))  \mmember{}  \mBbbP{})


By

---

Latex:
(Auto
  THEN  (InstLemma  `win2strat-properties`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}i  +  1\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}play-truncate(moves;2  *  (i  +  1))  \mmember{}  \{f:strat2play(g;(i  +  1)  -  1;s)| 
                                                                                                      ||f||  =  (2  *  (i  +  1))\}  \mkleeneclose{}\mcdot{}
  THENM  Auto
  ))

---

Home Index