Step
*
of Lemma
sg-pos-normalize
∀[g:SimpleGame]. (Pos(sg-normalize(g)) ~ {p:Pos(g)| sg-reachable(g;InitialPos(g);p)} )
BY
{ (Unfold `sg-normalize` 0 THEN Auto) }
Latex:
Latex:
\mforall{}[g:SimpleGame].  (Pos(sg-normalize(g))  \msim{}  \{p:Pos(g)|  sg-reachable(g;InitialPos(g);p)\}  )
By
Latex:
(Unfold  `sg-normalize`  0  THEN  Auto)
Home
Index