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