Stratification of Bisimilarity : $\sim$ does not coincide with $\sim_\omega$ I am reading Sangiorgi's paper On the origins of bisimulation an coinduction.
Definition 2.5, on page 5, defines Stratification of Bisimilarity:

Let $W$ be the states of an LTS. We set:

$\sim_0 \overset{\text{def}}{=} W\times W$

$s\sim_{n+1} t$, for $n\geq 0$, if:
(1) for all $s^\prime$ with $s \overset{\mu}{\rightarrow} s^\prime$, there is $t^\prime$ such that $t \overset{\mu}{\rightarrow} t^\prime$ and $s^\prime\sim_n t^\prime$;
(2) the converse, that is, whenever for all $t^\prime$ with $t \overset{\mu}{\rightarrow} t^\prime$, there is $s^\prime$ such that $s\overset{\mu}{\rightarrow}s^\prime$ and $s^\prime\sim_n t^\prime$.

$\sim_\omega \overset{\text{def}}{=} \bigcap_{n\geq 0}\sim_n$



The paper follows with the remark that, in general, $\sim_\omega$ does not coincide with $\sim$ (the usual bisimilarity), and provides the following example (Example 2.6 in the paper) to highlight that:
We take the LTS with $\{a\}$ as the set of (arrow) labels, and the set of states is $\{a^0, a^1, \dots, a^\omega, s, t\}$, and the transition function $\overset{a}{\rightarrow}$ is the least function such that:

$a^\omega\overset{a}{\rightarrow}a^\omega$
$\forall n\geq 1, a^n\overset{a}{\rightarrow} a^{n-1}$
$\forall n\in\mathbb{N}, s\overset{a}{\rightarrow} a^{n}$
$\forall n\in\mathbb{N}, t\overset{a}{\rightarrow} a^{n}$
$t\overset{a}{\rightarrow} a^{\omega}$

which is represented in this picture:

The example then states:

It is easy to prove, by induction on $n$, that, for all $n$, $s\sim_n t$, hence also $s\sim_\omega t$.

However, I do not understand how that holds, even for $\sim_1$: $s\sim_1 t$ if (from item (2)):
whenever for all $t^\prime$ with $t \overset{\mu}{\rightarrow} t^\prime$, there is $s^\prime$ such that $s\overset{\mu}{\rightarrow}s^\prime$ and $s^\prime\sim_0 t^\prime$. Let's take $a^\omega$ as $t^\prime$, we indeed have $t\overset{a}{\rightarrow} a^\omega$. So, we have to find $s^\prime$ such that $s\overset{a}{\rightarrow} s^\prime$ and $s^\prime \sim_0 a^\omega$.
Hence my question : which state is suitable for such $s^\prime$, since $s\not\overset{a}{\rightarrow} a^\omega$ ?
I found the answer of my question when writting it, which once again prove the effectiveness of writting down properly the question we have.

To show that $s \sim_1 t$, to map $a^\omega$, one can take any $a^i$ we want (e.g. $a^0$): by definition,
$\sim_0 \overset{\text{def}}{=} W\times W$, and therefore we indeed have that $s\overset{a}{\rightarrow} a^0$ and $a^0\sim_0 a^\omega$.
Something to notice is that, for each $n$, we have $a^\omega \sim_n a^m$ for $m\geq n$. Therefore, to show that $s\sim_{n+1} t$, to show item (2), one can simply take $a^n$ as $s^\prime$ when we take $a^\omega$ as $t^\prime$. The rest of the proof is trivial.