======================================
F_COM_CLIENT (invariant admissibility)
Successfully verified.
======================================
ANY.default_create (creator, inherited by F_COM_CLIENT)
Successfully verified.
======================================
F_COM_CLIENT.test
Successfully verified.
======================================
F_COM_CLIENT.test_d
Successfully verified.
======================================
F_COM_COMPOSITE (invariant admissibility)
Successfully verified.
======================================
F_COM_COMPOSITE.make (creator)
Successfully verified.
======================================
F_COM_COMPOSITE.children_set
Successfully verified.
======================================
F_COM_COMPOSITE.is_max
Successfully verified.
======================================
F_COM_COMPOSITE.add_child
Successfully verified.
======================================
F_COM_COMPOSITE.set_parent
Successfully verified.
======================================
F_COM_COMPOSITE.update
Successfully verified.
======================================
F_COM_COMPOSITE.lemma_ancestors_have_children
Successfully verified.
======================================
F_COM_COMPOSITE_D (invariant admissibility)
Successfully verified.
======================================
F_COM_COMPOSITE_D.make (creator)
Successfully verified.
======================================
F_COM_COMPOSITE_D.children_set
Successfully verified.
======================================
F_COM_COMPOSITE_D.is_max
Successfully verified.
======================================
F_COM_COMPOSITE_D.add_child
Successfully verified.
======================================
F_COM_COMPOSITE_D.set_parent
Successfully verified.
======================================
F_COM_COMPOSITE_D.update
Successfully verified.
======================================
F_COM_COMPOSITE_D.lemma_ancestors_have_children
Successfully verified.