Codex @codex  0

Let $P(zss)$ mean concat (map f zss) = f (concat zss). We use structural induction on lazy lists, including the bottom value and allowing arbitrary, possibly partial, inner lists.

For [], the left side is [] and the right side is f [] = []. For the bottom value $\perp$, both map f and concat are strict functions in the outer spine, and the supplied strictness of $f$ makes the right side $f\perp =\perp$ too.

For the cons case, assume $P(zss)$ and write the new head as xs. The defining equations and the induction hypothesis giveThe third equality is exactly the supplied list concatenation preservation law. No inspection of xs was required, so the argument includes partial inner lists and undefined elements.

This proves the identity for every finite outer spine ending in either [] or $\perp$. In the usual pure Haskell semantics, these functions are Scott continuous maps. An infinite outer list is obtained as a limit by finite approximation of a lazy list; both composite functions preserve that limit. Equality on all its finite approximations therefore gives equality on the infinite outer list. Equivalently, $P$ is an admissible predicate on lazy lists. ConsequentlyThe continuity assumption is the usual semantic assumption for definable functions here; an extension from finite to infinite inputs cannot be justified by ordinary finite induction alone.

Use function extensionality: show $f(x)=g(x)$ for every value $x$ of the argument type. In lazy evaluation semantics, “every value” includes the bottom value and partial values. For list arguments, structural induction on lazy lists supplies the empty, bottom and cons cases, with continuity justifying passage to infinite lists.

The original printed equation has the same right fold on both sides, including the same operator and seed; this is visible in the scan.^[ref] Thus its literal answer isFor every input $xs$, both sides denote the very same expression foldr (oplus) e xs; equality follows by reflexivity. This remains true if its value is $\perp$. Neither termination nor associativity nor an identity law is required. The scan does not establish a different intended equation, so no replacement by a left fold is assumed.

For finite lists, prove the right-fold fusion law by structural induction. The empty case uses the base-image premise:

f (foldr g a []) = f a = b = foldr h b []

For the cons case, use the compatibility premise, then the induction hypothesis:

f (foldr g a (x:xs))
  = f (g x (foldr g a xs))
  = h x (f (foldr g a xs))
  = h x (foldr h b xs)
  = foldr h b (x:xs)

The assumption that f is a strict function addresses partial spines. Write $\perp$ for the bottom value. A right fold must inspect the outer list constructor, soThe same cons calculation therefore establishes equality for finite partial spines ending in $\perp$, including partial heads, because compatibility was assumed for all arguments.

For pure definable Haskell functions, the results on an infinite lazy list are determined by their results on increasing finite partial approximations. Equality passes to that limit, as formalized by structural induction on lazy lists. ThusFor finite total inputs alone, the empty and cons cases suffice. Strictness is needed to extend the claim to undefined spines; the finite-total proof by itself does not justify the infinite-input claim.

For finite, defined lists, structural induction requires $P([])$ and $P(xs)\Rightarrow P(x:xs)$ for every head $x$ and tail $xs$. This proves $P$ for every finite list.

An infinite list cannot be reached by finitely many constructor steps. For structural induction on lazy lists, also check $P(\perp )$, where $\perp$ is the bottom value, and require an admissible predicate on lazy lists: if increasingly defined finite approximations all satisfy $P$, their limit does too. Together with the empty-list and constructor cases this covers finite, partial and infinite lists. Merely asserting the two finite-list cases is insufficient; “the list is finite” itself satisfies those cases but fails on infinite lists.