+lemma all other (red) edges are outside~$T_{min}$. Thus the blue edges are exactly~$T_{min}$.
+\qed
+
+\rem
+The MST problem is a~special case of the problem of finding the minimum basis
+of a~weighted matroid. Surprisingly, when we modify the Red-Blue procedure to
+use the standard definitions of cycles and cuts in matroids, it will always
+find the minimum basis. Some of the other MST algorithms also easily generalize to
+matroids and in some sense matroids are exactly the objects where ``the greedy approach works''. We
+will however not pursue this direction in our work, referring the reader to the Oxley's monograph
+\cite{oxley:matroids} instead.
+
+%--------------------------------------------------------------------------------
+
+\section{Classical algorithms}\id{classalg}%
+
+The three classical MST algorithms (Bor\o{u}vka's, Jarn\'\i{}k's, and Kruskal's) 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.
+
+\paran{Bor\o{u}vka's algorithm}%
+The oldest MST algorithm is based on a~simple idea: grow a~forest in a~sequence of
+iterations until it becomes connected. We start with a~forest of isolated
+vertices. In each iteration, we let each tree of the forest select the lightest
+edge of those having exactly one endpoint in the tree (we will call such edges
+the \df{neighboring edges} of the tree). We add all such edges to the forest and
+proceed with the next iteration.
+
+\algn{Bor\o{u}vka \cite{boruvka:ojistem}, Choquet \cite{choquet:mst}, Florek et al.~\cite{florek:liaison}, Sollin \cite{sollin:mst}}
+\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$ decreases by at least
+a~factor of two.
+
+\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\id{borcorr}%
+The 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_1,v_1]\,v_1u_2\,T_2[u_2,v_2]\,v_2u_3\,T_3[u_3,v_3]\, \ldots \,T_k[u_k,v_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 auxiliary graph whose vertices are the labels of the original
+trees and edges correspond to the chosen lightest inter-tree edges. We find the connected
+components of this graph, and these determine how are the original labels translated
+to the new labels.
+\qed
+
+\thm
+The Bor\o{u}vka's algorithm finds the MST in time $\O(m\log n)$.
+
+\proof
+Follows from the previous lemmata.
+\qed
+
+\paran{Jarn\'\i{}k's algorithm}%
+The next algorithm, discovered independently by Jarn\'\i{}k, Prim and Dijkstra, is similar
+to the Bor\o{u}vka's algorithm, but instead of the whole forest it concentrates on
+a~single tree. It starts with a~single vertex and it repeatedly extends the tree
+by the lightest neighboring edge until the tree spans the whole graph.
+
+\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
+The Jarn\'\i{}k's algorithm computes the MST of the input graph.
+
+\proof
+If~$G$ is connected, the algorithm always stops. In every step of
+the algorithm, $T$ is always a blue tree. because 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\id{jarnimpl}%
+The most important part of the algorithm is finding the \em{neighboring edges.}
+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 and delete the neighboring edges that became
+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
+The Jarn\'\i{}k's algorithm computes the MST of a~given graph in time $\O(m\log n)$.
+
+\rem
+We will show several faster implementations in Section \ref{iteralg}.
+
+\paran{Kruskal's algorithm}%
+The last of the three classical algorithms processes the edges of the
+graph~$G$ greedily. It starts with an~empty forest and it takes the edges of~$G$
+in order of their increasing weights. For every edge, it checks whether its
+addition to the forest produces a~cycle and if it does not, the edge is added.
+Otherwise, the edge is dropped and not considered again.
+
+\algn{Kruskal \cite{kruskal:mst}}
+\algo
+\algin A~graph~$G$ with an edge comparison oracle.
+\:Sort edges of~$G$ by their increasing weights.
+\:$T\=\hbox{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
+The 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 requires $\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 closely related to the well-known Disjoint Set Union problem:
+
+\problemn{Disjoint Set Union, DSU}
+Maintain an~equivalence relation on a~finite set under a~sequence of operations \<Union>
+and \<Find>. The \<Find> operation tests whether two elements are equivalent and \<Union>
+joins two different equivalence classes into one.
+
+\para
+We can maintain the connected components of our forest~$T$ as equivalence classes. When we want
+to add an~edge~$uv$, we first call $\<Find>(u,v)$ to check if both endpoints of the edge lie in
+the same component. If they do not, addition of this edge connects both components into one,
+so we perform $\<Union>(u,v)$ to merge the equivalence classes.
+
+Tarjan \cite{tarjan:setunion} has shown that there is a~data structure for the DSU problem
+of surprising efficiency:
+
+\thmn{Disjoint Set Union, Tarjan \cite{tarjan:setunion}}\id{dfu}%
+Starting with a~trivial equivalence with single-element classes, a~sequence of operations
+comprising of $n$~\<Union>s intermixed with $m\ge n$~\<Find>s can be processed in time
+$\O(m\timesalpha(m,n))$, where $\alpha(m,n)$ is a~certain inverse of the Ackermann's function
+(see Definition \ref{ackerinv}).
+\qed
+
+Using this data structure, we get the following bound:
+
+\thm\id{kruskal}%
+The Kruskal's algorithm finds the MST of a given graph in time $\O(m\log n)$.
+If the edges are already sorted by their weights, the time drops to
+$\O(m\timesalpha(m,n))$.
+
+\proof
+We spend $\O(m\log n)$ time on sorting, $\O(m\timesalpha(m,n))$ on processing the sequence
+of \<Union>s and \<Find>s, and $\O(m)$ on all other work.