Revisiting CSP-S 2020 T4 "Greedy Snake" Six Years Later

Problem Introduction

Six years ago, when I took CSP-S 2020, my coding skills were not particularly polished. After finishing the first two problems, I did not have much time left. So when I looked at T4, Snakes, I only wrote a 20-point special-case solution and left in a hurry. Six years later, I learned from Jiang Yanyan's video that many things had changed again in the OI community. This brought me back to Luogu, where I used to practice problems, and I found that after enough attempts, an LLM could even AC a newly released black problem that only the problem setter had solved.

Of course, that is not the main point today. The point is that I returned to the T4 Snakes problem where I once scraped together 20 points. A simplified statement is:

There are $n$ snakes, numbered $1, \dots, n$ . Their initial powers are positive integers $a_{i}$ , satisfying
$a_{1} \leq a_{2} \leq \dots \leq a_{n} .$
At any moment, snakes are compared by $(power, index)$ : the snake with larger power is stronger; if powers are equal, the snake with larger index is stronger. Therefore the strongest and weakest snakes are uniquely determined.

The current strongest snake may choose whether to eat the current weakest snake. If the strongest snake is $(x, i)$ and the weakest snake is $(y, j)$ , then after eating, the weakest snake dies and the strongest snake becomes
$(x - y, i) .$
Every snake is rational: when it becomes the current strongest snake, it eats the current weakest snake if and only if, under the same rules afterward, it will not eventually die. Otherwise, it refuses to eat, and the game ends immediately. The game also ends when only one snake remains.

The task is to compute how many snakes remain at the end. $n \leq 10^{6}$ .

There are already many solutions to this problem. However, while trying to revisit this problem set, I accidentally came up with another conjecture:

If the initial powers are strictly increasing rather than merely nondecreasing, that is,
$a_{1} < a_{2} < \dots < a_{n},$
then is the final number of remaining snakes always odd?

The answer is yes, but the proof is much more tedious than I had expected, even more tedious than the idea and implementation of the original problem itself. More importantly, the complete proof was generated entirely by an LLM, which seems to echo the earlier observation about LLMs ACing black problems.

Brief Idea

Here I will first break down the problem in a more human way of thinking, and in the next section give the AI-generated bottom-up Lemma-Theorem style proof.

Starting from the Original Solution

According to a solution to the original problem, in the general nondecreasing version there are two phases:

Phase 1, or safe steps: after every strongest snake eats, it does not become the weakest snake, so it can eat without worry.
Phase 2, or dangerous steps: after every strongest snake eats, it becomes the weakest snake, until some snake can safely eat again, meaning that after eating it either is not the weakest snake or only two snakes remain.
Once Phase 1 ends, the game is basically over, with whether one more snake can be eaten determined by the parity in Phase 2.

Let us focus on the sentence “determined by the parity in Phase 2.” First consider a dangerous step:

If there are only two snakes, the strongest snake's choice is obvious: it must eat.
If there are three snakes, after the strongest snake eats, it becomes the weakest snake, so it will certainly be eaten in the next round. Therefore the strongest snake will refuse to eat.
If there are four snakes, the strongest snake will certainly eat, because after it becomes the weakest snake, the conclusion from the previous line says that the current strongest snake will refuse to eat it.
And so on.

Thus, by the reasoning above, when $n$ is odd the strongest snake will refuse to eat; when $n$ is even it will eat, turning the game into the odd- $n$ case, and then the game immediately stops. The final number of snakes is odd, exactly what we want to prove.

So we have a very promising picture: if, once dangerous steps begin, the process never switches back to safe steps, then the problem is essentially solved. I tested a large number of random strictly increasing sequences and found no counterexample. In fact, if we weaken “strictly increasing” to “nondecreasing,” counterexamples appear quickly, for example 1 1 1 1, where the process immediately returns to Phase 1 after the first eating. This shows that the condition that the final number is odd is actually quite restrictive, which further strengthens the possibility that strictly increasing sequences really do satisfy “Phase 2 never switches back to Phase 1.”

The Core Inequality

Our approach is induction. First simulate one step where the strongest snake eats the weakest snake. Let the remaining snakes be $u_{i} = (b_{i}, id (u_{i}))$ , corresponding to power and index. Sort the current state from weakest to strongest:

u_{1} < u_{2} < \dots < u_{m - 1} < u_{m}

Assume the current step is a dangerous step. If this initial condition never holds, then the whole process consists only of safe steps, and the final answer is certainly $1$ , which satisfies the claim. After $u_{m}$ eats $u_{1}$ , the updated snake is $u_{m}^{'} = (b_{m} - b_{1}, id (u_{m}))$ , and $u_{m}^{'}$ is the weakest snake.

By induction, we need to prove that the next step is still dangerous. More concretely, the current strongest snake $u_{m - 1}$ will eat the weakest snake $u_{m}^{'}$ , and its new power becomes $b_{m - 1} - (b_{m} - b_{1}) = b_{m - 1} - b_{m} + b_{1}$ , with index $id (u_{m - 1})$ . We need to ensure that $(b_{m - 1} - b_{m} + b_{1}, id (u_{m - 1})) < u_{2}$ , which is equivalent to proving:

b_{m - 1} - b_{m} + b_{1} < b_{2} \lor (b_{m - 1} - b_{m} + b_{1} = b_{2} \land id (u_{m - 1}) < id (u_{2}))

Since $u_{1} < u_{2} < \dots < u_{m - 1} < u_{m}$ guarantees $b_{m - 1} \leq b_{m}$ , the first branch is immediate if the inequality is strict. If equality holds, meaning $(b_{1} = b_{2}) \land (b_{m - 1} = b_{m})$ , we need to prove $id (u_{m - 1}) < id (u_{2})$ . This is the core and difficult part of the problem.

Main Invariants and Brief Intuition

To prove this inequality, the following five invariants are used:

$A$ : There will never be three snakes with the same power.
$B$ : If a pair of snakes with the same power appears, then this power must be greater than the current “strongest power minus weakest power,” denoted by $Δ$ .
$C$ : For a snake $u_{r}$ in a low-power region, where $r \geq 3$ and its power is at most $Δ$ , if $u_{k}$ is to the right of $u_{r}$ , then $ι_{k} > ι_{r}$ .
$D$ : For an equal pair that is not at the very bottom, meaning its position satisfies $r \geq 2$ , the snake on the left has an index smaller than every snake to its right.
$E$ : Two equal pairs with different powers must have interleaving indices. For example, if $u_{s} < u_{s + 1} < u_{t} < u_{t + 1}$ and $b_{s} = b_{s + 1} < b_{t} = b_{t + 1}$ , then $ι_{s + 1} > ι_{t}$ . The desired $id (u_{m - 1}) < id (u_{2})$ is a direct corollary.

Note that all five properties we want to prove hold in both safe steps and dangerous steps, and they are obviously true in the strictly increasing initial state. So the argument is still a kind of simultaneous induction: assume $A, B, C, D, E$ hold, and then prove that after the strongest snake eats, the next state still satisfies $A^{'}, B^{'}, C^{'}, D^{'}, E^{'}$ . The dependencies are shown in the table below:

Property to prove in the next state	Main properties used in the current state
A'	B
B'	A, B
C'	A, C
D'	C, D
E'	A, B, D, E

Below is the intuition for each property. For convenience, write $ι_{r} = id (u_{r})$ .

A'

If three snakes with the same power appear, then the newly inserted snake must have power $Δ = b_{m} - b_{1}$ and coincide with two old snakes that also have power $Δ$ . This contradicts the previous assumption $B$ . Therefore $A^{'}$ holds.

B'

This is probably the hardest property to prove. There are two cases: whether the equal pair is newly created in this round, or already existed before.

If the pair is newly created, then when snake $u_{m}$ eats $u_{1}$ , its power is $d = Δ = b_{m} - b_{1}$ , while the new width satisfies $Δ^{'} \leq b_{m} - b_{2}$ . If $b_{1} \neq b_{2}$ , then we immediately get $Δ^{'} < Δ = d$ . If $b_{1} = b_{2}$ , meaning the two weakest snakes have the same power, property $B$ already says $Δ < b_{1}$ . Therefore, after $u_{m}$ eats $u_{1}$ , there is actually an old snake whose power is also $b_{m} - b_{1} < b_{1}$ in order to pair with the new snake, which contradicts the assumption that $u_{1}, u_{2}$ are the two weakest snakes.

If the pair already existed before, then the previous property $B$ already gives $d > Δ$ . If the new snake is not the weakest snake, then $Δ^{'} \leq Δ < d$ directly. Now consider the case where the new snake, which is also the weakest snake, has power $Δ$ . Then $Δ^{'} = b_{m - 1} - Δ$ . We want to prove $d > Δ^{'}$ . Since $Δ^{'} = b_{m - 1} - Δ \leq b_{m} - Δ = b_{1}$ , we have $Δ^{'} \leq b_{1}$ . On the other hand, if $d = b_{1}$ , then the original state would already have a pair of snakes with power $b_{1}$ , and together with the eaten snake $u_{1}$ there would be three snakes with the same power, contradicting property $A$ . Hence $d \neq b_{1}$ . And since this pair is not the weakest pair, otherwise $u_{1}$ would not have been the eaten snake, we get $d > b_{1}$ . Combining this with $Δ^{'} \leq b_{1}$ gives $Δ^{'} < d$ .

C'

$C^{'}$ is easy to understand intuitively: the new snake will not be inserted to the left of the low-power region. Even if the powers are equal, its larger index will place it farther to the right.

D'

There are two cases: an old equal pair remains unchanged, or a new equal pair is inserted. For the former, by the previous property $D$ , the rightmost snake $u_{m}$ has an index larger than the old equal pair, so no matter where this snake is inserted, the conclusion is unaffected.

For the case where a new equal pair appears, suppose the new equal pair is formed when $v = (Δ, ι_{m})$ collides with an old snake $u_{k}$ satisfying $b_{k} = Δ$ . We only need to consider whether $ι_{m} > ι_{k}$ holds. Since we are discussing a “non-bottom equal pair,” if $k = 2$ , then after deleting $u_{1}$ , $u_{2}$ and $v$ would form the bottom equal pair, a contradiction. Therefore $k \geq 3$ . This old snake $u_{k}$ lies in the low-power region, and $u_{m}$ is to the right of $u_{k}$ in the original state. Therefore, by property $C$ , the index of $u_{m}$ is greater than the index of $u_{k}$ .

E'

Here there are four cases, ordered from low to high: old-old, old-new, new-old, and new-new. The first case follows directly from $E$ by induction. The fourth case cannot happen by $A$ . Property $B$ says that the power $Δ$ of the new equal pair must be smaller than the power $d$ of any existing old equal pair, so the second case, old-new, is also impossible.

Only the new-old case remains. Again suppose the new equal pair is formed when $v = (Δ, ι_{m})$ collides with an old snake $u_{k}$ satisfying $b_{k} = Δ$ . Let the two snakes in the higher old pair be $u_{t}, u_{t + 1}$ . We need to prove $ι_{t} < max (ι_{k}, ι_{m})$ . Here we prove the stronger statement $ι_{t} < ι_{m}$ . By property $D$ , before $u_{m}$ eats, it must be to the right of $u_{t}, u_{t + 1}$ , because the pair is not at the very bottom. Therefore $ι_{t} < ι_{m}$ holds.

Complete Proof

Note that the following content was generated by GPT 5.5-Pro. I used three prompts in total:

The first prompt gave the problem statement;

The second prompt asked GPT to write out the concrete proof of $id (u_{m - 1}) < id (u_{2})$ ;

The third prompt was: “Please combine the previous outputs and write a complete proof.”

Here I only include the full output from the third prompt.

We now combine the previous conclusions into a complete proof. Represent a snake as

(x, i)

where $x$ is its power and $i$ is its index. Define the strength order

(x, i) ≺ (y, j)

if and only if

x < y,

x = y and i < j .

Thus, the larger an element is under $≺$ , the stronger it is.

Theorem

Starting from an initial state

a_{1} < a_{2} < \dots < a_{n},

if the game is played according to the rational rule in the statement, then the number of surviving snakes at the end is always odd.

1. The Forced Process and Notation

First define an auxiliary process, called the forced process: regardless of whether a snake is rational, at every step we force the current strongest snake to eat the current weakest snake.

Suppose a forced-reachable state contains $m$ snakes, ordered by strength as

u_{1} ≺ u_{2} ≺ \dots ≺ u_{m} .

Write

u_{r} = (b_{r}, ι_{r}),

where $b_{r}$ is the power and $ι_{r} = id (u_{r})$ .

Then

b_{1} \leq b_{2} \leq \dots \leq b_{m} .

If $b_{r} = b_{r + 1}$ , then since the snake with larger index is stronger, we have

ι_{r} < ι_{r + 1} .

After the current strongest snake $u_{m}$ eats the current weakest snake $u_{1}$ , the new snake is

v = (b_{m} - b_{1}, ι_{m}) .

Define the width of the current state as

Δ = b_{m} - b_{1} .

2. Core Invariants in the Forced Process

We first prove a stronger family of invariants. The key conclusion we will need later is the following:

If in a forced-reachable state the first two snakes have the same power and the last two snakes also have the same power, i.e.
$b_{1} = b_{2}, b_{m - 1} = b_{m},$
then
$ι_{m - 1} < ι_{2} .$

To prove this rigorously, we prove the following five properties simultaneously for all forced-reachable states.

Invariant A: No Three Snakes Have the Same Power

In any forced-reachable state, there cannot be three snakes with the same power.

Invariant B: The Power of an Equal Adjacent Pair Is Greater Than the Current Width

b_{r} = b_{r + 1} = d,

then

d > Δ = b_{m} - b_{1} .

Invariant C: Index Monotonicity in the Low-Power Region

r \geq 3, b_{r} \leq Δ,

then for every $s > r$ ,

ι_{r} < ι_{s} .

Invariant D: For a Non-Bottom Equal Pair, the Left Endpoint Has Smaller Index Than Every Snake to Its Right

r \geq 2, b_{r} = b_{r + 1},

then for every $s > r + 1$ ,

ι_{r} < ι_{s} .

Invariant E: Crossing Index Relation Between Two Equal Adjacent Pairs

b_{r} = b_{r + 1}, b_{s} = b_{s + 1}, r < s,

then

ι_{s} < ι_{r + 1} .

We prove that A–E hold for all forced-reachable states.

The Initial State Satisfies the Invariants

In the initial state,

a_{1} < a_{2} < \dots < a_{n} .

Thus there are no equal-power pairs, so A, B, D, and E are all vacuously true.

Moreover, the initial ordering is exactly

(a_{1}, 1) ≺ (a_{2}, 2) ≺ \dots ≺ (a_{n}, n),

so if $r \geq 3$ , then for every $s > r$ ,

ι_{r} = r < s = ι_{s} .

Therefore C also holds.

Induction Step

Assume a forced-reachable state

u_{1} ≺ u_{2} ≺ \dots ≺ u_{m}

satisfies A–E.

Write

u_{r} = (b_{r}, ι_{r}), Δ = b_{m} - b_{1} .

In the next forced step, the new snake is

v = (Δ, ι_{m}) .

The next state is obtained by reordering

u_{2}, u_{3}, \dots, u_{m - 1}, v,

and we denote it by

w_{1} ≺ w_{2} ≺ \dots ≺ w_{m - 1} .

Let their powers be

c_{1} \leq c_{2} \leq \dots \leq c_{m - 1},

and let the width of the next state be

Δ^{'} = c_{m - 1} - c_{1} .

The multiset of powers in the next state is

{b_{2}, b_{3}, \dots, b_{m - 1}, Δ} .

Thus

c_{1} = min (b_{2}, Δ), c_{m - 1} = max (b_{m - 1}, Δ) .

We now prove that A–E still hold in the next state.

1. Proof of B in the Next State

Take an equal adjacent pair in the next state, and let its power be $d$ .

There are two cases.

Case 1: It Is an Old Equal Pair

That is, this equal pair does not contain the new snake $v$ , but consists of two old snakes already present in the previous state.

Since the induction hypothesis A holds, the previous state has no three snakes of the same power. Therefore this old equal pair was also an equal adjacent pair in the previous state. By the induction hypothesis B,

d > Δ .

We need to prove

d > Δ^{'} .

Since $d > Δ$ and $d \leq b_{m - 1}$ , we have

c_{m - 1} = max (b_{m - 1}, Δ) = b_{m - 1} .

c_{1} = b_{2},

then

Δ^{'} = b_{m - 1} - b_{2} \leq b_{m} - b_{2} = (b_{m} - b_{1}) - (b_{2} - b_{1}) \leq Δ .

Hence

d > Δ \geq Δ^{'} .

c_{1} = Δ,

then

Δ^{'} = b_{m - 1} - Δ \leq b_{m} - Δ = b_{1} .

This old equal pair does not contain $u_{1}$ . If $d = b_{1}$ , then the previous state would contain at least the three snakes $u_{1}$ and these two old snakes, all with power $b_{1}$ , contradicting A. Therefore

d > b_{1} .

Hence

d > b_{1} \geq Δ^{'} .

Thus any old equal pair satisfies B.

Case 2: It Is a Newly Created Equal Pair

This means the power of the new snake $v$ ,

Δ,

is exactly the power of some old snake $u_{k}$ :

b_{k} = Δ, 2 \leq k \leq m - 1.

Thus the power of the new equal pair is

d = Δ .

Since $b_{k} = Δ \geq b_{2}$ , we have

c_{1} = b_{2} .

We need to prove

Δ > Δ^{'} .

b_{1} = b_{2},

then the previous state has a bottom equal pair $u_{1}, u_{2}$ . By the induction hypothesis B,

b_{1} > Δ .

On the other hand,

Δ = b_{k} \geq b_{2} = b_{1},

a contradiction.

Therefore

b_{1} < b_{2} .

Also,

c_{m - 1} \leq b_{m} = b_{1} + Δ .

Hence

c_{m - 1} < b_{2} + Δ .

Therefore

Δ^{'} = c_{m - 1} - b_{2} < Δ .

Thus the newly created equal pair also satisfies B.

Therefore B holds in the next state.

2. Proof of A in the Next State

The previous state contains no three snakes of the same power.

The only possible new power collision in the next state is caused by the new snake

v = (Δ, ι_{m}) .

If $v$ joins an already existing old equal pair, then three snakes of the same power would be created.

But if the previous state already had two old snakes of power $Δ$ , then it would contain an equal adjacent pair of power $Δ$ . This contradicts the induction hypothesis B, because B requires every equal adjacent pair of power $d$ to satisfy

d > Δ .

Therefore the new snake can coincide in power with at most one old snake, and it cannot create three snakes of the same power.

Thus A holds in the next state.

3. Proof of C in the Next State

We need to prove: if

r \geq 3, c_{r} \leq Δ^{'},

then for every $s > r$ ,

id (w_{r}) < id (w_{s}) .

First, $w_{r}$ cannot be the new snake $v$ .

If $w_{r} = v$ , then

c_{r} = Δ .

Since $r \geq 3$ , there are at least two snakes before $v$ in the next state. Hence

b_{2} \leq Δ .

Thus

c_{1} = b_{2} .

If $b_{1} = b_{2}$ , then the previous state has a bottom equal pair, and by B,

b_{1} > Δ,

contradicting $b_{2} \leq Δ$ .

Therefore

b_{1} < b_{2} .

Then

c_{m - 1} \leq b_{m} = b_{1} + Δ < b_{2} + Δ,

Δ^{'} = c_{m - 1} - b_{2} < Δ .

But if $w_{r} = v$ , then $c_{r} = Δ$ , contradicting $c_{r} \leq Δ^{'}$ .

Therefore $w_{r}$ must be an old snake. Let

w_{r} = u_{k} .

After deleting $u_{1}$ , the old snake $u_{2}$ can be at most the second snake in the next state; since $r \geq 3$ , we have

k \geq 3.

We now prove

b_{k} \leq Δ .

Assume the contrary:

b_{k} > Δ .

c_{1} = b_{2},

then

Δ^{'} = c_{m - 1} - b_{2} \leq b_{m} - b_{2} = (b_{m} - b_{1}) - (b_{2} - b_{1}) \leq Δ .

Thus

b_{k} > Δ \geq Δ^{'},

contradicting

b_{k} = c_{r} \leq Δ^{'} .

c_{1} = Δ < b_{2},

then

c_{m - 1} = b_{m - 1},

Δ^{'} = b_{m - 1} - Δ .

From $b_{k} \leq Δ^{'}$ , we get

b_{k} + Δ \leq b_{m - 1} \leq b_{m} = b_{1} + Δ .

Therefore

b_{k} \leq b_{1} .

But $k \geq 3$ , so

b_{k} \geq b_{2} \geq b_{1} .

Hence

b_{1} = b_{2} = b_{k},

which gives three snakes of the same power, contradicting A.

Therefore

b_{k} \leq Δ .

By C in the previous state, since

k \geq 3, b_{k} \leq Δ,

we know that for every $t > k$ ,

ι_{k} < ι_{t} .

Every snake to the right of $w_{r} = u_{k}$ in the next state is either an old snake $u_{t}$ with $t > k$ , or the new snake $v$ , whose index is $ι_{m}$ , with $m > k$ . Therefore

ι_{k} < id (w_{s})

for every $s > r$ .

Thus C holds in the next state.

4. Proof of D in the Next State

Take a non-bottom equal adjacent pair in the next state:

w_{r}, w_{r + 1}, r \geq 2,

with

c_{r} = c_{r + 1} .

We need to prove that for every $s > r + 1$ ,

id (w_{r}) < id (w_{s}) .

Case 1: It Is an Old Equal Pair

Suppose this pair was

u_{k}, u_{k + 1}

in the previous state.

Since it does not contain the deleted snake $u_{1}$ , we have

k \geq 2.

By D in the previous state,

ι_{k} < ι_{t}

for every

t > k + 1.

Every snake to the right of this old equal pair in the next state is either an old snake $u_{t}$ with $t > k + 1$ , or the new snake $v$ , whose index is $ι_{m}$ , with $m > k + 1$ . Therefore the conclusion holds.

Case 2: It Is a Newly Created Equal Pair

This means that for some $2 \leq k \leq m - 1$ ,

b_{k} = Δ,

and the new equal pair consists of the old snake $u_{k}$ and the new snake $v$ .

Since this equal pair is not a bottom equal pair in the next state, i.e. $r \geq 2$ , after deleting $u_{1}$ there is still at least one snake before them. Therefore

k \geq 3.

By C in the previous state, since

k \geq 3, b_{k} = Δ,

we know that for every $t > k$ ,

ι_{k} < ι_{t} .

In particular,

ι_{k} < ι_{m} .

Therefore, within this new equal pair, the left endpoint is the old snake $u_{k}$ , not the new snake $v$ .

Every snake to the right of this new equal pair in the next state is an old snake $u_{t}$ with $t > k$ . By the inequality above,

ι_{k} < ι_{t} .

Thus D holds in the next state.

5. Proof of E in the Next State

Take two equal adjacent pairs in the next state:

w_{r}, w_{r + 1}

and

w_{s}, w_{s + 1},

where

r < s .

We need to prove

id (w_{s}) < id (w_{r + 1}) .

Case 1: Both Equal Pairs Are Old Equal Pairs

They were also two equal adjacent pairs in the previous state, and their relative order is unchanged.

By E in the previous state, we immediately get

id (w_{s}) < id (w_{r + 1}) .

Case 2: The Lower Equal Pair Is New, and the Higher Equal Pair Is Old

The new equal pair consists of

v = (Δ, ι_{m})

and some old snake $u_{k}$ .

Thus the right endpoint index of this new equal pair is

max (ι_{k}, ι_{m}) .

Suppose the higher old equal pair was

u_{t}, u_{t + 1}

in the previous state.

This old equal pair does not contain $u_{1}$ , so

t \geq 2.

By D in the previous state,

ι_{t} < ι_{m} .

In the next state, the left endpoint index of this higher old equal pair is still $ι_{t}$ . Therefore

id (w_{s}) = ι_{t} < ι_{m} \leq max (ι_{k}, ι_{m}) = id (w_{r + 1}) .

So E holds.

Case 3: The Lower Equal Pair Is Old, and the Higher Equal Pair Is New

This case is impossible.

The power of a new equal pair must be

Δ .

By B in the previous state, the power of any old equal pair is strictly greater than $Δ$ . Therefore the new equal pair is weaker than every old equal pair, and it cannot be the higher equal pair.

Case 4: Both Equal Pairs Are New

This case is also impossible, because one step inserts only one new snake $v$ , so it can participate in at most one equal adjacent pair; moreover, A guarantees that no three snakes have the same power.

Therefore E holds in the next state.

Thus A–E hold for every forced-reachable state.

In particular, E gives the core conclusion we need later:

If in a forced-reachable state

b_{1} = b_{2}, b_{m - 1} = b_{m},

then take

r = 1, s = m - 1

in E, and get

ι_{m - 1} < ι_{2} .

That is,

id (u_{m - 1}) < id (u_{2}) .

3. Safe Steps and Dangerous Steps

Now return to the forced process.

In the state

u_{1} ≺ u_{2} ≺ \dots ≺ u_{m},

we force the strongest snake $u_{m}$ to eat the weakest snake $u_{1}$ , obtaining the new snake

v = (b_{m} - b_{1}, ι_{m}) .

If $v$ is not the weakest snake in the next state, we call this step a safe step.

If $m \geq 3$ and $v$ becomes the weakest snake in the next state, we call this step a dangerous step.

When $m = 2$ , after eating there is only one snake left, so the eater necessarily survives; therefore the step with $m = 2$ is regarded as a safe step.

4. A Snake in a Safe Step Always Eats

We prove:

If a step is safe, then the current strongest snake will eat in the rational game.

Suppose the current state is

u_{1} ≺ \dots ≺ u_{m},

and the current strongest snake is $u_{m}$ . After eating, it becomes

p = (Δ, ι_{m}), Δ = b_{m} - b_{1} .

Since this is a safe step, $p$ is not the weakest snake in the next state.

We first prove a protection property:

In the subsequent evolution of the forced process, before $p$ next becomes the strongest snake, $p$ will not become the weakest snake.

Proof.

First, a safe step implies

b_{1} < b_{2} .

Otherwise, if

b_{1} = b_{2},

then there is a bottom equal pair. By invariant B,

b_{1} > Δ .

Hence

b_{2} > Δ,

which means the new snake $p$ is weaker than $u_{2}$ , so $p$ would become the weakest snake, contradicting that the step is safe.

Therefore

b_{1} < b_{2} .

Now consider the state after the eating. Partition the snakes other than $p$ into two classes:

L = {x : x ≺ p},

the snakes weaker than $p$ , and

H = {x : p ≺ x},

the snakes stronger than $p$ .

Since this step is safe,

L \neq \emptyset .

H = \emptyset,

then $p$ is already the strongest snake, and the conclusion is immediate.

Now assume $H \neq \emptyset$ .

We prove that the following property is preserved:

For any
$h = (X, α) \in H, ℓ = (Y, β) \in L,$
we have
$(X - Y, α) ≺ p .$

Initially, both $h$ and $ℓ$ are old snakes from the previous state. Hence

X \leq b_{m}, Y \geq b_{2} .

Therefore

X - Y \leq b_{m} - b_{2} < b_{m} - b_{1} = Δ .

(X - Y, α) ≺ p .

Now assume this property holds at some moment, and that $p$ is not yet the strongest snake.

Since $H \neq \emptyset$ , the current strongest snake lies in $H$ ; since $L \neq \emptyset$ , the current weakest snake lies in $L$ .

Let the current strongest snake be

h_{*} = (X_{*}, α_{*}),

and the current weakest snake be

ℓ_{*} = (Y_{*}, β_{*}) .

The next forced step produces

z = (X_{*} - Y_{*}, α_{*}) .

By the preservation property,

z ≺ p .

Thus $z$ enters $L$ and does not move to the right of $p$ .

It remains only to check that the preservation property still holds.

For old $h \in H ∖ {h_{*}}$ and old $ℓ \in L ∖ {ℓ_{*}}$ , the property already held.

We only need to check the new weaker snake $z$ . Take any old

h = (X, α) \in H ∖ {h_{*}} .

Since $h_{*}$ is the current strongest snake,

h ≺ h_{*},

X \leq X_{*} .

Thus

X - (X_{*} - Y_{*}) = X - X_{*} + Y_{*} \leq Y_{*} .

Y_{*} < Δ,

then

X - (X_{*} - Y_{*}) < Δ,

(X - (X_{*} - Y_{*}), α) ≺ p .

Y_{*} = Δ,

then $ℓ_{*}$ and $p$ have the same power, and $ℓ_{*} ≺ p$ .

At this moment $ℓ_{*}$ and $p$ are the two weakest snakes in the current state. If equality occurs in the expression above, i.e.

X - (X_{*} - Y_{*}) = Δ,

then necessarily

X = X_{*} .

Thus $h$ and $h_{*}$ have the same power and are the two strongest snakes in the current state.

By the core invariant,

id (h) < id (p) .

Therefore even if the powers are the same,

(X - (X_{*} - Y_{*}), α) ≺ p .

Hence the preservation property holds.

Therefore, as long as $p$ has not become the strongest snake, each forced step moves one snake from $H$ into $L$ , and the new snake never moves to the right of $p$ . The snake $p$ itself neither becomes the weakest snake nor gets eaten.

Thus $p$ either eventually becomes the strongest snake, or the game stops before that; in either case, it does not die before then.

Now return to the rational game.

If, starting from the state after the eating, the game stops before $p$ becomes the strongest snake, then $p$ clearly survives.

If the game reaches a state where $p$ becomes the strongest snake, then it is $p$ 's turn to decide. By the game rule, $p$ eats only if it will eventually survive; otherwise it refuses and survives immediately.

Therefore, in a safe step, after the current strongest snake eats the weakest snake, it eventually survives.

Thus rationally it will eat.

5. Dangerous Steps Form a Consecutive Suffix

We now prove:

If a step is dangerous, then every subsequent step down to the state with $3$ snakes is also dangerous.

Consider a forced state

u_{1} ≺ u_{2} ≺ \dots ≺ u_{m}, m \geq 4.

Suppose this step is dangerous. That is, after the strongest snake $u_{m}$ eats the weakest snake $u_{1}$ , the new snake

v = (b_{m} - b_{1}, ι_{m})

becomes the weakest snake in the next state.

Thus

v ≺ u_{2} .

In the next state, the strongest snake is the old $u_{m - 1}$ , and the weakest snake is $v$ .

The next forced step makes $u_{m - 1}$ eat $v$ , producing the new snake

q = (b_{m - 1} - (b_{m} - b_{1}), ι_{m - 1}) .

Its power is

b_{m - 1} - b_{m} + b_{1} .

Since

b_{m - 1} \leq b_{m}, b_{1} \leq b_{2},

we have

b_{m - 1} - b_{m} + b_{1} \leq b_{2} .

If the inequality is strict, then $q$ is clearly the new weakest snake, so the next step is still dangerous.

The only case that requires attention is equality.

Equality holds if and only if

b_{m - 1} = b_{m}, b_{1} = b_{2} .

That is, in the current state the first two snakes have the same power, and the last two snakes also have the same power.

By the core invariant,

ι_{m - 1} < ι_{2} .

The power of $q$ is equal to $b_{2}$ , and its index is $ι_{m - 1}$ . Therefore

q = (b_{2}, ι_{m - 1}) ≺ (b_{2}, ι_{2}) = u_{2} .

Thus even when the powers are equal, $q$ is still weaker than $u_{2}$ , and it again becomes the weakest snake in the next state.

Therefore the next step is also dangerous.

Hence, once a step with $m \geq 4$ is dangerous, the step with $m - 1$ snakes is also dangerous.

Thus, if dangerous steps occur at all, they form a consecutive suffix:

S_{h} \to S_{h - 1} \to \dots \to S_{3} \to S_{2},

where

S_{k}

denotes the forced-process state with $k$ snakes.

Note that in the step $S_{2} \to S_{1}$ , after eating there is only one snake left, so the eater necessarily survives; we regard this step as safe.

6. Decisions in the Rational Game

Now consider the actual rational game.

The forced process gives a sequence of states

S_{n}, S_{n - 1}, \dots, S_{1} .

The actual game can only follow this forced path until the current strongest snake refuses at some step.

Let

E_{m}

denote the assertion: in state $S_{m}$ , the current strongest snake will eat.

We have already proved:

If $S_{m} \to S_{m - 1}$ is a safe step, then

E_{m} = true .

In particular,

E_{2} = true,

because after eating only the eater remains.

Now consider a dangerous step.

If $S_{m} \to S_{m - 1}$ is dangerous and $m \geq 3$ , then after eating, the current strongest snake becomes the weakest snake in $S_{m - 1}$ .

Therefore whether it survives depends exactly on whether the strongest snake in $S_{m - 1}$ eats:

If the strongest snake in $S_{m - 1}$ eats, then it is immediately eaten and dies.
If the strongest snake in $S_{m - 1}$ refuses, then the game stops immediately and it survives.

Thus, for a dangerous step,

E_{m} = \neg E_{m - 1} .

7. The Final Number of Surviving Snakes Is Odd

There are two cases.

Case 1: The Forced Process Has No Dangerous Steps

Then every step is safe.

By the result for safe steps, the current strongest snake eats at every step.

Thus the game continues until only one snake remains.

The final number of surviving snakes is

1,

which is odd.

Case 2: The Forced Process Has Dangerous Steps

Let the first state in the dangerous suffix be

S_{h} .

That is:

S_{h} \to S_{h - 1}, S_{h - 1} \to S_{h - 2}, \dots, S_{3} \to S_{2}

are all dangerous steps, while every

S_{m} \to S_{m - 1} (m > h)

is a safe step.

Therefore the actual game will certainly first reach $S_{h}$ .

In the dangerous suffix, we have

E_{2} = true,

and for $3 \leq m \leq h$ ,

E_{m} = \neg E_{m - 1} .

Hence

E_{3} = false,

E_{4} = true,

E_{5} = false,

E_{6} = true,

and so on.

That is,

E_{m} = true ⟺ m is even,

E_{m} = false ⟺ m is odd .

Therefore:

If $h$ is odd, then in $S_{h}$ the strongest snake refuses, and the game stops with $h$ snakes, an odd number.

If $h$ is even, then in $S_{h}$ the strongest snake eats, and the game enters $S_{h - 1}$ . Since $h - 1$ is odd, the strongest snake in $S_{h - 1}$ refuses, and the game stops with $h - 1$ snakes, also an odd number.

Conclusion

Whether or not the forced process contains dangerous steps, the actual rational game always ends with an odd number of surviving snakes.

Therefore the original claim holds:

The number of surviving snakes at the end is always odd.