D-HIGHEST : INFOD-HIGHEST is a flag setting or other piece of information.
A setting for DEFAULT-OB.
The default next obligation in mtree is the highest element of the
set of smallest obligations (i.e. given the set of all obligations with
the fewest possible literals, the first element of this set to be found
by breadth-first search).
TPS documentation homepage