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` 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