# Trees: deciding that a 6-vertex graph is a tree, with its leaves, a unique path and the unique cycle after adding an edge

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-tree/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-tree-01 · production-20261019-adopted-96



## Goal and scope

Let G=(V,E) with V={1,2,3,4,5,6} and E={{1,2},{2,3},{2,4},{4,5},{4,6}}. (1) Prove from the MKO's definition that G is a tree (V nonempty, connected, no simple cycle); (2) list its leaves; (3) find the path from 3 to 6 and prove it is unique; (4) add the edge {3,6}, write the simple cycle it creates and prove it is the only simple cycle; (5) contrast: a triangle plus an isolated vertex has |E|=|V|−1 but is not a tree; a single vertex without edges is a tree with no leaf.

Treats finite simple undirected graphs only (MKO assumption a1), with one concrete 6-vertex graph as the main example. Connectivity is proved with the lemma 'a walk contains a path', and acyclicity by deleting leaves one at a time with the lemma 'a vertex of degree at most 1 lies on no simple cycle'; both lemmas are proved here. Uniqueness of the path from 3 to 6 is proved for this example only, by exhaustion; the general theorems 'any two vertices of a tree have a unique path' and 'a tree has |V|−1 edges' are not proved here. The canonical MKO and its English edition are not changed.





## Givens and symbols


- graph_basics
- well_ordering
- nat_induction
- numeric_evaluation


- G1 — G=(V,E) with V={1,2,3,4,5,6} and E={{1,2},{2,3},{2,4},{4,5},{4,6}}; edges are undirected and each is listed once.
- G2 — The MKO's path conventions: a path repeats no vertex; the zero-edge path from a vertex to itself is valid. A leaf is a vertex of degree exactly 1.
- G3 — Contrast graphs: H=({1,2,3,4},{{1,2},{2,3},{1,3}}) and K=({7},∅).


- G=(V,E) — the main example graph
- N(v),\ \deg(v) — neighbour set and degree
- (v_0,v_1,v_2) — a path or cycle written as its vertex sequence
- G-v — delete the vertex v and the edges containing it
- G+e — add the new edge e
- H,\ K — the two contrast graphs





## Rules and sources


- graph_basics · prerequisite — (Simple undirected) graph: G=(V,E), where each edge is an unordered pair of distinct vertices; the degree of a vertex is the number of edges at it; handshake lemma Σ_v deg(v)=2|E|.
- well_ordering · prerequisite — Well-ordering principle: every nonempty subset of ℕ has a least element.
- nat_induction · prerequisite — Principle of induction: for a family P(n) starting at n₀, if P(n₀) holds and P(n)⇒P(n+1) for every n≥n₀, then P(n) holds for every n≥n₀.
- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
- set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x).
- exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
- contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
- order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
- logic_chain · prerequisite — Chaining: from P⇒Q and Q⇒R infer P⇒R; likewise for ⇔.
- subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B).
- contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
- and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
- case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
- mko_tree_def · cited — In a finite simple undirected graph G=(V,E), a tree is a graph with V nonempty, every pair of vertices joined by a path, and no simple cycle; a leaf is a vertex of degree exactly 1. · mko-tree
- walk_path_cycle · prerequisite — A walk of length k is a sequence of vertices w_0, w_1 and so on up to w_k in which each consecutive pair w_{j−1}, w_j is an edge; a path is a walk with no repeated vertex (k=0 allowed); a simple cycle is a walk of length k≥3 with w_k=w_0 and w_0 to w_{k−1} pairwise distinct.
- delete_vertex · prerequisite — G−v has vertex set V∖{v} and the edges of E not containing v; every walk, path or cycle of G−v is also one of G.
- L_walk_path · lemma — If a graph has a walk from u to v, it has a path from u to v.
- L_leaf_cycle · lemma — If deg_G(v)≤1, then G has a simple cycle ⇔ G−v has a simple cycle.





## Main derivation

S01 · definitionBefore

G\ \text{is a tree}

After

V\neq\varnothing\ \land\ \forall u,v\in V\ \exists\ \text{path}\ u\to v\ \land\ \neg\exists\ \text{simple cycle}

Conditions: none

Rule: mko_tree_def · Uses: G1, G2, mko_tree_def

Leaf basis: mko_tree_def + def_unfold

By the MKO's definition, proving that G is a tree requires three things: V is nonempty, any two vertices are joined by a path, and there is no simple cycle. Counting edges is not part of the definition.



S02 · impliesBefore

E=\{\{1,2\},\{2,3\},\{2,4\},\{4,5\},\{4,6\}\}

After

G\ \text{finite simple},\ |V|=6,\ |E|=5,\ V\neq\varnothing

Conditions: none

Rule: graph_basics · Uses: G1, graph_basics

Leaf basis: graph_basics + numeric_evaluation

Check each edge: both endpoints are in V and distinct, so there are no loops; the five edges are pairwise different as two-element sets, so there are no multiple edges; undirected edges ignore direction and each is listed once (the normalization of MKO assumption a1). So G is a finite simple undirected graph with |V|=6>0.



S03 · impliesBefore

N(v)\ \text{for}\ v\in V

After

\deg(1),\deg(2),\deg(3),\deg(4),\deg(5),\deg(6)=1,3,1,3,1,1

Conditions: none

Rule: graph_basics · Uses: S02, graph_basics

Leaf basis: graph_basics + numeric_evaluation

List neighbours: N(1)={2}, N(2)={1,3,4}, N(3)={2}, N(4)={2,5,6}, N(5)={4}, N(6)={4}. The degree is the number of neighbours. Handshake check: 1+3+1+3+1+1=10=2·5=2|E| (N1).



S04 · equivalentBefore

\{v\in V:\ \deg(v)=1\}

After

\{1,3,5,6\}

Conditions: none

Rule: def_unfold · Uses: S03, mko_tree_def

Leaf basis: def_unfold + set_builder

By the definition of a leaf (degree exactly 1), check all 6 vertices: 1, 3, 5, 6 have degree 1, while 2 and 4 have degree 3. The leaf set, in increasing order, is {1,3,5,6}.



S05 · impliesBefore

\text{vertex}\ 1

After

(1),\ (1,2),\ (1,2,3),\ (1,2,4),\ (1,2,4,5),\ (1,2,4,6)

Conditions: none

Rule: exists_intro · Uses: S03, G2, walk_path_cycle

Leaf basis: exists_intro + walk_path_cycle

Write one path from vertex 1 to each vertex. In each sequence consecutive vertices form edges of E ({1,2}, {2,3}, {2,4}, {4,5}, {4,6}) and no vertex repeats; (1) is the zero-edge path to itself.



S06 · impliesBefore

\forall u,v\in V:\ \text{walk}\ u\to 1\to v

After

\forall u,v\in V\ \exists\ \text{path}\ u\to v

Conditions: none

Rule: L_walk_path · Uses: S05, L_walk_path

Leaf basis: walk_path_cycle + well_ordering + contradiction

For any u, v: reverse the path from 1 to u of S05 (edges are undirected, so the reverse is still a walk), then append the path from 1 to v, giving a walk from u to v. By Lemma L_walk_path (proved in S06.1 and S06.2) there is a path from u to v. For example u=3, v=6: the walk (3,2,1,2,4,6) repeats 2, and the lemma's shortening gives the path (3,2,4,6). So G is connected.



S07 · equivalentBefore

G\ \text{has a simple cycle}

After

G_1=(\{2,4\},\{\{2,4\}\})\ \text{has a simple cycle}

Conditions: \deg(v)\le 1\ \text{at each removal}

Rule: L_leaf_cycle · Uses: S03, L_leaf_cycle, delete_vertex

Leaf basis: logic_chain + delete_vertex + graph_basics

Delete leaves one at a time, each time using Lemma L_leaf_cycle (proved in S07.1 and S07.2). In G, deg(1)=1, so G has a simple cycle ⇔ G−1 has one. In G−1, vertex 3 still has 2 as its only neighbour, degree 1, so delete it; then 5 (only neighbour 4) and 6 (only neighbour 4). Each deletion removes one edge, and after four of them the vertices {2,4} and the single edge {2,4} remain. Chaining the equivalences gives the claim.



S08 · equivalentBefore

G_1=(\{2,4\},\{\{2,4\}\})\ \text{has a simple cycle}

After

(\{4\},\varnothing)\ \text{has a simple cycle}

Conditions: \deg_{G_1}(2)=1

Rule: L_leaf_cycle · Uses: S07, L_leaf_cycle

Leaf basis: delete_vertex + graph_basics

In G_1 vertex 2 has the single neighbour 4, degree 1; one more use of the lemma deletes 2 and leaves the single-vertex graph ({4},∅).



S09 · impliesBefore

G\ \text{has a simple cycle}\iff(\{4\},\varnothing)\ \text{has one}

After

G\ \text{has no simple cycle}

Conditions: none

Rule: logic_chain · Uses: S07, S08, walk_path_cycle

Leaf basis: logic_chain + walk_path_cycle

A simple cycle needs at least 3 distinct vertices; ({4},∅) has one vertex and no edges, so it has no simple cycle. Chaining the equivalences of S07 and S08, G has no simple cycle either.



S10 · impliesBefore

V\neq\varnothing,\ \text{connected},\ \text{no simple cycle}

After

G\ \text{is a tree}

Conditions: none

Rule: mko_tree_def · Uses: S02, S06, S09, mko_tree_def

Leaf basis: mko_tree_def + and_intro_elim

S02 gives V nonempty, S06 gives connectivity and S09 gives no simple cycle; together these are exactly the MKO's definition of a tree.



S11 · impliesBefore

3,\ 6\in V

After

(3,2,4,6)\ \text{is a path from 3 to 6}

Conditions: none

Rule: exists_intro · Uses: S03, walk_path_cycle

Leaf basis: exists_intro + walk_path_cycle

{3,2}, {2,4} and {4,6} are in E and the four vertices 3, 2, 4, 6 are pairwise distinct, so (3,2,4,6) is a path from 3 to 6. Following MKO paragraph 1 it is written in its actual vertex order, not as the sorted set {2,3,4,6}.



S12 · impliesBefore

P\ \text{any path from 3 to 6}

After

P=(3,2,4,6)

Conditions: none

Rule: case_analysis · Uses: S03, S11, walk_path_cycle

Leaf basis: case_analysis + walk_path_cycle + graph_basics

Let P be any path from 3 to 6 with vertices p_0=3 through p_m=6. S12.1 to S12.3 exhaust every possible next vertex at each stage and show that P can only be (3,2,4,6).



S13 · impliesBefore

e=\{3,6\}

After

3,6\in V,\ 3\neq 6,\ e\notin E;\ G+e=(V,\,E\cup\{e\})

Conditions: none

Rule: graph_basics · Uses: G1, S10, graph_basics

Leaf basis: graph_basics

Check the add-an-edge premise of MKO assumption a3: the original graph is a tree (S10); 3 and 6 are in V and distinct; {3,6} is not among the five edges of E. So G+e is still a simple graph, with 6 edges.



S14 · impliesBefore

(3,2,4,6)\ \text{in}\ G,\ e=\{6,3\}

After

C=(3,2,4,6,3)\ \text{is a simple cycle in}\ G+e

Conditions: k=4\ge 3

Rule: walk_path_cycle · Uses: S11, S13, walk_path_cycle

Leaf basis: walk_path_cycle + exists_intro

Start at the smaller end label 3, follow the original path to 6, and return to 3 by the new edge: the length is k=4≥3, the first four vertices 3, 2, 4, 6 are pairwise distinct, {3,2}, {2,4}, {4,6} are in E and {6,3}=e. So C is a simple cycle of G+e, written according to the output convention of MKO paragraph 1.



S15 · impliesBefore

D\ \text{any simple cycle in}\ G+e

After

D=C\ \text{up to starting point and direction}

Conditions: none

Rule: case_analysis · Uses: S09, S12, S14

Leaf basis: case_analysis + contradiction + walk_path_cycle

If D did not use e, all its edges would be in E and it would be a simple cycle of G, contradicting S09; so D uses e. Since the vertices of D (apart from the repeated endpoint) are pairwise distinct, 3 and 6 each occur once and e is used exactly once. Rotate D, reversing it if needed, so that it starts at 3 and its last edge is e from 6 back to 3; removing that edge leaves a path from 3 to 6 that uses only edges of E. By S12 that path is (3,2,4,6), so D is C.



S16 · impliesBefore

H=(\{1,2,3,4\},\{\{1,2\},\{2,3\},\{1,3\}\})

After

|E_H|=|V_H|-1,\ \text{no path}\ 1\to 4;\ H\ \text{is not a tree}

Conditions: none

Rule: mko_tree_def · Uses: G3, walk_path_cycle, mko_tree_def

Leaf basis: mko_tree_def + contradiction + graph_basics

|V_H|=4 and |E_H|=3=4−1, the same edge count pattern as the main example, but deg(4)=0. A path from 1 to 4 has at least one edge (1≠4) and its last edge contains 4, which is impossible; so H is not connected. Moreover (1,2,3,1) is a simple cycle. H is not a tree.



S17 · impliesBefore

K=(\{7\},\varnothing)

After

K\ \text{is a tree},\ \text{leaves}(K)=\varnothing

Conditions: none

Rule: mko_tree_def · Uses: G2, G3, mko_tree_def

Leaf basis: mko_tree_def + walk_path_cycle

V={7} is nonempty; the only pair (7,7) is joined by the zero-edge path (7) (G2); a simple cycle needs at least 3 distinct vertices, so there is none. K is a tree. But deg(7)=0≠1, so by the definition K has no leaf (MKO assumption a2).







## Substeps and lemmas

S06.1 · impliesBefore

\text{the set of lengths of walks}\ u\to v\ \text{is nonempty}

After

\exists\ \text{a walk}\ W\ \text{from}\ u\ \text{to}\ v\ \text{of least length}\ k

Conditions: none

Rule: well_ordering · Uses: walk_path_cycle, well_ordering

Leaf basis: well_ordering

Assume there is a walk from u to v. The lengths of all such walks form a nonempty subset of ℕ, which by well-ordering has a least element k; take a walk W of length k with vertices w_0=u through w_k=v.



S06.2 · impliesBefore

w_i=w_j\ (i<j)\ \text{in the least walk}\ W

After

\text{a walk of length}\ k-(j-i)<k,\ \text{contradiction; so}\ W\ \text{is a path}

Conditions: i<j

Rule: contradiction · Uses: S06.1, contradiction

Leaf basis: contradiction + walk_path_cycle + order_basics

Suppose W repeats a vertex, w_i=w_j with i<j. Delete w_{i+1} through w_j, keeping w_0 to w_i followed by w_{j+1} to w_k; since w_i=w_j is adjacent to w_{j+1} (or, if j=k, the walk simply stops at w_i=v), this is still a walk from u to v, of length k−(j−i)<k, contradicting the minimality of k. So W repeats no vertex and is a path. S06.1 and S06.2 together prove Lemma L_walk_path.



S07.1 · impliesBefore

C\ \text{simple cycle in}\ G-v

After

C\ \text{simple cycle in}\ G

Conditions: none

Rule: subset_def · Uses: delete_vertex, walk_path_cycle

Leaf basis: subset_def + delete_vertex

(The ⇐ direction) The vertices and edges of G−v all belong to G, so the same vertex sequence still meets every condition of a simple cycle in G.



S07.2 · impliesBefore

C\ \text{simple cycle in}\ G,\ \deg_G(v)\le 1

After

v\notin C,\ C\ \text{simple cycle in}\ G-v

Conditions: k\ge 3

Rule: contrapositive · Uses: walk_path_cycle, graph_basics

Leaf basis: contrapositive + graph_basics + walk_path_cycle

(The ⇒ direction) In a simple cycle of length k≥3, each w_j (0≤j<k) has two cycle neighbours w_{j−1} and w_{j+1} (indices mod k), which differ because w_0 to w_{k−1} are pairwise distinct and k≥3; so every vertex of C has degree at least 2 in G. Contrapositively, a vertex v with deg_G(v)≤1 is not on C, no edge of C contains v, and C is a simple cycle of G−v. S07.1 and S07.2 together prove Lemma L_leaf_cycle.



S12.1 · impliesBefore

p_0=3\neq 6

After

p_1=2

Conditions: none

Rule: graph_basics · Uses: S03, walk_path_cycle

Leaf basis: graph_basics

3≠6, so P has at least one edge; p_1 must be a neighbour of 3, and N(3)={2}, so p_1=2.



S12.2 · case_splitBefore

p_1=2\neq 6

After

p_2=4

Conditions: none

Rule: case_analysis · Uses: S12.1, S03

Leaf basis: case_analysis + contradiction + graph_basics

2≠6, so P continues; p_2∈N(2)∖{3}={1,4} (a path repeats no vertex). Case p_2=1: 1≠6, so P must continue, but N(1)∖{3,2}=∅, so there is nowhere to go, a contradiction. Hence p_2=4.



S12.3 · case_splitBefore

p_2=4\neq 6

After

p_3=6,\ m=3,\ P=(3,2,4,6)

Conditions: none

Rule: case_analysis · Uses: S12.2, S03

Leaf basis: case_analysis + contradiction + graph_basics

4≠6, so P continues; p_3∈N(4)∖{3,2}={5,6}. Case p_3=5: 5≠6, so P must continue, but N(5)∖{3,2,4}=∅, a contradiction. Hence p_3=6; 6 occurs only once in the path and is its end, so m=3 and P=(3,2,4,6).







## Reverse audits


- S17 · premise_audit · G2, G3, mko_tree_def — It relies on two stated conventions: the zero-edge path is valid, and a leaf has degree exactly 1.
- S16 · premise_audit · G3, walk_path_cycle, mko_tree_def — Showing that a graph is not a tree requires only one failed condition; here two of them fail.
- S15 · premise_audit · S09, S12, S14, case_analysis — Uniqueness relies on G having no cycle (S09) and on the unique path (S12); cycles are identified when they differ only in starting point and direction, which the MKO handles by its fixed output convention.
- S14 · premise_audit · S11, S13, walk_path_cycle — Only existence is shown; uniqueness is in S15.
- S13 · premise_audit · G1, S10, graph_basics — If e were already in E, listing it again would create no new edge and the premise would fail (see the error controls).
- S12.3 · premise_audit · S12.2, S03, case_analysis — The two cases {5,6} exhaust all possibilities; the result is the path of S11.
- S12.2 · premise_audit · S12.1, S03, case_analysis — The two cases {1,4} exhaust all possibilities.
- S12.1 · premise_audit · S03, graph_basics — Only the neighbour list of 3 is used.
- S12 · premise_audit · S03, S11, walk_path_cycle, case_analysis — The exhaustion covers every neighbour at every stage, so it is a complete proof for this pair of vertices; it is not a proof of the general theorem.
- S11 · premise_audit · S03, walk_path_cycle, exists_intro — Only existence is shown; uniqueness is proved separately in S12.
- S10 · sufficient_goal_reduction · S02, S06, S09, mko_tree_def, and_intro_elim — Goal G: G is a tree. Sufficient condition H: the three conditions together; H⇒G by the definition. H is proved forwards in S02, S06 and S09, without using |E|=|V|−1 and without using G as a premise.
- S09 · premise_audit · S07, S08, logic_chain, walk_path_cycle — The conclusion relies on the whole chain of equivalences; if some deleted vertex had degree above 1 the chain would break, which is why S07 rechecks degrees each time.
- S08 · inverse_equivalence · L_leaf_cycle — The lemma is an equivalence, so the step is two-way.
- S07.2 · premise_audit · walk_path_cycle, graph_basics, contrapositive — The key is that k≥3 makes the two cycle neighbours distinct; with a 'cycle' (u,v,u) of length 2 the argument would fail, which is why the definition requires k≥3. The lemma itself is not used.
- S07.1 · premise_audit · delete_vertex, walk_path_cycle, subset_def — Only the inclusion of the subgraph is used; this direction needs no degree condition.
- S07 · inverse_equivalence · L_leaf_cycle, logic_chain — Each application of the lemma is an equivalence and equivalences chain, so the whole step is two-way; before each deletion the degree in the current graph is rechecked to be at most 1.
- S06.2 · premise_audit · S06.1, contradiction, walk_path_cycle — The contradiction rests only on the minimality of k and on the shortened sequence still being a walk; the lemma itself is not used.
- S06.1 · premise_audit · walk_path_cycle, well_ordering — Well-ordering needs nonemptiness, which the lemma's premise (a walk exists) supplies.
- S06 · premise_audit · S05, L_walk_path — Only 'vertex 1 reaches every vertex' and the lemma are needed; the 15 vertex pairs need not be listed one by one. Uniqueness of paths is not claimed.
- S05 · premise_audit · S03, walk_path_cycle, exists_intro — Each path only needs its edges and the no-repeat condition checked; this step does not claim the paths are unique.
- S04 · inverse_equivalence · S03, def_unfold — Both directions are checked point by point: each listed vertex has degree 1, and the unlisted 2 and 4 do not.
- S03 · premise_audit · S02, graph_basics, numeric_evaluation — Each edge {u,v} contributes v∈N(u) and u∈N(v) exactly once each; the matching handshake sum is an independent check of the neighbour lists.
- S02 · premise_audit · G1, graph_basics — This only checks the data format; no connectivity or acyclicity is claimed.
- S01 · premise_audit · G1, G2, mko_tree_def — This step only unfolds the definition and derives nothing new; the three conditions are proved separately later.





## Error controls and negative controls

Edge count alone does not determine whether a graph is a treeThe misconception the MKO names: deciding that a graph is a tree from |E|=|V|−1 alone. H (a triangle plus the isolated vertex 4) has 4 vertices and 3 edges, yet is disconnected and has a cycle. This guide decides that G is a tree without using the edge count at all, by proving connectivity and acyclicity directly (S06, S09).

A single-vertex tree has no leafK=({7},∅) is a tree, but deg(7)=0, not 1, so under this MKO's leaf convention its leaf set is empty. Calling a degree-0 vertex a leaf is another misconception the MKO names.

An existing edge cannot be 'added' again{2,4} is already in E; listing it again leaves the normalized edge set unchanged and creates no cycle. Treating (2,4,2) as a cycle fails the requirement k≥3 for a simple cycle. MKO assumption a3 requires the added edge to be absent from the original graph.

Write paths in vertex orderA path is a sequence, not a set. (3,2,4,6) differs from the sorted (2,3,4,6): the latter does not start at 3, and {3,4} is not an edge.


- H has 4 vertices and 3 edges, so H is a tree → reject — Vertex 4 is isolated, so H is disconnected; and (1,2,3,1) is a simple cycle.
- The vertex 7 of K=({7},∅) is a leaf → reject — deg(7)=0, while a leaf needs degree exactly 1.
- Adding {2,4} to G once more creates the cycle (2,4,2) → reject — {2,4} is already in E, so the edge set is unchanged; (2,4,2) has length 2<3 and is not a simple cycle.
- The path from 3 to 6 is (2,3,4,6) → reject — It does not start at 3, and {3,4}∉E; the correct path is (3,2,4,6).
- G+{3,6} has two different simple cycles, (3,2,4,6,3) and (6,4,2,3,6) → reject — The second is the same cycle with another starting point and the opposite direction; both have edge set {{3,2},{2,4},{4,6},{6,3}} (S15).





## Result and limitations

G is a tree: V is nonempty, vertex 1 reaches every vertex so G is connected, and deleting leaves down to a single vertex shows there is no simple cycle. The leaves are {1,3,5,6}. The unique path from 3 to 6 is (3,2,4,6). After adding the new edge {3,6} there is exactly one simple cycle, (3,2,4,6,3). Contrast: H has |E|=|V|−1 but is disconnected and has a cycle, so it is not a tree; the single-vertex graph K is a tree with an empty leaf set.


- The general theorems 'any two vertices of a tree have a unique path' and 'a finite tree has |V|−1 edges' are not proved here; the uniqueness in S12 is proved by exhaustion for 3 and 6 only.
- Cycles are identified when they differ only in starting point and direction; the MKO removes this choice by a fixed output convention (start at the smaller label, follow the original path).





## Verification and source binding

8 declared checks for this guide; only the listed expressions are covered.


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 2705a4400701f09e6a4f469a879e803b4a263ba61ee3436c9788c3e7c6c938dc
- original source SHA-256: 2705a4400701f09e6a4f469a879e803b4a263ba61ee3436c9788c3e7c6c938dc
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-tree-01.json)