---

Step * of Lemma win2-iff

∀g:SimpleGame. (win2(g) ⇐⇒ ∀p:{p:Pos(g)| Legal1(InitialPos(g);p)} . ∃q:{q:Pos(g)| Legal2(p;q)} . win2(g@q))
BY
{ (Auto
   THEN Try ((BLemma `respond-implies-win2` THEN Auto))
   THEN RenameVar `s' 2
   THEN Unfold `win2` 2
   THEN (InstLemma `win2strat-properties` [⌜g⌝;⌜1⌝;⌜s⌝]⋅ THENA Auto)
   THEN D -1
   THEN Reduce -1) }

1
1. g : SimpleGame
2. s : ∀[n:ℕ]. win2strat(g;n)
3. p : {p:Pos(g)| Legal1(InitialPos(g);p)} 
4. s ∈ win2strat(g;1 - 1)
5. s ∈ moves:{f:strat2play(g;0;s)| ||f|| = 2 ∈ ℤ}  ⟶ {p:Pos(g)| Legal2(moves[1];p)} 
⊢ ∃q:{q:Pos(g)| Legal2(p;q)} . win2(g@q)

---

Latex:

---

Latex:
\mforall{}g:SimpleGame
    (win2(g)  \mLeftarrow{}{}\mRightarrow{}  \mforall{}p:\{p:Pos(g)|  Legal1(InitialPos(g);p)\}  .  \mexists{}q:\{q:Pos(g)|  Legal2(p;q)\}  .  win2(g@q))


By

---

Latex:
(Auto
  THEN  Try  ((BLemma  `respond-implies-win2`  THEN  Auto))
  THEN  RenameVar  `s'  2
  THEN  Unfold  `win2`  2
  THEN  (InstLemma  `win2strat-properties`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  Reduce  -1)

---

Home Index