YES TRS: f(a(),b()) -> f(a(),c()) f(c(),d()) -> f(b(),d()) linear polynomial interpretations on N: f_A(x1,x2) = x1 f#_A(x1,x2) = x1 a_A = 0 a#_A = 2 b_A = 0 b#_A = 3 c_A = 4 c#_A = 1 d_A = 1 d#_A = 0 precedence: b > a > c > f > d