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