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