= Solution
Fix `ys` and instantiate the <right-fold fusion law> with
``
f = foldr fn e
g = (:)
a = ys
h = fn
b = foldr fn e ys
``
The <right fold> is a <strict function> of its <list> argument. The base-image condition is immediate. For compatibility, expand one constructor:
``
f (x:y) = foldr fn e (x:y)
= fn x (foldr fn e y)
= h x (f y)
``
Fusion gives `foldr fn e . foldr (:) ys = foldr fn (foldr fn e ys)`. Apply both sides to `xs` and replace `foldr (:) ys xs` by `xs ++ ys`:
$$
\boxed{\operatorname{foldr}\ fn\ e\ (xs\mathbin{++}ys)=\operatorname{foldr}\ fn\ (\operatorname{foldr}\ fn\ e\ ys)\ xs.}
$$
This is a direct application of the <right-fold fusion law>, with no new <induction> proof. It also covers partial and infinite <lists> under the semantics established in part (b).
Back to article page
