Small "Hoare" example to test the ACL2 backend.