YES Problem: f(s(X),Y) -> h(s(f(h(Y),X))) Proof: DP Processor: DPs: f#(s(X),Y) -> f#(h(Y),X) TRS: f(s(X),Y) -> h(s(f(h(Y),X))) Usable Rule Processor: DPs: f#(s(X),Y) -> f#(h(Y),X) TRS: Restore Modifier: DPs: f#(s(X),Y) -> f#(h(Y),X) TRS: f(s(X),Y) -> h(s(f(h(Y),X))) SCC Processor: #sccs: 1 #rules: 1 #arcs: 1/1 DPs: f#(s(X),Y) -> f#(h(Y),X) TRS: f(s(X),Y) -> h(s(f(h(Y),X))) Matrix Interpretation Processor: dimension: 1 interpretation: [f#](x0, x1) = x0, [h](x0) = 0, [f](x0, x1) = 0, [s](x0) = 1 orientation: f#(s(X),Y) = 1 >= 0 = f#(h(Y),X) f(s(X),Y) = 0 >= 0 = h(s(f(h(Y),X))) problem: DPs: TRS: f(s(X),Y) -> h(s(f(h(Y),X))) Qed