1, line -7: replace *s(s(s(0))+0)* by *s(s(s(0)+0))*.
(Sebastian Skalberg) (p)

15, line 9: replace "that" by "that if"" and "iff" by "then". (Aurelian Radoaca) (p)

25, line -10: replace $\gtrsim$ by $\gtrsim_{mul}$ (Aurelian Radoaca) (p)

27, line -14 and -18: replace "bool" by "order" in the type of the ML functions "rem1" and "mdiff". (Stephen Eldridge) (p)

29, line 1: replace "example" by "examples". (Markus Triska) (p)

29, penultimate line of the proof of Newman's Lemma: replace
*y _{1}* by

39, line 7: replace $\cal T$ by *T*. (Amine Chaieb) (p)

45, lines -7, and -8: replace $A$ by $\cal A$. (Aurelian Radoaca) (p)

51, line 6: replace *T* by $\cal T$ (in the range of the homomorphism).
(Sebastian Skalberg) (p)

52, line -15: replace *X* by *V*. (Amine Chaieb) (p)

60, Exercise 4.2: add "finite" before *E*. (Martin Lange) (p)

77, line 9: replace *V(t)* by *Var(t)*. (Dennis Pagano) (p)

96, line -8: replace left-arrow over *l* by right-arrow.
(Hisashi Kondo)

98, line 21 and 22: replace *s _{1}* by

101, Exercise 5.2: replace "ground" by "right-ground". (Robert McNaughton) (p)

103, Exercise 5.6: Two assumptions are missing. First, the set of ground terms must be non-empty. Under this assumption, the order defined on p.104 is a reduction order. To show that it is the largest order, one must additionally assume that the order > one starts with is total on ground terms. (Ralph Matthes) (p)

106, line -10: replace "2 > 1" by "3 > 2" and $\odot^A(1,2) = 1 = \odot^A(1,1)$ by $\odot^A(2,3) = 4 = \odot^A(2,2)$ (Aurelian Radoaca) (p)

111, Exercise 5.9: replace *k*|*s*|_{f} by
*k*(|*s*|_{f}+1)

114, in the paragraph after (1): replace both occurrences of *n*
by *n _{i}*. (Aurelian Radoaca) (p)

115, line 4: replace "variable" by "variable or a constant"

115-116: In the proof of Theorem 5.4.8 replace every occurrence
of *V(.)* by *Var(.)*.

120, lines 2 and 3: replace *l* by *n*. (Martin Lange) (p)

120, lines -5: replace *1 ≥ i ≥ n* by *1 ≤ i ≤ n*. (Aurelian Radoaca) (p)

134-135, proof of Theorem 6.1.1: add the assumption "and neither *l* nor
*r* is a variable" behind "*Var(l) = Var(r)*" (2 occurrences).

135: First sentence of section 6.2: insert "terminating" in front of "finite".

140, line 6: replace *t _{1}*
by

142: In Exercise 6.7 (b) replace both occurrences of *E* by *G*. (p)

144, line 3, below Fig 6.3: replace "cps" by "innercps". (Yamatodani Kiyoshi) (p)

153, line -2: replace *P _{1}^{≥}*
by

154: line 2: replace *P _{1}^{≥}*
by

156, Exercise 6.18: replace *h(p(x),q(x))* by *h(p(x),q(y))*.
(Aurelian Radoaca) (p)

158, line -7: replace "canonical" by "convergent". (Philipp Lucas) (p)

175, line -13: replace *s _{i-1}[sigma(u)]* by

178, lines -11,-12: replace *R _{i}* by

183, line -13 (second recursive call of *simpl*):
replace *E* by *E'*. (Jaco van de Pol) (p)

190, line -2: replace the last *f _{1}* with

192, line 25 (penultimate line in proof of Theorem 8.2.7):
replace *f _{l}* by

228, line -5: replace *S _{1}* by

233, Fig. 10.1: replace the last "Decompose" by "Delete" (Aurelian Radoaca) (p).

239 and 242, in the displayed equation marked with (*): replace the 3x1 zero-matrix by the 1x1 zero-matrix "(0)". (Sebastian Skalberg) (p)

240, line -12, the first line in the proof of Theorem 10.3.10: replace *M _{n,r}(sigma)* by

249, line 9: The sequence of inequalities in this line must be changed slightly. In addition, for the statement in line 10 to be true, the definition of the norm of a matrix must be changed. See here for details. (Markus Rosenkranz) (p)

253, line 18: replace $\models s \not\approx t$ by $\not\models s \approx t$. (Sebastian Skalberg) (p)

255, lines 6 and 11: replace *(s+1)*σ(t)+s*σ(t)*
by *(s+1)*σ _{1}(t)+s*σ_{2}(t)*.
(Aurelian Radoaca) (p)

255, line -15 through -11: The *tau* introduced locally with
"Let *tau* be..." clashes with the global *tau* that occurs in the
definition of *sigma*. It needs to be renamed to, for example,
*delta*. Thus on those 5 lines all occurrences of *tau*, except for
the 4th, 9th and 12th, should be replaced by *delta*.
(Sebastian Skalberg) (p)