= Solution
The necessary definedness condition is local: \b[every <predicate> application actually reached before the first false result must produce a Boolean value]. No condition is needed on <predicate> applications after that first false result, because the <list suffix> is then returned without further testing. If a reached test is bottom at a known cons cell, the reconstructed <list> is bottom at that position, while the original <list> still exposes a cons there; equality fails.
To prove sufficiency on finite <lists>, induct on the spine. The empty case gives `[] ++ [] = []`. At a true test the left <list prefix> contributes the head, and the <induction> hypothesis reconstructs the tail. At a false test the <list prefix> is empty and the <list suffix> is the whole current <list>. For an infinite true-tested <list prefix>, every finite output <list prefix> is copied correctly; the infinite <list prefix> hides the possibly divergent <list suffix> computation. A partial spine ending in bottom is reconstructed up to exactly the same bottom. Thus finiteness is sufficient for an elementary <induction> proof but is not itself necessary for the identity.
For the uniform <list fold> calculation in part (f), use the convenient stronger assumption that \b[the input is a finite total <list> and the <predicate> terminates on every element of that <list>]. This makes the reconstruction identity available on every <list suffix>, not only on the <list suffixes> visited by the original <list prefix> scan. A total <predicate> on the element type ensures this uniformly over all finite total inputs.
Back to article page
