search package:sbv

Iteratively search at increasing depths of button-presses to see if we can transform from the initial board position to a final board position.
The classic "binary-searches are broken" example: http://ai.googleblog.com/2006/06/extra-extra-read-all-about-it-nearly.html
Proving binary search correct
Encode binary search in a functional style.