+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}$
+due to our Red and Blue lemmata.
+
+When no further rules can be applied, the Black lemma guarantees that all edges
+are colored, so by the Blue lemma all blue edges are in~$T_{min}$ and by the Red
+lemma all other (red) edges are outside~$T_{min}$, so the blue edges are exactly~$T_{min}$.
+\qed
+
+%--------------------------------------------------------------------------------
+
+\section{Classical algorithms}
+
+The three classical MST algorithms can be easily stated in terms of the Red-Blue meta-algorithm.
+For each of them, we first show the general version of the algorithm, then we prove that
+it gives the correct result and finally we discuss the time complexity of various
+implementations.
+
+\algn{Bor\o{u}vka \cite{boruvka:ojistem}, Choquet \cite{choquet:mst}, Sollin \cite{sollin:mst} and others}
+\algo
+\algin A~graph~$G$ with an edge comparison oracle.
+\:$T\=$ a forest consisting of vertices of~$G$ and no edges.
+\:While $T$ is not connected:
+\::For each component $T_i$ of~$T$, choose the lightest edge $e_i$ from the cut
+ separating $T_i$ from the rest of~$T$.
+\::Add all $e_i$'s to~$T$.
+\algout Minimum spanning tree~$T$.
+\endalgo
+
+\lemma\id{boruvkadrop}%
+In each iteration of the algorithm, the number of trees in~$T$ drops at least twice.
+
+\proof
+Each tree gets merged with at least one of its neighbors, so each of the new trees
+contains two or more original trees.
+\qed
+
+\cor
+The algorithm stops in $\O(\log n)$ iterations.
+
+\lemma
+Bor\o{u}vka's algorithm outputs the MST of the input graph.
+
+\proof
+In every iteration of the algorithm, $T$ is a blue subgraph,
+because every addition of some edge~$e_i$ to~$T$ is a straightforward
+application of the Blue rule. We stop when the blue subgraph is connected, so
+we do not need the Red rule to explicitly exclude edges.
+
+It remains to show that adding the edges simultaneously does not
+produce a cycle. Consider the first iteration of the algorithm where $T$ contains a~cycle~$C$. Without
+loss of generality we can assume that $C=T_1[u_1v_1]\,v_1u_2\,T_2[u_2v_2]\,v_2u_3\,T_3[u_3v_3]\, \ldots \,T_k[u_kv_k]\,v_ku_1$.
+Each component $T_i$ has chosen its lightest incident edge~$e_i$ as either the edge $v_iu_{i+1}$
+or $v_{i-1}u_i$ (indexing cyclically). Suppose that $e_1=v_1u_2$ (otherwise we reverse the orientation
+of the cycle). Then $e_2=v_2u_3$ and $w(e_2)<w(e_1)$ and we can continue in the same way,
+getting $w(e_1)>w(e_2)>\ldots>w(e_k)>w(e_1)$, which is a contradiction.
+(Note that distinctness of edge weights was crucial here.)
+\qed
+
+\lemma\id{boruvkaiter}%
+Each iteration can be carried out in time $\O(m)$.
+
+\proof
+We assign a label to each tree and we keep a mapping from vertices to the
+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
+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.
+\qed
+
+\thm
+Bor\o{u}vka's algorithm finds the MST in time $\O(m\log n)$.
+
+\proof
+Follows from the previous lemmata.
+\qed
+
+\algn{Jarn\'\i{}k \cite{jarnik:ojistem}, Prim \cite{prim:mst}, Dijkstra \cite{dijkstra:mst}}\id{jarnik}%
+\algo
+\algin A~graph~$G$ with an edge comparison oracle.
+\:$T\=$ a single-vertex tree containing an~arbitrary vertex of~$G$.
+\:While there are vertices outside $T$:
+\::Pick the lightest edge $uv$ such that $u\in V(T)$ and $v\not\in V(T)$.
+\::$T\=T+uv$.
+\algout Minimum spanning tree~$T$.
+\endalgo
+
+\lemma
+Jarn\'\i{}k's algorithm computers the MST of the input graph.
+
+\proof
+If~$G$ is connected, the algorithm always stops. Let us prove that in every step of
+the algorithm, $T$ is always a blue tree. Step~4 corresponds to applying
+the Blue rule to the cut $\delta(T)$ separating~$T$ from the rest of the given graph. We need not care about
+the remaining edges, since for a connected graph the algorithm always stops with the right
+number of blue edges.
+\qed
+
+\impl
+The most important part of the algorithm is finding \em{neighboring edges,} i.e., edges
+of the cut $\delta(T)$. In a~straightforward implementation,
+searching for the lightest neighboring edge takes $\Theta(m)$ time, so the whole
+algorithm runs in time $\Theta(mn)$.
+
+We can do much better by using a binary
+heap to hold all neighboring edges. In each iteration, we find and delete the
+minimum edge from the heap and once we expand the tree, we insert the newly discovered
+neighboring edges to the heap while deleting the neighboring edges which become
+internal to the new tree. Since there are always at most~$m$ edges in the heap,
+each heap operation takes $\O(\log m)=\O(\log n)$ time. For every edge, we perform
+at most one insertion and at most one deletion, so we spend $\O(m\log n)$ time in total.
+From this, we can conclude:
+
+\thm
+Jarn\'\i{}k's algorithm finds the MST of a~given graph in time $\O(m\log n)$.
+
+\rem
+We will show several faster implementations in section \ref{fibonacci}.
+
+\algn{Kruskal \cite{kruskal:mst}, the Greedy algorithm}
+\algo
+\algin A~graph~$G$ with an edge comparison oracle.
+\:Sort edges of~$G$ by their increasing weight.
+\:$T\=\emptyset$. \cmt{an empty spanning subgraph}
+\:For all edges $e$ in their sorted order:
+\::If $T+e$ is acyclic, add~$e$ to~$T$.
+\::Otherwise drop~$e$.
+\algout Minimum spanning tree~$T$.
+\endalgo
+
+\lemma
+Kruskal's algorithm returns the MST of the input graph.
+
+\proof
+In every step, $T$ is a forest of blue trees. Adding~$e$ to~$T$
+in step~4 applies the Blue rule on the cut separating some pair of components of~$T$ ($e$ is the lightest,
+because all other edges of the cut have not been considered yet). Dropping~$e$ in step~5 corresponds
+to the Red rule on the cycle found ($e$~must be the heaviest, since all other edges of the
+cycle have been already processed). At the end of the algorithm, all edges are colored,
+so~$T$ must be the~MST.
+\qed
+
+\impl
+Except for the initial sorting, which in general takes $\Theta(m\log m)$ time, the only
+other non-trivial operation is the detection of cycles. What we need is a data structure
+for maintaining connected components, which supports queries and edge insertion.
+(This is also known under the name Disjoint Set Union problem, i.e., maintenance
+of an~equivalence relation on a~set with queries on whether two elements are equivalent
+and the operation of joining two equivalence classes into one.)
+The following theorem shows that it can be done with surprising efficiency.
+
+\thmn{Incremental connectivity}%
+When only edge insertions and connectivity queries are allowed, connected components
+can be maintained in $\O(\alpha(n))$ time amortized per operation.
+
+\proof
+Proven by Tarjan and van Leeuwen in \cite{tarjan:setunion}.
+\qed
+
+\FIXME{Define Ackermann's function. Use $\alpha(m,n)$?}
+
+\rem
+The cost of the operations on components is of course dwarfed by the complexity
+of sorting, so a much simpler (at least in terms of its analysis) data
+structure would be sufficient, as long as it has $\O(\log n)$ amortized complexity
+per operation. For example, we can label vertices with identifiers of the
+corresponding components and always recolor the smaller of the two components.
+
+\thm
+Kruskal's algorithm finds the MST of a given graph in time $\O(m\log n)$
+or $\O(m\timesalpha(n))$ if the edges are already sorted by their weights.
+
+\proof
+Follows from the above analysis.
+\qed
+
+%--------------------------------------------------------------------------------
+
+\section{Contractive algorithms}\id{contalg}%
+
+While the classical algorithms are based on growing suitable trees, they
+can be also reformulated in terms of edge contraction. Instead of keeping
+a forest of trees, we can keep each tree contracted to a single vertex.
+This replaces the relatively complex tree-edge incidencies by simple
+vertex-edge incidencies, potentially speeding up the calculation at the
+expense of having to perform the contractions.
+
+We will show a contractive version of the Bor\o{u}vka's algorithm
+in which these costs are carefully balanced, leading for example to
+a linear-time algorithm for MST in planar graphs.
+
+There are two definitions of edge contraction which differ when an edge of a
+triangle is contracted. Either we unify the other two edges to a single edge
+or we keep them as two parallel edges, leaving us with a~multigraph. We will
+use the multigraph version and we will show that we can easily reduce the multigraph
+to a simple graph later. (See \ref{contract} for the exact definitions.)
+
+We only need to be able to map edges of the contracted graph to the original
+edges, so each edge will carry a unique label $\ell(e)$ that will be preserved by
+contractions.
+
+\lemman{Flattening a multigraph}\id{flattening}%
+Let $G$ be a multigraph and $G'$ its subgraph such that all loops have been
+removed and each bundle of parallel edges replaced by its lightest edge.
+Then $G'$~has the same MST as~$G$.
+
+\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'$
+for~$e$ makes~$T$ lighter. \qed
+
+\rem Removal of the heavier of a pair of parallel edges can be also viewed
+as an application of the Red rule on a two-edge cycle. And indeed it is, the
+Red-Blue procedure works on multigraphs as well as on simple graphs and all the
+classical algorithms also do. We would only have to be more careful in the
+formulations and proofs, which we preferred to avoid.
+
+\algn{Contractive version of Bor\o{u}vka's algorithm}\id{contbor}
+\algo
+\algin A~graph~$G$ with an edge comparison oracle.
+\:$T\=\emptyset$.
+\:$\ell(e)\=e$ for all edges~$e$. \cmt{Initialize the labels.}
+\:While $n(G)>1$:
+\::For each vertex $v_i$ of~$G$, let $e_i$ be the lightest edge incident to~$v_i$.
+\::$T\=T\cup \{ \ell(e_i) \}$. \cmt{Remember labels of all selected edges.}
+\::Contract $G$ along all edges $e_i$, inheriting labels and weights.\foot{In other words, we ask the comparison oracle for the edge $\ell(e)$ instead of~$e$.}
+\::Flatten $G$, removing parallel edges and loops.
+\algout Minimum spanning tree~$T$.
+\endalgo
+
+\lemma\id{contiter}%
+Each iteration of the algorithm can be carried out in time~$\O(m)$.
+
+\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_i$, find
+connected components of this graph and renumber vertices in each component to
+the identifier of the component. This takes $\O(m)$ time.
+
+Flattening is performed by first removing the loops and then bucket-sorting the edges
+(as ordered pairs of vertex identifiers) lexicographically, which brings parallel
+edges together. The bucket sort uses two passes with $n$~buckets, so it takes
+$\O(n+m)=\O(m)$.
+\qed
+
+\thm
+The Contractive Bor\o{u}vka's algorithm finds the MST in time $\O(m\log n)$.
+
+\proof
+As in the original Bor\o{u}vka's algorithm, the number of iterations is $\O(\log n)$.
+Then apply the previous lemma.
+\qed
+
+\thmn{\cite{mm:mst}}\id{planarbor}%
+When the input graph is planar, the Contractive Bor\o{u}vka's algorithm runs in
+time $\O(n)$.
+
+\proof
+Let us denote the graph considered by the algorithm at the beginning of the $i$-th
+iteration by $G_i$ (starting with $G_0=G$) and its number of vertices and edges
+by $n_i$ and $m_i$ respectively. As we already know from the previous lemma,
+the $i$-th iteration takes $\O(m_i)$ time. We are going to prove that the
+$m_i$'s are decreasing geometrically.
+
+The number of trees in the non-contracting version of the algorithm drops
+at least by a factor of two in each iteration (Lemma \ref{boruvkadrop}) and the
+same must hold for the number of vertices in the contracting version.
+Therefore $n_i\le n/2^i$.
+
+However, every $G_i$ is planar, because the class of planar graphs is closed
+under edge deletion and contraction. The~$G_i$ is also simple as we explicitly removed multiple edges and
+loops at the end of the previous iteration. Hence we can use the standard theorem on
+the number of edges of planar simple graphs (see for example \cite{diestel:gt}) to get $m_i\le 3n_i \le 3n/2^i$.
+From this we get that the total time complexity is $\O(\sum_i m_i)=\O(\sum_i n/2^i)=\O(n)$.