Step
*
3
of Lemma
strat2play-longer
.....eq aux.....
1. g : SimpleGame
2. n : ℤ
3. 0 < n
4. <Ax, Ax> ∈ ∀[s:win2strat(g;n - 1)]. ∀[moves:strat2play(g;n - 1;s)]. ∀[x:sequence(Pos(g))].
((x ∈ strat2play(g;n - 1;s)) ∧ (seq-truncate(x;||moves||) = moves ∈ strat2play(g;n - 1;s))) supposing
((seq-truncate(x;||moves||) = moves ∈ sequence(Pos(g))) and
(||moves|| ≤ ||x||))
5. s : win2strat(g;n)
6. moves : strat2play(g;n;s)
7. x : sequence(Pos(g))
8. moves ∈ {moves:sequence(Pos(g))| ((2 * n) + 2) ≤ ||moves||}
9. ||moves|| ≤ ||x||
10. seq-truncate(x;||moves||) = moves ∈ sequence(Pos(g))
11. ∀i:ℕ||moves||. (x[i] = moves[i] ∈ Pos(g))
⊢ x ∈ strat2play(g;n;s)
BY
{ ((Assert ∀[s:win2strat(g;n - 1)]. ∀[moves:strat2play(g;n - 1;s)]. ∀[x:sequence(Pos(g))].
((x ∈ strat2play(g;n - 1;s)) ∧ (seq-truncate(x;||moves||) = moves ∈ strat2play(g;n - 1;s))) supposing
((seq-truncate(x;||moves||) = moves ∈ sequence(Pos(g))) and
(||moves|| ≤ ||x||)) BY
(UseWitness ⌜<Ax, Ax>⌝⋅ THEN Trivial))
THEN Thin 4
THEN PromoteHyp (-1) 4
THEN Unfold `strat2play` -6
THEN (SplitOnHypITE -6 THENA Auto)
THEN Try ((Assert ⌜False⌝⋅ THEN Complete (Auto)))
THEN DepIsectHD (-7)
THEN Unfold `strat2play` 0
THEN (SplitOnConclITE THENA Auto)
THEN Try ((Assert ⌜False⌝⋅ THEN Complete (Auto)))
THEN DepIsectCD
THEN InstHyp [⌜s⌝;⌜moves⌝;⌜x⌝] 4⋅
THEN (Auto THEN All (RepUR ``play-len play-item``))
THEN (MemTypeHD 8 THENA Auto)
THEN All (Fold `member`)
THEN ExRepD
THEN MemTypeCD
THEN Auto) }
1
1. g : SimpleGame
2. n : ℤ
3. 0 < n
4. ∀[s:win2strat(g;n - 1)]. ∀[moves:strat2play(g;n - 1;s)]. ∀[x:sequence(Pos(g))].
((x ∈ strat2play(g;n - 1;s)) ∧ (seq-truncate(x;||moves||) = moves ∈ strat2play(g;n - 1;s))) supposing
((seq-truncate(x;||moves||) = moves ∈ sequence(Pos(g))) and
(||moves|| ≤ ||x||))
5. s : win2strat(g;n)
6. moves : f:strat2play(g;n - 1;s) ⋂ {moves:sequence(Pos(g))|
(((2 * n) + 2) ≤ ||moves||)
∧ Legal1(moves[2 * n];moves[(2 * n) + 1])
∧ (moves[2 * n] = (s play-truncate(f;2 * n)) ∈ Pos(g))}
7. moves ∈ strat2play(g;n - 1;s)
8. moves ∈ sequence(Pos(g))
9. ((2 * n) + 2) ≤ ||moves||
10. Legal1(moves[2 * n];moves[(2 * n) + 1])
11. moves[2 * n] = (s play-truncate(moves;2 * n)) ∈ Pos(g)
12. x : sequence(Pos(g))
13. moves ∈ {moves:sequence(Pos(g))| ((2 * n) + 2) ≤ ||moves||}
14. ||moves|| ≤ ||x||
15. seq-truncate(x;||moves||) = moves ∈ sequence(Pos(g))
16. ∀i:ℕ||moves||. (x[i] = moves[i] ∈ Pos(g))
17. ¬(n = 0 ∈ ℤ)
18. ¬(n = 0 ∈ ℤ)
19. x ∈ strat2play(g;n - 1;s)
20. seq-truncate(x;||moves||) = moves ∈ strat2play(g;n - 1;s)
21. ((2 * n) + 2) ≤ ||x||
⊢ Legal1(x[2 * n];x[(2 * n) + 1])
2
1. g : SimpleGame
2. n : ℤ
3. 0 < n
4. ∀[s:win2strat(g;n - 1)]. ∀[moves:strat2play(g;n - 1;s)]. ∀[x:sequence(Pos(g))].
((x ∈ strat2play(g;n - 1;s)) ∧ (seq-truncate(x;||moves||) = moves ∈ strat2play(g;n - 1;s))) supposing
((seq-truncate(x;||moves||) = moves ∈ sequence(Pos(g))) and
(||moves|| ≤ ||x||))
5. s : win2strat(g;n)
6. moves : f:strat2play(g;n - 1;s) ⋂ {moves:sequence(Pos(g))|
(((2 * n) + 2) ≤ ||moves||)
∧ Legal1(moves[2 * n];moves[(2 * n) + 1])
∧ (moves[2 * n] = (s play-truncate(f;2 * n)) ∈ Pos(g))}
7. moves ∈ strat2play(g;n - 1;s)
8. moves ∈ sequence(Pos(g))
9. ((2 * n) + 2) ≤ ||moves||
10. Legal1(moves[2 * n];moves[(2 * n) + 1])
11. moves[2 * n] = (s play-truncate(moves;2 * n)) ∈ Pos(g)
12. x : sequence(Pos(g))
13. moves ∈ {moves:sequence(Pos(g))| ((2 * n) + 2) ≤ ||moves||}
14. ||moves|| ≤ ||x||
15. seq-truncate(x;||moves||) = moves ∈ sequence(Pos(g))
16. ∀i:ℕ||moves||. (x[i] = moves[i] ∈ Pos(g))
17. ¬(n = 0 ∈ ℤ)
18. ¬(n = 0 ∈ ℤ)
19. x ∈ strat2play(g;n - 1;s)
20. seq-truncate(x;||moves||) = moves ∈ strat2play(g;n - 1;s)
21. ((2 * n) + 2) ≤ ||x||
22. Legal1(x[2 * n];x[(2 * n) + 1])
⊢ x[2 * n] = (s play-truncate(x;2 * n)) ∈ Pos(g)
3
1. g : SimpleGame
2. n : ℤ
3. 0 < n
4. ∀[s:win2strat(g;n - 1)]. ∀[moves:strat2play(g;n - 1;s)]. ∀[x:sequence(Pos(g))].
((x ∈ strat2play(g;n - 1;s)) ∧ (seq-truncate(x;||moves||) = moves ∈ strat2play(g;n - 1;s))) supposing
((seq-truncate(x;||moves||) = moves ∈ sequence(Pos(g))) and
(||moves|| ≤ ||x||))
5. s : win2strat(g;n)
6. moves : f:strat2play(g;n - 1;s) ⋂ {moves:sequence(Pos(g))|
(((2 * n) + 2) ≤ ||moves||)
∧ Legal1(moves[2 * n];moves[(2 * n) + 1])
∧ (moves[2 * n] = (s play-truncate(f;2 * n)) ∈ Pos(g))}
7. moves ∈ strat2play(g;n - 1;s)
8. moves ∈ sequence(Pos(g))
9. ((2 * n) + 2) ≤ ||moves||
10. Legal1(moves[2 * n];moves[(2 * n) + 1])
11. moves[2 * n] = (s play-truncate(moves;2 * n)) ∈ Pos(g)
12. x : sequence(Pos(g))
13. moves ∈ {moves:sequence(Pos(g))| ((2 * n) + 2) ≤ ||moves||}
14. ||moves|| ≤ ||x||
15. seq-truncate(x;||moves||) = moves ∈ sequence(Pos(g))
16. ∀i:ℕ||moves||. (x[i] = moves[i] ∈ Pos(g))
17. ¬(n = 0 ∈ ℤ)
18. ¬(n = 0 ∈ ℤ)
19. x ∈ strat2play(g;n - 1;s)
20. seq-truncate(x;||moves||) = moves ∈ strat2play(g;n - 1;s)
21. m1 : sequence(Pos(g))
22. ((2 * n) + 2) ≤ ||m1||
23. Legal1(m1[2 * n];m1[(2 * n) + 1])
⊢ s play-truncate(x;2 * n) ∈ Pos(g)
Latex:
Latex:
.....eq aux.....
1. g : SimpleGame
2. n : \mBbbZ{}
3. 0 < n
4. <Ax, Ax> \mmember{} \mforall{}[s:win2strat(g;n - 1)]. \mforall{}[moves:strat2play(g;n - 1;s)]. \mforall{}[x:sequence(Pos(g))].
((x \mmember{} strat2play(g;n - 1;s)) \mwedge{} (seq-truncate(x;||moves||) = moves)) supposing
((seq-truncate(x;||moves||) = moves) and
(||moves|| \mleq{} ||x||))
5. s : win2strat(g;n)
6. moves : strat2play(g;n;s)
7. x : sequence(Pos(g))
8. moves \mmember{} \{moves:sequence(Pos(g))| ((2 * n) + 2) \mleq{} ||moves||\}
9. ||moves|| \mleq{} ||x||
10. seq-truncate(x;||moves||) = moves
11. \mforall{}i:\mBbbN{}||moves||. (x[i] = moves[i])
\mvdash{} x \mmember{} strat2play(g;n;s)
By
Latex:
((Assert \mforall{}[s:win2strat(g;n - 1)]. \mforall{}[moves:strat2play(g;n - 1;s)]. \mforall{}[x:sequence(Pos(g))].
((x \mmember{} strat2play(g;n - 1;s)) \mwedge{} (seq-truncate(x;||moves||) = moves)) supposing
((seq-truncate(x;||moves||) = moves) and
(||moves|| \mleq{} ||x||)) BY
(UseWitness \mkleeneopen{}<Ax, Ax>\mkleeneclose{}\mcdot{} THEN Trivial))
THEN Thin 4
THEN PromoteHyp (-1) 4
THEN Unfold `strat2play` -6
THEN (SplitOnHypITE -6 THENA Auto)
THEN Try ((Assert \mkleeneopen{}False\mkleeneclose{}\mcdot{} THEN Complete (Auto)))
THEN DepIsectHD (-7)
THEN Unfold `strat2play` 0
THEN (SplitOnConclITE THENA Auto)
THEN Try ((Assert \mkleeneopen{}False\mkleeneclose{}\mcdot{} THEN Complete (Auto)))
THEN DepIsectCD
THEN InstHyp [\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}moves\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}] 4\mcdot{}
THEN (Auto THEN All (RepUR ``play-len play-item``))
THEN (MemTypeHD 8 THENA Auto)
THEN All (Fold `member`)
THEN ExRepD
THEN MemTypeCD
THEN Auto)
Home
Index