Abstract
Richard Bird and collaborators have proposed a derivation of an
intricate cyclic program that implements the Morris-Pratt string
matching algorithm. Here we provide a proof of total correctness for
Bird's derivation and complete it by adding Knuth's
optimisation.