= Predicate prefix-suffix reconstruction
Concatenating the initial <list prefix> accepted by a <predicate> with the remaining <list suffix> reconstructs the input, provided every test reached before the first false result terminates. Prove the finite case by <structural induction>: a true test copies the head, and a false test returns the untouched <list suffix>. An undefined reached test is an obstruction because reconstruction loses an exposed cons cell. An infinite all-true <list prefix> can still reconstruct the input, since <list concatenation> never demands its second argument there.
Back to article page
