Step
*
1
1
2
1
1
1
1
2
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]))
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]))}
BY
{ (DupHyp (-1)
THEN (D -1 With ⌜k + 1⌝ THENA Auto)
THEN (D -1 THEN Thin (-1))
THEN Reduce -1
THEN (D -2 With ⌜k⌝ THENA Auto)
THEN D -1
THEN Thin (-2)
THEN (D -1 THENA Auto)
THEN Reduce -1
THEN D -1
THEN D -3
THEN D -2
THEN (MemTypeCD THENW Auto)
THEN Try (Trivial)) }
1
.....set predicate.....
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. Legal1(moves[2 * (k + 1)];moves[(2 * (k + 1)) + 1])
25. Legal2(moves[(2 * k) + 1];moves[2 * (k + 1)])
26. moves[2 * (k + 1)]
= if (||play-truncate(moves;2 * (k + 1))|| =z 2)
then m play-truncate(moves;2 * (k + 1))[1]
else s play-truncate(moves;2 * (k + 1))[1] seq-tl(seq-tl(play-truncate(moves;2 * (k + 1))))
fi
∈ Pos(g)
⊢ (((2 * k) + 2) ≤ ||seq-tl(seq-tl(moves))||)
∧ Legal1(seq-tl(seq-tl(moves))[2 * k];seq-tl(seq-tl(moves))[(2 * k) + 1])
∧ (seq-tl(seq-tl(moves))[2 * k] = (s moves[1] play-truncate(seq-tl(seq-tl(moves));2 * k)) ∈ Pos(g@m moves[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. Legal1(moves[2 * (k + 1)];moves[(2 * (k + 1)) + 1])
25. Legal2(moves[(2 * k) + 1];moves[2 * (k + 1)])
26. moves[2 * (k + 1)]
= if (||play-truncate(moves;2 * (k + 1))|| =z 2)
then m play-truncate(moves;2 * (k + 1))[1]
else s play-truncate(moves;2 * (k + 1))[1] seq-tl(seq-tl(play-truncate(moves;2 * (k + 1))))
fi
∈ Pos(g)
27. moves@0 : sequence(Pos(g@m moves[1]))
28. ((2 * k) + 2) ≤ ||moves@0||
29. Legal1(moves@0[2 * k];moves@0[(2 * k) + 1])
⊢ 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]))
18. k : \mBbbZ{}
19. 0 < k
20. k \mleq{} (n - 1 - 1)
21. \mneg{}(k = 0)
22. seq-tl(seq-tl(moves)) \mmember{} strat2play(g@m moves[1];k - 1;s moves[1])
23. moves[0] = InitialPos(g)
24. \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 * k) + 2) \mleq{} ||moves@0||)
\mwedge{} Legal1(moves@0[2 * k];moves@0[(2 * k) + 1])
\mwedge{} (moves@0[2 * k]
= (s moves[1] play-truncate(seq-tl(seq-tl(moves));2 * k)))\}
By
Latex:
(DupHyp (-1)
THEN (D -1 With \mkleeneopen{}k + 1\mkleeneclose{} THENA Auto)
THEN (D -1 THEN Thin (-1))
THEN Reduce -1
THEN (D -2 With \mkleeneopen{}k\mkleeneclose{} THENA Auto)
THEN D -1
THEN Thin (-2)
THEN (D -1 THENA Auto)
THEN Reduce -1
THEN D -1
THEN D -3
THEN D -2
THEN (MemTypeCD THENW Auto)
THEN Try (Trivial))
Home
Index