YES Problem: f(f(a(),a()),x) -> f(x,f(a(),f(a(),f(a(),a())))) Proof: DP Processor: DPs: f#(f(a(),a()),x) -> f#(a(),f(a(),a())) f#(f(a(),a()),x) -> f#(a(),f(a(),f(a(),a()))) f#(f(a(),a()),x) -> f#(x,f(a(),f(a(),f(a(),a())))) TRS: f(f(a(),a()),x) -> f(x,f(a(),f(a(),f(a(),a())))) EDG Processor: DPs: f#(f(a(),a()),x) -> f#(a(),f(a(),a())) f#(f(a(),a()),x) -> f#(a(),f(a(),f(a(),a()))) f#(f(a(),a()),x) -> f#(x,f(a(),f(a(),f(a(),a())))) TRS: f(f(a(),a()),x) -> f(x,f(a(),f(a(),f(a(),a())))) graph: f#(f(a(),a()),x) -> f#(x,f(a(),f(a(),f(a(),a())))) -> f#(f(a(),a()),x) -> f#(a(),f(a(),a())) f#(f(a(),a()),x) -> f#(x,f(a(),f(a(),f(a(),a())))) -> f#(f(a(),a()),x) -> f#(a(),f(a(),f(a(),a()))) f#(f(a(),a()),x) -> f#(x,f(a(),f(a(),f(a(),a())))) -> f#(f(a(),a()),x) -> f#(x,f(a(),f(a(),f(a(),a())))) CDG Processor: DPs: f#(f(a(),a()),x) -> f#(a(),f(a(),a())) f#(f(a(),a()),x) -> f#(a(),f(a(),f(a(),a()))) f#(f(a(),a()),x) -> f#(x,f(a(),f(a(),f(a(),a())))) TRS: f(f(a(),a()),x) -> f(x,f(a(),f(a(),f(a(),a())))) graph: Qed