MAYBE Problem: f(c(s(x),y)) -> f(c(x,s(y))) f(c(s(x),s(y))) -> g(c(x,y)) g(c(x,s(y))) -> g(c(s(x),y)) g(c(s(x),s(y))) -> f(c(x,y)) Proof: DP Processor: DPs: f#(c(s(x),y)) -> f#(c(x,s(y))) f#(c(s(x),s(y))) -> g#(c(x,y)) g#(c(x,s(y))) -> g#(c(s(x),y)) g#(c(s(x),s(y))) -> f#(c(x,y)) TRS: f(c(s(x),y)) -> f(c(x,s(y))) f(c(s(x),s(y))) -> g(c(x,y)) g(c(x,s(y))) -> g(c(s(x),y)) g(c(s(x),s(y))) -> f(c(x,y)) Usable Rule Processor: DPs: f#(c(s(x),y)) -> f#(c(x,s(y))) f#(c(s(x),s(y))) -> g#(c(x,y)) g#(c(x,s(y))) -> g#(c(s(x),y)) g#(c(s(x),s(y))) -> f#(c(x,y)) TRS: ADG Processor: DPs: f#(c(s(x),y)) -> f#(c(x,s(y))) f#(c(s(x),s(y))) -> g#(c(x,y)) g#(c(x,s(y))) -> g#(c(s(x),y)) g#(c(s(x),s(y))) -> f#(c(x,y)) TRS: graph: g#(c(s(x),s(y))) -> f#(c(x,y)) -> f#(c(s(x),y)) -> f#(c(x,s(y))) g#(c(s(x),s(y))) -> f#(c(x,y)) -> f#(c(s(x),s(y))) -> g#(c(x,y)) g#(c(x,s(y))) -> g#(c(s(x),y)) -> g#(c(x,s(y))) -> g#(c(s(x),y)) g#(c(x,s(y))) -> g#(c(s(x),y)) -> g#(c(s(x),s(y))) -> f#(c(x,y)) f#(c(s(x),s(y))) -> g#(c(x,y)) -> g#(c(x,s(y))) -> g#(c(s(x),y)) f#(c(s(x),s(y))) -> g#(c(x,y)) -> g#(c(s(x),s(y))) -> f#(c(x,y)) f#(c(s(x),y)) -> f#(c(x,s(y))) -> f#(c(s(x),y)) -> f#(c(x,s(y))) f#(c(s(x),y)) -> f#(c(x,s(y))) -> f#(c(s(x),s(y))) -> g#(c(x,y)) Restore Modifier: DPs: f#(c(s(x),y)) -> f#(c(x,s(y))) f#(c(s(x),s(y))) -> g#(c(x,y)) g#(c(x,s(y))) -> g#(c(s(x),y)) g#(c(s(x),s(y))) -> f#(c(x,y)) TRS: f(c(s(x),y)) -> f(c(x,s(y))) f(c(s(x),s(y))) -> g(c(x,y)) g(c(x,s(y))) -> g(c(s(x),y)) g(c(s(x),s(y))) -> f(c(x,y)) SCC Processor: #sccs: 1 #rules: 4 #arcs: 8/16 DPs: g#(c(s(x),s(y))) -> f#(c(x,y)) f#(c(s(x),s(y))) -> g#(c(x,y)) g#(c(x,s(y))) -> g#(c(s(x),y)) f#(c(s(x),y)) -> f#(c(x,s(y))) TRS: f(c(s(x),y)) -> f(c(x,s(y))) f(c(s(x),s(y))) -> g(c(x,y)) g(c(x,s(y))) -> g(c(s(x),y)) g(c(s(x),s(y))) -> f(c(x,y)) Open