---

Step * 1 of Lemma Game-minus_wf


1. G : W(GameA{i:l}();p.GameB(p))
⊢ -(G) ∈ Game
BY
{ WElim 1 }

1
1. a : GameA{i:l}()
2. f : GameB(a) ⟶ W(GameA{i:l}();a.GameB(a))
3. ∀b:GameB(a). (-(f b) ∈ Game)
⊢ -(Wsup(a;f)) ∈ Game

---

Latex:

---

Latex:

1.  G  :  W(GameA\{i:l\}();p.GameB(p))
\mvdash{}  -(G)  \mmember{}  Game


By

---

Latex:
WElim  1

---

Home Index