---

Step * 1 4 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. ∀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)
18. k : right-indices(g)
19. right-move(H;j) ≡ right-move(g;k)
20. right-move(H;j) ≡ right-move(K;i)
21. right-move(g;k) ≡ right-move(H;j)
⊢ right-move(g;k) ≡ right-move(K;i)
BY
{ ((FHyp 2 [-2;-1] THEN Auto) 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  \mequiv{}  H  {}\mRightarrow{}  H  \mequiv{}  K  {}\mRightarrow{}  m  \mequiv{}  K)))
3.  H  :  Game
4.  K  :  Game
5.  \mforall{}i:left-indices(g).  \mexists{}j:left-indices(H).  left-move(g;i)  \mequiv{}  left-move(H;j)
6.  \mforall{}i:right-indices(g).  \mexists{}j:right-indices(H).  right-move(g;i)  \mequiv{}  right-move(H;j)
7.  \mforall{}i:left-indices(H).  \mexists{}j:left-indices(g).  left-move(H;i)  \mequiv{}  left-move(g;j)
8.  \mforall{}i:right-indices(H).  \mexists{}j:right-indices(g).  right-move(H;i)  \mequiv{}  right-move(g;j)
9.  \mforall{}i:left-indices(H).  \mexists{}j:left-indices(K).  left-move(H;i)  \mequiv{}  left-move(K;j)
10.  \mforall{}i:right-indices(H).  \mexists{}j:right-indices(K).  right-move(H;i)  \mequiv{}  right-move(K;j)
11.  \mforall{}i:left-indices(K).  \mexists{}j:left-indices(H).  left-move(K;i)  \mequiv{}  left-move(H;j)
12.  \mforall{}i:left-indices(g).  \mexists{}j:left-indices(K).  left-move(g;i)  \mequiv{}  left-move(K;j)
13.  \mforall{}i:right-indices(g).  \mexists{}j:right-indices(K).  right-move(g;i)  \mequiv{}  right-move(K;j)
14.  \mforall{}i:left-indices(K).  \mexists{}j:left-indices(g).  left-move(K;i)  \mequiv{}  left-move(g;j)
15.  i  :  right-indices(K)
16.  j  :  right-indices(H)
17.  right-move(K;i)  \mequiv{}  right-move(H;j)
18.  k  :  right-indices(g)
19.  right-move(H;j)  \mequiv{}  right-move(g;k)
20.  right-move(H;j)  \mequiv{}  right-move(K;i)
21.  right-move(g;k)  \mequiv{}  right-move(H;j)
\mvdash{}  right-move(g;k)  \mequiv{}  right-move(K;i)


By

---

Latex:
((FHyp  2  [-2;-1]  THEN  Auto)  THEN  RepUR  ``left-option  right-option``  0  THEN  Auto)

---

Home Index