MAYBE Problem: a(f(),a(f(),x)) -> a(x,g()) a(x,g()) -> a(f(),a(g(),a(f(),x))) Proof: DP Processor: DPs: a#(f(),a(f(),x)) -> a#(x,g()) a#(x,g()) -> a#(f(),x) a#(x,g()) -> a#(g(),a(f(),x)) a#(x,g()) -> a#(f(),a(g(),a(f(),x))) TRS: a(f(),a(f(),x)) -> a(x,g()) a(x,g()) -> a(f(),a(g(),a(f(),x))) Open