Step * 1 2 2 of Lemma strat2play-add


1. SimpleGame
2. : ℕ
3. win2strat(g;n 1)
4. moves strat2play(g;n;s)
5. ||moves|| ((2 n) 2) ∈ ℤ
6. moves ∈ Pos(g)
7. Pos(g)
8. Pos(g)
9. Legal1(x;y)
10. (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))} 
BY
(MemTypeCD
   THEN Auto
   THEN RWW "seq-add-len seq-add-item" 0
   THEN Auto
   THEN AutoSplit
   THEN 5
   THEN HypSubst 0
   THEN Auto) }


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)
12.  moves  \mmember{}  sequence(Pos(g))
13.  ((2  *  n)  +  2)  \mleq{}  ||moves||
14.  (s  play-truncate(seq-add(seq-add(moves;x);y);2  *  (n  +  1)))  =  (s  moves)
\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:
(MemTypeCD
  THEN  Auto
  THEN  RWW  "seq-add-len  seq-add-item"  0
  THEN  Auto
  THEN  AutoSplit
  THEN  D  5
  THEN  HypSubst  5  0
  THEN  Auto)




Home Index