---

Step * 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)
⊢ ∀k:ℕ. ∀[x:win2strat(g;k)]. ∀[moves:strat2play(sg-normalize(g);k;x)].  (moves ∈ strat2play(g;k;x)) supposing k < n
BY
{ ((D 0 THENA Auto)
   THEN UseWitness ⌜Ax⌝⋅
   THEN Unfolds ``uall uimplies`` 0
   THEN ((NatInd (-1) THEN (MemTypeCD THENA Auto))
         THEN Try (((Assert ∀[x:win2strat(g;k - 1)]. ∀[moves:strat2play(sg-normalize(g);k - 1;x)].
                              (moves ∈ strat2play(g;k - 1;x)) 
                            supposing k - 1 < n BY
                           (Unfolds ``uall uimplies`` 0 THEN UseWitness ⌜Ax⌝⋅ THEN Trivial))
                    THEN Thin (-3)
                    THEN (D -1 THENA Auto)))
         )
   THEN (MemTypeCD THENW Auto)) }

1
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))

2
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))

---

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


By

---

Latex:
((D  0  THENA  Auto)
  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}
  THEN  Unfolds  ``uall  uimplies``  0
  THEN  ((NatInd  (-1)  THEN  (MemTypeCD  THENA  Auto))
              THEN  Try  (((Assert  \mforall{}[x:win2strat(g;k  -  1)].  \mforall{}[moves:strat2play(sg-normalize(g);k  -  1;x)].
                                                        (moves  \mmember{}  strat2play(g;k  -  1;x)) 
                                                    supposing  k  -  1  <  n  BY
                                                  (Unfolds  ``uall  uimplies``  0  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}  THEN  Trivial))
                                    THEN  Thin  (-3)
                                    THEN  (D  -1  THENA  Auto)))
              )
  THEN  (MemTypeCD  THENW  Auto))

---

Home Index