====================================== LONGEST_COMMON_PREFIX (invariant admissibility) Successfully verified. ====================================== ANY.default_create (creator, inherited by LONGEST_COMMON_PREFIX) Successfully verified. ====================================== LONGEST_COMMON_PREFIX.lcp Successfully verified. ====================================== LONGEST_COMMON_PREFIX.test_lcp Successfully verified.