corrected the subsitution composition order in the unification
implementation and shift permutation application in the substitution
function.