Problem: a() -> b() b() -> f(a(),a()) f(x,a()) -> b() Proof: Open