---

Step * 1 1 1 of Lemma sg-normalize-win2

.....aux..... 
1. g : SimpleGame
2. n : ℕ
3. ∀n:ℕn. win2strat(g;n) ≡ win2strat(sg-normalize(g);n)
4. x : s:win2strat(g;n - 1) ⋂ moves:{f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(g)| Legal2(moves[(2 * n) -\000C 1];p)} 
5. x ∈ win2strat(g;n - 1)
6. x ∈ moves:{f:strat2play(g;n - 1;x)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(g)| Legal2(moves[(2 * n) - 1];p)} 
7. ¬(n = 0 ∈ ℤ)
8. ¬(n = 0 ∈ ℤ)
9. win2strat(g;n - 1) ⊆r win2strat(sg-normalize(g);n - 1)
10. win2strat(sg-normalize(g);n - 1) ⊆r win2strat(g;n - 1)
11. moves : strat2play(sg-normalize(g);n - 1;x)
12. ||moves|| = (2 * n) ∈ ℤ
⊢ moves ∈ strat2play(g;n - 1;x)
BY
{ Assert ⌜∀k:ℕ
            ∀[x:win2strat(g;k)]. ∀[moves:strat2play(sg-normalize(g);k;x)].  (moves ∈ strat2play(g;k;x)) supposing k < n⌝
⋅ }

1
.....assertion..... 
1. g : SimpleGame
2. n : ℕ
3. ∀n:ℕn. win2strat(g;n) ≡ win2strat(sg-normalize(g);n)
4. x : s:win2strat(g;n - 1) ⋂ moves:{f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(g)| Legal2(moves[(2 * n) -\000C 1];p)} 
5. x ∈ win2strat(g;n - 1)
6. x ∈ moves:{f:strat2play(g;n - 1;x)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(g)| Legal2(moves[(2 * n) - 1];p)} 
7. ¬(n = 0 ∈ ℤ)
8. ¬(n = 0 ∈ ℤ)
9. win2strat(g;n - 1) ⊆r win2strat(sg-normalize(g);n - 1)
10. win2strat(sg-normalize(g);n - 1) ⊆r win2strat(g;n - 1)
11. moves : strat2play(sg-normalize(g);n - 1;x)
12. ||moves|| = (2 * n) ∈ ℤ
⊢ ∀k:ℕ. ∀[x:win2strat(g;k)]. ∀[moves:strat2play(sg-normalize(g);k;x)].  (moves ∈ strat2play(g;k;x)) supposing k < n

2
1. g : SimpleGame
2. n : ℕ
3. ∀n:ℕn. win2strat(g;n) ≡ win2strat(sg-normalize(g);n)
4. x : s:win2strat(g;n - 1) ⋂ moves:{f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(g)| Legal2(moves[(2 * n) -\000C 1];p)} 
5. x ∈ win2strat(g;n - 1)
6. x ∈ moves:{f:strat2play(g;n - 1;x)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(g)| Legal2(moves[(2 * n) - 1];p)} 
7. ¬(n = 0 ∈ ℤ)
8. ¬(n = 0 ∈ ℤ)
9. win2strat(g;n - 1) ⊆r win2strat(sg-normalize(g);n - 1)
10. win2strat(sg-normalize(g);n - 1) ⊆r win2strat(g;n - 1)
11. moves : strat2play(sg-normalize(g);n - 1;x)
12. ||moves|| = (2 * n) ∈ ℤ
13. ∀k:ℕ. ∀[x:win2strat(g;k)]. ∀[moves:strat2play(sg-normalize(g);k;x)].  (moves ∈ strat2play(g;k;x)) supposing k < n
⊢ moves ∈ strat2play(g;n - 1;x)

---

Latex:

---

Latex:
.....aux..... 
1.  g  :  SimpleGame
2.  n  :  \mBbbN{}
3.  \mforall{}n:\mBbbN{}n.  win2strat(g;n)  \mequiv{}  win2strat(sg-normalize(g);n)
4.  x  :  s:win2strat(g;n  -  1)  \mcap{}  moves:\{f:strat2play(g;n  -  1;s)|  ||f||  =  (2  *  n)\}    {}\mrightarrow{}  \{p:Pos(g)|  Legal2\000C(moves[(2  *  n)  -  1];p)\} 
5.  x  \mmember{}  win2strat(g;n  -  1)
6.  x  \mmember{}  moves:\{f:strat2play(g;n  -  1;x)|  ||f||  =  (2  *  n)\}    {}\mrightarrow{}  \{p:Pos(g)|  Legal2(moves[(2  *  n)  -  1];p)\}\000C 
7.  \mneg{}(n  =  0)
8.  \mneg{}(n  =  0)
9.  win2strat(g;n  -  1)  \msubseteq{}r  win2strat(sg-normalize(g);n  -  1)
10.  win2strat(sg-normalize(g);n  -  1)  \msubseteq{}r  win2strat(g;n  -  1)
11.  moves  :  strat2play(sg-normalize(g);n  -  1;x)
12.  ||moves||  =  (2  *  n)
\mvdash{}  moves  \mmember{}  strat2play(g;n  -  1;x)


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}k:\mBbbN{}
                    \mforall{}[x:win2strat(g;k)].  \mforall{}[moves:strat2play(sg-normalize(g);k;x)].
                        (moves  \mmember{}  strat2play(g;k;x)) 
                    supposing  k  <  n\mkleeneclose{}\mcdot{}

---

Home Index