---

Step * 1 of Lemma eq-Game_wf


1. G : Game
⊢ ∀H:Game. ((G ≡ H ∈ ℙ) ∧ (H ≡ G ∈ ℙ))
BY
{ (Unfold `Game` 1 THEN WElim 1) }

1
1. a : GameA{i:l}()
2. f : GameB(a) ⟶ W(GameA{i:l}();a.GameB(a))
3. ∀b:GameB(a). (λH.<Ax, Ax> ∈ ∀H:Game. ((f b ≡ H ∈ ℙ) ∧ (H ≡ f b ∈ ℙ)))
⊢ λH.<Ax, Ax> ∈ ∀H:Game. ((Wsup(a;f) ≡ H ∈ ℙ) ∧ (H ≡ Wsup(a;f) ∈ ℙ))

---

Latex:

---

Latex:

1.  G  :  Game
\mvdash{}  \mforall{}H:Game.  ((G  \mequiv{}  H  \mmember{}  \mBbbP{})  \mwedge{}  (H  \mequiv{}  G  \mmember{}  \mBbbP{}))


By

---

Latex:
(Unfold  `Game`  1  THEN  WElim  1)

---

Home Index