English
There is a Short instance for ofStateAux n s h whenever turnBound s ≤ n.
Русский
Существет инстанс Short для ofStateAux n s h при turnBound s ≤ n.
LaTeX
$$$ Short(ofStateAux(n,s,h)) $$$
Lean4
instance shortOfStateAux : ∀ (n : ℕ) {s : S} (h : turnBound s ≤ n), Short (ofStateAux n s h)
| 0, s, h =>
Short.mk'
(fun i => by
have i := (leftMovesOfStateAux _ _).toFun i
exfalso
exact turnBound_ne_zero_of_left_move i.2 (nonpos_iff_eq_zero.mp h))
fun j => by
have j := (rightMovesOfStateAux _ _).toFun j
exfalso
exact turnBound_ne_zero_of_right_move j.2 (nonpos_iff_eq_zero.mp h)
| n + 1, _, h =>
Short.mk' (fun i => shortOfRelabelling (relabellingMoveLeftAux (n + 1) h i).symm (shortOfStateAux n _)) fun j =>
shortOfRelabelling (relabellingMoveRightAux (n + 1) h j).symm (shortOfStateAux n _)
