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