MAYBE Problem: a(x1) -> x1 a(a(b(a(x1)))) -> b(b(a(a(a(x1))))) b(x1) -> a(x1) Proof: DP Processor: DPs: a#(a(b(a(x1)))) -> a#(a(x1)) a#(a(b(a(x1)))) -> a#(a(a(x1))) a#(a(b(a(x1)))) -> b#(a(a(a(x1)))) a#(a(b(a(x1)))) -> b#(b(a(a(a(x1))))) b#(x1) -> a#(x1) TRS: a(x1) -> x1 a(a(b(a(x1)))) -> b(b(a(a(a(x1))))) b(x1) -> a(x1) Open