YES Problem: cond(true(),x) -> cond(odd(x),p(p(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) -> p#(p(x)) cond#(true(),x) -> p#(p(p(x))) cond#(true(),x) -> odd#(x) cond#(true(),x) -> cond#(odd(x),p(p(p(x)))) odd#(s(s(x))) -> odd#(x) TRS: cond(true(),x) -> cond(odd(x),p(p(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) = x0, [p#](x0) = 1x0 + 0, [cond#](x0, x1) = 2x0 + 4x1 + 0, [s](x0) = 2x0 + 5, [false] = 0, [0] = 0, [p](x0) = -1x0 + 1, [odd](x0) = x0 + 1, [cond](x0, x1) = 1x0 + 3x1 + 4, [true] = 4 orientation: cond#(true(),x) = 4x + 6 >= 1x + 0 = p#(x) cond#(true(),x) = 4x + 6 >= x + 2 = p#(p(x)) cond#(true(),x) = 4x + 6 >= -1x + 2 = p#(p(p(x))) cond#(true(),x) = 4x + 6 >= x = odd#(x) cond#(true(),x) = 4x + 6 >= 2x + 5 = cond#(odd(x),p(p(p(x)))) odd#(s(s(x))) = 4x + 7 >= x = odd#(x) cond(true(),x) = 3x + 5 >= 1x + 4 = cond(odd(x),p(p(p(x)))) odd(0()) = 1 >= 0 = false() odd(s(0())) = 5 >= 4 = true() odd(s(s(x))) = 4x + 7 >= x + 1 = odd(x) p(0()) = 1 >= 0 = 0() p(s(x)) = 1x + 4 >= x = x problem: DPs: TRS: cond(true(),x) -> cond(odd(x),p(p(p(x)))) odd(0()) -> false() odd(s(0())) -> true() odd(s(s(x))) -> odd(x) p(0()) -> 0() p(s(x)) -> x Qed