---

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


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. x1 : Pos(g)
12. mvs : strat2play(g;n - 1;x)
13. ||mvs|| = (2 * n) ∈ ℤ
14. Legal2(mvs[(2 * n) - 1];x1)
15. mvs ∈ {moves:sequence(Pos(g))| ((2 * (n - 1)) + 2) ≤ ||moves||} 
16. ∀i:ℕ(2 * (n - 1)) + 1
      ((((i mod 2) = 0 ∈ ℤ) ⇒ (↓Legal1(mvs[i];mvs[i + 1]))) ∧ (((i mod 2) = 1 ∈ ℤ) ⇒ (↓Legal2(mvs[i];mvs[i + 1]))))
17. mvs[0] = InitialPos(g) ∈ Pos(g)
18. ∀i:ℕ(n - 1) + 1
      ((↓Legal1(mvs[2 * i];mvs[(2 * i) + 1]))
      ∧ (i < n - 1
        ⇒ ((↓Legal2(mvs[(2 * i) + 1];mvs[2 * (i + 1)]))
           ∧ (mvs[2 * (i + 1)] = (x play-truncate(mvs;2 * (i + 1))) ∈ Pos(g)))))
19. 1 ≤ n
20. (2 * 1) ≤ (2 * n)
21. 0 < (2 * n) + 1
22. if 0 <z 2 * n then mvs[0] else x1 fi  = InitialPos(g) ∈ Pos(g)
23. if ((2 * n) + 1) - 1 <z 2 * n then mvs[((2 * n) + 1) - 1] else x1 fi  = x1 ∈ Pos(g)
24. i : ℕ
25. ¬(2 * i) + 1 < 2 * n
26. (2 * i) + 1 < (2 * n) + 1
27. 2 * i < 2 * n
⊢ ↓Legal1(mvs[2 * i];x1)
BY
{ (Assert ((2 * i) + 1) = (2 * n) ∈ ℤ BY
         Auto) }

1
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. x1 : Pos(g)
12. mvs : strat2play(g;n - 1;x)
13. ||mvs|| = (2 * n) ∈ ℤ
14. Legal2(mvs[(2 * n) - 1];x1)
15. mvs ∈ {moves:sequence(Pos(g))| ((2 * (n - 1)) + 2) ≤ ||moves||} 
16. ∀i:ℕ(2 * (n - 1)) + 1
      ((((i mod 2) = 0 ∈ ℤ) ⇒ (↓Legal1(mvs[i];mvs[i + 1]))) ∧ (((i mod 2) = 1 ∈ ℤ) ⇒ (↓Legal2(mvs[i];mvs[i + 1]))))
17. mvs[0] = InitialPos(g) ∈ Pos(g)
18. ∀i:ℕ(n - 1) + 1
      ((↓Legal1(mvs[2 * i];mvs[(2 * i) + 1]))
      ∧ (i < n - 1
        ⇒ ((↓Legal2(mvs[(2 * i) + 1];mvs[2 * (i + 1)]))
           ∧ (mvs[2 * (i + 1)] = (x play-truncate(mvs;2 * (i + 1))) ∈ Pos(g)))))
19. 1 ≤ n
20. (2 * 1) ≤ (2 * n)
21. 0 < (2 * n) + 1
22. if 0 <z 2 * n then mvs[0] else x1 fi  = InitialPos(g) ∈ Pos(g)
23. if ((2 * n) + 1) - 1 <z 2 * n then mvs[((2 * n) + 1) - 1] else x1 fi  = x1 ∈ Pos(g)
24. i : ℕ
25. ¬(2 * i) + 1 < 2 * n
26. (2 * i) + 1 < (2 * n) + 1
27. 2 * i < 2 * n
28. ((2 * i) + 1) = (2 * n) ∈ ℤ
⊢ ↓Legal1(mvs[2 * i];x1)

---

Latex:

---

Latex:

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.  x1  :  Pos(g)
12.  mvs  :  strat2play(g;n  -  1;x)
13.  ||mvs||  =  (2  *  n)
14.  Legal2(mvs[(2  *  n)  -  1];x1)
15.  mvs  \mmember{}  \{moves:sequence(Pos(g))|  ((2  *  (n  -  1))  +  2)  \mleq{}  ||moves||\} 
16.  \mforall{}i:\mBbbN{}(2  *  (n  -  1))  +  1
            ((((i  mod  2)  =  0)  {}\mRightarrow{}  (\mdownarrow{}Legal1(mvs[i];mvs[i  +  1])))
            \mwedge{}  (((i  mod  2)  =  1)  {}\mRightarrow{}  (\mdownarrow{}Legal2(mvs[i];mvs[i  +  1]))))
17.  mvs[0]  =  InitialPos(g)
18.  \mforall{}i:\mBbbN{}(n  -  1)  +  1
            ((\mdownarrow{}Legal1(mvs[2  *  i];mvs[(2  *  i)  +  1]))
            \mwedge{}  (i  <  n  -  1
                {}\mRightarrow{}  ((\mdownarrow{}Legal2(mvs[(2  *  i)  +  1];mvs[2  *  (i  +  1)]))
                      \mwedge{}  (mvs[2  *  (i  +  1)]  =  (x  play-truncate(mvs;2  *  (i  +  1)))))))
19.  1  \mleq{}  n
20.  (2  *  1)  \mleq{}  (2  *  n)
21.  0  <  (2  *  n)  +  1
22.  if  0  <z  2  *  n  then  mvs[0]  else  x1  fi    =  InitialPos(g)
23.  if  ((2  *  n)  +  1)  -  1  <z  2  *  n  then  mvs[((2  *  n)  +  1)  -  1]  else  x1  fi    =  x1
24.  i  :  \mBbbN{}
25.  \mneg{}(2  *  i)  +  1  <  2  *  n
26.  (2  *  i)  +  1  <  (2  *  n)  +  1
27.  2  *  i  <  2  *  n
\mvdash{}  \mdownarrow{}Legal1(mvs[2  *  i];x1)


By

---

Latex:
(Assert  ((2  *  i)  +  1)  =  (2  *  n)  BY
              Auto)

---

Home Index