======================================
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.