---

Step * 1 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. ¬(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 - 1)]. ∀[moves:strat2play(sg-normalize(g);k - 1;x)].  (moves ∈ strat2play(g;k - 1;x))
12. x : win2strat(g;k)
⊢ Ax ∈ ⋂moves:strat2play(sg-normalize(g);k;x). (moves ∈ strat2play(g;k;x))
BY
{ ((D -2 With ⌜x⌝  THENA Auto)
   THEN (InstHyp [⌜k - 1⌝] 3⋅ THENA Auto)
   THEN D -1
   THEN (MemTypeCD THENW Auto)
   THEN MemCD) }

1
.....eq aux..... 
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 : strat2play(sg-normalize(g);k;x)
⊢ moves ∈ strat2play(g;k;x)

---

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.  \mforall{}[x:win2strat(g;k  -  1)].  \mforall{}[moves:strat2play(sg-normalize(g);k  -  1;x)].
            (moves  \mmember{}  strat2play(g;k  -  1;x))
12.  x  :  win2strat(g;k)
\mvdash{}  Ax  \mmember{}  \mcap{}moves:strat2play(sg-normalize(g);k;x).  (moves  \mmember{}  strat2play(g;k;x))


By

---

Latex:
((D  -2  With  \mkleeneopen{}x\mkleeneclose{}    THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}k  -  1\mkleeneclose{}]  3\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  (MemTypeCD  THENW  Auto)
  THEN  MemCD)

---

Home Index