---

Step * 4 of Lemma strat2play-longer

.....eq aux..... 
1. g : SimpleGame
2. n : ℤ
3. 0 < n
4. <Ax, Ax> ∈ ∀[s:win2strat(g;n - 1)]. ∀[moves:strat2play(g;n - 1;s)]. ∀[x:sequence(Pos(g))].
                ((x ∈ strat2play(g;n - 1;s)) ∧ (seq-truncate(x;||moves||) = moves ∈ strat2play(g;n - 1;s))) supposing 
                   ((seq-truncate(x;||moves||) = moves ∈ sequence(Pos(g))) and 
                   (||moves|| ≤ ||x||))
5. s : win2strat(g;n)
6. moves : strat2play(g;n;s)
7. x : sequence(Pos(g))
8. moves ∈ {moves:sequence(Pos(g))| ((2 * n) + 2) ≤ ||moves||} 
9. ||moves|| ≤ ||x||
10. seq-truncate(x;||moves||) = moves ∈ sequence(Pos(g))
11. ∀i:ℕ||moves||. (x[i] = moves[i] ∈ Pos(g))
⊢ seq-truncate(x;||moves||) = moves ∈ strat2play(g;n;s)
BY
{ ((Assert ∀[s:win2strat(g;n - 1)]. ∀[moves:strat2play(g;n - 1;s)]. ∀[x:sequence(Pos(g))].
             ((x ∈ strat2play(g;n - 1;s)) ∧ (seq-truncate(x;||moves||) = moves ∈ strat2play(g;n - 1;s))) supposing 
                ((seq-truncate(x;||moves||) = moves ∈ sequence(Pos(g))) and 
                (||moves|| ≤ ||x||)) BY
          (UseWitness ⌜<Ax, Ax>⌝⋅ THEN Trivial))
   THEN Thin 4
   THEN PromoteHyp (-1) 4
   THEN Unfold `strat2play` -6
   THEN (SplitOnHypITE -6  THENA Auto)
   THEN Try ((Assert ⌜False⌝⋅ THEN Complete (Auto)))
   THEN DepIsectHD (-7)
   THEN Unfold `strat2play` 0
   THEN (SplitOnConclITE THENA Auto)
   THEN Try ((Assert ⌜False⌝⋅ THEN Complete (Auto)))
   THEN DepIsectCD
   THEN (InstHyp [⌜s⌝;⌜moves⌝;⌜x⌝] 4⋅ THENA Auto)
   THEN ExRepD
   THEN Try (Trivial)
   THEN All (RepUR ``play-len play-item``)
   THEN (MemTypeHD 8 THENA Auto)
   THEN All (Fold `member`)
   THEN ExRepD) }

1
1. g : SimpleGame
2. n : ℤ
3. 0 < n
4. ∀[s:win2strat(g;n - 1)]. ∀[moves:strat2play(g;n - 1;s)]. ∀[x:sequence(Pos(g))].
     ((x ∈ strat2play(g;n - 1;s)) ∧ (seq-truncate(x;||moves||) = moves ∈ strat2play(g;n - 1;s))) supposing 
        ((seq-truncate(x;||moves||) = moves ∈ sequence(Pos(g))) and 
        (||moves|| ≤ ||x||))
5. s : win2strat(g;n)
6. 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))} 
7. moves ∈ strat2play(g;n - 1;s)
8. moves ∈ sequence(Pos(g))
9. ((2 * n) + 2) ≤ ||moves||
10. Legal1(moves[2 * n];moves[(2 * n) + 1])
11. moves[2 * n] = (s play-truncate(moves;2 * n)) ∈ Pos(g)
12. x : sequence(Pos(g))
13. moves ∈ {moves:sequence(Pos(g))| ((2 * n) + 2) ≤ ||moves||} 
14. ||moves|| ≤ ||x||
15. seq-truncate(x;||moves||) = moves ∈ sequence(Pos(g))
16. ∀i:ℕ||moves||. (x[i] = moves[i] ∈ Pos(g))
17. ¬(n = 0 ∈ ℤ)
18. ¬(n = 0 ∈ ℤ)
19. x ∈ strat2play(g;n - 1;s)
20. seq-truncate(x;||moves||) = moves ∈ strat2play(g;n - 1;s)
⊢ seq-truncate(x;||moves||)
= moves
∈ {moves@0:sequence(Pos(g))| 
   (((2 * n) + 2) ≤ ||moves@0||)
   ∧ Legal1(moves@0[2 * n];moves@0[(2 * n) + 1])
   ∧ (moves@0[2 * n] = (s play-truncate(seq-truncate(x;||moves||);2 * n)) ∈ Pos(g))} 

---

Latex:

---

Latex:
.....eq  aux..... 
1.  g  :  SimpleGame
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  <Ax,  Ax>  \mmember{}  \mforall{}[s:win2strat(g;n  -  1)].  \mforall{}[moves:strat2play(g;n  -  1;s)].  \mforall{}[x:sequence(Pos(g))].
                                ((x  \mmember{}  strat2play(g;n  -  1;s))  \mwedge{}  (seq-truncate(x;||moves||)  =  moves))  supposing 
                                      ((seq-truncate(x;||moves||)  =  moves)  and 
                                      (||moves||  \mleq{}  ||x||))
5.  s  :  win2strat(g;n)
6.  moves  :  strat2play(g;n;s)
7.  x  :  sequence(Pos(g))
8.  moves  \mmember{}  \{moves:sequence(Pos(g))|  ((2  *  n)  +  2)  \mleq{}  ||moves||\} 
9.  ||moves||  \mleq{}  ||x||
10.  seq-truncate(x;||moves||)  =  moves
11.  \mforall{}i:\mBbbN{}||moves||.  (x[i]  =  moves[i])
\mvdash{}  seq-truncate(x;||moves||)  =  moves


By

---

Latex:
((Assert  \mforall{}[s:win2strat(g;n  -  1)].  \mforall{}[moves:strat2play(g;n  -  1;s)].  \mforall{}[x:sequence(Pos(g))].
                      ((x  \mmember{}  strat2play(g;n  -  1;s))  \mwedge{}  (seq-truncate(x;||moves||)  =  moves))  supposing 
                            ((seq-truncate(x;||moves||)  =  moves)  and 
                            (||moves||  \mleq{}  ||x||))  BY
                (UseWitness  \mkleeneopen{}<Ax,  Ax>\mkleeneclose{}\mcdot{}  THEN  Trivial))
  THEN  Thin  4
  THEN  PromoteHyp  (-1)  4
  THEN  Unfold  `strat2play`  -6
  THEN  (SplitOnHypITE  -6    THENA  Auto)
  THEN  Try  ((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Complete  (Auto)))
  THEN  DepIsectHD  (-7)
  THEN  Unfold  `strat2play`  0
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  Try  ((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Complete  (Auto)))
  THEN  DepIsectCD
  THEN  (InstHyp  [\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}moves\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  4\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  Try  (Trivial)
  THEN  All  (RepUR  ``play-len  play-item``)
  THEN  (MemTypeHD  8  THENA  Auto)
  THEN  All  (Fold  `member`)
  THEN  ExRepD)

---

Home Index