 Solution

The list fold criterion is: there must be a value z and a definable combining function c such thatThe last equality says that all information needed about the tail factors through f xs; the combining function receives no other access to xs. These conditions give f = foldr c z.

Necessity follows from the defining equations of foldr, including its case distinction on the input list. Sufficiency follows by structural induction for finite lists and finite partial-list approximations. For infinite or partial lazy lists, the usual continuous semantics of these definable functions extends equality from the approximations to their limit. The strictness condition matters: agreement only on finite total lists does not establish agreement at $\perp$. This is the fold factorisation criterion.