---

Step * of Lemma play-truncate-trivial

∀[g:SimpleGame]. ∀[n:ℕ]. ∀[s:win2strat(g;n)]. ∀[f:strat2play(g;n;s)]. ∀[k:ℤ].
  play-truncate(f;k) ~ f supposing k = ||f|| ∈ ℤ
BY
{ (Auto
   THEN MoveToConcl (-1)
   THEN Strat2PlaySubtype 4
   THEN (GenConcl ⌜f = xx ∈ sequence(Pos(g))⌝⋅ THENA Auto)
   THEN All Thin) }

1
1. g : SimpleGame
2. k : ℤ
3. xx : sequence(Pos(g))
⊢ (k = ||xx|| ∈ ℤ) ⇒ (play-truncate(xx;k) ~ xx)

---

Latex:

---

Latex:
\mforall{}[g:SimpleGame].  \mforall{}[n:\mBbbN{}].  \mforall{}[s:win2strat(g;n)].  \mforall{}[f:strat2play(g;n;s)].  \mforall{}[k:\mBbbZ{}].
    play-truncate(f;k)  \msim{}  f  supposing  k  =  ||f||


By

---

Latex:
(Auto
  THEN  MoveToConcl  (-1)
  THEN  Strat2PlaySubtype  4
  THEN  (GenConcl  \mkleeneopen{}f  =  xx\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin)

---

Home Index