---

Step * of Lemma play-item_wf

∀[g:SimpleGame]. ∀[n:ℕ]. ∀[s:win2strat(g;n)]. ∀[moves:strat2play(g;n;s)]. ∀[i:ℕ(2 * n) + 2].  (moves[i] ∈ Pos(g))
BY
{ ((InstLemma `strat2play_subtype` [] THEN RepeatFor 3 (ParallelLast'))
   THEN Auto
   THEN (GenConcl ⌜moves = f ∈ {moves:sequence(Pos(g))| ((2 * n) + 2) ≤ ||moves||} ⌝⋅ THENA Auto)
   THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[g:SimpleGame].  \mforall{}[n:\mBbbN{}].  \mforall{}[s:win2strat(g;n)].  \mforall{}[moves:strat2play(g;n;s)].  \mforall{}[i:\mBbbN{}(2  *  n)  +  2].
    (moves[i]  \mmember{}  Pos(g))


By

---

Latex:
((InstLemma  `strat2play\_subtype`  []  THEN  RepeatFor  3  (ParallelLast'))
  THEN  Auto
  THEN  (GenConcl  \mkleeneopen{}moves  =  f\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ProveWfLemma)

---

Home Index