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) Usable Rule Processor: DPs: minus#(x,s(y)) -> p#(x) minus#(x,s(y)) -> minus#(p(x),y) TRS: p(0()) -> 0() p(s(x)) -> 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 graph: Qed