Both moves of a round are the same operation: restricting to the ball around Connector's vertex is $deleteVerts$ of the ball's complement, and isolating Splitter's batch is $deleteVerts$ of the batch — Lax12's $deleteVerts$, which removes the edges incident to a set and keeps the vertex type, is used for both, and is not restated here. Arenas therefore only ever lose edges, which is the invariant the win proof and the evaluator downstream both ride on (a vertex isolated once is isolated in every later arena).

$SplitterWins m r ℓ G$ is defined by recursion on the remaining round budget: with budget $0$ Splitter has won exactly if the arena is edgeless; with positive budget, if the arena is edgeless or for every Connector move there is a batch after which he wins with the rest of the budget. This says exactly "Splitter has a winning strategy within $ℓ$ rounds" without carrying strategy functions on the surface; the explicit strategy — the object the algorithm executes — appears proofs-side with the win theorem's discharge. (An inductive winning-position predicate would say the same thing, but its step constructor nests the ∀/∃ alternation of a round through $Exists$, which Lean's kernel rejects as a nested inductive; the recursion on the budget is the same mathematics and unfolds one round at a time.) Allowing the edgeless win at any budget, rather than only after a move, only enlarges Splitter's winning positions by games he has already won and matches the algorithm's base case, which stops at an edgeless arena before playing a round.

The batch is a $Set$ with an $ncard$ bound, the idiom of Lax12's quasi-wideness statements. The edgeless condition is $G = ⊥$, mathlib's empty graph.