MAYBE Problem: f(s(x),y) -> f(x,s(s(x))) f(x,s(s(y))) -> f(y,x) Proof: DP Processor: DPs: f#(s(x),y) -> f#(x,s(s(x))) f#(x,s(s(y))) -> f#(y,x) TRS: f(s(x),y) -> f(x,s(s(x))) f(x,s(s(y))) -> f(y,x) SCC Processor: #sccs: 1 #rules: 2 #arcs: 4/4 DPs: f#(s(x),y) -> f#(x,s(s(x))) f#(x,s(s(y))) -> f#(y,x) TRS: f(s(x),y) -> f(x,s(s(x))) f(x,s(s(y))) -> f(y,x) Open