---

Step * of Lemma strat2play-longer

∀[g:SimpleGame]. ∀[n:ℕ]. ∀[s:win2strat(g;n)]. ∀[moves:strat2play(g;n;s)]. ∀[x:sequence(Pos(g))].
  ((x ∈ strat2play(g;n;s)) ∧ (seq-truncate(x;||moves||) = moves ∈ strat2play(g;n;s))) supposing 
     ((seq-truncate(x;||moves||) = moves ∈ sequence(Pos(g))) and 
     (||moves|| ≤ ||x||))
BY
{ (RepeatFor 2 (Intro)
   THEN UseWitness ⌜<Ax, Ax>⌝⋅
   THEN NatInd (-1)
   THEN Unfold `uall` 0
   THEN RepeatFor 3 ((MemTypeCD THENW Auto))
   THEN OnVar `moves' Strat2PlaySubtype
   THEN Unfold `uimplies` 0
   THEN RepeatFor 2 ((MemTypeCD THENW Auto))
   THEN (Assert ∀i:ℕ||moves||. (x[i] = moves[i] ∈ Pos(g)) BY
               (Auto
                THEN ((StrengthenEquation (-2) THEN ApFunToHypEquands `z' ⌜z[i]⌝ ⌜Pos(g)⌝ (-1)⋅)
                      THENA (RepeatFor 2 (D -1) THEN Auto)
                      )
                THEN RWO "seq-truncate-item" (-1)
                THEN Auto))
   THEN RepeatFor 2 (MemCD)) }

1
.....eq aux..... 
1. g : SimpleGame
2. n : ℤ
3. s : win2strat(g;0)
4. moves : strat2play(g;0;s)
5. x : sequence(Pos(g))
6. moves ∈ {moves:sequence(Pos(g))| ((2 * 0) + 2) ≤ ||moves||} 
7. ||moves|| ≤ ||x||
8. seq-truncate(x;||moves||) = moves ∈ sequence(Pos(g))
9. ∀i:ℕ||moves||. (x[i] = moves[i] ∈ Pos(g))
⊢ x ∈ strat2play(g;0;s)

2
.....eq aux..... 
1. g : SimpleGame
2. n : ℤ
3. s : win2strat(g;0)
4. moves : strat2play(g;0;s)
5. x : sequence(Pos(g))
6. moves ∈ {moves:sequence(Pos(g))| ((2 * 0) + 2) ≤ ||moves||} 
7. ||moves|| ≤ ||x||
8. seq-truncate(x;||moves||) = moves ∈ sequence(Pos(g))
9. ∀i:ℕ||moves||. (x[i] = moves[i] ∈ Pos(g))
⊢ seq-truncate(x;||moves||) = moves ∈ strat2play(g;0;s)

3
.....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))
⊢ x ∈ strat2play(g;n;s)

4
.....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)

---

Latex:

---

Latex:
\mforall{}[g:SimpleGame].  \mforall{}[n:\mBbbN{}].  \mforall{}[s:win2strat(g;n)].  \mforall{}[moves:strat2play(g;n;s)].  \mforall{}[x:sequence(Pos(g))].
    ((x  \mmember{}  strat2play(g;n;s))  \mwedge{}  (seq-truncate(x;||moves||)  =  moves))  supposing 
          ((seq-truncate(x;||moves||)  =  moves)  and 
          (||moves||  \mleq{}  ||x||))


By

---

Latex:
(RepeatFor  2  (Intro)
  THEN  UseWitness  \mkleeneopen{}<Ax,  Ax>\mkleeneclose{}\mcdot{}
  THEN  NatInd  (-1)
  THEN  Unfold  `uall`  0
  THEN  RepeatFor  3  ((MemTypeCD  THENW  Auto))
  THEN  OnVar  `moves'  Strat2PlaySubtype
  THEN  Unfold  `uimplies`  0
  THEN  RepeatFor  2  ((MemTypeCD  THENW  Auto))
  THEN  (Assert  \mforall{}i:\mBbbN{}||moves||.  (x[i]  =  moves[i])  BY
                          (Auto
                            THEN  ((StrengthenEquation  (-2)  THEN  ApFunToHypEquands  `z'  \mkleeneopen{}z[i]\mkleeneclose{}  \mkleeneopen{}Pos(g)\mkleeneclose{}  (-1)\mcdot{})
                                        THENA  (RepeatFor  2  (D  -1)  THEN  Auto)
                                        )
                            THEN  RWO  "seq-truncate-item"  (-1)
                            THEN  Auto))
  THEN  RepeatFor  2  (MemCD))

---

Home Index