****NOTE: There is a mistake in the Unify pseudo-code on p. 303 in the
book. The last line of the algorithm should say 'add{var/x}' rather
than 'add{x/var}'.  The example below shows a reasonably complicated
unification example where this change plays a role.****



Unify ( g(b,b), g(y, g(y,Z)) )

->Unify-Internal ( g(b,b), g(y, g(y,Z)), {} )
  the "compound?" check is the one that gets executed and
  results in a recursive call to Unify-Internal...

-->Unify-Internal ( (b,b), (y, g(y,Z)), Unify-Internal (g, g, {}) )
					   |
					   |-> this recursive call
                                               returns {} since g=g.
   the "list?" check is the one that gets executed;
   also first (b,b) = b; rest (b,b) = b and
        first (y, g(y,Z)) = y; rest (y, g(y,Z)) = g(y,Z)
   so we get another recursive call to Unify-Internal...

--->Unify-Internal ( b, g(y,Z),  Unify-Internal (b, y, {})
				   |
				   |-> this calls Unify-Var (b, y, {})
				       which returns {{b/y}} (NOT
				       {{y/b}}) as the algorithm
				       without the fix above would
				       produce... 

    now we've got a call to Unify-Var since b is a variable

---->Unify-Var (b, g(y,Z), {{b/y}})
     since {b/y} is in the list of existing substitutions, the first
     "if" statement in Unify-Var is executed, causing yet another call
     to Unify-Internal...

-----> Unify-Internal (y, g(y,Z), {{b/y}})
       y is a variable, so we get another call to Unify-Var

------> Unify-Var (y, g(y,Z), {{b/y}})
        this time, nothing of the form {y/VAL} is in the list of
        existing substitutions, so the first "if" statement is not
        executed; the first else-if clause is also not executed since
        there is nothing of the form {g(y,Z)/VAL} in the list of
        substitutions; but the following else-if clause IS executed
        since y occurs in g(y,Z).  so the occurs-check line returns
        FAILURE

<------ FAILURE 
        this is passed all the way back up to the topmost call to
        Unify and returned.