Well, in this particular case, note that you have two equations written. These equations are true of foldl', and in fact foldl' is the
least defined function satisfying these equations (see
http://en.wikibooks.org/wiki/Haskell/Denotational_semantics for the underlying theory of "definedness"). It a very pretty idea.
However, this happy view of equations breaks down once you start using the "fall through" semantics, as in:
foo (x:y:xs) = x + y
foo xs = 0
In which the second equation does not always hold (foo [1,2,3] = 0 is false). Because of this, I am beginning to prefer not writing functions using "fall through", although occasionally it is too damned convenient to pass up.
Luke