In Girard Proofs and Types, The degree of a type is defined as follows
$$\begin{align*}\partial(T_i)&=1\text{ if }T_i\text{ is atomic}\\\partial(U\times V)=\partial(U\rightarrow V) &=\max(\partial(U), \partial(V))+1\end{align*}$$
I interpret this as corresponding to one more than the length of the longest path in a directed graph.
It defines the degree of a redex as $$\begin{align*}\partial(\pi^1\left<u, v\right>)=\partial(\pi^2\left<u, v\right>)&=\partial(U\times V) \text{ where }U\times V\text{ is the type of }\left<u, v\right>\\\partial((\lambda x. v)u)&=\partial(U\rightarrow V)\text{ where }U\rightarrow V\text{ is the type of }(\lambda x. v)\end{align*}$$ where $\pi^1$ and $\pi^2$ refer to the first and second projections of a pair with $\pi^1 \left<u, v\right> \rightsquigarrow u$ and $\pi^2 \left<u, v\right> \rightsquigarrow v$
It then continues to say
The degree $d(t)$ of a term is the sup of the degrees of the redexes it contains. By convention, a normal term (i.e. one containing no redex) has degree 0.
NB: A redex $r$ has two degrees: one as a redex, another as a term, for the redex may contain others; the second degree is greater than or equal to the first: $\partial(r)\leq d(r)$
I'm not sure how to interpret the definitions for the degrees of terms and redexes.
From my current understanding, if $u$ is a term of type $U$ and $v$ is a term with type $V$ then $\partial(\pi^1\left<u, v\right>)=2$ and $\partial(\pi^1\left<\pi^1\left<u, v\right>, \pi^2\left<u, v\right>\right>)=2$ as the type of $\left<\pi^1\left<u, v\right>, \pi^2\left<u, v\right>\right>$ is again $U \times V$ and $d(\pi^1\left<\pi^1\left<u, v\right>, \pi^2\left<u, v\right>\right>)=2$ as all the redexes have degree 2.
For the same reason, I also think $\partial(\pi^1\left<\pi^1\left<\pi^1\left<u, v\right>, \pi^2\left<u, v\right>\right>, \pi^2\left<\pi^1\left<u, v\right>, \pi^2\left<u, v\right>\right>\right>)=2$ but $\partial(\pi^1\left<\left<u, v\right>, v\right>)=3$ as $\partial((U \times V) \times V) = 3$.
I'd like to ask how to interpret the degree of a redex and a term and if the degree values I wrote down are correct.
