---

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


1. g : SimpleGame
2. n : ℕ
3. x : s:win2strat(sg-normalize(g);n - 1) ⋂ moves:{f:strat2play(sg-normalize(g);n - 1;s)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Po\000Cs(sg-normalize(g))| 
                                                                        Legal2(moves[(2 * n) - 1];p)} 
4. x ∈ win2strat(sg-normalize(g);n - 1)
5. x ∈ moves:{f:strat2play(sg-normalize(g);n - 1;x)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(sg-normalize(g))| 
                                                                    Legal2(moves[(2 * n) - 1];p)} 
6. ¬(n = 0 ∈ ℤ)
7. ¬(n = 0 ∈ ℤ)
8. moves : {f:strat2play(g;n - 1;x)| ||f|| = (2 * n) ∈ ℤ} 
9. win2strat(g;n - 1) ≡ win2strat(sg-normalize(g);n - 1)
⊢ x moves ∈ {p:Pos(g)| Legal2(moves[(2 * n) - 1];p)} 
BY
{ (PromoteHyp (-1) 3 THEN (Assert 0 < n BY Auto) THEN PromoteHyp (-1) 3) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
(PromoteHyp  (-1)  3  THEN  (Assert  0  <  n  BY  Auto)  THEN  PromoteHyp  (-1)  3)

---

Home Index