Every connected GRAPH has a spanning tree.

In the attempt of proving that every connected graph has a spanning tree we realized is much easier to prove that every graph has a spanning forest

A spanning forest of a graph is a subgraph that consists of a set of spanning trees, one for each maximal connected component of the initial graph.

  1. mktree preserves the maximal connected componets of each vertex

    GRAPH |- mcc(A, mktree(G)) = mcc(A, G)

    See th1.maude.
  2. mktree preserves the number of maximal connected componets

    GRAPH |- nomcc(mktree(G)) = nomcc(G)

    See th2.maude.
  3. mktree eliminates the cycles

    GRAPH |- nocycle(mktree(G)) = true

    See th3.maude.
Back