YES Problem: g(s(x)) -> f(x) f(0()) -> s(0()) f(s(x)) -> s(s(g(x))) g(0()) -> 0() Proof: DP Processor: DPs: g#(s(x)) -> f#(x) f#(s(x)) -> g#(x) TRS: g(s(x)) -> f(x) f(0()) -> s(0()) f(s(x)) -> s(s(g(x))) g(0()) -> 0() KBO Processor: argument filtering: pi(s) = [0] pi(g) = [0] pi(f) = [0] pi(0) = [] pi(g#) = 0 pi(f#) = 0 weight function: w0 = 1 w(0) = w(f) = w(s) = 1 w(f#) = w(g#) = w(g) = 0 precedence: g > f > f# ~ g# ~ 0 ~ s problem: DPs: TRS: g(s(x)) -> f(x) f(0()) -> s(0()) f(s(x)) -> s(s(g(x))) g(0()) -> 0() Qed