SIMPLIFY : UNIFOPSIMPLIFY is an unification command.
A call to TPS's version of Huet's SIMPL algorithm. Dpairs in the
current topnode are replaced by the dpairs returned by the call. It will
also find substitutions of the form (var . term) provided `var' does not
occur in `term'. This command will alter the unification tree.
The command format for SIMPLIFY is:
TPS documentation homepage