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