---

Step * 10 of Lemma Game-add-assoc


1. G : Game
2. ∀m:Game. ((left-option{i:l}(G;m) ∨ right-option{i:l}(G;m)) ⇒ (∀H,K:Game.  m ⊕ H ⊕ K ≡ m ⊕ H ⊕ K))
3. H : Game
4. ∀m:Game. ((left-option{i:l}(H;m) ∨ right-option{i:l}(H;m)) ⇒ (∀K:Game. G ⊕ m ⊕ K ≡ G ⊕ m ⊕ K))
5. K : Game
6. ∀m:Game. ((left-option{i:l}(K;m) ∨ right-option{i:l}(K;m)) ⇒ G ⊕ H ⊕ m ≡ G ⊕ H ⊕ m)
7. ∀i:left-indices(G ⊕ H ⊕ K). ∃j:left-indices(G ⊕ H ⊕ K). left-move(G ⊕ H ⊕ K;i) ≡ left-move(G ⊕ H ⊕ K;j)
8. x1 : right-indices(G)
⊢ ∃j:right-indices(G ⊕ H ⊕ K). right-move(G;x1) ⊕ H ⊕ K ≡ right-move(G ⊕ H ⊕ K;j)
BY
{ ((D 0 With ⌜inl x1⌝  THENW Auto)
   THEN Reduce 0
   THEN BLemma `eq-Game_inversion`
   THEN 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{}  (\mforall{}H,K:Game.    m  \moplus{}  H  \moplus{}  K  \mequiv{}  m  \moplus{}  H  \moplus{}  K))
3.  H  :  Game
4.  \mforall{}m:Game.  ((left-option\{i:l\}(H;m)  \mvee{}  right-option\{i:l\}(H;m))  {}\mRightarrow{}  (\mforall{}K:Game.  G  \moplus{}  m  \moplus{}  K  \mequiv{}  G  \moplus{}  m  \moplus{}  K))
5.  K  :  Game
6.  \mforall{}m:Game.  ((left-option\{i:l\}(K;m)  \mvee{}  right-option\{i:l\}(K;m))  {}\mRightarrow{}  G  \moplus{}  H  \moplus{}  m  \mequiv{}  G  \moplus{}  H  \moplus{}  m)
7.  \mforall{}i:left-indices(G  \moplus{}  H  \moplus{}  K)
          \mexists{}j:left-indices(G  \moplus{}  H  \moplus{}  K).  left-move(G  \moplus{}  H  \moplus{}  K;i)  \mequiv{}  left-move(G  \moplus{}  H  \moplus{}  K;j)
8.  x1  :  right-indices(G)
\mvdash{}  \mexists{}j:right-indices(G  \moplus{}  H  \moplus{}  K).  right-move(G;x1)  \moplus{}  H  \moplus{}  K  \mequiv{}  right-move(G  \moplus{}  H  \moplus{}  K;j)


By

---

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

---

Home Index