Step
*
3
2
1
of Lemma
strat2play-longer
.....subterm..... T:t
3:n
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])
⊢ (s play-truncate(x;2 * n)) = (s play-truncate(moves;2 * n)) ∈ Pos(g)
BY
{ ((InstLemma `play-truncate_wf` [⌜g⌝;⌜n - 1⌝;⌜s⌝;⌜moves⌝;⌜2 * n⌝]⋅ THENA (Auto THEN Unfold `play-len` 0 THEN Auto))
THEN (InstHyp [⌜s⌝;⌜play-truncate(moves;2 * n)⌝;⌜seq-truncate(x;2 * n)⌝] 4⋅
THENA (Auto
THEN Unfold `play-truncate` 0
THEN Auto
THEN (RWO "seq-len-truncate" 0 THEN Auto)
THEN RWO "seq-truncate-truncate" 0
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||
22. Legal1(x[2 * n];x[(2 * n) + 1])
23. play-truncate(moves;2 * n) ∈ {moves:strat2play(g;n - 1;s)| ||moves|| = (2 * n) ∈ ℤ}
⊢ seq-truncate(x;2 * n) = seq-truncate(moves;2 * n) ∈ sequence(Pos(g))
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])
23. play-truncate(moves;2 * n) ∈ {moves:strat2play(g;n - 1;s)| ||moves|| = (2 * n) ∈ ℤ}
24. (seq-truncate(x;2 * n) ∈ strat2play(g;n - 1;s))
∧ (seq-truncate(seq-truncate(x;2 * n);||play-truncate(moves;2 * n)||)
= play-truncate(moves;2 * n)
∈ strat2play(g;n - 1;s))
⊢ (s play-truncate(x;2 * n)) = (s play-truncate(moves;2 * n)) ∈ Pos(g)
Latex:
Latex:
.....subterm..... T:t
3:n
1. g : SimpleGame
2. n : \mBbbZ{}
3. 0 < n
4. \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 : f:strat2play(g;n - 1;s) \mcap{} \{moves:sequence(Pos(g))|
(((2 * n) + 2) \mleq{} ||moves||)
\mwedge{} Legal1(moves[2 * n];moves[(2 * n) + 1])
\mwedge{} (moves[2 * n] = (s play-truncate(f;2 * n)))\}
7. moves \mmember{} strat2play(g;n - 1;s)
8. moves \mmember{} sequence(Pos(g))
9. ((2 * n) + 2) \mleq{} ||moves||
10. Legal1(moves[2 * n];moves[(2 * n) + 1])
11. moves[2 * n] = (s play-truncate(moves;2 * n))
12. x : sequence(Pos(g))
13. moves \mmember{} \{moves:sequence(Pos(g))| ((2 * n) + 2) \mleq{} ||moves||\}
14. ||moves|| \mleq{} ||x||
15. seq-truncate(x;||moves||) = moves
16. \mforall{}i:\mBbbN{}||moves||. (x[i] = moves[i])
17. \mneg{}(n = 0)
18. \mneg{}(n = 0)
19. x \mmember{} strat2play(g;n - 1;s)
20. seq-truncate(x;||moves||) = moves
21. ((2 * n) + 2) \mleq{} ||x||
22. Legal1(x[2 * n];x[(2 * n) + 1])
\mvdash{} (s play-truncate(x;2 * n)) = (s play-truncate(moves;2 * n))
By
Latex:
((InstLemma `play-truncate\_wf` [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}n - 1\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}moves\mkleeneclose{};\mkleeneopen{}2 * n\mkleeneclose{}]\mcdot{}
THENA (Auto THEN Unfold `play-len` 0 THEN Auto)
)
THEN (InstHyp [\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}play-truncate(moves;2 * n)\mkleeneclose{};\mkleeneopen{}seq-truncate(x;2 * n)\mkleeneclose{}] 4\mcdot{}
THENA (Auto
THEN Unfold `play-truncate` 0
THEN Auto
THEN (RWO "seq-len-truncate" 0 THEN Auto)
THEN RWO "seq-truncate-truncate" 0
THEN Auto)
)
)
Home
Index