MAYBE Problem: f(x,c(x),c(y)) -> f(y,y,f(y,x,y)) f(s(x),y,z) -> f(x,s(c(y)),c(z)) f(c(x),x,y) -> c(y) g(x,y) -> x g(x,y) -> y Proof: DP Processor: DPs: f#(x,c(x),c(y)) -> f#(y,x,y) f#(x,c(x),c(y)) -> f#(y,y,f(y,x,y)) f#(s(x),y,z) -> f#(x,s(c(y)),c(z)) TRS: f(x,c(x),c(y)) -> f(y,y,f(y,x,y)) f(s(x),y,z) -> f(x,s(c(y)),c(z)) f(c(x),x,y) -> c(y) g(x,y) -> x g(x,y) -> y Usable Rule Processor: DPs: f#(x,c(x),c(y)) -> f#(y,x,y) f#(x,c(x),c(y)) -> f#(y,y,f(y,x,y)) f#(s(x),y,z) -> f#(x,s(c(y)),c(z)) TRS: f6(x,y) -> x f6(x,y) -> y f(x,c(x),c(y)) -> f(y,y,f(y,x,y)) f(s(x),y,z) -> f(x,s(c(y)),c(z)) f(c(x),x,y) -> c(y) CDG Processor: DPs: f#(x,c(x),c(y)) -> f#(y,x,y) f#(x,c(x),c(y)) -> f#(y,y,f(y,x,y)) f#(s(x),y,z) -> f#(x,s(c(y)),c(z)) TRS: f6(x,y) -> x f6(x,y) -> y f(x,c(x),c(y)) -> f(y,y,f(y,x,y)) f(s(x),y,z) -> f(x,s(c(y)),c(z)) f(c(x),x,y) -> c(y) graph: f#(s(x),y,z) -> f#(x,s(c(y)),c(z)) -> f#(s(x),y,z) -> f#(x,s(c(y)),c(z)) f#(x,c(x),c(y)) -> f#(y,y,f(y,x,y)) -> f#(x,c(x),c(y)) -> f#(y,x,y) f#(x,c(x),c(y)) -> f#(y,y,f(y,x,y)) -> f#(x,c(x),c(y)) -> f#(y,y,f(y,x,y)) f#(x,c(x),c(y)) -> f#(y,y,f(y,x,y)) -> f#(s(x),y,z) -> f#(x,s(c(y)),c(z)) f#(x,c(x),c(y)) -> f#(y,x,y) -> f#(x,c(x),c(y)) -> f#(y,x,y) f#(x,c(x),c(y)) -> f#(y,x,y) -> f#(x,c(x),c(y)) -> f#(y,y,f(y,x,y)) f#(x,c(x),c(y)) -> f#(y,x,y) -> f#(s(x),y,z) -> f#(x,s(c(y)),c(z)) Restore Modifier: DPs: f#(x,c(x),c(y)) -> f#(y,x,y) f#(x,c(x),c(y)) -> f#(y,y,f(y,x,y)) f#(s(x),y,z) -> f#(x,s(c(y)),c(z)) TRS: f(x,c(x),c(y)) -> f(y,y,f(y,x,y)) f(s(x),y,z) -> f(x,s(c(y)),c(z)) f(c(x),x,y) -> c(y) g(x,y) -> x g(x,y) -> y SCC Processor: #sccs: 2 #rules: 3 #arcs: 7/9 DPs: f#(x,c(x),c(y)) -> f#(y,y,f(y,x,y)) f#(x,c(x),c(y)) -> f#(y,x,y) TRS: f(x,c(x),c(y)) -> f(y,y,f(y,x,y)) f(s(x),y,z) -> f(x,s(c(y)),c(z)) f(c(x),x,y) -> c(y) g(x,y) -> x g(x,y) -> y Open DPs: f#(s(x),y,z) -> f#(x,s(c(y)),c(z)) TRS: f(x,c(x),c(y)) -> f(y,y,f(y,x,y)) f(s(x),y,z) -> f(x,s(c(y)),c(z)) f(c(x),x,y) -> c(y) g(x,y) -> x g(x,y) -> y Open