Errata

• Root-Labeling
  

  When trying to formalize the results of the paper in Isabelle/HOL, Christian Sternagel and René Thiemann discovered a serious bug in Lemmas 13 and 17. In the proofs it is claimed that by replacing in a presupposed minimal sequence all maximal proper subterms with a root symbol that belongs to F# by the same variable, a minimal sequence with the property that no function symbol occurring at a non-root position belongs to F# is obtained. This is wrong.

  Consider the TRSs P = { F(x,y,z) → F(x,y,g(x,y)) } and R = { g(x, x) → g(x, x) }. The P-step F(F(x,y,z),F(y,x,z),g(F(x,y,z),F(y,x,z))) → F(F(x,y,z),F(y,x,z),g(F(x,y,z),F(y,x,z))) gives rise to a minimal sequence since F(x,y,z), F(y,x,z) and g(F(x,y,z),F(y,x,z)) are R-normal forms. If we replace the proper F-rooted subterms by a fresh variable u, we obtain the P-step F(u,u,g(u,u)) → F(u,u,g(u,u)) which does not result in a minimal sequence as g(u,u) is not terminating w.r.t. R.

  More complicated counterexamples refute the statements of Lemmata 13 and 17. By imposing left-linearity or dropping the minimality requirement, the results in Section 4 are recovered.