Step
*
1
1
1
1
1
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. g@s seq-cons(InitialPos(g);seq-cons(p;seq-nil())) ∈ SimpleGame
15. Pos(g@s seq-cons(InitialPos(g);seq-cons(p;seq-nil()))) ⊆r Pos(g)
⊢ seq-cons(InitialPos(g);seq-cons(p;mvs)) ∈ strat2play(g;n;s)
BY
{ (Assert ⌜mvs ∈ sequence(Pos(g))⌝⋅ THENM (Assert seq-cons(InitialPos(g);seq-cons(p;mvs)) ∈ sequence(Pos(g)) BY Auto)) }
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. g@s seq-cons(InitialPos(g);seq-cons(p;seq-nil())) ∈ SimpleGame
15. Pos(g@s seq-cons(InitialPos(g);seq-cons(p;seq-nil()))) ⊆r Pos(g)
⊢ mvs ∈ sequence(Pos(g))
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. g@s seq-cons(InitialPos(g);seq-cons(p;seq-nil())) ∈ SimpleGame
15. Pos(g@s seq-cons(InitialPos(g);seq-cons(p;seq-nil()))) ⊆r Pos(g)
16. mvs ∈ sequence(Pos(g))
17. seq-cons(InitialPos(g);seq-cons(p;mvs)) ∈ sequence(Pos(g))
⊢ seq-cons(InitialPos(g);seq-cons(p;mvs)) ∈ strat2play(g;n;s)
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. g@s seq-cons(InitialPos(g);seq-cons(p;seq-nil())) \mmember{} SimpleGame
15. Pos(g@s seq-cons(InitialPos(g);seq-cons(p;seq-nil()))) \msubseteq{}r Pos(g)
\mvdash{} seq-cons(InitialPos(g);seq-cons(p;mvs)) \mmember{} strat2play(g;n;s)
By
Latex:
(Assert \mkleeneopen{}mvs \mmember{} sequence(Pos(g))\mkleeneclose{}\mcdot{}
THENM (Assert seq-cons(InitialPos(g);seq-cons(p;mvs)) \mmember{} sequence(Pos(g)) BY
Auto)
)
Home
Index