---

Step * 2 of Lemma eq-Game_weakening


1. g : Game
2. ∀m:Game. ((left-option{i:l}(g;m) ∨ right-option{i:l}(g;m)) ⇒ (∀H:Game. ((m = H ∈ Game) ⇒ m ≡ H)))
3. H : Game
4. g = H ∈ Game
5. ∀i:left-indices(H). ∃j:left-indices(g). left-move(H;i) ≡ left-move(g;j)
6. i : right-indices(H)
⊢ (∃x:left-indices(g). (right-move(H;i) = left-move(g;x) ∈ Game))
∨ (∃x:right-indices(g). (right-move(H;i) = right-move(g;x) ∈ Game))
BY
{ (HypSubst' (-3) 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:Game.  ((m  =  H)  {}\mRightarrow{}  m  \mequiv{}  H)))
3.  H  :  Game
4.  g  =  H
5.  \mforall{}i:left-indices(H).  \mexists{}j:left-indices(g).  left-move(H;i)  \mequiv{}  left-move(g;j)
6.  i  :  right-indices(H)
\mvdash{}  (\mexists{}x:left-indices(g).  (right-move(H;i)  =  left-move(g;x)))
\mvee{}  (\mexists{}x:right-indices(g).  (right-move(H;i)  =  right-move(g;x)))


By

---

Latex:
(HypSubst'  (-3)  0  THEN  Auto)

---

Home Index