---

Step * 1 of Lemma sg-normalize-win2

.....assertion..... 
1. g : SimpleGame
⊢ ∀[n:ℕ]. win2strat(g;n) ≡ win2strat(sg-normalize(g);n)
BY
{ (CompleteInductionOnNat
   THEN Auto
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN Unfold `win2strat` -1
   THEN Unfold `win2strat` 0
   THEN (SplitOnHypITE -1  THENA Auto)
   THEN (SplitOnConclITE THENA Auto)
   THEN Try (Trivial)
   THEN OnVar `x' DepIsectHD
   THEN ((InstHyp [⌜n - 1⌝] 3⋅ THENA Auto) THEN D -1)
   THEN (DepIsectCD THENL [Auto; (FunExt THENA Auto)])) }

1
1. g : SimpleGame
2. n : ℕ
3. ∀n:ℕn. win2strat(g;n) ≡ win2strat(sg-normalize(g);n)
4. x : s:win2strat(g;n - 1) ⋂ moves:{f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(g)| Legal2(moves[(2 * n) -\000C 1];p)} 
5. x ∈ win2strat(g;n - 1)
6. x ∈ moves:{f:strat2play(g;n - 1;x)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(g)| Legal2(moves[(2 * n) - 1];p)} 
7. ¬(n = 0 ∈ ℤ)
8. ¬(n = 0 ∈ ℤ)
9. win2strat(g;n - 1) ⊆r win2strat(sg-normalize(g);n - 1)
10. win2strat(sg-normalize(g);n - 1) ⊆r win2strat(g;n - 1)
11. moves : {f:strat2play(sg-normalize(g);n - 1;x)| ||f|| = (2 * n) ∈ ℤ} 
⊢ x moves ∈ {p:Pos(sg-normalize(g))| Legal2(moves[(2 * n) - 1];p)} 

2
1. g : SimpleGame
2. n : ℕ
3. ∀n:ℕn. win2strat(g;n) ≡ win2strat(sg-normalize(g);n)
4. x : s:win2strat(sg-normalize(g);n - 1) ⋂ moves:{f:strat2play(sg-normalize(g);n - 1;s)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Po\000Cs(sg-normalize(g))| 
                                                                        Legal2(moves[(2 * n) - 1];p)} 
5. x ∈ win2strat(sg-normalize(g);n - 1)
6. x ∈ moves:{f:strat2play(sg-normalize(g);n - 1;x)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(sg-normalize(g))| 
                                                                    Legal2(moves[(2 * n) - 1];p)} 
7. ¬(n = 0 ∈ ℤ)
8. ¬(n = 0 ∈ ℤ)
9. win2strat(g;n - 1) ⊆r win2strat(sg-normalize(g);n - 1)
10. win2strat(sg-normalize(g);n - 1) ⊆r win2strat(g;n - 1)
11. moves : {f:strat2play(g;n - 1;x)| ||f|| = (2 * n) ∈ ℤ} 
⊢ x moves ∈ {p:Pos(g)| Legal2(moves[(2 * n) - 1];p)} 

---

Latex:

---

Latex:
.....assertion..... 
1.  g  :  SimpleGame
\mvdash{}  \mforall{}[n:\mBbbN{}].  win2strat(g;n)  \mequiv{}  win2strat(sg-normalize(g);n)


By

---

Latex:
(CompleteInductionOnNat
  THEN  Auto
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  Unfold  `win2strat`  -1
  THEN  Unfold  `win2strat`  0
  THEN  (SplitOnHypITE  -1    THENA  Auto)
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  Try  (Trivial)
  THEN  OnVar  `x'  DepIsectHD
  THEN  ((InstHyp  [\mkleeneopen{}n  -  1\mkleeneclose{}]  3\mcdot{}  THENA  Auto)  THEN  D  -1)
  THEN  (DepIsectCD  THENL  [Auto;  (FunExt  THENA  Auto)]))

---

Home Index