====================================== ARRAY_SUM (invariant admissibility) Successfully verified. ====================================== ANY.default_create (creator, inherited by ARRAY_SUM) Successfully verified. ====================================== ARRAY_SUM.seq_sum Successfully verified. ====================================== ARRAY_SUM.array_sum Successfully verified.