---

Step * of Lemma Game-add-assoc

∀G,H,K:Game.  G ⊕ H ⊕ K ≡ G ⊕ H ⊕ K
BY
{ (RepeatFor 3 (((BLemma `Game-induction` THENA Auto) THEN RepeatFor 2 ((D 0 THENA Auto))))
   THEN D 0
   THEN Auto
   THEN Unfold `Game-add` -1
   THEN RepUR ``left-indices right-indices mkGame Wsup`` -1
   THEN Folds ``left-indices right-indices`` (-1)
   THEN D -1
   THEN Try (D -1)
   THEN Reduce 0) }

1
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. x : left-indices(G)
⊢ ∃j:left-indices(G ⊕ H ⊕ K). left-move(G;x) ⊕ H ⊕ K ≡ left-move(G ⊕ H ⊕ K;j)

2
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. x : left-indices(H)
⊢ ∃j:left-indices(G ⊕ H ⊕ K). G ⊕ left-move(H;x) ⊕ K ≡ left-move(G ⊕ H ⊕ K;j)

3
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)

4
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. x : right-indices(G)
⊢ ∃j:right-indices(G ⊕ H ⊕ K). right-move(G;x) ⊕ H ⊕ K ≡ right-move(G ⊕ H ⊕ K;j)

5
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. x : right-indices(H)
⊢ ∃j:right-indices(G ⊕ H ⊕ K). G ⊕ right-move(H;x) ⊕ K ≡ right-move(G ⊕ H ⊕ K;j)

6
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. y1 : right-indices(K)
⊢ ∃j:right-indices(G ⊕ H ⊕ K). G ⊕ H ⊕ right-move(K;y1) ≡ right-move(G ⊕ H ⊕ K;j)

7
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. x1 : left-indices(G)
⊢ ∃j:left-indices(G ⊕ H ⊕ K). left-move(G;x1) ⊕ H ⊕ K ≡ left-move(G ⊕ H ⊕ K;j)

8
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. y : left-indices(H)
⊢ ∃j:left-indices(G ⊕ H ⊕ K). G ⊕ left-move(H;y) ⊕ K ≡ left-move(G ⊕ H ⊕ K;j)

9
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. y : left-indices(K)
⊢ ∃j:left-indices(G ⊕ H ⊕ K). G ⊕ H ⊕ left-move(K;y) ≡ left-move(G ⊕ H ⊕ K;j)

10
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)

11
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. y : right-indices(H)
⊢ ∃j:right-indices(G ⊕ H ⊕ K). G ⊕ right-move(H;y) ⊕ K ≡ right-move(G ⊕ H ⊕ K;j)

12
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. y : right-indices(K)
⊢ ∃j:right-indices(G ⊕ H ⊕ K). G ⊕ H ⊕ right-move(K;y) ≡ right-move(G ⊕ H ⊕ K;j)

---

Latex:

---

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


By

---

Latex:
(RepeatFor  3  (((BLemma  `Game-induction`  THENA  Auto)  THEN  RepeatFor  2  ((D  0  THENA  Auto))))
  THEN  D  0
  THEN  Auto
  THEN  Unfold  `Game-add`  -1
  THEN  RepUR  ``left-indices  right-indices  mkGame  Wsup``  -1
  THEN  Folds  ``left-indices  right-indices``  (-1)
  THEN  D  -1
  THEN  Try  (D  -1)
  THEN  Reduce  0)

---

Home Index