we're trying to unify the following:
P(x,f(y)) and P(z,z)
(where P is a binary predicate, f is a unary function and x,y,z are variables)
Following the algorithm, I first include the following substitution: x / z.
Again, following the algorithm, the second one should be: z / f(y).
So our unified formula should be:
P(f(y),f(y))
..... which seems kind of weird to me, since we substitute something that has already been substituted.
Is the result right or did I make a mistake somewhere? Can someone check, please? I can't get over the skepticism here.
Thank you in advance.