YES TRS: cond(true(),x,y) -> cond(gr(x,y),p(x),y) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) p(0()) -> 0() p(s(x)) -> x max/plus interpretations on N: cond_A(x1,x2,x3) = max{0, 2, 1, 0} cond#_A(x1,x2,x3) = max{5, -2 + x1, 3 + x2, 2} true_A = 8 true#_A = 2 gr_A(x1,x2) = max{2, 1 + x1, 3} gr#_A(x1,x2) = max{0, 1, 6} p_A(x1) = max{1, -2 + x1} p#_A(x1) = max{6, 6} 0_A = 1 0#_A = 8 false_A = 3 false#_A = 7 s_A(x1) = max{1, 7 + x1} s#_A(x1) = max{3, 0} precedence: cond > p > 0 > false > gr = s > true