Definition


A unary operator F is snapshot-equivalence preserving or weakly invariant if relation r is snapshot equivalent, or weakly equivalent, to r' implies F(r) is snapshot equivalent, or weakly equivalent, to F(r'). This definition may be extended to operators that accept two or more argument relation instances.