YES TRS: p(0()) -> 0() p(s(x)) -> x le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) minus(x,y) -> if(le(x,y),x,y) if(true(),x,y) -> 0() if(false(),x,y) -> s(minus(p(x),y)) max/plus interpretations on N: p_A(x1) = max{2, -6 + x1} p#_A(x1) = max{0, 5 + x1} 0_A = 2 0#_A = 6 s_A(x1) = max{13, 6 + x1} s#_A(x1) = max{13, 2} le_A(x1,x2) = max{3, x1, -1} le#_A(x1,x2) = max{0, 3, 8} true_A = 3 true#_A = 7 false_A = 13 false#_A = 1 minus_A(x1,x2) = max{0, 6 + x1, 4} minus#_A(x1,x2) = max{4, 11 + x1, 13} if_A(x1,x2,x3) = max{5, 1 + x1, 6 + x2, 0} if#_A(x1,x2,x3) = max{3, x1, 5 + x2, 3} precedence: if > p = s = minus > le > true = false > 0