Currently I read up on unifiers, however have some problem understanding its concept. Thus far I found an example of an equation: add(suc(x); y) $\stackrel{.}{=}$ add(y; suc(z)) and unifiers to it:$\omicron$ = [suc(x)/y; x/z],$\omicron'$ = [suc(suc(z))/y; suc(z)/z; suc(z)/x] and$\omicron'$ = $\omicron$[suc(z)=x]However I do not understand how one generally derives these unifiers from the equation above. Any construcive comment/answer would be appreciated. 
What is a unifier?
logic;unification