Seemingly non sequitur in proof

Question

I'm trying to understand a small proof in an article about computing lumpability on Markov chains. There is a small detail that I cannot understand, i.e. I don't think it follows from the argument.

The article is Simple $O(m\log{n})$ Time Markov Lumping written by Valmari & Franceschinis.

Given a weighted graph they define the notion of compatible partition of its nodes. Which is a partition $P$ such that for all $B, B' \in P$ and all $s_1, s_2 \in B$ we have that:

$$ W(s_1, B') = W(s_2, B') $$

They describe an algorithm to compute the coarsest refinement of an initial partition that is compatible (the coarsest croip= compatible refinement of initial partition). The algorithm follows the idea of Paige and Tarjan to compute bisimulation: we take a block $S$ from the partition as a splitter and check whether some other block $B$ breaks the condition above, and if it does we split $B$ into $B_1, \ldots, B_k$ such that the $B_i$ satisfy the condition above when taking $B' = S$.

How exactly these checks are performed shouldn't be essential for the correctness of the algorithm. In the proof of correctness they prove the following lemma:

Lemma 2. Let $d_1, d_2$ be nodes of the graph. If the algorithm ever puts $d_1$ and $d_2$ into different blocks, then there is no croip where $d_1$ and $d_2$ are in the same block.

The proof for when the algorithm separates $d_1$ and $d_2$ during its execution is the following:

Proof. We show that it is an invariant property of the main loop of the algorithm (that is, always valid on line 2^*) that if two states are in different blocks of the algorithm, then they are in different blocks in every croip.

If $d_1$ and $d_2$ are in different blocks initially, then they are in different blocks in $I$ and thus in every croip.

The case remains where lines 14 to 20 separate $d_1$ and $d_2$ to different blocks.

This happens only if $W(d_1, S) \neq W(d_2, S)$. Let $P$ be an arbitrary croip. It follows from the invariant that each block of $P$ is either disjoint with $S$ or a subset of $S$, because otherwise the algorithm would have separated two states that belong to the same block of a croip. Therefore, there are blocks $S_1 , \ldots, S_k$ in $P$ such that $S_1 \cup \cdots \cup S_k = S$. The fact $W(d_1, S) \neq W(d_2, S)$ implies that there is $1 \leq i \leq k$ such that $W(d_1 , S_i) \neq W(d_2, S_i )$. So $d_1$ and $d_2$ belong to different blocks in $P$.

I have a problem understanding the text in bold. To me: it's simply false. They justify it saying otherwise the algorithm would have separated two states that belong to the same block of a croip.

However:

• we still haven't proved the algorithm correct, so I don't really see how the algorithm doing something should imply anything at this point
• I don't get if the two states separated are $d_1$ and $d_2$ or if they are referencing other states

So, I see this as a non sequitur, which would invalidate the proof of this lemma and thus the whole correctness proof of the algorithm.

Given that the algorithm was developed to fix a wrong algorithm published previously from other authors, I believe Valmari and Franceschinis were very careful in the proofs, so I'm probably missing something trivial. Can anybody point out what I'm missing?

---

^* The algorithm is simply a main loop that chooses a new splitter $S$ for each iteration and splits all the blocks in the partition and goes on.