---

Step * 1 of Lemma strat2play-add


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))
BY
{ ((Auto THEN Unfold `strat2play` 0)
   THEN (SplitOnConclITE THENA Auto)
   THEN Try ((Assert ⌜False⌝⋅ THEN Complete (Auto)))
   THEN DepIsectCD) }

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)
7. x : Pos(g)
8. y : Pos(g)
9. Legal1(x;y)
10. x = (s moves) ∈ Pos(g)
11. ¬((n + 1) = 0 ∈ ℤ)
⊢ seq-add(seq-add(moves;x);y) ∈ strat2play(g;(n + 1) - 1;s)

2
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)
7. x : Pos(g)
8. y : Pos(g)
9. Legal1(x;y)
10. x = (s moves) ∈ Pos(g)
11. ¬((n + 1) = 0 ∈ ℤ)
⊢ seq-add(seq-add(moves;x);y) ∈ {moves@0:sequence(Pos(g))| 
                                 (((2 * (n + 1)) + 2) ≤ ||moves@0||)
                                 ∧ Legal1(moves@0[2 * (n + 1)];moves@0[(2 * (n + 1)) + 1])
                                 ∧ (moves@0[2 * (n + 1)]
                                   = (s play-truncate(seq-add(seq-add(moves;x);y);2 * (n + 1)))
                                   ∈ Pos(g))} 

---

Latex:

---

Latex:

1.  [g]  :  SimpleGame
2.  [n]  :  \mBbbN{}
3.  [s]  :  win2strat(g;n  +  1)
4.  [moves]  :  strat2play(g;n;s)
5.  [\%]  :  ||moves||  =  ((2  *  n)  +  2)
6.  s  moves  \mmember{}  Pos(g)
\mvdash{}  \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))


By

---

Latex:
((Auto  THEN  Unfold  `strat2play`  0)
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  Try  ((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Complete  (Auto)))
  THEN  DepIsectCD)

---

Home Index