---

Step * of Lemma strat2play-invariant-1

∀g:SimpleGame. ∀n:ℕ. ∀s:win2strat(g;n). ∀moves:strat2play(g;n;s).
  ((moves[0] = InitialPos(g) ∈ Pos(g))
  ∧ (∀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
{ ((InductionOnNat THENA Auto) THEN RepeatFor 2 (Intro)) }

1
1. g : SimpleGame
2. n : ℤ
3. s : win2strat(g;0)
4. moves : strat2play(g;0;s)
⊢ (moves[0] = InitialPos(g) ∈ Pos(g))
∧ (∀i:ℕ0 + 1
     ((↓Legal1(moves[2 * i];moves[(2 * i) + 1]))
     ∧ (i < 0
       ⇒ ((↓Legal2(moves[(2 * i) + 1];moves[2 * (i + 1)]))
          ∧ (moves[2 * (i + 1)] = (s play-truncate(moves;2 * (i + 1))) ∈ Pos(g))))))

2
1. g : SimpleGame
2. n : ℤ
3. 0 < n
4. ∀s:win2strat(g;n - 1). ∀moves:strat2play(g;n - 1;s).
     ((moves[0] = InitialPos(g) ∈ Pos(g))
     ∧ (∀i:ℕ(n - 1) + 1
          ((↓Legal1(moves[2 * i];moves[(2 * i) + 1]))
          ∧ (i < n - 1
            ⇒ ((↓Legal2(moves[(2 * i) + 1];moves[2 * (i + 1)]))
               ∧ (moves[2 * (i + 1)] = (s play-truncate(moves;2 * (i + 1))) ∈ Pos(g)))))))
5. s : win2strat(g;n)
6. moves : strat2play(g;n;s)
⊢ (moves[0] = InitialPos(g) ∈ Pos(g))
∧ (∀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))))))

---

Latex:

---

Latex:
\mforall{}g:SimpleGame.  \mforall{}n:\mBbbN{}.  \mforall{}s:win2strat(g;n).  \mforall{}moves:strat2play(g;n;s).
    ((moves[0]  =  InitialPos(g))
    \mwedge{}  (\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)))))))))


By

---

Latex:
((InductionOnNat  THENA  Auto)  THEN  RepeatFor  2  (Intro))

---

Home Index