Unsure why (or whether?) a certain algorithm correctly computes a Minimum spanning tree
MAYBE-MST-C does obtain the minimum spanning tree correctly.
Define a &quot;local MST&quot; as a spanning tree for which any cycle resulting from adding some edge $e$ would not have any edges on the cycle with weight $&gt; w(e)$.
Lemma: The tree $T$ generated by MAYBE-MST-C is a local MST.
Proof:
any edge $e$ that is not already in $T$ at the end of the algorithm must have been removed, and thus it must have been a part of some cycle $c$, and was a maximal-weight edge on that cycle at the time $e$ was removed.
Note the rest of $c - {e}$ could have been deformed after $e$ was removed, but each deformation can only replace an edge $f$ with a longer path consisting of weights that are at most $w(f) \leq w(e)$. Hence, if $e$ were added back into $T$ at the very end and completed some cycle $c'$ that had the final result of all those deformations, $e$ is still guaranteed to be a maximal-weight edge on $c'$.
Main result: MAYBE-MST-C results in a minimal spanning tree.
proof: From the lemma, MAYBE-MST-C results in a local MST, and since local MSTs are minimum, the result immediately follows.