YES Problem: p(0()) -> 0() p(s(x)) -> x minus(x,0()) -> x minus(x,s(y)) -> minus(p(x),y) Proof: DP Processor: DPs: minus#(x,s(y)) -> p#(x) minus#(x,s(y)) -> minus#(p(x),y) TRS: p(0()) -> 0() p(s(x)) -> x minus(x,0()) -> x minus(x,s(y)) -> minus(p(x),y) TDG Processor: DPs: minus#(x,s(y)) -> p#(x) minus#(x,s(y)) -> minus#(p(x),y) TRS: p(0()) -> 0() p(s(x)) -> x minus(x,0()) -> x minus(x,s(y)) -> minus(p(x),y) graph: minus#(x,s(y)) -> minus#(p(x),y) -> minus#(x,s(y)) -> minus#(p(x),y) minus#(x,s(y)) -> minus#(p(x),y) -> minus#(x,s(y)) -> p#(x) CDG Processor: DPs: minus#(x,s(y)) -> p#(x) minus#(x,s(y)) -> minus#(p(x),y) TRS: p(0()) -> 0() p(s(x)) -> x minus(x,0()) -> x minus(x,s(y)) -> minus(p(x),y) graph: Qed