====================================== B_LOCAL (invariant admissibility) Successfully verified. ====================================== ANY.default_create (creator, inherited by B_LOCAL) Successfully verified. ====================================== B_LOCAL.default_values_for_local Successfully verified. ====================================== B_LOCAL.local_initialization Successfully verified. ====================================== B_LOCAL.local_assignment Successfully verified. ====================================== B_LOCAL.argument_assignment Successfully verified.