---

Step * of Lemma Game_ext

Game ≡ LR:GameA{i:l}() × (GameB(LR) ⟶ Game)
BY
{ (InstLemma  `W-ext` [⌜parm{i'}⌝;⌜GameA{i:l}()⌝;⌜λ2LR.GameB(LR)⌝]⋅ THEN Try (Fold `Game` (-1)) THEN Auto) }

---

Latex:

---

Latex:
Game  \mequiv{}  LR:GameA\{i:l\}()  \mtimes{}  (GameB(LR)  {}\mrightarrow{}  Game)


By

---

Latex:
(InstLemma    `W-ext`  [\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}GameA\{i:l\}()\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}LR.GameB(LR)\mkleeneclose{}]\mcdot{}
  THEN  Try  (Fold  `Game`  (-1))
  THEN  Auto)

---

Home Index