Height of tree is maximum of depths: Proof by induction I need help verifying the following proof by induction that establishes a connection between the given recursive definitions of the depth and height of a tree.
A position p corresponds to a node in the following.
depth:

*

*if p is the root, then the depth of p is 0

*otherwise, the depth of p is one plus the depth of parent of p

height:

*

*if p is a leaf, then the height of p is 0

*otherwise, the height of p is one more than the maximum of the heights of
p's children

Proposition: The height of a nonempty tree T is equal to the maximum of the depths of its leaf positions.
base case: A tree with 1 node consists solely of its root with a
depth of 0 per definition. Moreover, this root is a leaf with a height of 0,
also per definition.
induction step: Suppose we have a tree with n+1 nodes. All of the subtrees
located at the children of the tree's root have less than n+1 nodes, which
means we can apply the induction hypothesis to them. One of them has to have
maximum height h which is equal to the maximum depth d of its leaves. In the
path with maximum depth, the subtree's root has depth 0, its child in the
in the path has depth 1, and so on. Looking at the subtree as a part of the
whole tree, the subtrees root now has a depth of 1, its child in the path
has a depth of 2, and, finally, the leaf of this path now has a depth of
d+1.
The root above the subtree has a height of h+1.
This leaf also has to have the maximum depth of the whole tree. Otherwise,
there would have been a subtree with a leaf that has depth D > d and
therefore H > h, contradicting the fact that the subtree we were looking at
has maximum height h.
Is this proof by induction correct? Is it missing something? Is there are more elegant way to prove the proposition by induction?
 A: Your proof seems correct. You might want to re-write it in a less informal way though, e.g. as follows:
Let us define the depth and height as:
$$ d(x) = \begin{cases} 0 & \text{parent}(x) = nil \\ d(\text{parent}(x)) +1 & \text{otherwise} \end{cases} \hspace{1cm} h(x) = \begin{cases} 0 & \#\big(\text{children}(x)\big) = 0 \\ \max (\text{map}(h, \text{children}(x))) + 1 & \text{otherwise} \end{cases} $$
Note: the map applies $h$ to each element of the children list: e.g. $\text{map}\big(f, [a, b, c]\big) = \big[f(a), f(b), f(c)\big]$
Also note that, while the height is a property of a tree, the depth is a property of a node, and this will be reflected in the notation (I will also use the map notation to obtain the maximum depth: $\max(\text{map}(d, V))$, where $V$ is a set of vertices).
The proof proceeds by induction on the number of vertices:

*

*Base: Let $x$ be the only vertex of the tree; then $h(x) = 0$, as it has no children, and $d(x) = 0$, since it has no parent.


*Induction: $\#V = n + 1$; Let $r$ be the root of the tree. Each subtree of $T$ with a child of $r$ as its root has a maximum of $n$ vertices. Let $T' = (V', E')$ be the subtree with the maximum height among these subtrees of $T$. By inductive hp we know that $h(T') = \max(\text{map}(d, V'))$. Finally, from the definitions of $h$ and $d$, we derive that:
$$h(T) = h(T') + 1\hspace{1cm} \max(\text{map}(d, V)) = \max(\text{map}(d, V')) + 1 = h(T') + 1 = h(T)$$
Which concludes the proof.
Additional attention may be put into the last passage; despite intuitively making sense (adding one vertex "on top" adds one to the maximum depth), we may want to explicitly show that the depth of every node in the subtrees increases by one, and this happens in the "opposite direction" to the one we chose for our induction.
