MAYBE 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))) Open