Here is a more imperative version (using exceptions): The assumption is (as in the article) that each predicate terminates for every bit sequence and that the

Here is a more imperative version (using exceptions): The assumption is (as in the article) that each predicate terminates for every bit sequence and that the predicates are actual functions, i.e. they have no state. Also, predicates don’t catch exceptions. We can implement find as follows: Start with n = 0 and generate the bit sequences with all prefixes of length n. Have them throw an exception if somebody tries to access an index past that prefix. This way, you get finitely many partial bit sequences. Apply the predicate to all these sequences. There are three cases: - The predicate returns true for one of the partial sequences. Because it doesn’t catch exceptions, it only looked at values within the prefix. Hence, the result of the predicate doesn’t change if we change the rest of the sequence—for example, we can set the rest of the sequence to 0 and we have found a sequence that satisfies the predicate. - The predicte returns false for all our partial sequences. Similarly to the case above, the result does not depend on bits beyond the prefix, so no matter what we do, we will not find a sequence satisfying the predicate and we can return any sequence (by the definition of find, it returns any sequence if the predicate is unsatisfiable). - For some of our partial sequences, we get an exception. Then we increase n and try again. This algorithm has to terminate: if it doesn’t, we get the third case each time. But taking the bit sequence that we get by always extending our prefix on a path that keeps throwing exceptions, we get a bit sequence on which our predicate does not terminate, contrary to our assumption that it always does.