English
Given a state s and a bound n with turnBound s ≤ n, we can form a PGame whose Left moves come from l(s), Right moves from r(s), and whose subgames are obtained recursively from turnBound_of_left and turnBound_of_right.
Русский
Заданному состоянию s и границе n с turnBound s ≤ n можно сопоставить игру PGame, LeftMoves из l(s), RightMoves из r(s) и рекурсивные подигры из turnBound_of_left и turnBound_of_right.
LaTeX
$$$\text{ofStateAux}(n,s,h) = PGame\left(\{t\mid t\in l(s)\}, \{t\mid t\in r(s)\}, t\mapsto\text{ofStateAux}(n-1,t,\text{turnBound_of_left}(t)) , t\mapsto\text{ofStateAux}(n-1,t,\text{turnBound_of_right}(t))\right)$$$
Lean4
/-- Construct a `PGame` from a state and a (not necessarily optimal) bound on the number of
turns remaining.
-/
def ofStateAux : ∀ (n : ℕ) (s : S), turnBound s ≤ n → PGame
| 0, s, h =>
PGame.mk { t // t ∈ l s } { t // t ∈ r s }
(fun t => by exfalso; exact turnBound_ne_zero_of_left_move t.2 (nonpos_iff_eq_zero.mp h)) fun t => by exfalso;
exact turnBound_ne_zero_of_right_move t.2 (nonpos_iff_eq_zero.mp h)
| n + 1, s, h =>
PGame.mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n t (turnBound_of_left t.2 n h)) fun t =>
ofStateAux n t (turnBound_of_right t.2 n h)
