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) TDG 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) graph: b#(x1) -> a#(x1) -> a#(a(b(a(x1)))) -> b#(b(a(a(a(x1))))) b#(x1) -> a#(x1) -> a#(a(b(a(x1)))) -> b#(a(a(a(x1)))) b#(x1) -> a#(x1) -> a#(a(b(a(x1)))) -> a#(a(a(x1))) b#(x1) -> a#(x1) -> a#(a(b(a(x1)))) -> a#(a(x1)) a#(a(b(a(x1)))) -> b#(b(a(a(a(x1))))) -> b#(x1) -> a#(x1) a#(a(b(a(x1)))) -> b#(a(a(a(x1)))) -> b#(x1) -> a#(x1) a#(a(b(a(x1)))) -> a#(a(a(x1))) -> a#(a(b(a(x1)))) -> b#(b(a(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)))) -> a#(a(a(x1))) -> a#(a(b(a(x1)))) -> a#(a(a(x1))) a#(a(b(a(x1)))) -> a#(a(a(x1))) -> a#(a(b(a(x1)))) -> a#(a(x1)) a#(a(b(a(x1)))) -> a#(a(x1)) -> a#(a(b(a(x1)))) -> b#(b(a(a(a(x1))))) a#(a(b(a(x1)))) -> a#(a(x1)) -> a#(a(b(a(x1)))) -> b#(a(a(a(x1)))) a#(a(b(a(x1)))) -> a#(a(x1)) -> a#(a(b(a(x1)))) -> a#(a(a(x1))) a#(a(b(a(x1)))) -> a#(a(x1)) -> a#(a(b(a(x1)))) -> a#(a(x1)) Open