YES Problem: f(0(x1)) -> s(0(x1)) d(0(x1)) -> 0(x1) d(s(x1)) -> s(s(d(p(s(x1))))) f(s(x1)) -> d(f(p(s(x1)))) p(s(x1)) -> x1 Proof: DP Processor: DPs: d#(s(x1)) -> p#(s(x1)) d#(s(x1)) -> d#(p(s(x1))) f#(s(x1)) -> p#(s(x1)) f#(s(x1)) -> f#(p(s(x1))) f#(s(x1)) -> d#(f(p(s(x1)))) TRS: f(0(x1)) -> s(0(x1)) d(0(x1)) -> 0(x1) d(s(x1)) -> s(s(d(p(s(x1))))) f(s(x1)) -> d(f(p(s(x1)))) p(s(x1)) -> x1 TDG Processor: DPs: d#(s(x1)) -> p#(s(x1)) d#(s(x1)) -> d#(p(s(x1))) f#(s(x1)) -> p#(s(x1)) f#(s(x1)) -> f#(p(s(x1))) f#(s(x1)) -> d#(f(p(s(x1)))) TRS: f(0(x1)) -> s(0(x1)) d(0(x1)) -> 0(x1) d(s(x1)) -> s(s(d(p(s(x1))))) f(s(x1)) -> d(f(p(s(x1)))) p(s(x1)) -> x1 graph: d#(s(x1)) -> d#(p(s(x1))) -> d#(s(x1)) -> d#(p(s(x1))) d#(s(x1)) -> d#(p(s(x1))) -> d#(s(x1)) -> p#(s(x1)) f#(s(x1)) -> d#(f(p(s(x1)))) -> d#(s(x1)) -> d#(p(s(x1))) f#(s(x1)) -> d#(f(p(s(x1)))) -> d#(s(x1)) -> p#(s(x1)) f#(s(x1)) -> f#(p(s(x1))) -> f#(s(x1)) -> d#(f(p(s(x1)))) f#(s(x1)) -> f#(p(s(x1))) -> f#(s(x1)) -> f#(p(s(x1))) f#(s(x1)) -> f#(p(s(x1))) -> f#(s(x1)) -> p#(s(x1)) CDG Processor: DPs: d#(s(x1)) -> p#(s(x1)) d#(s(x1)) -> d#(p(s(x1))) f#(s(x1)) -> p#(s(x1)) f#(s(x1)) -> f#(p(s(x1))) f#(s(x1)) -> d#(f(p(s(x1)))) TRS: f(0(x1)) -> s(0(x1)) d(0(x1)) -> 0(x1) d(s(x1)) -> s(s(d(p(s(x1))))) f(s(x1)) -> d(f(p(s(x1)))) p(s(x1)) -> x1 graph: f#(s(x1)) -> d#(f(p(s(x1)))) -> d#(s(x1)) -> p#(s(x1)) f#(s(x1)) -> d#(f(p(s(x1)))) -> d#(s(x1)) -> d#(p(s(x1))) SCC Processor: #sccs: 0 #rules: 0 #arcs: 2/25