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]