---

Step * 1 of Lemma respond-implies-win2

.....subterm..... T:t
1:n
1. g : SimpleGame
2. m : p:{p:Pos(g)| Legal1(InitialPos(g);p)}  ⟶ {q:Pos(g)| Legal2(p;q)} 
3. s : ∀p:{p:Pos(g)| Legal1(InitialPos(g);p)} . ∀[n:ℕ]. win2strat(g@m p;n)
4. n : ℤ
5. 0 < n
6. λmoves.if (||moves|| =z 2) then m moves[1] else s moves[1] seq-tl(seq-tl(moves)) fi  ∈ win2strat(g;n - 1)
7. ¬(n = 0 ∈ ℤ)
8. moves : {f:strat2play(g;n - 1;λmoves.if (||moves|| =z 2) then m moves[1] else s moves[1] seq-tl(seq-tl(moves)) fi )| 
            ||f|| = (2 * n) ∈ ℤ} 
⊢ if (||moves|| =z 2) then m moves[1] else s moves[1] seq-tl(seq-tl(moves)) fi  ∈ {p:Pos(g)| 
                                                                                   Legal2(moves[(2 * n) - 1];p)} 
BY
{ (D -1
   THEN (Assert moves[1] ∈ {p:Pos(g)| Legal1(InitialPos(g);p)}  BY
               ((Strat2PlayInvariant (-2) THENA Auto)
                THEN D -1
                THEN (D -1 With ⌜0⌝  THENA Auto)
                THEN D -1
                THEN Thin (-1)
                THEN Reduce -1
                THEN D -1
                THEN (MemTypeCD THEN Auto)
                THEN RWO "-2<" 0
                THEN Auto))
   ) }

1
1. g : SimpleGame
2. m : p:{p:Pos(g)| Legal1(InitialPos(g);p)}  ⟶ {q:Pos(g)| Legal2(p;q)} 
3. s : ∀p:{p:Pos(g)| Legal1(InitialPos(g);p)} . ∀[n:ℕ]. win2strat(g@m p;n)
4. n : ℤ
5. 0 < n
6. λmoves.if (||moves|| =z 2) then m moves[1] else s moves[1] seq-tl(seq-tl(moves)) fi  ∈ win2strat(g;n - 1)
7. ¬(n = 0 ∈ ℤ)
8. moves : strat2play(g;n - 1;λmoves.if (||moves|| =z 2) then m moves[1] else s moves[1] seq-tl(seq-tl(moves)) fi )
9. ||moves|| = (2 * n) ∈ ℤ
10. moves[1] ∈ {p:Pos(g)| Legal1(InitialPos(g);p)} 
⊢ if (||moves|| =z 2) then m moves[1] else s moves[1] seq-tl(seq-tl(moves)) fi  ∈ {p:Pos(g)| 
                                                                                   Legal2(moves[(2 * n) - 1];p)} 

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  g  :  SimpleGame
2.  m  :  p:\{p:Pos(g)|  Legal1(InitialPos(g);p)\}    {}\mrightarrow{}  \{q:Pos(g)|  Legal2(p;q)\} 
3.  s  :  \mforall{}p:\{p:Pos(g)|  Legal1(InitialPos(g);p)\}  .  \mforall{}[n:\mBbbN{}].  win2strat(g@m  p;n)
4.  n  :  \mBbbZ{}
5.  0  <  n
6.  \mlambda{}moves.if  (||moves||  =\msubz{}  2)  then  m  moves[1]  else  s  moves[1]  seq-tl(seq-tl(moves))  fi 
      \mmember{}  win2strat(g;n  -  1)
7.  \mneg{}(n  =  0)
8.  moves  :  \{f:strat2play(g;n  -  1;\mlambda{}moves.if  (||moves||  =\msubz{}  2)
                                                                                then  m  moves[1]
                                                                                else  s  moves[1]  seq-tl(seq-tl(moves))
                                                                                fi  )| 
                        ||f||  =  (2  *  n)\} 
\mvdash{}  if  (||moves||  =\msubz{}  2)  then  m  moves[1]  else  s  moves[1]  seq-tl(seq-tl(moves))  fi    \mmember{}  \{p:Pos(g)| 
                                                                                                                                                                      Legal2(moves[(2
                                                                                                                                                                      *  n)  -  1];p)\} 


By

---

Latex:
(D  -1
  THEN  (Assert  moves[1]  \mmember{}  \{p:Pos(g)|  Legal1(InitialPos(g);p)\}    BY
                          ((Strat2PlayInvariant  (-2)  THENA  Auto)
                            THEN  D  -1
                            THEN  (D  -1  With  \mkleeneopen{}0\mkleeneclose{}    THENA  Auto)
                            THEN  D  -1
                            THEN  Thin  (-1)
                            THEN  Reduce  -1
                            THEN  D  -1
                            THEN  (MemTypeCD  THEN  Auto)
                            THEN  RWO  "-2<"  0
                            THEN  Auto))
  )

---

Home Index