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