---

Step * of Lemma shift-play_wf

∀[Pos:Type]. ∀[Mv:Pos ⟶ Type]. ∀[n:ℕ]. ∀[p:ℕn ⟶ MoveChoice(Pos;a.Mv[a])].
  (shift-play(p) ∈ ℕn - 1 ⟶ MoveChoice(Pos;a.Mv[a]))
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[Pos:Type].  \mforall{}[Mv:Pos  {}\mrightarrow{}  Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[p:\mBbbN{}n  {}\mrightarrow{}  MoveChoice(Pos;a.Mv[a])].
    (shift-play(p)  \mmember{}  \mBbbN{}n  -  1  {}\mrightarrow{}  MoveChoice(Pos;a.Mv[a]))


By

---

Latex:
ProveWfLemma

---

Home Index