---

Step * of Lemma sg-normalize-win2

∀[g:SimpleGame]. win2(g) ≡ win2(sg-normalize(g))
BY
{ (Auto THEN Unfold `win2` 0 THEN Assert ⌜∀[n:ℕ]. win2strat(g;n) ≡ win2strat(sg-normalize(g);n)⌝⋅) }

1
.....assertion..... 
1. g : SimpleGame
⊢ ∀[n:ℕ]. win2strat(g;n) ≡ win2strat(sg-normalize(g);n)

2
1. g : SimpleGame
2. ∀[n:ℕ]. win2strat(g;n) ≡ win2strat(sg-normalize(g);n)
⊢ ∀[n:ℕ]. win2strat(g;n) ≡ ∀[n:ℕ]. win2strat(sg-normalize(g);n)

---

Latex:

---

Latex:
\mforall{}[g:SimpleGame].  win2(g)  \mequiv{}  win2(sg-normalize(g))


By

---

Latex:
(Auto  THEN  Unfold  `win2`  0  THEN  Assert  \mkleeneopen{}\mforall{}[n:\mBbbN{}].  win2strat(g;n)  \mequiv{}  win2strat(sg-normalize(g);n)\mkleeneclose{}\mcdot{})

---

Home Index