---

Step * 2 of Lemma strat2play-add1


1. g : SimpleGame
2. n : ℕ
3. s : win2strat(g;n)
4. moves : strat2play(g;n;s)
5. ∀[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||))
6. x : Pos(g)
7. moves ∈ sequence(Pos(g))
8. ((2 * n) + 2) ≤ ||moves||
⊢ seq-truncate(seq-add(moves;x);||moves||) = moves ∈ sequence(Pos(g))
BY
{ ((GenConcl ⌜moves = xx ∈ sequence(Pos(g))⌝⋅ THENA Auto)
   THEN D -2
   THEN RepUR ``seq-truncate seq-len seq-add sequence`` 0
   THEN EqCD
   THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  SimpleGame
2.  n  :  \mBbbN{}
3.  s  :  win2strat(g;n)
4.  moves  :  strat2play(g;n;s)
5.  \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||))
6.  x  :  Pos(g)
7.  moves  \mmember{}  sequence(Pos(g))
8.  ((2  *  n)  +  2)  \mleq{}  ||moves||
\mvdash{}  seq-truncate(seq-add(moves;x);||moves||)  =  moves


By

---

Latex:
((GenConcl  \mkleeneopen{}moves  =  xx\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  RepUR  ``seq-truncate  seq-len  seq-add  sequence``  0
  THEN  EqCD
  THEN  Auto)

---

Home Index