YES TRS: cond(true(),x,y) -> cond(gr(x,y),p(x),s(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, 3, 1, 2} cond#_A(x1,x2,x3) = max{9, -1 + x1, 5 + x2, 1} true_A = 14 true#_A = 3 gr_A(x1,x2) = max{1, -1 + x1, 1} gr#_A(x1,x2) = max{13, 4, 2} p_A(x1) = max{3, -5 + x1} p#_A(x1) = max{12, 10} s_A(x1) = max{15, 5 + x1} s#_A(x1) = max{0, 4} 0_A = 3 0#_A = 11 false_A = 2 false#_A = 5 precedence: cond > gr = s > true = p > 0 > false