---

Step * 1 1 1 1 2 1 of Lemma strat2play-invariant


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
8. i = (((i ÷ 2) * 2) + (i rem 2)) ∈ ℤ
9. 0 ≤ (i rem 2)
10. i rem 2 < 2
11. 0 ≤ (i ÷ 2)
12. Legal1(moves[2 * (i ÷ 2)];moves[(2 * (i ÷ 2)) + 1])
13. i ÷ 2 < n
⇒ ((↓Legal2(moves[(2 * (i ÷ 2)) + 1];moves[2 * ((i ÷ 2) + 1)]))
   ∧ (moves[2 * ((i ÷ 2) + 1)] = (s play-truncate(moves;2 * ((i ÷ 2) + 1))) ∈ Pos(g)))
14. (i rem 2) = 1 ∈ ℤ
⊢ ↓Legal2(moves[(2 * (i ÷ 2)) + 1];moves[((2 * (i ÷ 2)) + 1) + 1])
BY
{ D -2 }

1
.....antecedent..... 
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
8. i = (((i ÷ 2) * 2) + (i rem 2)) ∈ ℤ
9. 0 ≤ (i rem 2)
10. i rem 2 < 2
11. 0 ≤ (i ÷ 2)
12. Legal1(moves[2 * (i ÷ 2)];moves[(2 * (i ÷ 2)) + 1])
13. (i rem 2) = 1 ∈ ℤ
⊢ i ÷ 2 < n

2
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
8. i = (((i ÷ 2) * 2) + (i rem 2)) ∈ ℤ
9. 0 ≤ (i rem 2)
10. i rem 2 < 2
11. 0 ≤ (i ÷ 2)
12. Legal1(moves[2 * (i ÷ 2)];moves[(2 * (i ÷ 2)) + 1])
13. (i rem 2) = 1 ∈ ℤ
14. (↓Legal2(moves[(2 * (i ÷ 2)) + 1];moves[2 * ((i ÷ 2) + 1)]))
∧ (moves[2 * ((i ÷ 2) + 1)] = (s play-truncate(moves;2 * ((i ÷ 2) + 1))) ∈ Pos(g))
⊢ ↓Legal2(moves[(2 * (i ÷ 2)) + 1];moves[((2 * (i ÷ 2)) + 1) + 1])

---

Latex:

---

Latex:

1.  g  :  SimpleGame
2.  n  :  \mBbbN{}
3.  s  :  win2strat(g;n)
4.  moves  :  strat2play(g;n;s)
5.  moves[0]  =  InitialPos(g)
6.  \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)))))))
7.  i  :  \mBbbN{}(2  *  n)  +  1
8.  i  =  (((i  \mdiv{}  2)  *  2)  +  (i  rem  2))
9.  0  \mleq{}  (i  rem  2)
10.  i  rem  2  <  2
11.  0  \mleq{}  (i  \mdiv{}  2)
12.  Legal1(moves[2  *  (i  \mdiv{}  2)];moves[(2  *  (i  \mdiv{}  2))  +  1])
13.  i  \mdiv{}  2  <  n
{}\mRightarrow{}  ((\mdownarrow{}Legal2(moves[(2  *  (i  \mdiv{}  2))  +  1];moves[2  *  ((i  \mdiv{}  2)  +  1)]))
      \mwedge{}  (moves[2  *  ((i  \mdiv{}  2)  +  1)]  =  (s  play-truncate(moves;2  *  ((i  \mdiv{}  2)  +  1)))))
14.  (i  rem  2)  =  1
\mvdash{}  \mdownarrow{}Legal2(moves[(2  *  (i  \mdiv{}  2))  +  1];moves[((2  *  (i  \mdiv{}  2))  +  1)  +  1])


By

---

Latex:
D  -2

---

Home Index