---

Step * 1 2 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: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)
BY
{ ((Assert ∃k:right-indices(K). right-move(H;j) ≡ right-move(K;k) BY
          Auto)
   THEN ParallelLast
   THEN (FHyp 2 [-3;-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:left-indices(H).  \mexists{}j:left-indices(g).  left-move(H;i)  \mequiv{}  left-move(g;j)
7.  \mforall{}i:right-indices(H).  \mexists{}j:right-indices(g).  right-move(H;i)  \mequiv{}  right-move(g;j)
8.  \mforall{}i:left-indices(H).  \mexists{}j:left-indices(K).  left-move(H;i)  \mequiv{}  left-move(K;j)
9.  \mforall{}i:right-indices(H).  \mexists{}j:right-indices(K).  right-move(H;i)  \mequiv{}  right-move(K;j)
10.  \mforall{}i:left-indices(K).  \mexists{}j:left-indices(H).  left-move(K;i)  \mequiv{}  left-move(H;j)
11.  \mforall{}i:right-indices(K).  \mexists{}j:right-indices(H).  right-move(K;i)  \mequiv{}  right-move(H;j)
12.  \mforall{}i:left-indices(g).  \mexists{}j:left-indices(K).  left-move(g;i)  \mequiv{}  left-move(K;j)
13.  i  :  right-indices(g)
14.  j  :  right-indices(H)
15.  right-move(g;i)  \mequiv{}  right-move(H;j)
\mvdash{}  \mexists{}j:right-indices(K).  right-move(g;i)  \mequiv{}  right-move(K;j)


By

---

Latex:
((Assert  \mexists{}k:right-indices(K).  right-move(H;j)  \mequiv{}  right-move(K;k)  BY
                Auto)
  THEN  ParallelLast
  THEN  (FHyp  2  [-3;-1]  THEN  Auto)
  THEN  RepUR  ``left-option  right-option``  0
  THEN  Auto)

---

Home Index