---

Step * of Lemma strat2play-add

∀[g:SimpleGame]. ∀[n:ℕ]. ∀[s:win2strat(g;n + 1)]. ∀[moves:strat2play(g;n;s)].
  ∀[x,y:Pos(g)].
    (seq-add(seq-add(moves;x);y) ∈ strat2play(g;n + 1;s)) supposing ((x = (s moves) ∈ Pos(g)) and Legal1(x;y)) 
  supposing ||moves|| = ((2 * n) + 2) ∈ ℤ
BY
{ (RepeatFor 5 (Intro)
   THEN (Assert s moves ∈ Pos(g) BY
               ((Unhide THENA Auto)
                THEN Unfold `win2strat` 3
                THEN (SplitOnHypITE -3  THENA Auto)
                THEN Try ((DepIsectHD 3
                           THEN ((Subst' (n + 1) - 1 ~ n -5 THENA Auto) THEN (Subst' (n + 1) - 1 ~ n -4 THENA Auto))
                           THEN (Subst' 2 * (n + 1) ~ (2 * n) + 2 -4 THENA Auto)
                           THEN DoSubsume
                           THEN Auto))
                THEN Auto))
   ) }

1
1. [g] : SimpleGame
2. [n] : ℕ
3. [s] : win2strat(g;n + 1)
4. [moves] : strat2play(g;n;s)
5. [%] : ||moves|| = ((2 * n) + 2) ∈ ℤ
6. s moves ∈ Pos(g)
⊢ ∀[x,y:Pos(g)].
    (seq-add(seq-add(moves;x);y) ∈ strat2play(g;n + 1;s)) supposing ((x = (s moves) ∈ Pos(g)) and Legal1(x;y))

---

Latex:

---

Latex:
\mforall{}[g:SimpleGame].  \mforall{}[n:\mBbbN{}].  \mforall{}[s:win2strat(g;n  +  1)].  \mforall{}[moves:strat2play(g;n;s)].
    \mforall{}[x,y:Pos(g)].
        (seq-add(seq-add(moves;x);y)  \mmember{}  strat2play(g;n  +  1;s))  supposing 
              ((x  =  (s  moves))  and 
              Legal1(x;y)) 
    supposing  ||moves||  =  ((2  *  n)  +  2)


By

---

Latex:
(RepeatFor  5  (Intro)
  THEN  (Assert  s  moves  \mmember{}  Pos(g)  BY
                          ((Unhide  THENA  Auto)
                            THEN  Unfold  `win2strat`  3
                            THEN  (SplitOnHypITE  -3    THENA  Auto)
                            THEN  Try  ((DepIsectHD  3
                                                  THEN  ((Subst'  (n  +  1)  -  1  \msim{}  n  -5  THENA  Auto)
                                                              THEN  (Subst'  (n  +  1)  -  1  \msim{}  n  -4  THENA  Auto)
                                                              )
                                                  THEN  (Subst'  2  *  (n  +  1)  \msim{}  (2  *  n)  +  2  -4  THENA  Auto)
                                                  THEN  DoSubsume
                                                  THEN  Auto))
                            THEN  Auto))
  )

---

Home Index