Solving the nice puzzle below, I found it easier to define a stream coinductively than to define a function from natural numbers inductively. You’re standing in front of a 100 story building with two identical bowling balls. You’ve been tasked with testing the bowling balls’ resilience. The building has a stairwell with a window at each story from which you can (conveniently) drop bowling balls. To test the bowling balls you need to find the first floor at which they break. It might be the 100th floor or it might be the 50th floor, but if it breaks somewhere in the middle you know it will break at every floor above. Devise an algorithm which guarantees you’ll find the first floor at which one of your bowling balls will break. You’re graded on your algorithm’s worst-case running time. “Running time” here means the number of times we drop a ball.