YES Problem: not(true()) -> false() not(false()) -> true() odd(0()) -> false() odd(s(x)) -> not(odd(x)) +(x,0()) -> x +(x,s(y)) -> s(+(x,y)) +(s(x),y) -> s(+(x,y)) Proof: DP Processor: DPs: odd#(s(x)) -> odd#(x) odd#(s(x)) -> not#(odd(x)) +#(x,s(y)) -> +#(x,y) +#(s(x),y) -> +#(x,y) TRS: not(true()) -> false() not(false()) -> true() odd(0()) -> false() odd(s(x)) -> not(odd(x)) +(x,0()) -> x +(x,s(y)) -> s(+(x,y)) +(s(x),y) -> s(+(x,y)) TDG Processor: DPs: odd#(s(x)) -> odd#(x) odd#(s(x)) -> not#(odd(x)) +#(x,s(y)) -> +#(x,y) +#(s(x),y) -> +#(x,y) TRS: not(true()) -> false() not(false()) -> true() odd(0()) -> false() odd(s(x)) -> not(odd(x)) +(x,0()) -> x +(x,s(y)) -> s(+(x,y)) +(s(x),y) -> s(+(x,y)) graph: +#(s(x),y) -> +#(x,y) -> +#(s(x),y) -> +#(x,y) +#(s(x),y) -> +#(x,y) -> +#(x,s(y)) -> +#(x,y) +#(x,s(y)) -> +#(x,y) -> +#(s(x),y) -> +#(x,y) +#(x,s(y)) -> +#(x,y) -> +#(x,s(y)) -> +#(x,y) odd#(s(x)) -> odd#(x) -> odd#(s(x)) -> not#(odd(x)) odd#(s(x)) -> odd#(x) -> odd#(s(x)) -> odd#(x) CDG Processor: DPs: odd#(s(x)) -> odd#(x) odd#(s(x)) -> not#(odd(x)) +#(x,s(y)) -> +#(x,y) +#(s(x),y) -> +#(x,y) TRS: not(true()) -> false() not(false()) -> true() odd(0()) -> false() odd(s(x)) -> not(odd(x)) +(x,0()) -> x +(x,s(y)) -> s(+(x,y)) +(s(x),y) -> s(+(x,y)) graph: Qed