class interface P_TREE_NODE[G] invariant child: first_child /= Void implies first_child.parent = Current; sole_root: parent = Void implies right = Void and left = Void; -- no node twice in the same tree good_family: end of P_TREE_NODE[G]