Using the unification algorithm to determine whether pairs of formulas are unifiable I would like to use the unification algorithm to determine whether or not the following pairs of formulas are unifiable, and if so, find a most general unifier, showing all my working. Am I doing it correctly? I have a feeling that ii) is not unifiable...
i) $G(x, y, W(x)) \quad G(J, W(z), z)$ 
Step 1. 
$A = G(x, y, W(x)) \\
B = G(J, W(z), z) \\
t_A = x \\
t_B = J \\
mgu = [x/J]$
Step 2. 
$A = G(J, y, W(J)) \\
B = G(J, W(z), z) \\
t_A = y \\
t_B = W(z) \\
mgu = [x/J][y/W(z)] = [x/J,~y/W(z)] $
Step 3. 
$A = G(J, W(z), W(J)) \\
B = G(J, W(z), z) \\
t_A = W(J) \\
t_B = z \\
mgu = [x/J,~y/W(z)][W(J)/z] = [x/J,~y/W(z),~W(J)/z]$
Step 4. 
$A = G(J, W(z), z) \\
B = G(J, W(z), z) \\
⇒ unifiable, ~ mgu = [x/J,~y/W(z),~W(J)/z]$
ii) $G(x, W(x), x) \quad G(J, y, W(y))$
Step 1. 
$A = G(x, W(x), x) \\
B = G(J, y, W(y)) \\
t_A = x \\
t_B = J \\
mgu = [x/J]$
Step 2. 
$A = G(J, W(J), J) \\
B = G(J, y, W(y)) \\
t_A = W(J) \\
t_B = y \\
mgu = [x/J][W(J)/y] = [x/J,~W(J)/y] $
Step 3. 
$A = G(J, y, J) \\
B = G(J, y, W(y)) \\
t_A = W(J) \\
t_B = y \\
mgu = [x/J,~W(J)/y][J/W(y)] = [x/J,~W(J)/y,~J/W(y)]$
Step 4. 
$A = G(J, y, W(y)) \\
B = G(J, y, W(y)) \\
⇒ unifiable, ~ mgu = [x/J,~W(J)/y,~J/W(y)]$
 A: (i) does unify. (ii) fails to unify.
However, it appears you have a misunderstanding about unifiers.  A unifier is a substitution that maps variables to terms (which themselves might contain, or even just be, variables).  Your notation, particularly in your final step 4, suggests that you think you can map arbitrary terms to arbitrary other terms.  Assuming $J$ isn't a variable, a substitution like $[J/W(y)]$ simply doesn't make any sense.  Assuming $[T/x]$ means "replace the variable $x$ with the term $T$", your mgus should always be of the form $[T_1/x_1,T_2/x_2,\dots T_n/x_n]$.
While this may not be what you were taught, I recommend (and most computer implementations of unification work this way) that you simply generate a bunch of constraints and then "solve" them rather than trying to substitute as you go.
In the first case, you get $x = J, y = W(z), z = W(x)$ from which you can readily produce the substitution $[J/x,W(W(J))/y,W(J)/z]$.  In the second case, you get $x = J, y = W(x), x = W(y)$ from which you can easily see that $J \neq W(y)$ no matter what $y$ is.  In a slight variant of (ii) where the second term is $G(x,y,W(y))$ you get $x = x, y = W(x), x = W(y)$.  This simplifies to $x = W(W(x)), y = W(W(y))$. In this case unification fails because it fails the occurs check. Substitutions that replace a variable with a term that contains the variable as a (strict) subterm are disallowed.
