Natural-number fold fusion law
ID: natural-number-fold-fusion-law
Suppose is a strict function, and . The zero case of the asserted equation is the base identity; the successor case rewrites as and applies structural induction. At an undefined argument, the strict function premise makes both sides the bottom value. For pure definable Haskell functions, equality on finite partial approximations extends to infinite constructor chains by continuity in the information order. For finite total arguments alone, the zero and successor proof does not require strictness.
New to topics? Read the docs here!