f(X; Y; g(a)) = f(g(Y ); Z; X).
Your first step is to notice that f/3
= f/3
, which is case 3. Case 3 will succeed if X=g(Y), Y=Z, and g(a) = X.
Then X=g(Y)
might trivially be true; let's replace X with g(Y) in both sides:
f(g(Y); Y; g(a)) = f(g(Y); Z; g(y))
OK, moving along let's unify Y with Z. I don't see a case for this.
f(g(Y); Y; g(a)) = f(g(Y); Y; g(Y))
Moving along, the next thing we have is g(a) = g(Y)
. This succeeds unifying Y=a. The resultant term is:
f(g(a); a; g(a)) = f(g(a); a; g(a))
which is looks obvious. X = g(a), Y = Z = a.
I have no idea if this is right, but that's my guess.