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