====================================== SUM_AND_MAX (invariant admissibility) Successfully verified. ====================================== ANY.default_create (creator, inherited by SUM_AND_MAX) Successfully verified. ====================================== SUM_AND_MAX.sum_and_max Successfully verified.