---

Step * 1 2 1 1 1 1 2 2 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) ∈ ℤ
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)
16. ∀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)))))
17. moves ∈ sequence(Pos(sg-normalize(g)))
18. Legal1(moves[0];moves[1])
19. k : ℤ
20. 0 < k
21. k ≤ (n - 1)
22. ¬(k = 0 ∈ ℤ)
23. moves ∈ strat2play(sg-normalize(g);k - 1;x)
⊢ moves ∈ {moves@0:sequence(Pos(sg-normalize(g)))| 
           (((2 * k) + 2) ≤ ||moves@0||)
           ∧ Legal1(moves@0[2 * k];moves@0[(2 * k) + 1])
           ∧ (moves@0[2 * k] = (x play-truncate(moves;2 * k)) ∈ Pos(sg-normalize(g)))} 
BY
{ (DupHyp (-8)
   THEN (D -1 With ⌜k - 1⌝  THENA Auto)
   THEN (RepeatFor 2 (D -1) THENA Auto)
   THEN D -1
   THEN RepeatFor 2 (Thin (-2))
   THEN (Subst' (k - 1) + 1 ~ k -1 THENA Auto)
   THEN (D -9 With ⌜k⌝  THENA Auto)
   THEN D -1
   THEN Thin (-1)
   THEN D -1) }

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 : 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)
16. moves ∈ sequence(Pos(sg-normalize(g)))
17. Legal1(moves[0];moves[1])
18. k : ℤ
19. 0 < k
20. k ≤ (n - 1)
21. ¬(k = 0 ∈ ℤ)
22. moves ∈ strat2play(sg-normalize(g);k - 1;x)
23. moves[2 * k] = (x play-truncate(moves;2 * k)) ∈ Pos(g)
24. Legal1(moves[2 * k];moves[(2 * k) + 1])
⊢ moves ∈ {moves@0:sequence(Pos(sg-normalize(g)))| 
           (((2 * k) + 2) ≤ ||moves@0||)
           ∧ Legal1(moves@0[2 * k];moves@0[(2 * k) + 1])
           ∧ (moves@0[2 * k] = (x play-truncate(moves;2 * k)) ∈ Pos(sg-normalize(g)))} 

---

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)
12.  x  \mmember{}  win2strat(g;n  -  1)
13.  moves  \mmember{}  \{moves:sequence(Pos(g))|  ((2  *  (n  -  1))  +  2)  \mleq{}  ||moves||\} 
14.  sequence(Pos(sg-normalize(g)))  \msubseteq{}r  sequence(Pos(g))
15.  moves[0]  =  InitialPos(g)
16.  \mforall{}i:\mBbbN{}(n  -  1)  +  1
            ((\mdownarrow{}Legal1(moves[2  *  i];moves[(2  *  i)  +  1]))
            \mwedge{}  (i  <  n  -  1
                {}\mRightarrow{}  ((\mdownarrow{}Legal2(moves[(2  *  i)  +  1];moves[2  *  (i  +  1)]))
                      \mwedge{}  (moves[2  *  (i  +  1)]  =  (x  play-truncate(moves;2  *  (i  +  1)))))))
17.  moves  \mmember{}  sequence(Pos(sg-normalize(g)))
18.  Legal1(moves[0];moves[1])
19.  k  :  \mBbbZ{}
20.  0  <  k
21.  k  \mleq{}  (n  -  1)
22.  \mneg{}(k  =  0)
23.  moves  \mmember{}  strat2play(sg-normalize(g);k  -  1;x)
\mvdash{}  moves  \mmember{}  \{moves@0:sequence(Pos(sg-normalize(g)))| 
                      (((2  *  k)  +  2)  \mleq{}  ||moves@0||)
                      \mwedge{}  Legal1(moves@0[2  *  k];moves@0[(2  *  k)  +  1])
                      \mwedge{}  (moves@0[2  *  k]  =  (x  play-truncate(moves;2  *  k)))\} 


By

---

Latex:
(DupHyp  (-8)
  THEN  (D  -1  With  \mkleeneopen{}k  -  1\mkleeneclose{}    THENA  Auto)
  THEN  (RepeatFor  2  (D  -1)  THENA  Auto)
  THEN  D  -1
  THEN  RepeatFor  2  (Thin  (-2))
  THEN  (Subst'  (k  -  1)  +  1  \msim{}  k  -1  THENA  Auto)
  THEN  (D  -9  With  \mkleeneopen{}k\mkleeneclose{}    THENA  Auto)
  THEN  D  -1
  THEN  Thin  (-1)
  THEN  D  -1)

---

Home Index