> Define the function C: Analysis -> Analysis by > C(A)(g) = > if g = fm > then Unknown > else lub ({j | (f, g, j) in N and A(f) = Uncalled} > U {A(f) | (f, g) in T}) I think you want A(f) <> Uncalled in the first set.