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