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