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