YES TRS: f(g(i(a(),b(),b'()),c()),d()) -> if(e(),f(.(b(),c()),d'()),f(.(b'(),c()),d'())) f(g(h(a(),b()),c()),d()) -> if(e(),f(.(b(),g(h(a(),b()),c())),d()),f(c(),d'())) linear polynomial interpretations on N: f_A(x1,x2) = 1 f#_A(x1,x2) = x1 + x2 + 2 g_A(x1,x2) = 4 g#_A(x1,x2) = 8 i_A(x1,x2,x3) = x1 + x2 i#_A(x1,x2,x3) = 1 a_A = 1 a#_A = 10 b_A = 1 b#_A = 3 b'_A = 1 b'#_A = 4 c_A = 1 c#_A = 5 d_A = 0 d#_A = 8 if_A(x1,x2,x3) = 0 if#_A(x1,x2,x3) = 0 e_A = 1 e#_A = 0 ._A(x1,x2) = 3 .#_A(x1,x2) = 5 d'_A = 4 d'#_A = 2 h_A(x1,x2) = 1 h#_A(x1,x2) = 11 precedence: h > g > d > c > a > b' > i > f > if = d' > b > e = .