Step
*
2
1
of Lemma
strat2play-invariant-1
1. g : SimpleGame
2. n : ℤ
3. 0 < n
4. s : s:win2strat(g;n - 1) ⋂ moves:{f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ} ⟶ {p:Pos(g)| Legal2(moves[(2 * n) -\000C 1];p)}
5. s ∈ win2strat(g;n - 1)
6. s ∈ moves:{f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ} ⟶ {p:Pos(g)| Legal2(moves[(2 * n) - 1];p)}
7. moves : f:strat2play(g;n - 1;s) ⋂ {moves:sequence(Pos(g))|
(((2 * n) + 2) ≤ ||moves||)
∧ Legal1(moves[2 * n];moves[(2 * n) + 1])
∧ (moves[2 * n] = (s play-truncate(f;2 * n)) ∈ Pos(g))}
8. moves ∈ strat2play(g;n - 1;s)
9. moves ∈ sequence(Pos(g))
10. [%22] : (((2 * n) + 2) ≤ ||moves||)
∧ Legal1(moves[2 * n];moves[(2 * n) + 1])
∧ (moves[2 * n] = (s play-truncate(moves;2 * n)) ∈ Pos(g))
11. moves ∈ strat2play(g;n;s)
12. s ∈ win2strat(g;n)
13. ¬(n = 0 ∈ ℤ)
14. ¬(n = 0 ∈ ℤ)
15. moves[0] = InitialPos(g) ∈ Pos(g)
16. ∀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)))))
⊢ ∀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
{ ((D 0 THENA Auto) THEN (Decide ⌜i ≤ (n - 1)⌝⋅ THENA Auto)) }
1
1. g : SimpleGame
2. n : ℤ
3. 0 < n
4. s : s:win2strat(g;n - 1) ⋂ moves:{f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ} ⟶ {p:Pos(g)| Legal2(moves[(2 * n) -\000C 1];p)}
5. s ∈ win2strat(g;n - 1)
6. s ∈ moves:{f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ} ⟶ {p:Pos(g)| Legal2(moves[(2 * n) - 1];p)}
7. moves : f:strat2play(g;n - 1;s) ⋂ {moves:sequence(Pos(g))|
(((2 * n) + 2) ≤ ||moves||)
∧ Legal1(moves[2 * n];moves[(2 * n) + 1])
∧ (moves[2 * n] = (s play-truncate(f;2 * n)) ∈ Pos(g))}
8. moves ∈ strat2play(g;n - 1;s)
9. moves ∈ sequence(Pos(g))
10. [%22] : (((2 * n) + 2) ≤ ||moves||)
∧ Legal1(moves[2 * n];moves[(2 * n) + 1])
∧ (moves[2 * n] = (s play-truncate(moves;2 * n)) ∈ Pos(g))
11. moves ∈ strat2play(g;n;s)
12. s ∈ win2strat(g;n)
13. ¬(n = 0 ∈ ℤ)
14. ¬(n = 0 ∈ ℤ)
15. moves[0] = InitialPos(g) ∈ Pos(g)
16. ∀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)))))
17. i : ℕn + 1
18. 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))))
2
1. g : SimpleGame
2. n : ℤ
3. 0 < n
4. s : s:win2strat(g;n - 1) ⋂ moves:{f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ} ⟶ {p:Pos(g)| Legal2(moves[(2 * n) -\000C 1];p)}
5. s ∈ win2strat(g;n - 1)
6. s ∈ moves:{f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ} ⟶ {p:Pos(g)| Legal2(moves[(2 * n) - 1];p)}
7. moves : f:strat2play(g;n - 1;s) ⋂ {moves:sequence(Pos(g))|
(((2 * n) + 2) ≤ ||moves||)
∧ Legal1(moves[2 * n];moves[(2 * n) + 1])
∧ (moves[2 * n] = (s play-truncate(f;2 * n)) ∈ Pos(g))}
8. moves ∈ strat2play(g;n - 1;s)
9. moves ∈ sequence(Pos(g))
10. [%22] : (((2 * n) + 2) ≤ ||moves||)
∧ Legal1(moves[2 * n];moves[(2 * n) + 1])
∧ (moves[2 * n] = (s play-truncate(moves;2 * n)) ∈ Pos(g))
11. moves ∈ strat2play(g;n;s)
12. s ∈ win2strat(g;n)
13. ¬(n = 0 ∈ ℤ)
14. ¬(n = 0 ∈ ℤ)
15. moves[0] = InitialPos(g) ∈ Pos(g)
16. ∀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)))))
17. i : ℕn + 1
18. ¬(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:
1. g : SimpleGame
2. n : \mBbbZ{}
3. 0 < n
4. s : s:win2strat(g;n - 1) \mcap{} moves:\{f:strat2play(g;n - 1;s)| ||f|| = (2 * n)\} {}\mrightarrow{} \{p:Pos(g)| Legal2\000C(moves[(2 * n) - 1];p)\}
5. s \mmember{} win2strat(g;n - 1)
6. s \mmember{} moves:\{f:strat2play(g;n - 1;s)| ||f|| = (2 * n)\} {}\mrightarrow{} \{p:Pos(g)| Legal2(moves[(2 * n) - 1];p)\}\000C
7. moves : f:strat2play(g;n - 1;s) \mcap{} \{moves:sequence(Pos(g))|
(((2 * n) + 2) \mleq{} ||moves||)
\mwedge{} Legal1(moves[2 * n];moves[(2 * n) + 1])
\mwedge{} (moves[2 * n] = (s play-truncate(f;2 * n)))\}
8. moves \mmember{} strat2play(g;n - 1;s)
9. moves \mmember{} sequence(Pos(g))
10. [\%22] : (((2 * n) + 2) \mleq{} ||moves||)
\mwedge{} Legal1(moves[2 * n];moves[(2 * n) + 1])
\mwedge{} (moves[2 * n] = (s play-truncate(moves;2 * n)))
11. moves \mmember{} strat2play(g;n;s)
12. s \mmember{} win2strat(g;n)
13. \mneg{}(n = 0)
14. \mneg{}(n = 0)
15. moves[0] = InitialPos(g)
16. \mforall{}i:\mBbbN{}(n - 1) + 1
((\mdownarrow{}Legal1(moves[2 * i];moves[(2 * i) + 1]))
\mwedge{} (i < n - 1
{}\mRightarrow{} ((\mdownarrow{}Legal2(moves[(2 * i) + 1];moves[2 * (i + 1)]))
\mwedge{} (moves[2 * (i + 1)] = (s play-truncate(moves;2 * (i + 1)))))))
\mvdash{} \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:
((D 0 THENA Auto) THEN (Decide \mkleeneopen{}i \mleq{} (n - 1)\mkleeneclose{}\mcdot{} THENA Auto))
Home
Index