f(X,P,h(U,V),k(a,Z))
  -
f(g(Y,Z),Q,Y,U)
  ------

{X <- g(Y,Z)}

f(g(Y,Z),P,h(U,V),k(a,Z))
         -
f(g(Y,Z),Q,Y,U)
         -

{Q <- P}

f(g(Y,Z),P,h(U,V),k(a,Z))
           ------
f(g(Y,Z),P,Y,U)
           -

{Y <- h(U,V)}

f(g(h(U,V),Z),P,h(U,V),k(a,Z))
                       ------
f(g(h(U,V),Z),P,h(U,V),U)
                       -

{U <- k(a,Z)}

f(g(h(k(a,Z),V),Z),P,h(k(a,Z),V),k(a,Z))
f(g(h(k(a,Z),V),Z),P,h(k(a,Z),V),k(a,Z))

mgu: {X <- g(Y,Z)} {Q <- P} {Y <- h(U,V)} {U <- k(a,Z)} =
{X <- g(h(k(a,Z),V),Z), Q <- P, U <- k(a,Z), Y <- h(k(a,Z),V)}.