NO Problem: g(f(x,y)) -> f(f(g(g(x)),g(g(y))),f(g(g(x)),g(g(y)))) Proof: Unfolding Processor: loop length: 2 terms: g(g(f(x4,x5))) g(f(f(g(g(x4)),g(g(x5))),f(g(g(x4)),g(g(x5))))) context: f(f(g(g(f(g(g(x4)),g(g(x5))))),g(g(f(g(g(x4)),g(g(x5)))))),f(g(g(f(g(g(x4)),g(g(x5))))),[])) substitution: x4 -> g(g(x4)) x5 -> g(g(x5)) Qed