Problem: f(X,n__g(X),Y) -> f(activate(Y),activate(Y),activate(Y)) g(b()) -> c() b() -> c() g(X) -> n__g(X) activate(n__g(X)) -> g(X) activate(X) -> X Proof: Unfolding Processor: loop length: 6 terms: f(X,n__g(X),n__g(b())) f(activate(n__g(b())),activate(n__g(b())),activate(n__g(b()))) f(g(b()),activate(n__g(b())),activate(n__g(b()))) f(c(),activate(n__g(b())),activate(n__g(b()))) f(c(),n__g(b()),activate(n__g(b()))) f(c(),n__g(c()),activate(n__g(b()))) context: [] substitution: X -> c() Qed