---

Step * 1 2 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)
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))} 
BY
{ (OnVar `moves' Strat2PlaySubtype
   THEN (MemTypeHD  (-1) THENA Auto)
   THEN Fold `member` (-2)
   THEN All (Unfolds ``play-len play-item``)
   THEN Assert ⌜(s play-truncate(seq-add(seq-add(moves;x);y);2 * (n + 1))) = (s moves) ∈ Pos(g)⌝⋅) }

1
.....assertion..... 
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 ∈ ℤ)
12. moves ∈ sequence(Pos(g))
13. ((2 * n) + 2) ≤ ||moves||
⊢ (s play-truncate(seq-add(seq-add(moves;x);y);2 * (n + 1))) = (s moves) ∈ Pos(g)

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


By

---

Latex:
(OnVar  `moves'  Strat2PlaySubtype
  THEN  (MemTypeHD    (-1)  THENA  Auto)
  THEN  Fold  `member`  (-2)
  THEN  All  (Unfolds  ``play-len  play-item``)
  THEN  Assert  \mkleeneopen{}(s  play-truncate(seq-add(seq-add(moves;x);y);2  *  (n  +  1)))  =  (s  moves)\mkleeneclose{}\mcdot{})

---

Home Index