======================================
L_CONSTRAINT (invariant admissibility)
Successfully verified.
======================================
ANY.default_create (creator, inherited by L_CONSTRAINT)
Successfully verified.
======================================
L_CONSTRAINT.func
Successfully verified.
======================================
L_GENERIC (invariant admissibility)
Successfully verified.
======================================
ANY.default_create (creator, inherited by L_GENERIC)
Successfully verified.
======================================
L_GENERIC.g_function
Successfully verified.
======================================
L_GENERIC.h_function
Successfully verified.
======================================
L_GENERIC_USE (invariant admissibility)
Successfully verified.
======================================
ANY.default_create (creator, inherited by L_GENERIC_USE)
Successfully verified.
======================================
L_GENERIC_USE.use
Successfully verified.