Proof of Nuprl Lemma : eq-Game

Step * 1 of Lemma eq-Game_transitivity

1. g : Game
2. ∀m:Game. ((left-option{i:l}(g;m) ∨ right-option{i:l}(g;m)) ⇒ (∀H,K:Game. (m ≡ H ⇒ H ≡ K ⇒ m ≡ K)))
3. H : Game
4. K : Game
5. g ≡ H
6. H ≡ K
⊢ g ≡ K
BY

{ ((All (Unfold `eq-Game`) THEN Fold `eq-Game` 2) THEN Auto THEN ∀h:hyp. ((D h With ⌜i⌝  THENA Trivial) THEN ExRepD) ) }

1
1. g : Game
2. ∀m:Game. ((left-option{i:l}(g;m) ∨ right-option{i:l}(g;m)) ⇒ (∀H,K:Game.  (m ≡ H ⇒ H ≡ K ⇒ m ≡ K)))
3. H : Game
4. K : Game
5. ∀i:right-indices(g). ∃j:right-indices(H). right-move(g;i) ≡ right-move(H;j)
6. ∀i:left-indices(H). ∃j:left-indices(g). left-move(H;i) ≡ left-move(g;j)
7. ∀i:right-indices(H). ∃j:right-indices(g). right-move(H;i) ≡ right-move(g;j)
8. ∀i:left-indices(H). ∃j:left-indices(K). left-move(H;i) ≡ left-move(K;j)
9. ∀i:right-indices(H). ∃j:right-indices(K). right-move(H;i) ≡ right-move(K;j)
10. ∀i:left-indices(K). ∃j:left-indices(H). left-move(K;i) ≡ left-move(H;j)
11. ∀i:right-indices(K). ∃j:right-indices(H). right-move(K;i) ≡ right-move(H;j)
12. i : left-indices(g)
13. j : left-indices(H)
14. left-move(g;i) ≡ left-move(H;j)
⊢ ∃j:left-indices(K). left-move(g;i) ≡ left-move(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 ⇒ H ≡ K ⇒ m ≡ K)))
3. H : Game
4. K : Game
5. ∀i:left-indices(g). ∃j:left-indices(H). left-move(g;i) ≡ left-move(H;j)
6. ∀i:left-indices(H). ∃j:left-indices(g). left-move(H;i) ≡ left-move(g;j)
7. ∀i:right-indices(H). ∃j:right-indices(g). right-move(H;i) ≡ right-move(g;j)
8. ∀i:left-indices(H). ∃j:left-indices(K). left-move(H;i) ≡ left-move(K;j)
9. ∀i:right-indices(H). ∃j:right-indices(K). right-move(H;i) ≡ right-move(K;j)
10. ∀i:left-indices(K). ∃j:left-indices(H). left-move(K;i) ≡ left-move(H;j)
11. ∀i:right-indices(K). ∃j:right-indices(H). right-move(K;i) ≡ right-move(H;j)
12. ∀i:left-indices(g). ∃j:left-indices(K). left-move(g;i) ≡ left-move(K;j)
13. i : right-indices(g)
14. j : right-indices(H)
15. right-move(g;i) ≡ right-move(H;j)
⊢ ∃j:right-indices(K). right-move(g;i) ≡ right-move(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 ⇒ H ≡ K ⇒ m ≡ K)))
3. H : Game
4. K : Game
5. ∀i:left-indices(g). ∃j:left-indices(H). left-move(g;i) ≡ left-move(H;j)
6. ∀i:right-indices(g). ∃j:right-indices(H). right-move(g;i) ≡ right-move(H;j)
7. ∀i:left-indices(H). ∃j:left-indices(g). left-move(H;i) ≡ left-move(g;j)
8. ∀i:right-indices(H). ∃j:right-indices(g). right-move(H;i) ≡ right-move(g;j)
9. ∀i:left-indices(H). ∃j:left-indices(K). left-move(H;i) ≡ left-move(K;j)
10. ∀i:right-indices(H). ∃j:right-indices(K). right-move(H;i) ≡ right-move(K;j)
11. ∀i:right-indices(K). ∃j:right-indices(H). right-move(K;i) ≡ right-move(H;j)
12. ∀i:left-indices(g). ∃j:left-indices(K). left-move(g;i) ≡ left-move(K;j)
13. ∀i:right-indices(g). ∃j:right-indices(K). right-move(g;i) ≡ right-move(K;j)
14. i : left-indices(K)
15. j : left-indices(H)
16. left-move(K;i) ≡ left-move(H;j)
⊢ ∃j:left-indices(g). left-move(K;i) ≡ left-move(g;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 ⇒ H ≡ K ⇒ m ≡ K)))
3. H : Game
4. K : Game
5. ∀i:left-indices(g). ∃j:left-indices(H). left-move(g;i) ≡ left-move(H;j)
6. ∀i:right-indices(g). ∃j:right-indices(H). right-move(g;i) ≡ right-move(H;j)
7. ∀i:left-indices(H). ∃j:left-indices(g). left-move(H;i) ≡ left-move(g;j)
8. ∀i:right-indices(H). ∃j:right-indices(g). right-move(H;i) ≡ right-move(g;j)
9. ∀i:left-indices(H). ∃j:left-indices(K). left-move(H;i) ≡ left-move(K;j)
10. ∀i:right-indices(H). ∃j:right-indices(K). right-move(H;i) ≡ right-move(K;j)
11. ∀i:left-indices(K). ∃j:left-indices(H). left-move(K;i) ≡ left-move(H;j)
12. ∀i:left-indices(g). ∃j:left-indices(K). left-move(g;i) ≡ left-move(K;j)
13. ∀i:right-indices(g). ∃j:right-indices(K). right-move(g;i) ≡ right-move(K;j)
14. ∀i:left-indices(K). ∃j:left-indices(g). left-move(K;i) ≡ left-move(g;j)
15. i : right-indices(K)
16. j : right-indices(H)
17. right-move(K;i) ≡ right-move(H;j)
⊢ ∃j:right-indices(g). right-move(K;i) ≡ right-move(g;j)

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 \mequiv{} H {}\mRightarrow{} H \mequiv{} K {}\mRightarrow{} m \mequiv{} K))) 3. H : Game 4. K : Game 5. g \mequiv{} H 6. H \mequiv{} K \mvdash{} g \mequiv{} K By Latex: ((All (Unfold `eq-Game`) THEN Fold `eq-Game` 2) THEN Auto THEN \mforall{}h:hyp. ((D h With \mkleeneopen{}i\mkleeneclose{} THENA Trivial) THEN ExRepD) ) Home Index