======================================
F_I_CLIENT (invariant admissibility)
Successfully verified.
======================================
ANY.default_create (creator, inherited by F_I_CLIENT)
Successfully verified.
======================================
F_I_CLIENT.test
Successfully verified.
======================================
F_I_CLIENT.test_d
Successfully verified.
======================================
F_I_COLLECTION (invariant admissibility)
Successfully verified.
======================================
F_I_COLLECTION.make (creator)
Successfully verified.
======================================
F_I_COLLECTION.capacity
Successfully verified.
======================================
F_I_COLLECTION.add
Successfully verified.
======================================
F_I_COLLECTION.remove_last
Successfully verified.
======================================
F_I_COLLECTION_D (invariant admissibility)
Successfully verified.
======================================
F_I_COLLECTION_D.make (creator)
Successfully verified.
======================================
F_I_COLLECTION_D.capacity
Successfully verified.
======================================
F_I_COLLECTION_D.add
Successfully verified.
======================================
F_I_COLLECTION_D.remove_last
Successfully verified.
======================================
F_I_ITERATOR (invariant admissibility)
Successfully verified.
======================================
F_I_ITERATOR.make (creator)
Successfully verified.
======================================
F_I_ITERATOR.item
Successfully verified.
======================================
F_I_ITERATOR.forth
Successfully verified.
======================================
F_I_ITERATOR_D (invariant admissibility)
Successfully verified.
======================================
F_I_ITERATOR_D.make (creator)
Successfully verified.
======================================
F_I_ITERATOR_D.item
Successfully verified.
======================================
F_I_ITERATOR_D.forth
Successfully verified.