NO Problem: a(x1) -> x1 a(b(x1)) -> b(c(x1)) c(c(x1)) -> b(a(c(a(a(x1))))) Proof: DP Processor: DPs: a#(b(x1)) -> c#(x1) c#(c(x1)) -> a#(x1) c#(c(x1)) -> a#(a(x1)) c#(c(x1)) -> c#(a(a(x1))) c#(c(x1)) -> a#(c(a(a(x1)))) TRS: a(x1) -> x1 a(b(x1)) -> b(c(x1)) c(c(x1)) -> b(a(c(a(a(x1))))) TDG Processor: DPs: a#(b(x1)) -> c#(x1) c#(c(x1)) -> a#(x1) c#(c(x1)) -> a#(a(x1)) c#(c(x1)) -> c#(a(a(x1))) c#(c(x1)) -> a#(c(a(a(x1)))) TRS: a(x1) -> x1 a(b(x1)) -> b(c(x1)) c(c(x1)) -> b(a(c(a(a(x1))))) graph: c#(c(x1)) -> c#(a(a(x1))) -> c#(c(x1)) -> a#(c(a(a(x1)))) c#(c(x1)) -> c#(a(a(x1))) -> c#(c(x1)) -> c#(a(a(x1))) c#(c(x1)) -> c#(a(a(x1))) -> c#(c(x1)) -> a#(a(x1)) c#(c(x1)) -> c#(a(a(x1))) -> c#(c(x1)) -> a#(x1) c#(c(x1)) -> a#(c(a(a(x1)))) -> a#(b(x1)) -> c#(x1) c#(c(x1)) -> a#(a(x1)) -> a#(b(x1)) -> c#(x1) c#(c(x1)) -> a#(x1) -> a#(b(x1)) -> c#(x1) a#(b(x1)) -> c#(x1) -> c#(c(x1)) -> a#(c(a(a(x1)))) a#(b(x1)) -> c#(x1) -> c#(c(x1)) -> c#(a(a(x1))) a#(b(x1)) -> c#(x1) -> c#(c(x1)) -> a#(a(x1)) a#(b(x1)) -> c#(x1) -> c#(c(x1)) -> a#(x1) Loop Processor: loop length: 14 terms: c(a(c(a(a(b(a(c(a(a(x1)))))))))) c(c(a(a(b(a(c(a(a(x1))))))))) c(c(a(b(c(a(c(a(a(x1))))))))) b(a(c(a(a(a(b(c(a(c(a(a(x1)))))))))))) b(a(c(a(a(b(c(c(a(c(a(a(x1)))))))))))) b(a(c(a(b(c(c(c(a(c(a(a(x1)))))))))))) b(a(c(b(c(c(c(c(a(c(a(a(x1)))))))))))) b(a(c(b(b(a(c(a(a(c(c(a(c(a(a(x1))))))))))))))) b(a(c(b(b(a(c(a(c(c(a(c(a(a(x1)))))))))))))) b(a(c(b(b(a(c(a(c(c(a(c(a(x1))))))))))))) b(a(c(b(b(a(c(c(c(a(c(a(x1)))))))))))) b(a(c(b(b(a(b(a(c(a(a(c(a(c(a(x1))))))))))))))) b(a(c(b(b(b(c(a(c(a(a(c(a(c(a(x1))))))))))))))) b(a(c(b(b(b(c(a(c(a(a(c(c(a(x1)))))))))))))) context: b(a(c(b(b(b([])))))) substitution: x1 -> a(x1) Qed