I got this problem from Rustan Leino, who got it from Michael Jackson, as a variation of a problem he got from Koen Claessen.
I solved it and wrote up my solution.
A park contains paths that intersect at various places. The intersections are all three-way intersections and, with one exception, they're indistinguishable from each other. The one exception is an intersection where there's a restaurant.
Once you enter an intersection, you can continue to the left or continue to the right, but you can't turn around to exit the intersection the way you just entered it. Fortunately, even with this restriction, the restaurant is reachable from everywhere in the park. Your task is to find your way to the restaurant.
The park has strict littering regulations, so you're not allowed to modify the paths or intersections. (For example, you're not allowed to leave a note at an intersection saying you've been there.) However, you're allowed to do some bookkeeping on a pad of paper that you bring with you at all times. (In computer-science parlance, you're allowed some state.)
How can you be certain to find the restaurant? Note that it's not sufficient to use a probabilistic algorithm to find the restaurant with probability one; you must use an algorithm that's guaranteed to eventually reach the restaurant.
Define a path to be a sequence of instructions, each of which is "continue to the left" or "continue to the right". We can abbreviate these instructions as L and R.
Enumerate all the one-length paths (L and R) and follow all of them in succession. Then, enumerate all the two-length paths (LL, LR, RL, and RR) and follow all of them in succession. Continue with the three-length paths, the four-length paths, etc., until you find the restaurant.
The key to proving this works is to show that there exists a path $P$ such that, no matter where you start, if you take path $P$ you eventually reach the restaurant at some point along the path. To do this, we start with the following definitions.
Let $N$ be the number of intersections in the park, and denote those intersections by the numbers $1$ through $N$. Define $\mathsf{Endpoint}(i, p)$ for any node $i$ and path $p$ to be the node you wind up at if you follow path $p$ starting from node $i$.
Since the restaurant is reachable from anywhere in the park, we can define a function $\mathsf{FindFrom}$ such that $\mathsf{FindFrom}(i)$ is a path that takes you from node $i$ to the restaurant.
Now, define the function $\mathsf{FindFromAny}$ recursively as follows. Let $\mathsf{FindFromAny}(1) = \mathsf{FindFrom}(1).$ For any $1 < n \leq N$, let $\mathsf{FindFromAny}(n) = \mathsf{FindFromAny}(n-1) + \mathsf{FindFrom}(\mathsf{Endpoint}(n, \mathsf{FindFromAny}(n-1)))$ where $+$ denotes path concatenation.
Lemma. For any $1 \leq i \leq j \leq N$, if you follow path $\mathsf{FindFromAny}(j)$ starting from node $i$, you reach the restaurant at some point along that path.
Proof. We prove this by induction on $j$. For the base case, consider $j=1$. Given this, $i$ must be $1$, so $\mathsf{FindFromAny}(j) = \mathsf{FindFrom}(i).$ This means that the path will take you from node $i$ to the restaurant.
For the inductive step, suppose $j = J > 1$ and the lemma holds for $j = J-1.$ If $i \leq J-1,$ then by the inductive hypothesis we know that if you follow path $\mathsf{FindFromAny}(J-1)$ from node $i$ then you eventually reach the restaurant. So, if you take path $\mathsf{FindFromAny}(J),$ which starts off that way, you eventually find the restaurant. Now, the only remaining case to consider is $i = J.$ For this case, we note that there are two parts to the path $\mathsf{FindFromAny}(J).$ The first part, $\mathsf{FindFromAny}(J-1),$ will take us from node $i=J$ to node $\mathsf{Endpoint}(J, \mathsf{FindFromAny}(J-1))$ by the definition of $\mathsf{Endpoint}.$ The second part, $\mathsf{FindFrom}(\mathsf{Endpoint}(J, \mathsf{FindFromAny}(J-1))),$ will take us from there to the restaurant by the definition of $\mathsf{FindFrom}.$ Thus, in all cases you eventually reach the restaurant.
The induction is complete, so the lemma holds. $\Box$
Let $P = \mathsf{FindFromAny}(N).$ By the lemma, if you start from any intersection in the park and follow path $P,$ you eventually reach the restaurant. Because you enumerate paths in increasing path-length order, you eventually enumerate all the paths of length $|P|,$ which includes $P.$ This causes you to follow path $P$ starting from some intersection, which gets you to the restaurant.