---

Step * 3 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. y1 : left-indices(K)
⊢ ∃j:left-indices(G ⊕ H ⊕ K). G ⊕ H ⊕ left-move(K;y1) ≡ left-move(G ⊕ H ⊕ K;j)
BY
{ ((D 0 With ⌜inr y1 ⌝  THENW Auto)
   THEN Reduce 0
   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.  y1  :  left-indices(K)
\mvdash{}  \mexists{}j:left-indices(G  \moplus{}  H  \moplus{}  K).  G  \moplus{}  H  \moplus{}  left-move(K;y1)  \mequiv{}  left-move(G  \moplus{}  H  \moplus{}  K;j)


By

---

Latex:
((D  0  With  \mkleeneopen{}inr  y1  \mkleeneclose{}    THENW  Auto)
  THEN  Reduce  0
  THEN  BackThruSomeHyp
  THEN  RepUR  ``left-option  right-option``  0
  THEN  Auto)

---

Home Index