(ld "defpkg.lisp") (certify-book "bitonic-sort" 3)