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)) linear polynomial interpretations on N: f_A(x1) = 1 f#_A(x1) = 1 0_A = 1 0#_A = 1 true_A = 1 true#_A = 0 1_A = 1 1#_A = 1 false_A = 1 false#_A = 0 s_A(x1) = 1 s#_A(x1) = x1 if_A(x1,x2,x3) = x2 + x3 if#_A(x1,x2,x3) = x1 g_A(x1,x2) = 2 g#_A(x1,x2) = x2 + 1 c_A(x1) = x1 + 3 c#_A(x1) = 0 precedence: 0 = if > true = g > f = 1 = c > false = s