Proof of Nuprl Lemma : Game-add

Step * of Lemma Game-add_functionality

∀G1,H1,G2,H2:Game.  (G1 ≡ G2 ⇒ H1 ≡ H2 ⇒ G1 ⊕ H1 ≡ G2 ⊕ H2)
BY
{ (RepeatFor 4 (((BLemma `Game-induction` THENA Auto) THEN RepeatFor 2 ((D 0 THENA Auto))))
   THEN 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) }

1
1. G1 : Game
2. ∀m:Game
     ((left-option{i:l}(G1;m) ∨ right-option{i:l}(G1;m)) ⇒ (∀H1,G2,H2:Game.  (m ≡ G2 ⇒ H1 ≡ H2 ⇒ m ⊕ H1 ≡ G2 ⊕ H2)))
3. H1 : Game
4. ∀m:Game
     ((left-option{i:l}(H1;m) ∨ right-option{i:l}(H1;m)) ⇒ (∀G2,H2:Game.  (G1 ≡ G2 ⇒ m ≡ H2 ⇒ G1 ⊕ m ≡ G2 ⊕ H2)))
5. G2 : Game
6. ∀m:Game. ((left-option{i:l}(G2;m) ∨ right-option{i:l}(G2;m)) ⇒ (∀H2:Game. (G1 ≡ m ⇒ H1 ≡ H2 ⇒ G1 ⊕ H1 ≡ m ⊕ H2)))
7. H2 : Game
8. ∀m:Game. ((left-option{i:l}(H2;m) ∨ right-option{i:l}(H2;m)) ⇒ G1 ≡ G2 ⇒ H1 ≡ m ⇒ G1 ⊕ H1 ≡ G2 ⊕ m)
9. G1 ≡ G2
10. H1 ≡ H2
11. x : left-indices(G1)
⊢ ∃j:left-indices(G2 ⊕ H2). left-move(G1 ⊕ H1;inl x) ≡ left-move(G2 ⊕ H2;j)

2
1. G1 : Game
2. ∀m:Game
     ((left-option{i:l}(G1;m) ∨ right-option{i:l}(G1;m)) ⇒ (∀H1,G2,H2:Game.  (m ≡ G2 ⇒ H1 ≡ H2 ⇒ m ⊕ H1 ≡ G2 ⊕ H2)))
3. H1 : Game
4. ∀m:Game
     ((left-option{i:l}(H1;m) ∨ right-option{i:l}(H1;m)) ⇒ (∀G2,H2:Game.  (G1 ≡ G2 ⇒ m ≡ H2 ⇒ G1 ⊕ m ≡ G2 ⊕ H2)))
5. G2 : Game
6. ∀m:Game. ((left-option{i:l}(G2;m) ∨ right-option{i:l}(G2;m)) ⇒ (∀H2:Game. (G1 ≡ m ⇒ H1 ≡ H2 ⇒ G1 ⊕ H1 ≡ m ⊕ H2)))
7. H2 : Game
8. ∀m:Game. ((left-option{i:l}(H2;m) ∨ right-option{i:l}(H2;m)) ⇒ G1 ≡ G2 ⇒ H1 ≡ m ⇒ G1 ⊕ H1 ≡ G2 ⊕ m)
9. G1 ≡ G2
10. H1 ≡ H2
11. y : left-indices(H1)
⊢ ∃j:left-indices(G2 ⊕ H2). left-move(G1 ⊕ H1;inr y ) ≡ left-move(G2 ⊕ H2;j)

3
1. G1 : Game
2. ∀m:Game
     ((left-option{i:l}(G1;m) ∨ right-option{i:l}(G1;m)) ⇒ (∀H1,G2,H2:Game.  (m ≡ G2 ⇒ H1 ≡ H2 ⇒ m ⊕ H1 ≡ G2 ⊕ H2)))
3. H1 : Game
4. ∀m:Game
     ((left-option{i:l}(H1;m) ∨ right-option{i:l}(H1;m)) ⇒ (∀G2,H2:Game.  (G1 ≡ G2 ⇒ m ≡ H2 ⇒ G1 ⊕ m ≡ G2 ⊕ H2)))
5. G2 : Game
6. ∀m:Game. ((left-option{i:l}(G2;m) ∨ right-option{i:l}(G2;m)) ⇒ (∀H2:Game. (G1 ≡ m ⇒ H1 ≡ H2 ⇒ G1 ⊕ H1 ≡ m ⊕ H2)))
7. H2 : Game
8. ∀m:Game. ((left-option{i:l}(H2;m) ∨ right-option{i:l}(H2;m)) ⇒ G1 ≡ G2 ⇒ H1 ≡ m ⇒ G1 ⊕ H1 ≡ G2 ⊕ m)
9. G1 ≡ G2
10. H1 ≡ H2

11. ∀i:left-indices(G1 ⊕ H1). ∃j:left-indices(G2 ⊕ H2). left-move(G1 ⊕ H1;i) ≡ left-move(G2 ⊕ H2;j)

12. x : right-indices(G1)
⊢ ∃j:right-indices(G2 ⊕ H2). right-move(G1 ⊕ H1;inl x) ≡ right-move(G2 ⊕ H2;j)

4
1. G1 : Game
2. ∀m:Game
((left-option{i:l}(G1;m) ∨ right-option{i:l}(G1;m)) ⇒ (∀H1,G2,H2:Game. (m ≡ G2 ⇒ H1 ≡ H2 ⇒ m ⊕ H1 ≡ G2 ⊕ H2)))
3. H1 : Game
4. ∀m:Game
((left-option{i:l}(H1;m) ∨ right-option{i:l}(H1;m)) ⇒ (∀G2,H2:Game. (G1 ≡ G2 ⇒ m ≡ H2 ⇒ G1 ⊕ m ≡ G2 ⊕ H2)))
5. G2 : Game
6. ∀m:Game. ((left-option{i:l}(G2;m) ∨ right-option{i:l}(G2;m)) ⇒ (∀H2:Game. (G1 ≡ m ⇒ H1 ≡ H2 ⇒ G1 ⊕ H1 ≡ m ⊕ H2)))
7. H2 : Game
8. ∀m:Game. ((left-option{i:l}(H2;m) ∨ right-option{i:l}(H2;m)) ⇒ G1 ≡ G2 ⇒ H1 ≡ m ⇒ G1 ⊕ H1 ≡ G2 ⊕ m)
9. G1 ≡ G2
10. H1 ≡ H2

11. ∀i:left-indices(G1 ⊕ H1). ∃j:left-indices(G2 ⊕ H2). left-move(G1 ⊕ H1;i) ≡ left-move(G2 ⊕ H2;j)

12. y : right-indices(H1)
⊢ ∃j:right-indices(G2 ⊕ H2). right-move(G1 ⊕ H1;inr y ) ≡ right-move(G2 ⊕ H2;j)

5
1. G1 : Game
2. ∀m:Game
     ((left-option{i:l}(G1;m) ∨ right-option{i:l}(G1;m)) ⇒ (∀H1,G2,H2:Game.  (m ≡ G2 ⇒ H1 ≡ H2 ⇒ m ⊕ H1 ≡ G2 ⊕ H2)))
3. H1 : Game
4. ∀m:Game
     ((left-option{i:l}(H1;m) ∨ right-option{i:l}(H1;m)) ⇒ (∀G2,H2:Game.  (G1 ≡ G2 ⇒ m ≡ H2 ⇒ G1 ⊕ m ≡ G2 ⊕ H2)))
5. G2 : Game
6. ∀m:Game. ((left-option{i:l}(G2;m) ∨ right-option{i:l}(G2;m)) ⇒ (∀H2:Game. (G1 ≡ m ⇒ H1 ≡ H2 ⇒ G1 ⊕ H1 ≡ m ⊕ H2)))
7. H2 : Game
8. ∀m:Game. ((left-option{i:l}(H2;m) ∨ right-option{i:l}(H2;m)) ⇒ G1 ≡ G2 ⇒ H1 ≡ m ⇒ G1 ⊕ H1 ≡ G2 ⊕ m)
9. G1 ≡ G2
10. H1 ≡ H2
11. x : left-indices(G2)
⊢ ∃j:left-indices(G1 ⊕ H1). left-move(G2 ⊕ H2;inl x) ≡ left-move(G1 ⊕ H1;j)

6
1. G1 : Game
2. ∀m:Game
     ((left-option{i:l}(G1;m) ∨ right-option{i:l}(G1;m)) ⇒ (∀H1,G2,H2:Game.  (m ≡ G2 ⇒ H1 ≡ H2 ⇒ m ⊕ H1 ≡ G2 ⊕ H2)))
3. H1 : Game
4. ∀m:Game
     ((left-option{i:l}(H1;m) ∨ right-option{i:l}(H1;m)) ⇒ (∀G2,H2:Game.  (G1 ≡ G2 ⇒ m ≡ H2 ⇒ G1 ⊕ m ≡ G2 ⊕ H2)))
5. G2 : Game
6. ∀m:Game. ((left-option{i:l}(G2;m) ∨ right-option{i:l}(G2;m)) ⇒ (∀H2:Game. (G1 ≡ m ⇒ H1 ≡ H2 ⇒ G1 ⊕ H1 ≡ m ⊕ H2)))
7. H2 : Game
8. ∀m:Game. ((left-option{i:l}(H2;m) ∨ right-option{i:l}(H2;m)) ⇒ G1 ≡ G2 ⇒ H1 ≡ m ⇒ G1 ⊕ H1 ≡ G2 ⊕ m)
9. G1 ≡ G2
10. H1 ≡ H2
11. y : left-indices(H2)
⊢ ∃j:left-indices(G1 ⊕ H1). left-move(G2 ⊕ H2;inr y ) ≡ left-move(G1 ⊕ H1;j)

7
1. G1 : Game
2. ∀m:Game
     ((left-option{i:l}(G1;m) ∨ right-option{i:l}(G1;m)) ⇒ (∀H1,G2,H2:Game.  (m ≡ G2 ⇒ H1 ≡ H2 ⇒ m ⊕ H1 ≡ G2 ⊕ H2)))
3. H1 : Game
4. ∀m:Game
     ((left-option{i:l}(H1;m) ∨ right-option{i:l}(H1;m)) ⇒ (∀G2,H2:Game.  (G1 ≡ G2 ⇒ m ≡ H2 ⇒ G1 ⊕ m ≡ G2 ⊕ H2)))
5. G2 : Game
6. ∀m:Game. ((left-option{i:l}(G2;m) ∨ right-option{i:l}(G2;m)) ⇒ (∀H2:Game. (G1 ≡ m ⇒ H1 ≡ H2 ⇒ G1 ⊕ H1 ≡ m ⊕ H2)))
7. H2 : Game
8. ∀m:Game. ((left-option{i:l}(H2;m) ∨ right-option{i:l}(H2;m)) ⇒ G1 ≡ G2 ⇒ H1 ≡ m ⇒ G1 ⊕ H1 ≡ G2 ⊕ m)
9. G1 ≡ G2
10. H1 ≡ H2

11. ∀i:left-indices(G2 ⊕ H2). ∃j:left-indices(G1 ⊕ H1). left-move(G2 ⊕ H2;i) ≡ left-move(G1 ⊕ H1;j)

12. x : right-indices(G2)
⊢ ∃j:right-indices(G1 ⊕ H1). right-move(G2 ⊕ H2;inl x) ≡ right-move(G1 ⊕ H1;j)

8
1. G1 : Game
2. ∀m:Game
((left-option{i:l}(G1;m) ∨ right-option{i:l}(G1;m)) ⇒ (∀H1,G2,H2:Game. (m ≡ G2 ⇒ H1 ≡ H2 ⇒ m ⊕ H1 ≡ G2 ⊕ H2)))
3. H1 : Game
4. ∀m:Game
((left-option{i:l}(H1;m) ∨ right-option{i:l}(H1;m)) ⇒ (∀G2,H2:Game. (G1 ≡ G2 ⇒ m ≡ H2 ⇒ G1 ⊕ m ≡ G2 ⊕ H2)))
5. G2 : Game
6. ∀m:Game. ((left-option{i:l}(G2;m) ∨ right-option{i:l}(G2;m)) ⇒ (∀H2:Game. (G1 ≡ m ⇒ H1 ≡ H2 ⇒ G1 ⊕ H1 ≡ m ⊕ H2)))
7. H2 : Game
8. ∀m:Game. ((left-option{i:l}(H2;m) ∨ right-option{i:l}(H2;m)) ⇒ G1 ≡ G2 ⇒ H1 ≡ m ⇒ G1 ⊕ H1 ≡ G2 ⊕ m)
9. G1 ≡ G2
10. H1 ≡ H2

11. ∀i:left-indices(G2 ⊕ H2). ∃j:left-indices(G1 ⊕ H1). left-move(G2 ⊕ H2;i) ≡ left-move(G1 ⊕ H1;j)

12. y : right-indices(H2)
⊢ ∃j:right-indices(G1 ⊕ H1). right-move(G2 ⊕ H2;inr y ) ≡ right-move(G1 ⊕ H1;j)

Latex:

Latex:
\mforall{}G1,H1,G2,H2:Game. (G1 \mequiv{} G2 {}\mRightarrow{} H1 \mequiv{} H2 {}\mRightarrow{} G1 \moplus{} H1 \mequiv{} G2 \moplus{} H2) By Latex: (RepeatFor 4 (((BLemma `Game-induction` THENA Auto) THEN RepeatFor 2 ((D 0 THENA Auto)))) THEN 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) Home Index