MAYBE Problem: f(f(a(),a()),x) -> f(a(),f(b(),f(a(),x))) f(x,f(y,z)) -> f(f(x,y),z) Proof: DP Processor: DPs: f#(f(a(),a()),x) -> f#(a(),x) f#(f(a(),a()),x) -> f#(b(),f(a(),x)) f#(f(a(),a()),x) -> f#(a(),f(b(),f(a(),x))) f#(x,f(y,z)) -> f#(x,y) f#(x,f(y,z)) -> f#(f(x,y),z) TRS: f(f(a(),a()),x) -> f(a(),f(b(),f(a(),x))) f(x,f(y,z)) -> f(f(x,y),z) CDG Processor: DPs: f#(f(a(),a()),x) -> f#(a(),x) f#(f(a(),a()),x) -> f#(b(),f(a(),x)) f#(f(a(),a()),x) -> f#(a(),f(b(),f(a(),x))) f#(x,f(y,z)) -> f#(x,y) f#(x,f(y,z)) -> f#(f(x,y),z) TRS: f(f(a(),a()),x) -> f(a(),f(b(),f(a(),x))) f(x,f(y,z)) -> f(f(x,y),z) graph: f#(f(a(),a()),x) -> f#(b(),f(a(),x)) -> f#(x,f(y,z)) -> f#(x,y) f#(f(a(),a()),x) -> f#(b(),f(a(),x)) -> f#(x,f(y,z)) -> f#(f(x,y),z) f#(f(a(),a()),x) -> f#(a(),f(b(),f(a(),x))) -> f#(x,f(y,z)) -> f#(x,y) f#(f(a(),a()),x) -> f#(a(),f(b(),f(a(),x))) -> f#(x,f(y,z)) -> f#(f(x,y),z) f#(f(a(),a()),x) -> f#(a(),x) -> f#(f(a(),a()),x) -> f#(a(),x) f#(f(a(),a()),x) -> f#(a(),x) -> f#(f(a(),a()),x) -> f#(b(),f(a(),x)) f#(f(a(),a()),x) -> f#(a(),x) -> f#(f(a(),a()),x) -> f#(a(),f(b(),f(a(),x))) f#(f(a(),a()),x) -> f#(a(),x) -> f#(x,f(y,z)) -> f#(x,y) f#(f(a(),a()),x) -> f#(a(),x) -> f#(x,f(y,z)) -> f#(f(x,y),z) f#(x,f(y,z)) -> f#(f(x,y),z) -> f#(f(a(),a()),x) -> f#(a(),x) f#(x,f(y,z)) -> f#(f(x,y),z) -> f#(f(a(),a()),x) -> f#(b(),f(a(),x)) f#(x,f(y,z)) -> f#(f(x,y),z) -> f#(f(a(),a()),x) -> f#(a(),f(b(),f(a(),x))) f#(x,f(y,z)) -> f#(f(x,y),z) -> f#(x,f(y,z)) -> f#(x,y) f#(x,f(y,z)) -> f#(f(x,y),z) -> f#(x,f(y,z)) -> f#(f(x,y),z) f#(x,f(y,z)) -> f#(x,y) -> f#(f(a(),a()),x) -> f#(a(),x) f#(x,f(y,z)) -> f#(x,y) -> f#(f(a(),a()),x) -> f#(b(),f(a(),x)) f#(x,f(y,z)) -> f#(x,y) -> f#(f(a(),a()),x) -> f#(a(),f(b(),f(a(),x))) f#(x,f(y,z)) -> f#(x,y) -> f#(x,f(y,z)) -> f#(x,y) f#(x,f(y,z)) -> f#(x,y) -> f#(x,f(y,z)) -> f#(f(x,y),z) SCC Processor: #sccs: 1 #rules: 5 #arcs: 19/25 DPs: f#(f(a(),a()),x) -> f#(b(),f(a(),x)) f#(x,f(y,z)) -> f#(f(x,y),z) f#(x,f(y,z)) -> f#(x,y) f#(f(a(),a()),x) -> f#(a(),f(b(),f(a(),x))) f#(f(a(),a()),x) -> f#(a(),x) TRS: f(f(a(),a()),x) -> f(a(),f(b(),f(a(),x))) f(x,f(y,z)) -> f(f(x,y),z) Open