YES Problem: cond(true(),x) -> cond(odd(x),p(x)) odd(0()) -> false() odd(s(0())) -> true() odd(s(s(x))) -> odd(x) p(0()) -> 0() p(s(x)) -> x Proof: DP Processor: DPs: cond#(true(),x) -> p#(x) cond#(true(),x) -> odd#(x) cond#(true(),x) -> cond#(odd(x),p(x)) odd#(s(s(x))) -> odd#(x) TRS: cond(true(),x) -> cond(odd(x),p(x)) odd(0()) -> false() odd(s(0())) -> true() odd(s(s(x))) -> odd(x) p(0()) -> 0() p(s(x)) -> x Arctic Interpretation Processor: dimension: 1 interpretation: [odd#](x0) = -6x0 + 0, [p#](x0) = -14x0 + 0, [cond#](x0, x1) = -3x0 + -2x1 + 0, [s](x0) = 2x0 + 5, [false] = 0, [0] = 1, [p](x0) = -1x0 + 2, [odd](x0) = x0 + -5, [cond](x0, x1) = -3x0 + -2x1 + 0, [true] = 4 orientation: cond#(true(),x) = -2x + 1 >= -14x + 0 = p#(x) cond#(true(),x) = -2x + 1 >= -6x + 0 = odd#(x) cond#(true(),x) = -2x + 1 >= -3x + 0 = cond#(odd(x),p(x)) odd#(s(s(x))) = -2x + 1 >= -6x + 0 = odd#(x) cond(true(),x) = -2x + 1 >= -3x + 0 = cond(odd(x),p(x)) odd(0()) = 1 >= 0 = false() odd(s(0())) = 5 >= 4 = true() odd(s(s(x))) = 4x + 7 >= x + -5 = odd(x) p(0()) = 2 >= 1 = 0() p(s(x)) = 1x + 4 >= x = x problem: DPs: TRS: cond(true(),x) -> cond(odd(x),p(x)) odd(0()) -> false() odd(s(0())) -> true() odd(s(s(x))) -> odd(x) p(0()) -> 0() p(s(x)) -> x Qed