---

Step * 1 2 1 of Lemma strat2play-add

.....assertion..... 
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||
⊢ (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) ∈ ℤ}  ⟶ {p:Pos(g)| Legal2(moves[(2 * (n + 1)) - 1];p)} \000C BY
         (Unfold `win2strat` 3
          THEN (SplitOnHypITE 3  THENA Auto)
          THEN Try ((Assert ⌜False⌝⋅ THEN Complete (Auto)))
          THEN DepIsectHD 3
          THEN NthHypSq 5 
          THEN 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)} 
⊢ (s play-truncate(seq-add(seq-add(moves;x);y);2 * (n + 1))) = (s moves) ∈ Pos(g)

---

Latex:

---

Latex:
.....assertion..... 
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||
\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{}  \{p:Pos(g)| 
                                                                                                                  Legal2(moves[(2  *  (n  +  1))  -  1];p)\}    BY
              (Unfold  `win2strat`  3
                THEN  (SplitOnHypITE  3    THENA  Auto)
                THEN  Try  ((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Complete  (Auto)))
                THEN  DepIsectHD  3
                THEN  NthHypSq  5 
                THEN  Auto))

---

Home Index