---

Step * 3 1 of Lemma Game-minus_functionality


1. G1 : Game
2. ∀m:Game. ((left-option{i:l}(G1;m) ∨ right-option{i:l}(G1;m)) ⇒ (∀G2:Game. (m ≡ G2 ⇒ -(m) ≡ -(G2))))
3. G2 : Game
4. ∀m:Game. ((left-option{i:l}(G2;m) ∨ right-option{i:l}(G2;m)) ⇒ G1 ≡ m ⇒ -(G1) ≡ -(m))
5. G1 ≡ G2
6. i : right-indices(G2)
7. j : right-indices(G1)
8. right-move(G2;i) ≡ right-move(G1;j)
⊢ ∃j:left-indices(-(G1)). left-move(-(G2);i) ≡ left-move(-(G1);j)
BY
{ (((D 0 With ⌜j⌝  THENA Auto) THEN Reduce 0)
   THEN (BLemma `eq-Game_inversion` THENA Auto)
   THEN BackThruSomeHyp
   THEN Auto
   THEN RepUR ``left-option right-option`` 0
   THEN Auto
   THEN BLemma `eq-Game_inversion`
   THEN Auto) }

---

Latex:

---

Latex:

1.  G1  :  Game
2.  \mforall{}m:Game
          ((left-option\{i:l\}(G1;m)  \mvee{}  right-option\{i:l\}(G1;m))  {}\mRightarrow{}  (\mforall{}G2:Game.  (m  \mequiv{}  G2  {}\mRightarrow{}  -(m)  \mequiv{}  -(G2))))
3.  G2  :  Game
4.  \mforall{}m:Game.  ((left-option\{i:l\}(G2;m)  \mvee{}  right-option\{i:l\}(G2;m))  {}\mRightarrow{}  G1  \mequiv{}  m  {}\mRightarrow{}  -(G1)  \mequiv{}  -(m))
5.  G1  \mequiv{}  G2
6.  i  :  right-indices(G2)
7.  j  :  right-indices(G1)
8.  right-move(G2;i)  \mequiv{}  right-move(G1;j)
\mvdash{}  \mexists{}j:left-indices(-(G1)).  left-move(-(G2);i)  \mequiv{}  left-move(-(G1);j)


By

---

Latex:
(((D  0  With  \mkleeneopen{}j\mkleeneclose{}    THENA  Auto)  THEN  Reduce  0)
  THEN  (BLemma  `eq-Game\_inversion`  THENA  Auto)
  THEN  BackThruSomeHyp
  THEN  Auto
  THEN  RepUR  ``left-option  right-option``  0
  THEN  Auto
  THEN  BLemma  `eq-Game\_inversion`
  THEN  Auto)

---

Home Index