---

Step * 1 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. ¬(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 < n
10. x : win2strat(g;0)
⊢ Ax ∈ ⋂moves:strat2play(sg-normalize(g);0;x). (moves ∈ strat2play(g;0;x))
BY
{ ((MemTypeCD THENW Auto)
   THEN MemCD
   THEN (Unfold `strat2play` -1 THEN Reduce -1)
   THEN Unfold `strat2play` 0
   THEN Reduce 0
   THEN (RWO "sg-pos-normalize sg-init-normalize sg-legal1-normalize" (-1) THENA Auto)
   THEN All (Unfold `play-item`)
   THEN D -1
   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  <  n
10.  x  :  win2strat(g;0)
\mvdash{}  Ax  \mmember{}  \mcap{}moves:strat2play(sg-normalize(g);0;x).  (moves  \mmember{}  strat2play(g;0;x))


By

---

Latex:
((MemTypeCD  THENW  Auto)
  THEN  MemCD
  THEN  (Unfold  `strat2play`  -1  THEN  Reduce  -1)
  THEN  Unfold  `strat2play`  0
  THEN  Reduce  0
  THEN  (RWO  "sg-pos-normalize  sg-init-normalize  sg-legal1-normalize"  (-1)  THENA  Auto)
  THEN  All  (Unfold  `play-item`)
  THEN  D  -1
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index