---

Step * of Lemma isom-games_inversion

∀[g1,g2:SimpleGame].  (g1 ≅ g2 ⇒ g2 ≅ g1)
BY
{ (Auto THEN RepeatFor 2 (D -1) THEN (D 0 With ⌜g⌝  THENA Auto) THEN D 0 With ⌜f⌝  THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[g1,g2:SimpleGame].    (g1  \mcong{}  g2  {}\mRightarrow{}  g2  \mcong{}  g1)


By

---

Latex:
(Auto  THEN  RepeatFor  2  (D  -1)  THEN  (D  0  With  \mkleeneopen{}g\mkleeneclose{}    THENA  Auto)  THEN  D  0  With  \mkleeneopen{}f\mkleeneclose{}    THEN  Auto)

---

Home Index