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 TDG 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 graph: odd#(s(s(x))) -> odd#(x) -> odd#(s(s(x))) -> odd#(x) cond#(true(),x) -> odd#(x) -> odd#(s(s(x))) -> odd#(x) cond#(true(),x) -> cond#(odd(x),p(x)) -> cond#(true(),x) -> cond#(odd(x),p(x)) cond#(true(),x) -> cond#(odd(x),p(x)) -> cond#(true(),x) -> odd#(x) cond#(true(),x) -> cond#(odd(x),p(x)) -> cond#(true(),x) -> p#(x) SCC Processor: #sccs: 2 #rules: 2 #arcs: 5/16 DPs: cond#(true(),x) -> cond#(odd(x),p(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: [cond#](x0, x1) = -2x0 + x1 + 0, [s](x0) = 2x0 + 4, [false] = 0, [0] = 0, [p](x0) = -1x0 + 1, [odd](x0) = 1x0, [cond](x0, x1) = -3x0 + -1x1 + 0, [true] = 4 orientation: cond#(true(),x) = x + 2 >= -1x + 1 = cond#(odd(x),p(x)) cond(true(),x) = -1x + 1 >= -2x + 0 = cond(odd(x),p(x)) odd(0()) = 1 >= 0 = false() odd(s(0())) = 5 >= 4 = true() odd(s(s(x))) = 5x + 7 >= 1x = odd(x) p(0()) = 1 >= 0 = 0() p(s(x)) = 1x + 3 >= 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 DPs: 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 KBO Processor: argument filtering: pi(true) = [] pi(cond) = [] pi(odd) = [] pi(p) = 0 pi(0) = [] pi(false) = [] pi(s) = [0] pi(odd#) = 0 weight function: w0 = 1 w(odd#) = w(false) = w(0) = w(p) = w(odd) = w(cond) = w(true) = 1 w(s) = 0 precedence: odd# > s ~ 0 ~ odd ~ cond > false ~ p ~ true 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