(length.1) length([]) = 0 (length.2') length(h:t) = 1 + length(t)Evaluation is as follows.
length([6,5,4,3]) = length(6:[5,4,3]) = 1 + length([5,4,3]) by (length.2') = 1 + length(5:[4,3]) = 1 + (1 + length([4,3])) by (length.2') = 1 + (1 + length(4:[3])) = 1 + (1 + (1 + length([3]))) by (length.2') = 1 + (1 + (1 + length(3:[]))) = 1 + (1 + (1 + (1 + length([])))) by (length.2') = 1 + (1 + (1 + (1 + 0))) by (length.1) = 4