---

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


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 : strat2play(g;n - 1;x)
11. ||moves|| = (2 * n) ∈ ℤ
⊢ moves ∈ strat2play(sg-normalize(g);n - 1;x)
BY
{ ((Assert x ∈ win2strat(g;n - 1) BY
          (SubsumeC ⌜win2strat(sg-normalize(g);n - 1)⌝⋅ THEN Auto))
   THEN OnVar `moves' Strat2PlaySubtype
   THEN (Assert sequence(Pos(sg-normalize(g))) ⊆r sequence(Pos(g)) BY
               (RWO "sg-pos-normalize" 0 THEN Auto))
   THEN (OnVar `moves' Strat2PlayInvariant THENA Auto)
   THEN Assert ⌜moves ∈ sequence(Pos(sg-normalize(g)))⌝⋅) }

1
.....assertion..... 
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 : strat2play(g;n - 1;x)
11. ||moves|| = (2 * n) ∈ ℤ
12. x ∈ win2strat(g;n - 1)
13. moves ∈ {moves:sequence(Pos(g))| ((2 * (n - 1)) + 2) ≤ ||moves||} 
14. sequence(Pos(sg-normalize(g))) ⊆r sequence(Pos(g))
15. (moves[0] = InitialPos(g) ∈ Pos(g))
∧ (∀i:ℕ(n - 1) + 1
     ((↓Legal1(moves[2 * i];moves[(2 * i) + 1]))
     ∧ (i < n - 1
       ⇒ ((↓Legal2(moves[(2 * i) + 1];moves[2 * (i + 1)]))
          ∧ (moves[2 * (i + 1)] = (x play-truncate(moves;2 * (i + 1))) ∈ Pos(g))))))
⊢ moves ∈ sequence(Pos(sg-normalize(g)))

2
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 : strat2play(g;n - 1;x)
11. ||moves|| = (2 * n) ∈ ℤ
12. x ∈ win2strat(g;n - 1)
13. moves ∈ {moves:sequence(Pos(g))| ((2 * (n - 1)) + 2) ≤ ||moves||} 
14. sequence(Pos(sg-normalize(g))) ⊆r sequence(Pos(g))
15. (moves[0] = InitialPos(g) ∈ Pos(g))
∧ (∀i:ℕ(n - 1) + 1
     ((↓Legal1(moves[2 * i];moves[(2 * i) + 1]))
     ∧ (i < n - 1
       ⇒ ((↓Legal2(moves[(2 * i) + 1];moves[2 * (i + 1)]))
          ∧ (moves[2 * (i + 1)] = (x play-truncate(moves;2 * (i + 1))) ∈ Pos(g))))))
16. moves ∈ sequence(Pos(sg-normalize(g)))
⊢ moves ∈ strat2play(sg-normalize(g);n - 1;x)

---

Latex:

---

Latex:

1.  g  :  SimpleGame
2.  n  :  \mBbbN{}
3.  0  <  n
4.  win2strat(g;n  -  1)  \mequiv{}  win2strat(sg-normalize(g);n  -  1)
5.  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)\} 
6.  x  \mmember{}  win2strat(sg-normalize(g);n  -  1)
7.  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)\} 
8.  \mneg{}(n  =  0)
9.  \mneg{}(n  =  0)
10.  moves  :  strat2play(g;n  -  1;x)
11.  ||moves||  =  (2  *  n)
\mvdash{}  moves  \mmember{}  strat2play(sg-normalize(g);n  -  1;x)


By

---

Latex:
((Assert  x  \mmember{}  win2strat(g;n  -  1)  BY
                (SubsumeC  \mkleeneopen{}win2strat(sg-normalize(g);n  -  1)\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  OnVar  `moves'  Strat2PlaySubtype
  THEN  (Assert  sequence(Pos(sg-normalize(g)))  \msubseteq{}r  sequence(Pos(g))  BY
                          (RWO  "sg-pos-normalize"  0  THEN  Auto))
  THEN  (OnVar  `moves'  Strat2PlayInvariant  THENA  Auto)
  THEN  Assert  \mkleeneopen{}moves  \mmember{}  sequence(Pos(sg-normalize(g)))\mkleeneclose{}\mcdot{})

---

Home Index