---

Step * 2 of Lemma strat2play-invariant-1


1. g : SimpleGame
2. n : ℤ
3. 0 < n
4. ∀s:win2strat(g;n - 1). ∀moves:strat2play(g;n - 1;s).
     ((moves[0] = InitialPos(g) ∈ Pos(g))
     ∧ (∀i:ℕ(n - 1) + 1
          ((↓Legal1(moves[2 * i];moves[(2 * i) + 1]))
          ∧ (i < n - 1
            ⇒ ((↓Legal2(moves[(2 * i) + 1];moves[2 * (i + 1)]))
               ∧ (moves[2 * (i + 1)] = (s play-truncate(moves;2 * (i + 1))) ∈ Pos(g)))))))
5. s : win2strat(g;n)
6. moves : strat2play(g;n;s)
⊢ (moves[0] = InitialPos(g) ∈ Pos(g))
∧ (∀i:ℕn + 1
     ((↓Legal1(moves[2 * i];moves[(2 * i) + 1]))
     ∧ (i < n
       ⇒ ((↓Legal2(moves[(2 * i) + 1];moves[2 * (i + 1)]))
          ∧ (moves[2 * (i + 1)] = (s play-truncate(moves;2 * (i + 1))) ∈ Pos(g))))))
BY
{ ((Assert moves ∈ strat2play(g;n;s) BY
          Declaration)
   THEN (Assert s ∈ win2strat(g;n) BY
               Declaration)
   THEN Unfold `strat2play` -3
   THEN (SplitOnHypITE -3  THENA Auto)
   THEN ((DepIsectHD (-4) THEN (MemTypeHD (-4) THENA Auto) THEN All (Fold `member`)) ORELSE Auto)
   THEN Unfold `win2strat` 5
   THEN (SplitOnHypITE 5  THENA Auto)
   THEN Try (Trivial)
   THEN DepIsectHD 5
   THEN (D 4 With ⌜s⌝  THENA Auto)
   THEN (D -1 With ⌜moves⌝  THENA Auto)
   THEN ParallelLast) }

1
1. g : SimpleGame
2. n : ℤ
3. 0 < n
4. s : s:win2strat(g;n - 1) ⋂ moves:{f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(g)| Legal2(moves[(2 * n) -\000C 1];p)} 
5. s ∈ win2strat(g;n - 1)
6. s ∈ moves:{f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(g)| Legal2(moves[(2 * n) - 1];p)} 
7. moves : f:strat2play(g;n - 1;s) ⋂ {moves:sequence(Pos(g))| 
                                      (((2 * n) + 2) ≤ ||moves||)
                                      ∧ Legal1(moves[2 * n];moves[(2 * n) + 1])
                                      ∧ (moves[2 * n] = (s play-truncate(f;2 * n)) ∈ Pos(g))} 
8. moves ∈ strat2play(g;n - 1;s)
9. moves ∈ sequence(Pos(g))
10. [%22] : (((2 * n) + 2) ≤ ||moves||)
∧ Legal1(moves[2 * n];moves[(2 * n) + 1])
∧ (moves[2 * n] = (s play-truncate(moves;2 * n)) ∈ Pos(g))
11. moves ∈ strat2play(g;n;s)
12. s ∈ win2strat(g;n)
13. ¬(n = 0 ∈ ℤ)
14. ¬(n = 0 ∈ ℤ)
15. moves[0] = InitialPos(g) ∈ Pos(g)
16. ∀i:ℕ(n - 1) + 1
      ((↓Legal1(moves[2 * i];moves[(2 * i) + 1]))
      ∧ (i < n - 1
        ⇒ ((↓Legal2(moves[(2 * i) + 1];moves[2 * (i + 1)]))
           ∧ (moves[2 * (i + 1)] = (s play-truncate(moves;2 * (i + 1))) ∈ Pos(g)))))
⊢ ∀i:ℕn + 1
    ((↓Legal1(moves[2 * i];moves[(2 * i) + 1]))
    ∧ (i < n
      ⇒ ((↓Legal2(moves[(2 * i) + 1];moves[2 * (i + 1)]))
         ∧ (moves[2 * (i + 1)] = (s play-truncate(moves;2 * (i + 1))) ∈ Pos(g)))))

---

Latex:

---

Latex:

1.  g  :  SimpleGame
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  \mforall{}s:win2strat(g;n  -  1).  \mforall{}moves:strat2play(g;n  -  1;s).
          ((moves[0]  =  InitialPos(g))
          \mwedge{}  (\mforall{}i:\mBbbN{}(n  -  1)  +  1
                    ((\mdownarrow{}Legal1(moves[2  *  i];moves[(2  *  i)  +  1]))
                    \mwedge{}  (i  <  n  -  1
                        {}\mRightarrow{}  ((\mdownarrow{}Legal2(moves[(2  *  i)  +  1];moves[2  *  (i  +  1)]))
                              \mwedge{}  (moves[2  *  (i  +  1)]  =  (s  play-truncate(moves;2  *  (i  +  1)))))))))
5.  s  :  win2strat(g;n)
6.  moves  :  strat2play(g;n;s)
\mvdash{}  (moves[0]  =  InitialPos(g))
\mwedge{}  (\mforall{}i:\mBbbN{}n  +  1
          ((\mdownarrow{}Legal1(moves[2  *  i];moves[(2  *  i)  +  1]))
          \mwedge{}  (i  <  n
              {}\mRightarrow{}  ((\mdownarrow{}Legal2(moves[(2  *  i)  +  1];moves[2  *  (i  +  1)]))
                    \mwedge{}  (moves[2  *  (i  +  1)]  =  (s  play-truncate(moves;2  *  (i  +  1))))))))


By

---

Latex:
((Assert  moves  \mmember{}  strat2play(g;n;s)  BY
                Declaration)
  THEN  (Assert  s  \mmember{}  win2strat(g;n)  BY
                          Declaration)
  THEN  Unfold  `strat2play`  -3
  THEN  (SplitOnHypITE  -3    THENA  Auto)
  THEN  ((DepIsectHD  (-4)  THEN  (MemTypeHD  (-4)  THENA  Auto)  THEN  All  (Fold  `member`))  ORELSE  Auto)
  THEN  Unfold  `win2strat`  5
  THEN  (SplitOnHypITE  5    THENA  Auto)
  THEN  Try  (Trivial)
  THEN  DepIsectHD  5
  THEN  (D  4  With  \mkleeneopen{}s\mkleeneclose{}    THENA  Auto)
  THEN  (D  -1  With  \mkleeneopen{}moves\mkleeneclose{}    THENA  Auto)
  THEN  ParallelLast)

---

Home Index