MT-DEFAULT-OB-MATE : FLAGMT-DEFAULT-OB-MATE is a flag or parameter.
Determines how ADD-CONN chooses the default obligation for
the second literal of the given pair (it is possible that this literal
will occur several times on the path, in several different obligations).
LOWEST : Chooses the obligation which lies lowest (i.e. furthest from the
HIGHEST : Chooses the obligation nearest to the root (but not the root).
HI-LO : Finds the obligation which occurs lowest; this obligation was
first added at some point in the matingstree. Then chooses the highest
obligation which was added at the same point in the matingstree.
MT-DEFAULT-OB-MATE takes values of type SYMBOL.
It belongs to subjects MTREE-TOP .
Its default value is LOWEST
Its current value is LOWEST.
TPS documentation homepage