---

Step * 1 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||
⊢ ||moves|| ≤ ||seq-add(moves;x)||
BY
{ (RWO "seq-add-len" 0 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{}  ||moves||  \mleq{}  ||seq-add(moves;x)||


By

---

Latex:
(RWO  "seq-add-len"  0  THEN  Auto)

---

Home Index