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