---

Step * of Lemma strat2play-invariant

∀g:SimpleGame. ∀n:ℕ. ∀s:win2strat(g;n). ∀moves:strat2play(g;n;s). ∀i:ℕ(2 * n) + 1.
  ((((i mod 2) = 0 ∈ ℤ) ⇒ (↓Legal1(moves[i];moves[i + 1])))
  ∧ (((i mod 2) = 1 ∈ ℤ) ⇒ (↓Legal2(moves[i];moves[i + 1]))))
BY
{ (InstLemma `strat2play-invariant-1` [] THEN RepeatFor 4 (ParallelLast') THEN D -1 THEN (D 0 THENA Auto)) }

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

---

Latex:

---

Latex:
\mforall{}g:SimpleGame.  \mforall{}n:\mBbbN{}.  \mforall{}s:win2strat(g;n).  \mforall{}moves:strat2play(g;n;s).  \mforall{}i:\mBbbN{}(2  *  n)  +  1.
    ((((i  mod  2)  =  0)  {}\mRightarrow{}  (\mdownarrow{}Legal1(moves[i];moves[i  +  1])))
    \mwedge{}  (((i  mod  2)  =  1)  {}\mRightarrow{}  (\mdownarrow{}Legal2(moves[i];moves[i  +  1]))))


By

---

Latex:
(InstLemma  `strat2play-invariant-1`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  D  -1
  THEN  (D  0  THENA  Auto))

---

Home Index