Step
*
2
1
1
2
1
2
1
1
1
of Lemma
win2strat-strat2play-wf
1. g : SimpleGame
2. n : ℤ
3. 0 < n
4. win2strat(g;n - 1) ∈ Type
5. ∀[s:win2strat(g;n - 1)]. (strat2play(g;n - 1;s) ∈ 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:win2strat(g;n)]. (strat2play(g;n;s) ∈ Type)
10. 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)}
11. s ∈ win2strat(g;n - 1)
12. s ∈ moves:{f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ} ⟶ {p:Pos(g)| Legal2(moves[(2 * n) - 1];p)}
13. strat2play(g;n;s) ∈ Type
14. ∀[f:strat2play(g;n;s)]. (||f|| ∈ ℤ)
15. f : 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))}
16. f ∈ strat2play(g;n - 1;s)
17. f = f ∈ sequence(Pos(g))
18. ((2 * n) + 2) ≤ ||f||
19. Legal1(f[2 * n];f[(2 * n) + 1])
20. f[2 * n] = (s play-truncate(f;2 * n)) ∈ Pos(g)
21. k : {(2 * n) + 2..||f|| + 1-}
22. s ∈ win2strat(g;n)
23. ¬(n = 0 ∈ ℤ)
24. f ∈ strat2play(g;n;s)
25. ¬(n = 0 ∈ ℤ)
26. ¬(n = 0 ∈ ℤ)
⊢ seq-truncate(f;k) ∈ strat2play(g;n - 1;s)
BY
{ (BHyp 7 THEN Try (Trivial)) }
1
.....wf.....
1. g : SimpleGame
2. n : ℤ
3. 0 < n
4. win2strat(g;n - 1) ∈ Type
5. ∀[s:win2strat(g;n - 1)]. (strat2play(g;n - 1;s) ∈ 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:win2strat(g;n)]. (strat2play(g;n;s) ∈ Type)
10. 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)}
11. s ∈ win2strat(g;n - 1)
12. s ∈ moves:{f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ} ⟶ {p:Pos(g)| Legal2(moves[(2 * n) - 1];p)}
13. strat2play(g;n;s) ∈ Type
14. ∀[f:strat2play(g;n;s)]. (||f|| ∈ ℤ)
15. f : 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))}
16. f ∈ strat2play(g;n - 1;s)
17. f = f ∈ sequence(Pos(g))
18. ((2 * n) + 2) ≤ ||f||
19. Legal1(f[2 * n];f[(2 * n) + 1])
20. f[2 * n] = (s play-truncate(f;2 * n)) ∈ Pos(g)
21. k : {(2 * n) + 2..||f|| + 1-}
22. s ∈ win2strat(g;n)
23. ¬(n = 0 ∈ ℤ)
24. f ∈ strat2play(g;n;s)
25. ¬(n = 0 ∈ ℤ)
26. ¬(n = 0 ∈ ℤ)
⊢ k ∈ {(2 * (n - 1)) + 2..||f|| + 1-}
Latex:
Latex:
1. g : SimpleGame
2. n : \mBbbZ{}
3. 0 < n
4. win2strat(g;n - 1) \mmember{} Type
5. \mforall{}[s:win2strat(g;n - 1)]. (strat2play(g;n - 1;s) \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. \mforall{}[s:win2strat(g;n)]. (strat2play(g;n;s) \mmember{} Type)
10. s : s:win2strat(g;n - 1) \mcap{} moves:\{f:strat2play(g;n - 1;s)| ||f|| = (2 * n)\} {}\mrightarrow{} \{p:Pos(g)| Legal\000C2(moves[(2 * n) - 1];p)\}
11. s \mmember{} win2strat(g;n - 1)
12. s \mmember{} moves:\{f:strat2play(g;n - 1;s)| ||f|| = (2 * n)\} {}\mrightarrow{} \{p:Pos(g)| Legal2(moves[(2 * n) - 1];p)\000C\}
13. strat2play(g;n;s) \mmember{} Type
14. \mforall{}[f:strat2play(g;n;s)]. (||f|| \mmember{} \mBbbZ{})
15. f : 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)))\}
16. f \mmember{} strat2play(g;n - 1;s)
17. f = f
18. ((2 * n) + 2) \mleq{} ||f||
19. Legal1(f[2 * n];f[(2 * n) + 1])
20. f[2 * n] = (s play-truncate(f;2 * n))
21. k : \{(2 * n) + 2..||f|| + 1\msupminus{}\}
22. s \mmember{} win2strat(g;n)
23. \mneg{}(n = 0)
24. f \mmember{} strat2play(g;n;s)
25. \mneg{}(n = 0)
26. \mneg{}(n = 0)
\mvdash{} seq-truncate(f;k) \mmember{} strat2play(g;n - 1;s)
By
Latex:
(BHyp 7 THEN Try (Trivial))
Home
Index