Here's two implementations of break, a snappy one from the prelude,
and a slow stupid stateful one.

They are quickchecked to be identical.

Is there a way to prove they are identical mathematically? What are
the techniques involved? Or to transform one to the other?