Make write+lock privatization `read_global` more precise using semi-distributive property

[sim642]

This uses the following lattice property which is true in even non-distributive lattices:

$$ a \sqcup (b \sqcap c) \sqsubseteq (a \sqcup b) \sqcap (a \sqcup c) $$

I don't have an example program where this makes a difference, but according to lattice theory it can only be more precise (and use fewer operations!).