YES Problem: f(x,0()) -> s(0()) f(s(x),s(y)) -> s(f(x,y)) g(0(),x) -> g(f(x,x),x) Proof: DP Processor: DPs: f#(s(x),s(y)) -> f#(x,y) g#(0(),x) -> f#(x,x) g#(0(),x) -> g#(f(x,x),x) TRS: f(x,0()) -> s(0()) f(s(x),s(y)) -> s(f(x,y)) g(0(),x) -> g(f(x,x),x) Usable Rule Processor: DPs: f#(s(x),s(y)) -> f#(x,y) g#(0(),x) -> f#(x,x) g#(0(),x) -> g#(f(x,x),x) TRS: f6(x,y) -> x f6(x,y) -> y f(x,0()) -> s(0()) f(s(x),s(y)) -> s(f(x,y)) ADG Processor: DPs: f#(s(x),s(y)) -> f#(x,y) g#(0(),x) -> f#(x,x) g#(0(),x) -> g#(f(x,x),x) TRS: f6(x,y) -> x f6(x,y) -> y f(x,0()) -> s(0()) f(s(x),s(y)) -> s(f(x,y)) graph: g#(0(),x) -> f#(x,x) -> f#(s(x),s(y)) -> f#(x,y) f#(s(x),s(y)) -> f#(x,y) -> f#(s(x),s(y)) -> f#(x,y) Restore Modifier: DPs: f#(s(x),s(y)) -> f#(x,y) g#(0(),x) -> f#(x,x) g#(0(),x) -> g#(f(x,x),x) TRS: f(x,0()) -> s(0()) f(s(x),s(y)) -> s(f(x,y)) g(0(),x) -> g(f(x,x),x) SCC Processor: #sccs: 1 #rules: 1 #arcs: 2/9 DPs: f#(s(x),s(y)) -> f#(x,y) TRS: f(x,0()) -> s(0()) f(s(x),s(y)) -> s(f(x,y)) g(0(),x) -> g(f(x,x),x) Matrix Interpretation Processor: dimension: 1 interpretation: [f#](x0, x1) = x1 + 1, [g](x0, x1) = x1 + 1, [s](x0) = x0 + 1, [f](x0, x1) = x0 + x1 + 1, [0] = 1 orientation: f#(s(x),s(y)) = y + 2 >= y + 1 = f#(x,y) f(x,0()) = x + 2 >= 2 = s(0()) f(s(x),s(y)) = x + y + 3 >= x + y + 2 = s(f(x,y)) g(0(),x) = x + 1 >= x + 1 = g(f(x,x),x) problem: DPs: TRS: f(x,0()) -> s(0()) f(s(x),s(y)) -> s(f(x,y)) g(0(),x) -> g(f(x,x),x) Qed