---

Step * 1 of Lemma Game-minus-minus


1. G : Game
2. ∀m:Game. ((left-option{i:l}(G;m) ∨ right-option{i:l}(G;m)) ⇒ -(-(m)) ≡ m)
⊢ -(-(G)) ≡ G
BY
{ (D 0
   THEN Unfold `Game-minus` 0
   THEN RepUR ``left-indices right-indices left-move right-move mkGame Wsup`` 0
   THEN Folds ``left-indices right-indices left-move right-move `` 0
   THEN Auto
   THEN (D 0 With ⌜i⌝  THEN Auto)
   THEN (BackThruSomeHyp ORELSE ((BLemma `eq-Game_inversion` THENA Auto) THEN BackThruSomeHyp))
   THEN RepUR ``left-option right-option`` 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  G  :  Game
2.  \mforall{}m:Game.  ((left-option\{i:l\}(G;m)  \mvee{}  right-option\{i:l\}(G;m))  {}\mRightarrow{}  -(-(m))  \mequiv{}  m)
\mvdash{}  -(-(G))  \mequiv{}  G


By

---

Latex:
(D  0
  THEN  Unfold  `Game-minus`  0
  THEN  RepUR  ``left-indices  right-indices  left-move  right-move  mkGame  Wsup``  0
  THEN  Folds  ``left-indices  right-indices  left-move  right-move  ``  0
  THEN  Auto
  THEN  (D  0  With  \mkleeneopen{}i\mkleeneclose{}    THEN  Auto)
  THEN  (BackThruSomeHyp  ORELSE  ((BLemma  `eq-Game\_inversion`  THENA  Auto)  THEN  BackThruSomeHyp))
  THEN  RepUR  ``left-option  right-option``  0
  THEN  Auto)

---

Home Index