# How can I compute the most general unifier for these two expressions?

I have the following first order logic expressions:

$$f(g(a, h(b)), g(x, y)),~f(g(z,y), g(y, y))$$

and I want to compute the most general unifier for them. If I follow the algorithm found on these slides then I get the following.

\begin{align*} S_0 &= \{f(g(a, h(b)), g(x, y)), f(g(z,y), g(y, y))\}\\ D_0 &= \{g(a, h(b)),g(z,y)\} &[\text{first disagreement set}]\\ &\text{(need to unify these two functions)}\\ D_0'&= \{a,z\} &[\text{first sub-disagreement set}]\\ \sigma &= \{z=a\}\\ D_0''&=\{h(b),y\} &[\text{second sub-disagreement set}]\\ \sigma &= \{z=a, y=h(b)\}\\ S_1 &= \{f(g(a, h(b)), g(x, h(b))), f(g(a,h(b)), g(h(b), h(b)))\}\\ D_0 &= \{x,h(b)\} &[\text{second disagreement set}]\\ \sigma &= \{z=a,y=h(b),x=h(b)\}\\ S_2 &= \{f(g(a, h(b)), g(h(b), h(b))), f(g(a,h(b)), g(h(b), h(b)))\} \end{align*} No disagreement, unifier found! $$\sigma = \{z=a,y=h(b),x=h(b)\}$$.

However, this is not the most general unifier as we have $$\{y=h(b),x=h(b)\}\in \sigma$$, so i think the MGU should actually be $$\sigma' = \{z=a,y=h(b),x=y\}$$.

Is this correct? When I use Prolog to unify them, it gives $$\sigma'$$. What did I do wrong in my following of the algorithm, so that it gave me a unifier that wasn't the most general?