YES TRS: f(0()) -> true() f(1()) -> false() f(s(x)) -> f(x) if(true(),x,y) -> x if(false(),x,y) -> y g(s(x),s(y)) -> if(f(x),s(x),s(y)) g(x,c(y)) -> g(x,g(s(c(y)),y)) max/plus interpretations on N: f_A(x1) = max{1, -6} f#_A(x1) = max{1, -5 + x1} 0_A = 1 0#_A = 1 true_A = 0 true#_A = 0 1_A = 1 1#_A = 3 false_A = 0 false#_A = 2 s_A(x1) = max{6, 1} s#_A(x1) = max{12, x1} if_A(x1,x2,x3) = max{0, 5 + x1, x2, x3} if#_A(x1,x2,x3) = max{12, 10, 12, 15} g_A(x1,x2) = max{6, -1, -1} g#_A(x1,x2) = max{13, 14, 10 + x2} c_A(x1) = max{10, 7 + x1} c#_A(x1) = max{8, 9} precedence: c > 1 = g > 0 = false = s = if > f > true