Step
*
1
1
2
1
1
1
1
2
1
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]))
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])}
BY
{ (DupHyp (-1)
THEN (D -1 With ⌜1⌝ THENA Auto)
THEN (D -1 THEN Thin (-1))
THEN Reduce -1
THEN (D -2 With ⌜0⌝ THENA Auto)
THEN D -1
THEN Thin (-2)
THEN (D -1 THENA Auto)
THEN Reduce -1
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. ↓Legal1(moves[2];moves[3])
22. ↓Legal2(moves[1];moves[2])
23. moves[2]
= if (||play-truncate(moves;2)|| =z 2)
then m play-truncate(moves;2)[1]
else s play-truncate(moves;2)[1] seq-tl(seq-tl(play-truncate(moves;2)))
fi
∈ 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])}
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]))
18. k : \mBbbZ{}
19. 0 \mleq{} (n - 1 - 1)
20. moves[0] = InitialPos(g)
21. \mforall{}i:\mBbbN{}(n - 1) + 1
((\mdownarrow{}Legal1(moves[2 * i];moves[(2 * i) + 1]))
\mwedge{} (i < n - 1
{}\mRightarrow{} ((\mdownarrow{}Legal2(moves[(2 * i) + 1];moves[2 * (i + 1)]))
\mwedge{} (moves[2 * (i + 1)]
= ((\mlambda{}moves....)
play-truncate(moves;2 * (i + 1)))))))
\mvdash{} seq-tl(seq-tl(moves)) \mmember{} \{moves@0:sequence(Pos(g@m moves[1]))|
(2 \mleq{} ||moves@0||)
\mwedge{} (moves@0[0] = InitialPos(g@m moves[1]))
\mwedge{} Legal1(moves@0[0];moves@0[1])\}
By
Latex:
(DupHyp (-1)
THEN (D -1 With \mkleeneopen{}1\mkleeneclose{} THENA Auto)
THEN (D -1 THEN Thin (-1))
THEN Reduce -1
THEN (D -2 With \mkleeneopen{}0\mkleeneclose{} THENA Auto)
THEN D -1
THEN Thin (-2)
THEN (D -1 THENA Auto)
THEN Reduce -1
THEN D -1)
Home
Index