---

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


1. g : SimpleGame
2. n : ℕ
3. ∀n:ℕn. win2strat(g;n) ≡ win2strat(sg-normalize(g);n)
4. ¬(n = 0 ∈ ℤ)
5. ¬(n = 0 ∈ ℤ)
6. win2strat(g;n - 1) ⊆r win2strat(sg-normalize(g);n - 1)
7. win2strat(sg-normalize(g);n - 1) ⊆r win2strat(g;n - 1)
8. k : ℤ
9. 0 < k
10. k < n
11. x : win2strat(g;k)
12. ∀[moves:strat2play(sg-normalize(g);k - 1;x)]. (moves ∈ strat2play(g;k - 1;x))
13. win2strat(g;k - 1) ⊆r win2strat(sg-normalize(g);k - 1)
14. win2strat(sg-normalize(g);k - 1) ⊆r win2strat(g;k - 1)
15. moves : f:strat2play(sg-normalize(g);k - 1;x) ⋂ {moves:sequence(Pos(sg-normalize(g)))| 
                                                     (((2 * k) + 2) ≤ ||moves||)
                                                     ∧ Legal1(moves[2 * k];moves[(2 * k) + 1])
                                                     ∧ (moves[2 * k]
                                                       = (x play-truncate(f;2 * k))
                                                       ∈ Pos(sg-normalize(g)))} 
16. moves ∈ strat2play(sg-normalize(g);k - 1;x)
17. 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)))} 
⊢ moves ∈ {moves@0:sequence(Pos(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(g))} 
BY
{ ((RWO "sg-pos-normalize sg-init-normalize sg-legal1-normalize" (-1) THENA Auto)
   THEN All (Unfold `play-item`)
   THEN (MemTypeHD (-1) THENA Auto)
   THEN Fold `member` (-2)
   THEN MemTypeCD
   THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  SimpleGame
2.  n  :  \mBbbN{}
3.  \mforall{}n:\mBbbN{}n.  win2strat(g;n)  \mequiv{}  win2strat(sg-normalize(g);n)
4.  \mneg{}(n  =  0)
5.  \mneg{}(n  =  0)
6.  win2strat(g;n  -  1)  \msubseteq{}r  win2strat(sg-normalize(g);n  -  1)
7.  win2strat(sg-normalize(g);n  -  1)  \msubseteq{}r  win2strat(g;n  -  1)
8.  k  :  \mBbbZ{}
9.  0  <  k
10.  k  <  n
11.  x  :  win2strat(g;k)
12.  \mforall{}[moves:strat2play(sg-normalize(g);k  -  1;x)].  (moves  \mmember{}  strat2play(g;k  -  1;x))
13.  win2strat(g;k  -  1)  \msubseteq{}r  win2strat(sg-normalize(g);k  -  1)
14.  win2strat(sg-normalize(g);k  -  1)  \msubseteq{}r  win2strat(g;k  -  1)
15.  moves  :  f:strat2play(sg-normalize(g);k  -  1;x)  \mcap{}  \{moves:sequence(Pos(sg-normalize(g)))| 
                                                                                                          (((2  *  k)  +  2)  \mleq{}  ||moves||)
                                                                                                          \mwedge{}  Legal1(moves[2  *  k];moves[(2  *  k)  +  1])
                                                                                                          \mwedge{}  (moves[2  *  k]  =  (x  play-truncate(f;2  *  k)))\} 
16.  moves  \mmember{}  strat2play(sg-normalize(g);k  -  1;x)
17.  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)))\} 
\mvdash{}  moves  \mmember{}  \{moves@0:sequence(Pos(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:
((RWO  "sg-pos-normalize  sg-init-normalize  sg-legal1-normalize"  (-1)  THENA  Auto)
  THEN  All  (Unfold  `play-item`)
  THEN  (MemTypeHD  (-1)  THENA  Auto)
  THEN  Fold  `member`  (-2)
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index