====================================== F_PIP_CLIENT (invariant admissibility) Successfully verified. ====================================== ANY.default_create (creator, inherited by F_PIP_CLIENT) Successfully verified. ====================================== F_PIP_CLIENT.test Successfully verified. ====================================== F_PIP_CLIENT.test_d Successfully verified. ====================================== F_PIP_NODE (invariant admissibility) Successfully verified. ====================================== F_PIP_NODE.make (creator) Successfully verified. ====================================== F_PIP_NODE.is_max Successfully verified. ====================================== F_PIP_NODE.acquire Successfully verified. ====================================== F_PIP_NODE.set_parent Successfully verified. ====================================== F_PIP_NODE.update_value Successfully verified. ====================================== F_PIP_NODE_D (invariant admissibility) Successfully verified. ====================================== F_PIP_NODE_D.make (creator) Successfully verified. ====================================== F_PIP_NODE_D.is_max Successfully verified. ====================================== F_PIP_NODE_D.acquire Successfully verified. ====================================== F_PIP_NODE_D.set_parent Successfully verified. ====================================== F_PIP_NODE_D.update_value Successfully verified.