safety definition

[Stephen Weeks]

I propose changing condition *4 in safety to the following equivalent one.

*4  for all tail calls (f, g) in T with f \not = g,
       ~R(f) or A(g) in {f, A(f), Unknown}

The point is, if f = g, then the previous *4 doesn't impose any constraint,
since A(g) = A(f) in {f, A(f), Unknown}.

This is the reasoning you give in the proof of safety of the call analysis, but
I thought it might be nice to move this into the definition.