---

Step * 1 of Lemma win2-iff


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)
BY
{ ((Assert seq-cons(InitialPos(g);seq-cons(p;seq-nil())) ∈ {f:strat2play(g;0;s)| ||f|| = 2 ∈ ℤ}  BY
          ((MemTypeCD THEN Auto)
           THEN D -3
           THEN Unfold `strat2play` 0
           THEN Reduce 0
           THEN MemTypeCD
           THEN Auto
           THEN All (Unfold  `play-item`)
           THEN Auto
           THEN (Subst' ||seq-cons(InitialPos(g);seq-cons(p;seq-nil()))|| ~ 2 0 THENA Computation)
           THEN Auto))
   THEN (Assert s seq-cons(InitialPos(g);seq-cons(p;seq-nil())) ∈ {q:Pos(g)| Legal2(p;q)}  BY
               Auto)
   THEN D 0 With ⌜s seq-cons(InitialPos(g);seq-cons(p;seq-nil()))⌝ 
   THEN Auto
   THEN (D 0 THENA Auto)) }

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)} 
6. seq-cons(InitialPos(g);seq-cons(p;seq-nil())) ∈ {f:strat2play(g;0;s)| ||f|| = 2 ∈ ℤ} 
7. s seq-cons(InitialPos(g);seq-cons(p;seq-nil())) ∈ {q:Pos(g)| Legal2(p;q)} 
8. [n] : ℕ
⊢ win2strat(g@s seq-cons(InitialPos(g);seq-cons(p;seq-nil()));n)

---

Latex:

---

Latex:

1.  g  :  SimpleGame
2.  s  :  \mforall{}[n:\mBbbN{}].  win2strat(g;n)
3.  p  :  \{p:Pos(g)|  Legal1(InitialPos(g);p)\} 
4.  s  \mmember{}  win2strat(g;1  -  1)
5.  s  \mmember{}  moves:\{f:strat2play(g;0;s)|  ||f||  =  2\}    {}\mrightarrow{}  \{p:Pos(g)|  Legal2(moves[1];p)\} 
\mvdash{}  \mexists{}q:\{q:Pos(g)|  Legal2(p;q)\}  .  win2(g@q)


By

---

Latex:
((Assert  seq-cons(InitialPos(g);seq-cons(p;seq-nil()))  \mmember{}  \{f:strat2play(g;0;s)|  ||f||  =  2\}    BY
                ((MemTypeCD  THEN  Auto)
                  THEN  D  -3
                  THEN  Unfold  `strat2play`  0
                  THEN  Reduce  0
                  THEN  MemTypeCD
                  THEN  Auto
                  THEN  All  (Unfold    `play-item`)
                  THEN  Auto
                  THEN  (Subst'  ||seq-cons(InitialPos(g);seq-cons(p;seq-nil()))||  \msim{}  2  0  THENA  Computation)
                  THEN  Auto))
  THEN  (Assert  s  seq-cons(InitialPos(g);seq-cons(p;seq-nil()))  \mmember{}  \{q:Pos(g)|  Legal2(p;q)\}    BY
                          Auto)
  THEN  D  0  With  \mkleeneopen{}s  seq-cons(InitialPos(g);seq-cons(p;seq-nil()))\mkleeneclose{} 
  THEN  Auto
  THEN  (D  0  THENA  Auto))

---

Home Index