---

Step * of Lemma strat2play-add1

∀[g:SimpleGame]. ∀[n:ℕ]. ∀[s:win2strat(g;n)]. ∀[moves:strat2play(g;n;s)]. ∀[x:Pos(g)].
  (seq-add(moves;x) ∈ strat2play(g;n;s))
BY
{ (InstLemma  `strat2play-longer` []
   THEN RepeatFor 4 (ParallelLast')
   THEN Intro
   THEN Unhide
   THEN (Strat2PlaySubtype 4 THEN (MemTypeHD (-1) THENA Auto) THEN Fold `member` (-2))
   THEN BackThruSomeHyp
   THEN Auto) }

1
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)||

2
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||
⊢ seq-truncate(seq-add(moves;x);||moves||) = moves ∈ sequence(Pos(g))

---

Latex:

---

Latex:
\mforall{}[g:SimpleGame].  \mforall{}[n:\mBbbN{}].  \mforall{}[s:win2strat(g;n)].  \mforall{}[moves:strat2play(g;n;s)].  \mforall{}[x:Pos(g)].
    (seq-add(moves;x)  \mmember{}  strat2play(g;n;s))


By

---

Latex:
(InstLemma    `strat2play-longer`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  Intro
  THEN  Unhide
  THEN  (Strat2PlaySubtype  4  THEN  (MemTypeHD  (-1)  THENA  Auto)  THEN  Fold  `member`  (-2))
  THEN  BackThruSomeHyp
  THEN  Auto)

---

Home Index