English
Similar relabelling for moveRight with ofStateAux, reducing to n−1 bound state.
Русский
Аналогичная ребаллинговка для moveRight с ofStateAux, приводящая к состоянию с bound n−1.
LaTeX
$$$\text{relabellingMoveRightAux}(n,s,h,t) : \text{Relabelling}(\text{moveRight}(\text{ofStateAux}(n,s,h),t))\; (\text{ofStateAux}(n-1,\,(\text{rightMovesOfStateAux}(n,h) t).2, \text{turnBound_of_right}(...) ))$$$
Lean4
/-- The relabelling showing `moveRight` applied to a game constructed using `ofStateAux`
has itself been constructed using `ofStateAux`.
-/
def relabellingMoveRightAux (n : ℕ) {s : S} (h : turnBound s ≤ n) (t : RightMoves (ofStateAux n s h)) :
Relabelling (moveRight (ofStateAux n s h) t)
(ofStateAux (n - 1) ((rightMovesOfStateAux n h) t : S)
(turnBound_of_right ((rightMovesOfStateAux n h) t).2 (n - 1) (Nat.le_trans h le_tsub_add))) :=
by
induction n
· have t' := (rightMovesOfStateAux 0 h) t
exfalso; exact turnBound_ne_zero_of_right_move t'.2 (nonpos_iff_eq_zero.mp h)
· rfl
