= Right-fold fusion law
{title2=$f\circ\operatorname{foldr}(g,a)=\operatorname{foldr}(h,b)$}
If $f$ is strict, $f(a)=b$, and $f(g(x,y))=h(x,f(y))$, then $f\circ\operatorname{foldr}(g,a)=\operatorname{foldr}(h,b)$. The empty case uses the base image and the cons case uses compatibility followed by <structural induction>. Strictness handles a bottom-valued spine. For pure definable continuous <functions>, equality on finite <partial lists> extends to infinite <lists> by finite approximation. For finite total inputs alone, <induction> does not require the strictness hypothesis.
Back to article page
