For every edge list and every initial state \(uf\), the state \(\texttt{Kruskal.ufAfterProcessEdges}\) produces induces the same partition of the vertices as merging all the edges unconditionally, i.e. it has the same partition as \(uf.\mathrm{mergeAll}\) applied to the whole list.

Running \(\texttt{Kruskal.processEdges}\) with an accumulator \(acc\) yields \(acc^{\mathrm{rev}}\) followed by the output of the same run started from the empty accumulator; the accumulator only contributes a reversed prefix.

Merging the edges selected by the greedy loop into \(uf\) gives the same partition as merging all the input edges into \(uf\): the discarded edges never change connectivity.

If the endpoints of \(e\) already have the same union–find representative, then the greedy loop on \(e :: rest\) from state \(uf\) returns exactly the output of the loop on \(rest\) from the same state.

If the endpoints of \(e\) lie in different components of \(uf\), then the total weight of the greedy output on \(e :: rest\) equals \(e.\mathrm{weight}\) plus the total weight of the greedy output on \(rest\) started from the merged state \(uf.\mathrm{merge}\, e.u\, e.v\).

Let \(uf\) be a union–find state whose classes are exactly the reachability classes of a base edge list, and let the input list \(edges\) be sorted by nondecreasing weight. Then for any competing sublist \(S \subseteq edges\) that induces the same partition as \(edges\) does over \(uf\), the greedy output satisfies