---

Step * 1 2 1 1 2 of Lemma strat2play-add


1. g : SimpleGame
2. n : ℕ
3. s : win2strat(g;n + 1)
4. moves : strat2play(g;n;s)
5. ||moves|| = ((2 * n) + 2) ∈ ℤ
6. s moves ∈ Pos(g)
7. x : Pos(g)
8. y : Pos(g)
9. Legal1(x;y)
10. x = (s moves) ∈ Pos(g)
11. ¬((n + 1) = 0 ∈ ℤ)
12. moves ∈ sequence(Pos(g))
13. ((2 * n) + 2) ≤ ||moves||
14. s ∈ moves:{f:strat2play(g;n;s)| ||f|| = ((2 * n) + 2) ∈ ℤ}  ⟶ {p:Pos(g)| Legal2(moves[(2 * (n + 1)) - 1];p)} 
15. play-truncate(seq-add(seq-add(moves;x);y);2 * (n + 1)) = moves ∈ {f:strat2play(g;n;s)| ||f|| = ((2 * n) + 2) ∈ ℤ} 
⊢ (s play-truncate(seq-add(seq-add(moves;x);y);2 * (n + 1))) = (s moves) ∈ Pos(g)
BY
{ (Assert s ∈ moves:{f:strat2play(g;n;s)| ||f|| = ((2 * n) + 2) ∈ ℤ}  ⟶ Pos(g) BY
         Auto) }

1
1. g : SimpleGame
2. n : ℕ
3. s : win2strat(g;n + 1)
4. moves : strat2play(g;n;s)
5. ||moves|| = ((2 * n) + 2) ∈ ℤ
6. s moves ∈ Pos(g)
7. x : Pos(g)
8. y : Pos(g)
9. Legal1(x;y)
10. x = (s moves) ∈ Pos(g)
11. ¬((n + 1) = 0 ∈ ℤ)
12. moves ∈ sequence(Pos(g))
13. ((2 * n) + 2) ≤ ||moves||
14. s ∈ moves:{f:strat2play(g;n;s)| ||f|| = ((2 * n) + 2) ∈ ℤ}  ⟶ {p:Pos(g)| Legal2(moves[(2 * (n + 1)) - 1];p)} 
15. play-truncate(seq-add(seq-add(moves;x);y);2 * (n + 1)) = moves ∈ {f:strat2play(g;n;s)| ||f|| = ((2 * n) + 2) ∈ ℤ} 
16. s ∈ moves:{f:strat2play(g;n;s)| ||f|| = ((2 * n) + 2) ∈ ℤ}  ⟶ Pos(g)
⊢ (s play-truncate(seq-add(seq-add(moves;x);y);2 * (n + 1))) = (s moves) ∈ Pos(g)

---

Latex:

---

Latex:

1.  g  :  SimpleGame
2.  n  :  \mBbbN{}
3.  s  :  win2strat(g;n  +  1)
4.  moves  :  strat2play(g;n;s)
5.  ||moves||  =  ((2  *  n)  +  2)
6.  s  moves  \mmember{}  Pos(g)
7.  x  :  Pos(g)
8.  y  :  Pos(g)
9.  Legal1(x;y)
10.  x  =  (s  moves)
11.  \mneg{}((n  +  1)  =  0)
12.  moves  \mmember{}  sequence(Pos(g))
13.  ((2  *  n)  +  2)  \mleq{}  ||moves||
14.  s  \mmember{}  moves:\{f:strat2play(g;n;s)|  ||f||  =  ((2  *  n)  +  2)\}    {}\mrightarrow{}  \{p:Pos(g)|  Legal2(moves[(2  *  (n  +  1))\000C  -  1];p)\} 
15.  play-truncate(seq-add(seq-add(moves;x);y);2  *  (n  +  1))  =  moves
\mvdash{}  (s  play-truncate(seq-add(seq-add(moves;x);y);2  *  (n  +  1)))  =  (s  moves)


By

---

Latex:
(Assert  s  \mmember{}  moves:\{f:strat2play(g;n;s)|  ||f||  =  ((2  *  n)  +  2)\}    {}\mrightarrow{}  Pos(g)  BY
              Auto)

---

Home Index