Definition: The length of a linked list of natural numbers \(L\), \(length: L \to \mathbb{N}\) is defined by \[\begin{array}{llll} \textrm{Basis Step:} & & length(~[]~) &= 0 \\ \textrm{Recursive Step:} & \textrm{If } l \in L\textrm{ and }n \in \mathbb{N}\textrm{, then } & length(~(n, l)~) &= 1+ length(l) \end{array}\]