YES Problem: g(c(x,s(y))) -> g(c(s(x),y)) f(c(s(x),y)) -> f(c(x,s(y))) f(f(x)) -> f(d(f(x))) f(x) -> x Proof: DP Processor: DPs: g#(c(x,s(y))) -> g#(c(s(x),y)) f#(c(s(x),y)) -> f#(c(x,s(y))) f#(f(x)) -> f#(d(f(x))) TRS: g(c(x,s(y))) -> g(c(s(x),y)) f(c(s(x),y)) -> f(c(x,s(y))) f(f(x)) -> f(d(f(x))) f(x) -> x TDG Processor: DPs: g#(c(x,s(y))) -> g#(c(s(x),y)) f#(c(s(x),y)) -> f#(c(x,s(y))) f#(f(x)) -> f#(d(f(x))) TRS: g(c(x,s(y))) -> g(c(s(x),y)) f(c(s(x),y)) -> f(c(x,s(y))) f(f(x)) -> f(d(f(x))) f(x) -> x graph: f#(f(x)) -> f#(d(f(x))) -> f#(f(x)) -> f#(d(f(x))) f#(f(x)) -> f#(d(f(x))) -> f#(c(s(x),y)) -> f#(c(x,s(y))) f#(c(s(x),y)) -> f#(c(x,s(y))) -> f#(f(x)) -> f#(d(f(x))) f#(c(s(x),y)) -> f#(c(x,s(y))) -> f#(c(s(x),y)) -> f#(c(x,s(y))) g#(c(x,s(y))) -> g#(c(s(x),y)) -> g#(c(x,s(y))) -> g#(c(s(x),y)) SCC Processor: #sccs: 2 #rules: 3 #arcs: 5/9 DPs: g#(c(x,s(y))) -> g#(c(s(x),y)) TRS: g(c(x,s(y))) -> g(c(s(x),y)) f(c(s(x),y)) -> f(c(x,s(y))) f(f(x)) -> f(d(f(x))) f(x) -> x CDG Processor: DPs: g#(c(x,s(y))) -> g#(c(s(x),y)) TRS: g(c(x,s(y))) -> g(c(s(x),y)) f(c(s(x),y)) -> f(c(x,s(y))) f(f(x)) -> f(d(f(x))) f(x) -> x graph: Qed DPs: f#(f(x)) -> f#(d(f(x))) f#(c(s(x),y)) -> f#(c(x,s(y))) TRS: g(c(x,s(y))) -> g(c(s(x),y)) f(c(s(x),y)) -> f(c(x,s(y))) f(f(x)) -> f(d(f(x))) f(x) -> x EDG Processor: DPs: f#(f(x)) -> f#(d(f(x))) f#(c(s(x),y)) -> f#(c(x,s(y))) TRS: g(c(x,s(y))) -> g(c(s(x),y)) f(c(s(x),y)) -> f(c(x,s(y))) f(f(x)) -> f(d(f(x))) f(x) -> x graph: f#(c(s(x),y)) -> f#(c(x,s(y))) -> f#(c(s(x),y)) -> f#(c(x,s(y))) CDG Processor: DPs: f#(f(x)) -> f#(d(f(x))) f#(c(s(x),y)) -> f#(c(x,s(y))) TRS: g(c(x,s(y))) -> g(c(s(x),y)) f(c(s(x),y)) -> f(c(x,s(y))) f(f(x)) -> f(d(f(x))) f(x) -> x graph: Qed