(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