YES Problem: f(g(x),s(0()),y) -> f(g(s(0())),y,g(x)) g(s(x)) -> s(g(x)) g(0()) -> 0() Proof: DP Processor: DPs: f#(g(x),s(0()),y) -> g#(s(0())) f#(g(x),s(0()),y) -> f#(g(s(0())),y,g(x)) g#(s(x)) -> g#(x) TRS: f(g(x),s(0()),y) -> f(g(s(0())),y,g(x)) g(s(x)) -> s(g(x)) g(0()) -> 0() CDG Processor: DPs: f#(g(x),s(0()),y) -> g#(s(0())) f#(g(x),s(0()),y) -> f#(g(s(0())),y,g(x)) g#(s(x)) -> g#(x) TRS: f(g(x),s(0()),y) -> f(g(s(0())),y,g(x)) g(s(x)) -> s(g(x)) g(0()) -> 0() graph: f#(g(x),s(0()),y) -> g#(s(0())) -> g#(s(x)) -> g#(x) SCC Processor: #sccs: 0 #rules: 0 #arcs: 1/9