Step
*
2
1
1
1
1
1
1
of Lemma
win2strat-strat2play-wf
1. g : SimpleGame
2. n : ℤ
3. n ≠ 0
4. 0 < n
5. win2strat(g;n - 1) ∈ Type
6. ∀[s:win2strat(g;n - 1)]. ∀[f:strat2play(g;n - 1;s)]. (||f|| ∈ ℤ)
7. ∀[s:win2strat(g;n - 1)]. ∀[f:strat2play(g;n - 1;s)]. ∀[k:{(2 * (n - 1)) + 2..||f|| + 1-}].
(seq-truncate(f;k) ∈ strat2play(g;n - 1;s))
8. win2strat(g;n) ∈ Type
9. 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)}
10. s ∈ win2strat(g;n - 1)
11. s ∈ moves:{f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ} ⟶ {p:Pos(g)| Legal2(moves[(2 * n) - 1];p)}
12. ¬(n = 0 ∈ ℤ)
13. strat2play(g;n - 1;s) ∈ Type
14. f : strat2play(g;n - 1;s)
15. f ∈ {moves:sequence(Pos(g))| (2 * n) ≤ ||moves||}
16. ||f|| ∈ ℤ
17. seq-truncate(f;2 * n) ∈ {f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ}
⊢ {moves:sequence(Pos(g))|
(((2 * n) + 2) ≤ ||moves||)
∧ Legal1(moves[2 * n];moves[(2 * n) + 1])
∧ (moves[2 * n] = (s seq-truncate(f;2 * n)) ∈ Pos(g))} ∈ Type
BY
{ (GenConclTerm ⌜s seq-truncate(f;2 * n)⌝⋅ THENA Auto) }
1
1. g : SimpleGame
2. n : ℤ
3. n ≠ 0
4. 0 < n
5. win2strat(g;n - 1) ∈ Type
6. ∀[s:win2strat(g;n - 1)]. ∀[f:strat2play(g;n - 1;s)]. (||f|| ∈ ℤ)
7. ∀[s:win2strat(g;n - 1)]. ∀[f:strat2play(g;n - 1;s)]. ∀[k:{(2 * (n - 1)) + 2..||f|| + 1-}].
(seq-truncate(f;k) ∈ strat2play(g;n - 1;s))
8. win2strat(g;n) ∈ Type
9. 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)}
10. s ∈ win2strat(g;n - 1)
11. s ∈ moves:{f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ} ⟶ {p:Pos(g)| Legal2(moves[(2 * n) - 1];p)}
12. ¬(n = 0 ∈ ℤ)
13. strat2play(g;n - 1;s) ∈ Type
14. f : strat2play(g;n - 1;s)
15. f ∈ {moves:sequence(Pos(g))| (2 * n) ≤ ||moves||}
16. ||f|| ∈ ℤ
17. seq-truncate(f;2 * n) ∈ {f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ}
18. p : Pos(g)
⊢ seq-truncate(f;2 * n)[(2 * n) - 1] ∈ Pos(g)
2
1. g : SimpleGame
2. n : ℤ
3. n ≠ 0
4. 0 < n
5. win2strat(g;n - 1) ∈ Type
6. ∀[s:win2strat(g;n - 1)]. ∀[f:strat2play(g;n - 1;s)]. (||f|| ∈ ℤ)
7. ∀[s:win2strat(g;n - 1)]. ∀[f:strat2play(g;n - 1;s)]. ∀[k:{(2 * (n - 1)) + 2..||f|| + 1-}].
(seq-truncate(f;k) ∈ strat2play(g;n - 1;s))
8. win2strat(g;n) ∈ Type
9. 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)}
10. s ∈ win2strat(g;n - 1)
11. s ∈ moves:{f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ} ⟶ {p:Pos(g)| Legal2(moves[(2 * n) - 1];p)}
12. ¬(n = 0 ∈ ℤ)
13. strat2play(g;n - 1;s) ∈ Type
14. f : strat2play(g;n - 1;s)
15. f ∈ {moves:sequence(Pos(g))| (2 * n) ≤ ||moves||}
16. ||f|| ∈ ℤ
17. seq-truncate(f;2 * n) ∈ {f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ}
18. v : {p:Pos(g)| Legal2(seq-truncate(f;2 * n)[(2 * n) - 1];p)}
19. (s seq-truncate(f;2 * n)) = v ∈ {p:Pos(g)| Legal2(seq-truncate(f;2 * n)[(2 * n) - 1];p)}
⊢ {moves:sequence(Pos(g))|
(((2 * n) + 2) ≤ ||moves||) ∧ Legal1(moves[2 * n];moves[(2 * n) + 1]) ∧ (moves[2 * n] = v ∈ Pos(g))} ∈ Type
Latex:
Latex:
1. g : SimpleGame
2. n : \mBbbZ{}
3. n \mneq{} 0
4. 0 < n
5. win2strat(g;n - 1) \mmember{} Type
6. \mforall{}[s:win2strat(g;n - 1)]. \mforall{}[f:strat2play(g;n - 1;s)]. (||f|| \mmember{} \mBbbZ{})
7. \mforall{}[s:win2strat(g;n - 1)]. \mforall{}[f:strat2play(g;n - 1;s)]. \mforall{}[k:\{(2 * (n - 1)) + 2..||f|| + 1\msupminus{}\}].
(seq-truncate(f;k) \mmember{} strat2play(g;n - 1;s))
8. win2strat(g;n) \mmember{} Type
9. 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)\}
10. s \mmember{} win2strat(g;n - 1)
11. s \mmember{} moves:\{f:strat2play(g;n - 1;s)| ||f|| = (2 * n)\} {}\mrightarrow{} \{p:Pos(g)| Legal2(moves[(2 * n) - 1];p)\000C\}
12. \mneg{}(n = 0)
13. strat2play(g;n - 1;s) \mmember{} Type
14. f : strat2play(g;n - 1;s)
15. f \mmember{} \{moves:sequence(Pos(g))| (2 * n) \mleq{} ||moves||\}
16. ||f|| \mmember{} \mBbbZ{}
17. seq-truncate(f;2 * n) \mmember{} \{f:strat2play(g;n - 1;s)| ||f|| = (2 * n)\}
\mvdash{} \{moves:sequence(Pos(g))|
(((2 * n) + 2) \mleq{} ||moves||)
\mwedge{} Legal1(moves[2 * n];moves[(2 * n) + 1])
\mwedge{} (moves[2 * n] = (s seq-truncate(f;2 * n)))\} \mmember{} Type
By
Latex:
(GenConclTerm \mkleeneopen{}s seq-truncate(f;2 * n)\mkleeneclose{}\mcdot{} THENA Auto)
Home
Index