---

Step * 1 1 2 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. [%19] : ||mvs|| = (2 * n) ∈ ℤ
14. Legal2(mvs[(2 * n) - 1];x1)
⊢ sg-reachable(g;InitialPos(g);x1)
BY
{ (OnVar `mvs' Strat2PlaySubtype⋅
   THEN (OnVar `mvs' Strat2PlayInvariant2⋅ THENA Auto)
   THEN (OnVar `mvs' Strat2PlayInvariant⋅ THENA Auto)
   THEN Unfold `play-len` -5
   THEN (D 0 With ⌜seq-add(seq-truncate(mvs;2 * n);x1)⌝  THENW Auto)
   THEN (RWW "seq-add-len seq-add-item" 0 THENA Auto)
   THEN (Assert 1 ≤ n BY
               Auto)
   THEN (Mul ⌜2⌝ (-1)⋅ THENA Auto)
   THEN (RWW  "seq-len-truncate seq-truncate-item" 0 THEN Auto)
   THEN All (Unfold `play-item`)
   THEN RepeatFor 2 (AutoSplit)) }

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
⊢ ↓Legal2(mvs[(2 * i) - 1];mvs[2 * i])

2
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
27. 2 * i < (2 * n) + 1
28. (2 * i) - 1 < 2 * n
⊢ ↓Legal2(mvs[(2 * i) - 1];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.  [\%19]  :  ||mvs||  =  (2  *  n)
14.  Legal2(mvs[(2  *  n)  -  1];x1)
\mvdash{}  sg-reachable(g;InitialPos(g);x1)


By

---

Latex:
(OnVar  `mvs'  Strat2PlaySubtype\mcdot{}
  THEN  (OnVar  `mvs'  Strat2PlayInvariant2\mcdot{}  THENA  Auto)
  THEN  (OnVar  `mvs'  Strat2PlayInvariant\mcdot{}  THENA  Auto)
  THEN  Unfold  `play-len`  -5
  THEN  (D  0  With  \mkleeneopen{}seq-add(seq-truncate(mvs;2  *  n);x1)\mkleeneclose{}    THENW  Auto)
  THEN  (RWW  "seq-add-len  seq-add-item"  0  THENA  Auto)
  THEN  (Assert  1  \mleq{}  n  BY
                          Auto)
  THEN  (Mul  \mkleeneopen{}2\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  (RWW    "seq-len-truncate  seq-truncate-item"  0  THEN  Auto)
  THEN  All  (Unfold  `play-item`)
  THEN  RepeatFor  2  (AutoSplit))

---

Home Index