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