To prove that the procedure stops, let us notice that no edge is ever recolored,
so we must run out of black edges after at most~$m$ steps. Recoloring
to the same color is avoided by the conditions built in the rules, recoloring to
-a different color would mean that the an edge would be both inside and outside~$T_{min}$
+a different color would mean that the edge would be both inside and outside~$T_{min}$
due to our Red and Blue lemmata.
When no further rules can be applied, the Black lemma guarantees that all edges
labels of the trees they belong to. We scan all edges, map their endpoints
to the particular trees and for each tree we maintain the lightest incident edge
so far encountered. Instead of merging the trees one by one (which would be too
-slow), we build an auxilliary graph whose vertices are the labels of the original
+slow), we build an auxiliary graph whose vertices are the labels of the original
trees and edges correspond to the chosen lightest inter-tree edges. We find connected
components of this graph, these determine how are the original labels translated
to the new labels.
\proof
Every spanning tree of~$G'$ is a spanning tree of~$G$. In the other direction:
Loops can be never contained in a spanning tree. If there is a spanning tree~$T$
-containing a~removed edge~$e$ parallel to an edge~$e'\in G'$, exchaning $e'$
+containing a~removed edge~$e$ parallel to an edge~$e'\in G'$, exchanging $e'$
for~$e$ makes~$T$ lighter. (This is indeed the multigraph version of the Red
lemma applied to a~two-edge cycle, as we will see in \ref{multimst}.)
\qed
\proof
The only non-trivial parts are steps 6 and~7. Contractions can be handled similarly
to the unions in the original Bor\o{u}vka's algorithm (see \ref{boruvkaiter}):
-We build an auxillary graph containing only the selected edges~$e_k$, find
+We build an auxiliary graph containing only the selected edges~$e_k$, find
connected components of this graph and renumber vertices in each component to
the identifier of the component. This takes $\O(m_i)$ time.