---

Step * 1 of Lemma play-truncate-trivial


1. g : SimpleGame
2. k : ℤ
3. xx : sequence(Pos(g))
⊢ (k = ||xx|| ∈ ℤ) ⇒ (play-truncate(xx;k) ~ xx)
BY
{ (D -1 THEN RepUR ``play-truncate seq-truncate play-len seq-len`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  SimpleGame
2.  k  :  \mBbbZ{}
3.  xx  :  sequence(Pos(g))
\mvdash{}  (k  =  ||xx||)  {}\mRightarrow{}  (play-truncate(xx;k)  \msim{}  xx)


By

---

Latex:
(D  -1  THEN  RepUR  ``play-truncate  seq-truncate  play-len  seq-len``  0  THEN  Auto)

---

Home Index