---

Step * of Lemma Game-add-comm

∀G,H:Game.  G ⊕ H ≡ H ⊕ G
BY
{ ((BLemma `Game-induction` THENA Auto)
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN BLemma `Game-induction`
   THEN Auto
   THEN Unfold `Game-add` 0
   THEN D 0
   THEN RepUR ``left-indices right-indices left-move right-move mkGame Wsup`` 0
   THEN Folds ``left-indices left-move right-indices right-move`` 0
   THEN Auto
   THEN D -1
   THEN Reduce 0
   THEN ((D 0 With ⌜inr x ⌝  THENW Complete (Auto)) ORELSE (D 0 With ⌜inl y⌝  THENW Complete (Auto)))
   THEN Reduce 0
   THEN Try (Complete (((BackThruSomeHyp THEN RepUR ``left-option right-option`` 0) THEN Auto)))
   THEN (BLemma `eq-Game_inversion` THEN Auto)
   THEN (BackThruSomeHyp THEN RepUR ``left-option right-option`` 0)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}G,H:Game.    G  \moplus{}  H  \mequiv{}  H  \moplus{}  G


By

---

Latex:
((BLemma  `Game-induction`  THENA  Auto)
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  BLemma  `Game-induction`
  THEN  Auto
  THEN  Unfold  `Game-add`  0
  THEN  D  0
  THEN  RepUR  ``left-indices  right-indices  left-move  right-move  mkGame  Wsup``  0
  THEN  Folds  ``left-indices  left-move  right-indices  right-move``  0
  THEN  Auto
  THEN  D  -1
  THEN  Reduce  0
  THEN  ((D  0  With  \mkleeneopen{}inr  x  \mkleeneclose{}    THENW  Complete  (Auto))  ORELSE  (D  0  With  \mkleeneopen{}inl  y\mkleeneclose{}    THENW  Complete  (Auto)))
  THEN  Reduce  0
  THEN  Try  (Complete  (((BackThruSomeHyp  THEN  RepUR  ``left-option  right-option``  0)  THEN  Auto)))
  THEN  (BLemma  `eq-Game\_inversion`  THEN  Auto)
  THEN  (BackThruSomeHyp  THEN  RepUR  ``left-option  right-option``  0)
  THEN  Auto)

---

Home Index