NO Problem: f(g(x),x) -> a() c() -> h(c(),g(c())) h(x,g(x)) -> f(g(x),h(x,g(c()))) Proof: Containment Processor: loop length: 1 terms: c() context: h([],g(c())) substitution: Qed