Step
*
1
1
2
1
1
3
2
of Lemma
respond-implies-win2
1. g : SimpleGame
2. m : p:{p:Pos(g)| Legal1(InitialPos(g);p)} ⟶ {q:Pos(g)| Legal2(p;q)}
3. s : ∀p:{p:Pos(g)| Legal1(InitialPos(g);p)} . ∀[n:ℕ]. win2strat(g@m p;n)
4. n : ℤ
5. 0 < n
6. λmoves.if (||moves|| =z 2) then m moves[1] else s moves[1] seq-tl(seq-tl(moves)) fi ∈ win2strat(g;n - 1)
7. ¬(n = 0 ∈ ℤ)
8. moves : strat2play(g;n - 1;λmoves.if (||moves|| =z 2) then m moves[1] else s moves[1] seq-tl(seq-tl(moves)) fi )
9. ||moves|| = (2 * n) ∈ ℤ
10. moves[1] ∈ {p:Pos(g)| Legal1(InitialPos(g);p)}
11. 2 ≤ n
12. 4 ≤ (2 * n)
13. s moves[1] ∈ win2strat(g@m moves[1];n - 1 - 1)
14. s moves[1] ∈ moves@0:{f:strat2play(g@m moves[1];n - 1 - 1;s moves[1])| ||f|| = (2 * (n - 1)) ∈ ℤ} ⟶ {p:Pos(g@m mov\000Ces[1])|
Legal2(moves@0[(2 * (n - 1))
- 1];p)}
15. seq-tl(seq-tl(moves)) ∈ {f:strat2play(g@m moves[1];n - 1 - 1;s moves[1])| ||f|| = (2 * (n - 1)) ∈ ℤ}
16. (s moves[1] seq-tl(seq-tl(moves)))
= (s moves[1] seq-tl(seq-tl(moves)))
∈ {p:Pos(g@m moves[1])| Legal2(seq-tl(seq-tl(moves))[(2 * (n - 1)) - 1];p)}
⊢ {p:Pos(g@m moves[1])| Legal2(seq-tl(seq-tl(moves))[(2 * (n - 1)) - 1];p)} ⊆r {p:Pos(g)|
Legal2(moves[(2 * n) - 1];p)}
BY
{ (D 0 THENA Auto) }
1
.....subterm..... T:t
1:n
1. g : SimpleGame
2. m : p:{p:Pos(g)| Legal1(InitialPos(g);p)} ⟶ {q:Pos(g)| Legal2(p;q)}
3. s : ∀p:{p:Pos(g)| Legal1(InitialPos(g);p)} . ∀[n:ℕ]. win2strat(g@m p;n)
4. n : ℤ
5. 0 < n
6. λmoves.if (||moves|| =z 2) then m moves[1] else s moves[1] seq-tl(seq-tl(moves)) fi ∈ win2strat(g;n - 1)
7. ¬(n = 0 ∈ ℤ)
8. moves : strat2play(g;n - 1;λmoves.if (||moves|| =z 2) then m moves[1] else s moves[1] seq-tl(seq-tl(moves)) fi )
9. ||moves|| = (2 * n) ∈ ℤ
10. moves[1] ∈ {p:Pos(g)| Legal1(InitialPos(g);p)}
11. 2 ≤ n
12. 4 ≤ (2 * n)
13. s moves[1] ∈ win2strat(g@m moves[1];n - 1 - 1)
14. s moves[1] ∈ moves@0:{f:strat2play(g@m moves[1];n - 1 - 1;s moves[1])| ||f|| = (2 * (n - 1)) ∈ ℤ} ⟶ {p:Pos(g@m mov\000Ces[1])|
Legal2(moves@0[(2 * (n - 1))
- 1];p)}
15. seq-tl(seq-tl(moves)) ∈ {f:strat2play(g@m moves[1];n - 1 - 1;s moves[1])| ||f|| = (2 * (n - 1)) ∈ ℤ}
16. (s moves[1] seq-tl(seq-tl(moves)))
= (s moves[1] seq-tl(seq-tl(moves)))
∈ {p:Pos(g@m moves[1])| Legal2(seq-tl(seq-tl(moves))[(2 * (n - 1)) - 1];p)}
17. x : {p:Pos(g@m moves[1])| Legal2(seq-tl(seq-tl(moves))[(2 * (n - 1)) - 1];p)}
⊢ x ∈ {p:Pos(g)| Legal2(moves[(2 * n) - 1];p)}
Latex:
Latex:
1. g : SimpleGame
2. m : p:\{p:Pos(g)| Legal1(InitialPos(g);p)\} {}\mrightarrow{} \{q:Pos(g)| Legal2(p;q)\}
3. s : \mforall{}p:\{p:Pos(g)| Legal1(InitialPos(g);p)\} . \mforall{}[n:\mBbbN{}]. win2strat(g@m p;n)
4. n : \mBbbZ{}
5. 0 < n
6. \mlambda{}moves.if (||moves|| =\msubz{} 2) then m moves[1] else s moves[1] seq-tl(seq-tl(moves)) fi
\mmember{} win2strat(g;n - 1)
7. \mneg{}(n = 0)
8. moves : strat2play(g;n - 1;\mlambda{}moves.if (||moves|| =\msubz{} 2)
then m moves[1]
else s moves[1] seq-tl(seq-tl(moves))
fi )
9. ||moves|| = (2 * n)
10. moves[1] \mmember{} \{p:Pos(g)| Legal1(InitialPos(g);p)\}
11. 2 \mleq{} n
12. 4 \mleq{} (2 * n)
13. s moves[1] \mmember{} win2strat(g@m moves[1];n - 1 - 1)
14. s moves[1] \mmember{} moves@0:\{f:strat2play(g@m moves[1];n - 1 - 1;s moves[1])| ||f|| = (2 * (n - 1))\}
{}\mrightarrow{} \{p:Pos(g@m moves[1])| Legal2(moves@0[(2 * (n - 1)) - 1];p)\}
15. seq-tl(seq-tl(moves)) \mmember{} \{f:strat2play(g@m moves[1];n - 1 - 1;s moves[1])|
||f|| = (2 * (n - 1))\}
16. (s moves[1] seq-tl(seq-tl(moves))) = (s moves[1] seq-tl(seq-tl(moves)))
\mvdash{} \{p:Pos(g@m moves[1])| Legal2(seq-tl(seq-tl(moves))[(2 * (n - 1)) - 1];p)\} \msubseteq{}r \{p:Pos(g)|
Legal2(moves[(2
* n) - 1];p)\}
By
Latex:
(D 0 THENA Auto)
Home
Index