---

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

.....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)
BY
{ ((Assert ¬(k = 0 ∈ ℤ) BY
          Auto)
   THEN Unfold `strat2play` -2
   THEN Unfold `strat2play` 0
   THEN (SplitOnHypITE -2  THENA Auto)
   THEN (SplitOnConclITE THENA Auto)
   THEN Try (Trivial)
   THEN RepeatFor 3 (Thin (-1))
   THEN DepIsectHD  (-1)
   THEN DepIsectCD
   THEN Try ((D 12 With ⌜moves⌝  THEN Trivial))) }

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

---

Latex:

---

Latex:
.....eq  aux..... 
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  :  strat2play(sg-normalize(g);k;x)
\mvdash{}  moves  \mmember{}  strat2play(g;k;x)


By

---

Latex:
((Assert  \mneg{}(k  =  0)  BY
                Auto)
  THEN  Unfold  `strat2play`  -2
  THEN  Unfold  `strat2play`  0
  THEN  (SplitOnHypITE  -2    THENA  Auto)
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  Try  (Trivial)
  THEN  RepeatFor  3  (Thin  (-1))
  THEN  DepIsectHD    (-1)
  THEN  DepIsectCD
  THEN  Try  ((D  12  With  \mkleeneopen{}moves\mkleeneclose{}    THEN  Trivial)))

---

Home Index