Step
*
1
1
1
1
of Lemma
win2-iff
1. g : SimpleGame
2. s : ∀[n:ℕ]. win2strat(g;n)
3. p : {p:Pos(g)| Legal1(InitialPos(g);p)}
4. s ∈ win2strat(g;1 - 1)
5. s ∈ moves:{f:strat2play(g;0;s)| ||f|| = 2 ∈ ℤ} ⟶ {p:Pos(g)| Legal2(moves[1];p)}
6. seq-cons(InitialPos(g);seq-cons(p;seq-nil())) ∈ {f:strat2play(g;0;s)| ||f|| = 2 ∈ ℤ}
7. s seq-cons(InitialPos(g);seq-cons(p;seq-nil())) ∈ {q:Pos(g)| Legal2(p;q)}
8. n : ℤ
9. 0 < n
10. λmvs.(s seq-cons(InitialPos(g);seq-cons(p;mvs))) ∈ win2strat(g@s seq-cons(InitialPos(g);seq-cons(p;seq-nil()));n
- 1)
11. ¬(n = 0 ∈ ℤ)
12. mvs : strat2play(g@s seq-cons(InitialPos(g);seq-cons(p;seq-nil()));n
- 1;λmvs.(s seq-cons(InitialPos(g);seq-cons(p;mvs))))
13. ||mvs|| = (2 * n) ∈ ℤ
14. s ∈ win2strat(g;(n + 1) - 1)
15. s ∈ moves:{f:strat2play(g;(n + 1) - 1;s)| ||f|| = (2 * (n + 1)) ∈ ℤ} ⟶ {p:Pos(g)| Legal2(moves[(2 * (n + 1)) - 1];\000Cp)}
⊢ s seq-cons(InitialPos(g);seq-cons(p;mvs)) ∈ {p@0:Pos(g@s seq-cons(InitialPos(g);seq-cons(p;seq-nil())))|
Legal2(mvs[(2 * n) - 1];p@0)}
BY
{ Assert ⌜seq-cons(InitialPos(g);seq-cons(p;mvs)) ∈ {f:strat2play(g;(n + 1) - 1;s)| ||f|| = (2 * (n + 1)) ∈ ℤ} ⌝⋅ }
1
.....assertion.....
1. g : SimpleGame
2. s : ∀[n:ℕ]. win2strat(g;n)
3. p : {p:Pos(g)| Legal1(InitialPos(g);p)}
4. s ∈ win2strat(g;1 - 1)
5. s ∈ moves:{f:strat2play(g;0;s)| ||f|| = 2 ∈ ℤ} ⟶ {p:Pos(g)| Legal2(moves[1];p)}
6. seq-cons(InitialPos(g);seq-cons(p;seq-nil())) ∈ {f:strat2play(g;0;s)| ||f|| = 2 ∈ ℤ}
7. s seq-cons(InitialPos(g);seq-cons(p;seq-nil())) ∈ {q:Pos(g)| Legal2(p;q)}
8. n : ℤ
9. 0 < n
10. λmvs.(s seq-cons(InitialPos(g);seq-cons(p;mvs))) ∈ win2strat(g@s seq-cons(InitialPos(g);seq-cons(p;seq-nil()));n
- 1)
11. ¬(n = 0 ∈ ℤ)
12. mvs : strat2play(g@s seq-cons(InitialPos(g);seq-cons(p;seq-nil()));n
- 1;λmvs.(s seq-cons(InitialPos(g);seq-cons(p;mvs))))
13. ||mvs|| = (2 * n) ∈ ℤ
14. s ∈ win2strat(g;(n + 1) - 1)
15. s ∈ moves:{f:strat2play(g;(n + 1) - 1;s)| ||f|| = (2 * (n + 1)) ∈ ℤ} ⟶ {p:Pos(g)| Legal2(moves[(2 * (n + 1)) - 1];\000Cp)}
⊢ seq-cons(InitialPos(g);seq-cons(p;mvs)) ∈ {f:strat2play(g;(n + 1) - 1;s)| ||f|| = (2 * (n + 1)) ∈ ℤ}
2
1. g : SimpleGame
2. s : ∀[n:ℕ]. win2strat(g;n)
3. p : {p:Pos(g)| Legal1(InitialPos(g);p)}
4. s ∈ win2strat(g;1 - 1)
5. s ∈ moves:{f:strat2play(g;0;s)| ||f|| = 2 ∈ ℤ} ⟶ {p:Pos(g)| Legal2(moves[1];p)}
6. seq-cons(InitialPos(g);seq-cons(p;seq-nil())) ∈ {f:strat2play(g;0;s)| ||f|| = 2 ∈ ℤ}
7. s seq-cons(InitialPos(g);seq-cons(p;seq-nil())) ∈ {q:Pos(g)| Legal2(p;q)}
8. n : ℤ
9. 0 < n
10. λmvs.(s seq-cons(InitialPos(g);seq-cons(p;mvs))) ∈ win2strat(g@s seq-cons(InitialPos(g);seq-cons(p;seq-nil()));n
- 1)
11. ¬(n = 0 ∈ ℤ)
12. mvs : strat2play(g@s seq-cons(InitialPos(g);seq-cons(p;seq-nil()));n
- 1;λmvs.(s seq-cons(InitialPos(g);seq-cons(p;mvs))))
13. ||mvs|| = (2 * n) ∈ ℤ
14. s ∈ win2strat(g;(n + 1) - 1)
15. s ∈ moves:{f:strat2play(g;(n + 1) - 1;s)| ||f|| = (2 * (n + 1)) ∈ ℤ} ⟶ {p:Pos(g)| Legal2(moves[(2 * (n + 1)) - 1];\000Cp)}
16. seq-cons(InitialPos(g);seq-cons(p;mvs)) ∈ {f:strat2play(g;(n + 1) - 1;s)| ||f|| = (2 * (n + 1)) ∈ ℤ}
⊢ s seq-cons(InitialPos(g);seq-cons(p;mvs)) ∈ {p@0:Pos(g@s seq-cons(InitialPos(g);seq-cons(p;seq-nil())))|
Legal2(mvs[(2 * n) - 1];p@0)}
Latex:
Latex:
1. g : SimpleGame
2. s : \mforall{}[n:\mBbbN{}]. win2strat(g;n)
3. p : \{p:Pos(g)| Legal1(InitialPos(g);p)\}
4. s \mmember{} win2strat(g;1 - 1)
5. s \mmember{} moves:\{f:strat2play(g;0;s)| ||f|| = 2\} {}\mrightarrow{} \{p:Pos(g)| Legal2(moves[1];p)\}
6. seq-cons(InitialPos(g);seq-cons(p;seq-nil())) \mmember{} \{f:strat2play(g;0;s)| ||f|| = 2\}
7. s seq-cons(InitialPos(g);seq-cons(p;seq-nil())) \mmember{} \{q:Pos(g)| Legal2(p;q)\}
8. n : \mBbbZ{}
9. 0 < n
10. \mlambda{}mvs.(s seq-cons(InitialPos(g);seq-cons(p;mvs)))
\mmember{} win2strat(g@s seq-cons(InitialPos(g);seq-cons(p;seq-nil()));n - 1)
11. \mneg{}(n = 0)
12. mvs : strat2play(g@s seq-cons(InitialPos(g);seq-cons(p;seq-nil()));n
- 1;\mlambda{}mvs.(s seq-cons(InitialPos(g);seq-cons(p;mvs))))
13. ||mvs|| = (2 * n)
14. s \mmember{} win2strat(g;(n + 1) - 1)
15. s \mmember{} moves:\{f:strat2play(g;(n + 1) - 1;s)| ||f|| = (2 * (n + 1))\} {}\mrightarrow{} \{p:Pos(g)|
Legal2(moves[(2 * (n + 1)) - 1];p)\}
\mvdash{} s seq-cons(InitialPos(g);seq-cons(p;mvs))
\mmember{} \{p@0:Pos(g@s seq-cons(InitialPos(g);seq-cons(p;seq-nil())))| Legal2(mvs[(2 * n) - 1];p@0)\}
By
Latex:
Assert \mkleeneopen{}seq-cons(InitialPos(g);seq-cons(p;mvs)) \mmember{} \{f:strat2play(g;(n + 1) - 1;s)|
||f|| = (2 * (n + 1))\} \mkleeneclose{}\mcdot{}
Home
Index