Step
*
1
1
2
1
1
1
1
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. moves[1] ∈ {p:Pos(g)| Legal1(InitialPos(g);p)}
16. g@m moves[1] ∈ SimpleGame
17. seq-tl(seq-tl(moves)) ∈ sequence(Pos(g@m moves[1]))
⊢ seq-tl(seq-tl(moves)) ∈ strat2play(g@m moves[1];n - 1 - 1;s moves[1])
BY
{ (Strat2PlayWf' THEN (Strat2PlayInvariant 8 THENA Auto) THEN D -1) }
1
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. moves[1] ∈ {p:Pos(g)| Legal1(InitialPos(g);p)}
16. g@m moves[1] ∈ SimpleGame
17. seq-tl(seq-tl(moves)) ∈ sequence(Pos(g@m moves[1]))
18. k : ℤ
19. 0 ≤ (n - 1 - 1)
20. moves[0] = InitialPos(g) ∈ Pos(g)
21. ∀i:ℕ(n - 1) + 1
((↓Legal1(moves[2 * i];moves[(2 * i) + 1]))
∧ (i < n - 1
⇒ ((↓Legal2(moves[(2 * i) + 1];moves[2 * (i + 1)]))
∧ (moves[2 * (i + 1)]
= ((λmoves.if (||moves|| =z 2) then m moves[1] else s moves[1] seq-tl(seq-tl(moves)) fi )
play-truncate(moves;2 * (i + 1)))
∈ Pos(g)))))
⊢ seq-tl(seq-tl(moves)) ∈ {moves@0:sequence(Pos(g@m moves[1]))|
(2 ≤ ||moves@0||)
∧ (moves@0[0] = InitialPos(g@m moves[1]) ∈ Pos(g@m moves[1]))
∧ Legal1(moves@0[0];moves@0[1])}
2
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. moves[1] ∈ {p:Pos(g)| Legal1(InitialPos(g);p)}
16. g@m moves[1] ∈ SimpleGame
17. seq-tl(seq-tl(moves)) ∈ sequence(Pos(g@m moves[1]))
18. k : ℤ
19. 0 < k
20. k ≤ (n - 1 - 1)
21. ¬(k = 0 ∈ ℤ)
22. seq-tl(seq-tl(moves)) ∈ strat2play(g@m moves[1];k - 1;s moves[1])
23. moves[0] = InitialPos(g) ∈ Pos(g)
24. ∀i:ℕ(n - 1) + 1
((↓Legal1(moves[2 * i];moves[(2 * i) + 1]))
∧ (i < n - 1
⇒ ((↓Legal2(moves[(2 * i) + 1];moves[2 * (i + 1)]))
∧ (moves[2 * (i + 1)]
= ((λmoves.if (||moves|| =z 2) then m moves[1] else s moves[1] seq-tl(seq-tl(moves)) fi )
play-truncate(moves;2 * (i + 1)))
∈ Pos(g)))))
⊢ seq-tl(seq-tl(moves)) ∈ {moves@0:sequence(Pos(g@m moves[1]))|
(((2 * k) + 2) ≤ ||moves@0||)
∧ Legal1(moves@0[2 * k];moves@0[(2 * k) + 1])
∧ (moves@0[2 * k]
= (s moves[1] play-truncate(seq-tl(seq-tl(moves));2 * k))
∈ Pos(g@m moves[1]))}
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. moves[1] \mmember{} \{p:Pos(g)| Legal1(InitialPos(g);p)\}
16. g@m moves[1] \mmember{} SimpleGame
17. seq-tl(seq-tl(moves)) \mmember{} sequence(Pos(g@m moves[1]))
\mvdash{} seq-tl(seq-tl(moves)) \mmember{} strat2play(g@m moves[1];n - 1 - 1;s moves[1])
By
Latex:
(Strat2PlayWf' THEN (Strat2PlayInvariant 8 THENA Auto) THEN D -1)
Home
Index