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