---

Step * 1 1 2 1 1 1 1 2 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:ℕ
      ((2 * i) + 1 < (2 * n) + 1
      ⇒ (↓Legal1(if 2 * i <z 2 * n then mvs[2 * i] else x1 fi ;if (2 * i) + 1 <z 2 * n
                  then mvs[(2 * i) + 1]
                  else x1
                  fi )))
25. i : ℕ+
26. 2 * i < (2 * n) + 1
27. (2 * i) - 1 < 2 * n
28. 2 * i < 2 * n
⊢ ↓Legal2(mvs[(2 * i) - 1];mvs[2 * i])
BY
{ (InstHyp [⌜(2 * i) - 1⌝] 16⋅ THEN 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:ℕ
      ((2 * i) + 1 < (2 * n) + 1
      ⇒ (↓Legal1(if 2 * i <z 2 * n then mvs[2 * i] else x1 fi ;if (2 * i) + 1 <z 2 * n
                  then mvs[(2 * i) + 1]
                  else x1
                  fi )))
25. i : ℕ+
26. 2 * i < (2 * n) + 1
27. (2 * i) - 1 < 2 * n
28. 2 * i < 2 * n
29. ((((2 * i) - 1) mod 2) = 0 ∈ ℤ) ⇒ (↓Legal1(mvs[(2 * i) - 1];mvs[((2 * i) - 1) + 1]))
30. ((((2 * i) - 1) mod 2) = 1 ∈ ℤ) ⇒ (↓Legal2(mvs[(2 * i) - 1];mvs[((2 * i) - 1) + 1]))
⊢ ↓Legal2(mvs[(2 * i) - 1];mvs[2 * i])

---

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.  \mforall{}i:\mBbbN{}
            ((2  *  i)  +  1  <  (2  *  n)  +  1
            {}\mRightarrow{}  (\mdownarrow{}Legal1(if  2  *  i  <z  2  *  n  then  mvs[2  *  i]  else  x1  fi  ;if  (2  *  i)  +  1  <z  2  *  n
                                    then  mvs[(2  *  i)  +  1]
                                    else  x1
                                    fi  )))
25.  i  :  \mBbbN{}\msupplus{}
26.  2  *  i  <  (2  *  n)  +  1
27.  (2  *  i)  -  1  <  2  *  n
28.  2  *  i  <  2  *  n
\mvdash{}  \mdownarrow{}Legal2(mvs[(2  *  i)  -  1];mvs[2  *  i])


By

---

Latex:
(InstHyp  [\mkleeneopen{}(2  *  i)  -  1\mkleeneclose{}]  16\mcdot{}  THEN  Auto)

---

Home Index